proofs(agda): the wager experiment for coercions and roles (stages 0 and 1)

.github/workflows/proofs.yml

@@ -7,6 +7,8 @@
 # with a checksum, the Lean toolchain from the committed lean-toolchain file,
 # and no floating setup action is involved. A missing prover FAILS (the gate
 # never skips), so this workflow existing is what makes green mean "proved".
+# The agda job follows the same pattern: Agda comes from a version-pinned
+# release tarball with a checksum, and the cubical library from a pinned commit.
 name: proofs
 
 on:
@@ -84,3 +86,55 @@ jobs:
 
       - name: Status drift gate (PROOF-STATUS must match MANIFEST)
         run: ./scripts/check-proof-status.sh
+
+  agda:
+    name: agda proof gate (wager experiment)
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    env:
+      # Pins. Keep them equal to verification/proofs/agda/Wager/TOOLCHAIN.adoc.
+      AGDA_VERSION: "2.8.0"
+      AGDA_SHA256: 824081b8dcbe431289a50ac6bd83e451f390c51c3884ac7a8c4a5c0df2632faf
+      CUBICAL_TAG: v0.9
+      CUBICAL_COMMIT: b150186d2544e7efeddd31e5d14a8b9ecbb100f7
+    steps:
+      - uses: actions/checkout@v7.0.1
+
+      - name: Cache Agda, the cubical library and its interface files (keyed on the pins)
+        uses: actions/cache@v6.1.0
+        with:
+          path: ~/.agda-toolchain
+          key: agda-2.8.0-cubical-b150186d-${{ runner.os }}
+
+      - name: Install Agda (pinned tarball, checksum-verified)
+        run: |
+          set -euo pipefail
+          T="$HOME/.agda-toolchain"
+          if [ ! -x "$T/bin/agda" ]; then
+            mkdir -p "$T/bin"
+            curl -sSfL --proto '=https' --tlsv1.2 -o /tmp/agda.tar.xz \
+              "https://github.com/agda/agda/releases/download/v${AGDA_VERSION}/Agda-v${AGDA_VERSION}-linux.tar.xz"
+            echo "${AGDA_SHA256}  /tmp/agda.tar.xz" | sha256sum -c -
+            tar -xJf /tmp/agda.tar.xz -C "$T/bin"
+          fi
+          echo "$T/bin" >> "$GITHUB_PATH"
+          "$T/bin/agda" --version
+
+      - name: Install the cubical library (pinned commit)
+        run: |
+          set -euo pipefail
+          T="$HOME/.agda-toolchain"
+          if [ ! -d "$T/cubical/.git" ]; then
+            git clone --depth 1 --branch "$CUBICAL_TAG" https://github.com/agda/cubical "$T/cubical"
+          fi
+          got="$(git -C "$T/cubical" rev-parse HEAD)"
+          if [ "$got" != "$CUBICAL_COMMIT" ]; then
+            echo "FAIL: cubical is at $got, expected $CUBICAL_COMMIT" >&2
+            exit 1
+          fi
+          appdir="$(agda --print-agda-app-dir)"
+          mkdir -p "$appdir"
+          echo "$T/cubical/cubical.agda-lib" > "$appdir/libraries"
+
+      - name: Proof gate (compile + coverage)
+        run: ./scripts/check-proofs.sh agda

CHANGELOG.adoc

@@ -20,6 +20,9 @@ open proof obligation.
 * Instantiated identity descriptiles (CLADE/ECOSYSTEM/ANCHOR/STATE/META)
 and the AFFIRMATION honesty snapshot with the systemet identity and an
 honest status (theory specified; proofs OPEN; no compiler here).
+* Added the wager experiment for coercions and roles in Cubical Agda
+(`+verification/proofs/agda/Wager/+`, stages 0 and 1), with an `+agda+` job
+in the proofs workflow. The experiment claims no ET obligation.
 
 ==== Changed
 

Justfile

@@ -48,7 +48,7 @@
     @echo "Version: {{version}}"
     @echo "RSR Tier: {{tier}}"
     @echo "Recipes: $(just --summary | wc -w)"
     @[ -f ".machine_readable/6a2/STATE.a2ml" ] && grep -oP 'phase\s*=\s*"\K[^"]+' .machine_readable/6a2/STATE.a2ml | head -1 | xargs -I{} echo "Phase: {}" || true
 
 # Run Invariant Path overlay tools for this repository
 invariant-path *ARGS:
@@ -107,6 +107,7 @@
 # An absent prover FAILS (never skips) — see scripts/check-proofs.sh.
 test *args:
     ./scripts/check-proofs.sh lean4
+    ./scripts/check-proofs.sh agda
     ./scripts/check-proof-status.sh
 
 # Run tests with verbose output
@@ -387,7 +388,7 @@
 
 # Update STATE.a2ml timestamp
 state-touch:
     @if [ -f ".machine_readable/6a2/STATE.a2ml" ]; then \
         sed -i 's/last-updated = "[^"]*"/last-updated = "'"$(date +%Y-%m-%d)"'"/' .machine_readable/6a2/STATE.a2ml && \
         echo "STATE.a2ml timestamp updated"; \
     fi

docs/status/PROOF-STATUS.adoc

@@ -13,6 +13,7 @@ summary from the per-prover MANIFESTs and fails if this file disagrees.
 // Machine-readable ground-truth markers — checked by scripts/check-proof-status.sh.
 // Do not edit by hand without changing the MANIFEST accordingly.
 // gate:lean4 gated=20 quarantined=0
+// gate:agda gated=29 quarantined=0
 
 == Summary
 
@@ -23,6 +24,7 @@ summary from the per-prover MANIFESTs and fails if this file disagrees.
 | ET obligations (DOM — the theory itself) | 15 | 2 | 2 | 11
 | MECH-1: L1 conversion, Lean4 (covers ET-1, ET-2, part of ET-3) | 1 | — | in progress | —
 | MECH-2: L2 grade algebras, Lean4 (covers ET-4, ET-5) | 1 | 1 | — | —
+| WAGER: the wager experiment for coercions and roles, Cubical Agda (claims no ET obligation) | 1 | - | in progress | -
 |===
 
 The Done/In-progress claims above are scoped to the *mechanized core
@@ -70,6 +72,49 @@ every theorem depends on nothing outside Lean's three-axiom trusted base
 | *Proven* (4 algebras + 1 generic construction)
 |===
 
+== The wager experiment (verified by `./scripts/check-proofs.sh agda`)
+
+This track is an experiment. It adds no ET obligation and it changes no ET
+status. A new obligation needs an ADR from the repository owner.
+
+The experiment decides, for a defined fragment, whether grades,
+conversion-only equality and tropes can replace the coercions and roles of
+System FC. Its own status file is
+`verification/proofs/agda/Wager/VERDICT.adoc`. The headline statements are
+types in `verification/proofs/agda/Wager/Statements.agda`.
+
+All items below compile under Agda 2.8.0 with `--cubical --safe` and
+`agda/cubical` v0.9 (pins in `verification/proofs/agda/Wager/TOOLCHAIN.adoc`).
+There is no `postulate`. The library forces `--guardedness` on each file, and
+no file uses coinduction. One warning class is silenced
+(`UnsupportedIndexedMatch`); `DESIGN-CHOICES.adoc` gives the reason.
+
+[cols="1,3,2", options="header"]
+|===
+| Stage | Artefact (Agda identifier) | Status
+
+| 1
+| `Wager.Proofs.l1-equality` : `DefEq t u ↔ nf t ≡ nf u`, for the L1 language
+  of the experiment (graded kind arrows, products, sums, a signature of
+  constants and total inspection primitives)
+| *Proven* for the experiment calculus. This is not the ET-2 calculus, and
+  it claims nothing for ET-2
+
+| 1
+| `Wager.Proofs.t0-substitution`, `t0-preservation`, `t0-progress` : graded
+  substitution, preservation and progress of the target calculus, for each
+  signature and each grade algebra
+| *Proven*
+
+| 1
+| `Wager.Proofs.affine-is-grade-algebra`, `level-is-grade-algebra`
+| *Proven* (law checks computed over the finite carriers)
+
+| 2 to 7
+| T1 to T7 of the experiment
+| not attempted
+|===
+
 == Mechanization slots
 
 [cols="1,3,2,2", options="header"]
@@ -115,6 +160,7 @@ just proof-check-all          # every prover with a MANIFEST; absent prover = FA
 just proof-check-lean4        # compile + coverage + lake build + axiom audit
 just proof-scan-dangerous     # comment-aware banned-construct scan
 ./scripts/check-proofs.sh lean4
+./scripts/check-proofs.sh agda    # the wager experiment (needs Agda 2.8.0 and cubical v0.9)
 ./scripts/check-proof-status.sh   # this file vs MANIFEST ground truth
 ----
 

verification/proofs/README.adoc

@@ -14,20 +14,30 @@ the template's own manifests. Git history retains them.
 [source]
 ----
 proofs/
-└── lean4/                       # the active development (hermetic, no deps)
-    ├── lean-toolchain           # pinned toolchain (elan)
-    ├── lakefile.toml
+├── lean4/                       # the active development (hermetic, no deps)
+│   ├── lean-toolchain           # pinned toolchain (elan)
+│   ├── lakefile.toml
+│   ├── MANIFEST                 # every file listed: gated | quarantine
+│   ├── Systemet.lean            # root import (coverage anchor)
+│   └── Systemet/
+│       ├── L1/...               # MECH-1: conversion for the core calculus
+│       │                        #   (ET-1, ET-2, part of ET-3)
+│       ├── L2/...               # MECH-2: grade-algebra laws + instances
+│       │                        #   (ET-4, ET-5)
+│       └── Audit.lean           # #print axioms over every headline theorem
+└── agda/                        # the wager experiment (Cubical Agda 2.8.0, cubical v0.9)
+    ├── wager.agda-lib           # library file: depends on cubical-0.9, no flags
     ├── MANIFEST                 # every file listed: gated | quarantine
-    ├── Systemet.lean            # root import (coverage anchor)
-    └── Systemet/
-        ├── L1/...               # MECH-1: conversion for the core calculus
-        │                        #   (ET-1, ET-2, part of ET-3)
-        ├── L2/...               # MECH-2: grade-algebra laws + instances
-        │                        #   (ET-4, ET-5)
-        └── Audit.lean           # #print axioms over every headline theorem
+    └── Wager/
+        ├── Statements.agda      # headline theorems as types only (review this file)
+        ├── Proofs.agda          # one inhabitant for each statement
+        ├── Grade/ L1/ L2/ ...   # the target calculus and its metatheory
+        ├── Examples/            # accepted and rejected closed examples
+        ├── VERDICT.adoc         # status of the experiment (it claims no ET obligation)
+        └── TOOLCHAIN.adoc       # pinned toolchain and the gate-failure record
 ----
 
-Other prover directories (idris2, agda, coq, tlaplus) are created only when
+Other prover directories (idris2, coq, tlaplus) are created only when
 a real systemet development lands in them, together with their MANIFEST.
 An on-disk proof file not listed in a MANIFEST fails the gate.
 
@@ -37,6 +47,7 @@ An on-disk proof file not listed in a MANIFEST fails the gate.
 ----
 just proof-check-all       # all provers with a MANIFEST (absent prover = FAIL)
 just proof-check-lean4     # the Lean4 development
+just proof-check-agda      # the wager experiment (Cubical Agda)
 just proof-scan-dangerous  # banned-construct scan (comment-aware)
 ----
 

verification/proofs/agda/MANIFEST

@@ -0,0 +1,32 @@
+# MANIFEST for verification/proofs/agda, read by scripts/check-proofs.sh
+# <source-root>|<module-path-relative-to-source-root>|gated|<note>
+# gated = must compile; quarantine = known-broken, must keep failing.
+verification/proofs/agda|Wager/Everything.agda|gated|import graph root (imports every Wager module)
+verification/proofs/agda|Wager/Statements.agda|gated|headline theorems as types only (the file a human reviews)
+verification/proofs/agda|Wager/Grade/Algebra.agda|gated|Stage 1: grade operations and the 15 law fields of the Lean class
+verification/proofs/agda|Wager/Grade/Finite.agda|gated|Stage 1: Boolean law checks for a finite carrier, with soundness
+verification/proofs/agda|Wager/Grade/Affine.agda|gated|Stage 1: Affine {0,1,omega} instance (systemet order)
+verification/proofs/agda|Wager/Grade/Level.agda|gated|Stage 1: two-point lattice instance Low <= High
+verification/proofs/agda|Wager/L1/Signature.agda|gated|Stage 1: signature of the L1 language
+verification/proofs/agda|Wager/L1/Syntax.agda|gated|Stage 1: kinds with graded arrows, types, renaming, substitution
+verification/proofs/agda|Wager/L1/SyntaxLemmas.agda|gated|Stage 1: laws of renaming and substitution
+verification/proofs/agda|Wager/L1/Conversion.agda|gated|Stage 1: DefEq (beta, delta, equivalence, congruence)
+verification/proofs/agda|Wager/L1/Normal.agda|gated|Stage 1: beta-normal forms, embedding, inspect
+verification/proofs/agda|Wager/L1/Eval.agda|gated|Stage 1: total normalizer nf by evaluation
+verification/proofs/agda|Wager/L1/Completeness.agda|gated|Stage 1: DefEq t u -> nf t = nf u
+verification/proofs/agda|Wager/L1/Soundness.agda|gated|Stage 1: DefEq t (emb (nf t))
+verification/proofs/agda|Wager/L1/Equality.agda|gated|Stage 1: DefEq t u <-> nf t = nf u
+verification/proofs/agda|Wager/L1/Heads.agda|gated|Stage 1: heads and injectivity of type formers up to DefEq
+verification/proofs/agda|Wager/L1/Kinding.agda|gated|Stage 1: graded kinding judgement
+verification/proofs/agda|Wager/L2/Signature.agda|gated|Stage 1: literals and trope transitions
+verification/proofs/agda|Wager/L2/Usage.agda|gated|Stage 1: usage vectors and usage matrices
+verification/proofs/agda|Wager/L2/Term.agda|gated|Stage 1: terms, values, reduction
+verification/proofs/agda|Wager/L2/Typing.agda|gated|Stage 1: declarative graded typing judgement with subusage
+verification/proofs/agda|Wager/L2/UsageLaws.agda|gated|Stage 1: laws of usage vectors and matrices from the algebra laws
+verification/proofs/agda|Wager/L2/Renaming.agda|gated|Stage 1 (T0): typing is stable under renaming; weakening
+verification/proofs/agda|Wager/L2/Substitution.agda|gated|Stage 1 (T0): graded substitution
+verification/proofs/agda|Wager/L2/Inversion.agda|gated|Stage 1: inversion of typing (for rejected examples)
+verification/proofs/agda|Wager/L2/Preservation.agda|gated|Stage 1 (T0): preservation
+verification/proofs/agda|Wager/L2/Progress.agda|gated|Stage 1 (T0): canonical forms and progress
+verification/proofs/agda|Wager/Proofs.agda|gated|one inhabitant for each statement of Statements.agda
+verification/proofs/agda|Wager/Examples/Stage1.agda|gated|Stage 1: accepted and rejected closed examples