Merge branch 'main' into dependabot/github_actions/actions/upload-artifact-7.0.0

Author: hyperpolymath

.github/workflows/codeql.yml

@@ -29,12 +29,12 @@ jobs:
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: Initialize CodeQL
-        uses: github/codeql-action/init@0d579ffd059c29b07949a3cce3983f0780820c98 # v3.28.1
+        uses: github/codeql-action/init@b1bff81932f5cdfc8695c7752dcee935dcd061c8 # v3.28.1
         with:
           languages: ${{ matrix.language }}
           build-mode: ${{ matrix.build-mode }}
 
       - name: Perform CodeQL Analysis
-        uses: github/codeql-action/analyze@0d579ffd059c29b07949a3cce3983f0780820c98 # v3.28.1
+        uses: github/codeql-action/analyze@b1bff81932f5cdfc8695c7752dcee935dcd061c8 # v3.28.1
         with:
           category: "/language:${{ matrix.language }}"

.github/workflows/hypatia-scan.yml

@@ -130,7 +130,7 @@ jobs:
 
       - name: Comment on PR with findings
         if: github.event_name == 'pull_request' && steps.scan.outputs.findings_count > 0
-        uses: actions/github-script@f28e40c7f34bde8b3046d885e986cb6290c5673b # v7
+        uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8.0.0
         with:
           script: |
             const fs = require('fs');

.github/workflows/scorecard-enforcer.yml

@@ -30,7 +30,7 @@ jobs:
           publish_results: true
 
       - name: Upload SARIF
-        uses: github/codeql-action/upload-sarif@0d579ffd059c29b07949a3cce3983f0780820c98 # v4
+        uses: github/codeql-action/upload-sarif@b1bff81932f5cdfc8695c7752dcee935dcd061c8 # v4
         with:
           sarif_file: results.sarif
 

.github/workflows/scorecard.yml

@@ -27,6 +27,6 @@ jobs:
           results_format: sarif
 
       - name: Upload results
-        uses: github/codeql-action/upload-sarif@0d579ffd059c29b07949a3cce3983f0780820c98 # v3.31.8
+        uses: github/codeql-action/upload-sarif@b1bff81932f5cdfc8695c7752dcee935dcd061c8 # v3.31.8
         with:
           sarif_file: results.sarif

rescript-ecosystem/ppx-proven-record/README.adoc

@@ -0,0 +1,39 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+= ppx-proven-record
+Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+ReScript PPX for verified record subset destructuring.
+
+== Usage
+
+[source,rescript]
+----
+@rest let { className, ?children, ...otherProps } = props
+----
+
+Expands at compile time to explicit field extraction with a typed remainder.
+
+== How It Works
+
+The PPX implements the `computeComplement` algorithm from `proven/SafeRecord`,
+which is formally verified in Idris2 to produce exhaustive, disjoint partitions.
+The PPX is a direct transliteration — it does not call Idris2 at runtime, but
+implements the same algorithm the proofs guarantee correct.
+
+== Formal Foundation
+
+* Idris2 proofs: `proven/src/Proven/SafeRecord/`
+* Paper: `proven/docs/papers/safe-record-destructuring.adoc`
+* Ephapax linear spec: `nextgen-languages/ephapax/` (future)
+
+== Build
+
+[source,bash]
+----
+# The PPX is an OCaml binary (ReScript PPX convention)
+dune build
+----
+
+== Status
+
+Scaffolded. Implementation pending.

rescript-ecosystem/ppx-proven-record/src/ppx_proven_record.ml

@@ -0,0 +1,28 @@
+(* SPDX-License-Identifier: PMPL-1.0-or-later *)
+(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> *)
+(*
+ * ppx_proven_record — ReScript PPX for verified record subset destructuring.
+ *
+ * Transforms:
+ *   @rest let { className, ?children, ...otherProps } = props
+ *
+ * Into:
+ *   let className = props.className
+ *   let children = props.children
+ *   let otherProps = { onClick: props.onClick, style: props.style, ... }
+ *
+ * The algorithm is a direct transliteration of computeComplement from
+ * proven/src/Proven/SafeRecord/Proofs.idr, which is formally verified
+ * to produce exhaustive, disjoint partitions.
+ *
+ * Status: Scaffold — implementation pending.
+ *)
+
+(* TODO: Implement the PPX transformation using ppxlib *)
+(* Key steps:
+ *   1. Find @rest attributes on let bindings
+ *   2. Extract the requested field names from the pattern
+ *   3. Look up the record type from the type environment
+ *   4. Compute the complement (remaining fields)
+ *   5. Generate explicit destructuring code
+ *)