Repository navigation
feat(proofs): reversibility as a Loss grade — Agda kernel module pinned to resource-algebra (JNK-01, B of 3) - #150
Merged
Conversation
…mlink farm retired The Idris2 ABI surface was three trees: flat sources in src/abi/, the src/idris-abi/ symlink farm from #140 (so an .ipkg could reach them), and generated/idrisiser/. Collapse the first two into one: - src/abi/JanusKey/ABI/{Types,Layout,Foreign,Proofs}.idr, laid out by module name; src/abi/januskey-abi.ipkg beside them (sourcedir "."). - Foreign.idr now declares JanusKey.ABI.Foreign and imports JanusKey.ABI.{Types,Layout} (was Januskey.*, J1-3). No other content change in this commit. - src/idris-abi/ deleted. - scripts/check-abi-tree.sh (just abi-tree-check; first step of idris-abi.yml): fails on a second .ipkg, a second Foreign.idr, a symlink under src/abi, a module whose declared name differs from its path, or a package/file mismatch. Negative control run locally (symlink farm + casing split reintroduced -> FAIL; removed -> OK). - References repointed: Justfile, .github/workflows/idris-abi.yml, .machine_readable/contractiles/{Justfile,Mustfile.a2ml} (the dead $$f recipe replaced by the package check), tests/aspect/cross_cutting_test.sh, ffi/zig/{src/main.zig,include/januskey.h} comments, QUICKSTART-DEV.adoc, bot directives, PROOF-NEEDS.adoc. Not claimed here: the package still does not typecheck. Foreign.idr is the RSR template FFI (januskey_init/process/...) and never described ffi/zig's jk_* exports; the header's "generated from src/abi/Foreign.idr" comment was false and is corrected. Types.idr keeps its ten known errors. Both are the next commits. generated/idrisiser/ is outside the gate, unchanged. Refs: JNK-01 (ISSUES-2026-10-12), J1-3, P0-2 (#140). Assisted-by: Claude (claude.ai session, 2026-10-12) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9
…ed to resource-algebra verification/proofs/agda/Reversibility.agda (--safe --without-K, builtins only, resource-algebra's Prelude) grades januskey steps in the Loss instance (echo loss: 𝟙 = fin 0, 𝟘 = inf) and proves, for traces of steps: - all-lossless-trace: a trace of 𝟙 steps has grade 𝟙 (⊗ unit law). - lossless-trace-all: a trace of grade 𝟙 has only 𝟙 steps — a hidden loss cannot be papered over by composition. - obliterate-absorbs / obliterated-not-lossless: a trace containing an inf step has grade inf whatever precedes or follows it (annihilation, both sides), so it is never lossless. - wrap-unwrap-𝟙 / wrap-unwrap-id: the wrap/unwrap pair is a two-step trace of grade 𝟙, with the cancellation law `unwrap (wrap x) ≡ x` carried as an explicit premise (ReversiblePair.cancels), discharged outside Agda by crates/reversible-core's wrap/unwrap round-trip property test — cited, not assumed away. Expected rejections (tests/reject-agda, both refused at the intended claim): HiddenLoss (`1 != 0`), ReviveAfterObliterate (`inf != fin 0`). Gate: scripts/check-agda.sh (just test-agda; .github/workflows/agda-proofs.yml, DESIGNED until its first green run on the Debian 2.6.4.3 pin). Sibling: scripts/fetch-siblings.sh pins hyperpolymath/resource-algebra at cf9235c532712a783a404c359a1055f40134794a. Verified locally with Agda 2.6.3 under --safe --without-K --no-libraries --ignore-interfaces --double-check. Not claimed: a step's grade is derived from its code (it is an annotation whose soundness condition is the cancellation premise); file contents; anything cryptographic; the FFI-bridge homomorphism (OPEN on resource-algebra, filed from JNK-01). The Idris2 IsCNO/ReversibleOp pair corresponds to ReversiblePair by transcription — ASSUMED. Refs: JNK-01 step 3 (ISSUES-2026-10-12). Assisted-by: Claude (claude.ai session, 2026-10-12) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9
…he test that discharges the premise check-agda.sh counted any failure of a tests/reject-agda fixture as the expected refusal, so a fixture broken by an unrelated change (a renamed import, a parse error) would keep the gate green while testing nothing. Its reason column was also always empty: Agda does not print "error". - Each fixture now carries `-- expect: <text>`; the gate fails if the line is missing, if the fixture is accepted, or if the refusal log does not contain that text. An empty fixture directory also fails. HiddenLoss expects `1 != 0`, ReviveAfterObliterate `inf != fin 0`. - Passing fixtures print `[PASS] refused as expected: <file> (<text>)`. Negative controls run locally (Agda 2.6.3, not committed): a fixture refused for a missing import -> FAIL "refused, but not with '1 != 0'"; no expect line -> FAIL; an accepted fixture -> FAIL. Reversibility.agda (comments only, no definition changed): the cancellation premise was cited as "crates/reversible-core/tests/ property_tests.rs (wrap/unwrap round trip)". No such test or API exists; unwrap_safety_test.rs is about Rust's .unwrap(). The premise is execute/undo (ReversibleExecutor in crates/reversible-core/src/lib.rs), tested by crates/januskey-cli/tests/property_tests.rs:: execute_then_undo_is_identity, already a TESTED ledger row. The comments now say so. Refs: JNK-01 step 3. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9
agda-proofs.yml ran in `debian:trixie-slim` by tag while the rest of the prover setup is pinned (agda-bin=2.6.4.3-1+b2, resource-algebra by commit, actions/checkout by SHA) and idris-abi.yml pins its image by digest. The tag moves with every Debian point release, so the job could change under the same commit. Pinned to the trixie-slim index digest resolved from registry-1.docker.io on 2026-10-13. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9
Contributor
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 54 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
9 tasks done
Owner
Author
|
CI on
Generated by Claude Code |
Owner
Author
|
@coderabbitai review Generated by Claude Code |
Contributor
|
hyperpolymath
marked this pull request as ready for review
October 13, 2026 23:57
hyperpolymath
enabled auto-merge (squash)
October 13, 2026 23:58
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
hyperpolymath
disabled auto-merge
October 13, 2026 23:58
… claims ledger (JNK-01, C of 3) (#151) ## Summary JNK-01, stacked PR **C of 3**. The base is B, #150, which sits on A, #149. Review the commits from `0e477cb` on. With this PR the Idris2 ABI typechecks, its obligations are gated, and the dashboards carry a proof count that `dashboard-check` measures. It covers #145's acceptance criteria; #145 will be closed with the gate link once this is green. | Commit | What | |---|---| | `0e477cb` | Handoff patch 0003, unchanged. `Foreign.idr` declares the 13 real `jk_*` symbols from `januskey.h`; `Status` closed sum with total decoder, round-trip and injectivity; op-kind/algorithm codecs; `closeOnce : (1 h : LibHandle Open) -> IO (LibHandle Closed)` | | `7ff5767` | Handoff patch 0004, unchanged. Types/Layout/Proofs typecheck; placeholders replaced by `seqCNO`, `copyIsCNO`, `tamperBreaksLink`, `obliterateNotReversible`, or removed | | `91ee42f` | Handoff patch 0005, unchanged. `check-abi-layout.sh` (Idris ↔ header ↔ Zig), `check-idris-reject.sh` with three fixtures, status table in PROOF-NEEDS | | `922fa43` | **Found while verifying.** Rejection fixtures must fail for their stated reason, and `DoubleClose` was not testing a double close (below). The aspect-test census now covers `assert_smaller`, `partial` and holes, as PROOF-NEEDS already claimed it did | | `8327321` | #145 items 3 and 5: the Proofs header and the adversary lemmas restated honestly. `revokedKeyUnusable` removed: it took no revocation | | `c132e0f` | **Runbook step 4.** Claims ledger: 8 PROVEN, 5 new TESTED, 2 ASSUMED, 4 OPEN rows. README/TOPOLOGY/READINESS reconciled. `dashboard-check.yml` gets Idris2 and Agda | | `4a89651` | Merge of B's Debian digest pin (no new content) | ### Two findings the handoff did not have 1. **`DoubleClose` did not test a double close.** Idris2 refused it at the *first* `closeOnce h` (line 14, col 18) with "Trying to use linear name h in non-linear context". IO's `>>=` is not linear, so a *single* close in `do` is refused the same way. The fixture now puts both closes in a linear pair (`closeOnce h # closeOnce h`) and is refused with **"There are 2 uses of linear name h"**. Positive controls typecheck: `closeOnce h` and `closeOnce h # pure ()`. The consequence, now in `LibHandle`'s docstring: a linearly held handle cannot be closed inside plain IO `do` at all. Sequencing linear steps needs `Control.Linear.LIO`, which this module does not use. 2. **Pinning the expected message has its own trap.** Idris echoes source lines in its errors, so a fixture's `-- expect:` comment matched itself, and my first wrong-reason control *passed*. The gate now matches message lines only (` NN | ` excerpts excluded), and that control now fails. ## How has this been verified? ### HANDOFF §3, run exactly on the unmodified five-patch stack (`d565dbf`), Idris2 0.8.0 (bootstrap build of tag v0.8.0) and Agda 2.6.3 Every line matches the handoff. Filtered for length: Agda's per-dependency "Checking" lines, the 29 individual aspect `[PASS]` lines and section banners. ``` $ bash scripts/check-abi-tree.sh [check-abi-tree] OK: one ABI tree (4 modules, 1 package) $ bash scripts/check-abi-layout.sh [check-abi-layout] OK struct sizes (hash, keyid, oblit): 32 16 112 [check-abi-layout] OK oblit proof size vs header comment: 112 [check-abi-layout] OK status codes: 0 1 2 3 4 5 6 7 8 9 10 11 [check-abi-layout] OK status count: 12 [check-abi-layout] OK op kinds: 0 1 2 3 4 5 6 7 [check-abi-layout] OK algorithms: 0 1 2 3 4 [check-abi-layout] OK exported symbols: jk_close jk_execute jk_generate_key jk_init jk_obliterate jk_open jk_revoke_key jk_rotate_key jk_tx_begin jk_tx_commit jk_tx_rollback jk_undo jk_version [check-abi-layout] OK zig exports: (same 13) [check-abi-layout] OK: Idris2 ABI, januskey.h and ffi/zig agree $ idris2 --version Idris 2, version 0.8.0 $ idris2 --typecheck src/abi/januskey-abi.ipkg 1/4: Building JanusKey.ABI.Types (JanusKey/ABI/Types.idr) 2/4: Building JanusKey.ABI.Layout (JanusKey/ABI/Layout.idr) 3/4: Building JanusKey.ABI.Foreign (JanusKey/ABI/Foreign.idr) 4/4: Building JanusKey.ABI.Proofs (JanusKey/ABI/Proofs.idr) $ bash scripts/check-idris-reject.sh [check-idris-reject] refused as expected: tests/reject-idris/DoubleClose.idr (Error: While processing right hand side of twice. Trying to use linear name h in non-linea) [check-idris-reject] refused as expected: tests/reject-idris/ForgottenClose.idr (Error: While processing right hand side of leak. There are 0 uses of linear name h. ) [check-idris-reject] refused as expected: tests/reject-idris/UnknownStatusIsOk.idr (Error: While processing right hand side of twelveIsOk. When unifying:) $ bash scripts/check-agda.sh Agda version 2.6.3 resource-algebra at cf9235c refused as expected: tests/reject-agda/HiddenLoss.agda () refused as expected: tests/reject-agda/ReviveAfterObliterate.agda () [check-agda] OK $ bash tests/aspect/cross_cutting_test.sh PASS: 29 FAIL: 0 $ just test-proofs test-proofs-reject test-agda ... (the same output) ... exit 0 ``` The empty `()` reasons and the `DoubleClose` reason ("non-linear context") are the two anomalies that commits `5f17a45` (in B) and `922fa43` fix. ### This head: `just test-proofs test-proofs-reject test-agda` and the aspect test ``` [check-abi-tree] OK: one ABI tree (4 modules, 1 package) [check-abi-layout] PASS: Idris2 ABI, januskey.h and ffi/zig agree [OK] ABI package typechecks [check-idris-reject] PASS refused as expected: tests/reject-idris/DoubleClose.idr (There are 2 uses of linear name h) [check-idris-reject] PASS refused as expected: tests/reject-idris/ForgottenClose.idr (There are 0 uses of linear name h) [check-idris-reject] PASS refused as expected: tests/reject-idris/UnknownStatusIsOk.idr (Mismatch between: Just Ok and Nothing) [PASS] refused as expected: tests/reject-agda/HiddenLoss.agda (1 != 0) [PASS] refused as expected: tests/reject-agda/ReviveAfterObliterate.agda (inf != fin 0) [check-agda] OK PASS: 32 FAIL: 0 ``` ### `cargo run -q -p dashboard-check -- --check .` on this head The command exits 0 and every row is discharged; the final line is `✓ 119 tests measured, 8 PROVEN claims`. - Positive control: before the dashboard edits, the checker reported exactly the three stale "0 proofs" claims (TOPOLOGY:80, READINESS:12, READINESS:67). - Negative control: in a scratch copy with `seqCNO`'s proof broken, all seven Idris PROVEN rows fail with `` `idris2 --typecheck src/abi/januskey-abi.ipkg` failed ``. This is the first time PROVEN has been exercised on real rows rather than the unit tests' fake runner (#146). Negative controls for the gates, run locally and not committed: - **Rejection gate:** a fixture refused for a missing import fails; the old `DoubleClose` shape fails ("refused, but not with 'There are 2 uses of linear name h'"); a missing expect line fails; an accepted fixture fails; an unknown fixture name fails. - **Census:** each of `assert_smaller`, bare `partial`, `%default partial` and `?hole` in a scratch module fails its own check, and the same words in comments or docstrings do not. - **Layout gate:** a perturbed status code fails. ## Status rows moved | ID | Was | Now | Artefact | |---|---|---|---| | A-1, A-2, C-1…C-5 | — (the package did not typecheck) | PROVEN | `Foreign.idr::statusCodeInjective`, `::opKindRoundTrip`; `Proofs.idr::seqCNO`, `::tamperBreaksLink`; `Layout.idr::copyIsCNO`, `::obliterateNotReversible`, `::oblitAligned`; command `idris2 --typecheck src/abi/januskey-abi.ipkg` | | G-1 | — | PROVEN | `Reversibility.agda::lossless-trace-all`; command `bash scripts/check-agda.sh` | | A-3, A-4 ×2, A-5, bypass census | — | TESTED | `check-abi-layout.sh`; `tests/reject-idris/{DoubleClose,ForgottenClose,UnknownStatusIsOk}.idr`; `tests/aspect/cross_cutting_test.sh` | | A-4 (status table) | "PROVEN at the type; TESTED" | TESTED | one status per row; the fixtures are the evidence | | X-1 | EXTERNAL | ASSUMED | EXTERNAL is not a ledger status | | G-2 | ASSUMED (transcription) | ASSUMED | unchanged, now a ledger row | | G-3, E-1 (new), six security obligations, MPR-linked-to-Rust | OPEN (#145) | OPEN | file artefacts; #145 closes with this stack | ## Type of change - [x] 🐛 Bug fix: the ABI did not typecheck; the FFI described a template, not `ffi/zig` - [x] 🕳️ Soundness fix: tautological "proofs" removed; non-discriminating fixture fixed; census enforced - [x] 📖 Documentation: PROOF-NEEDS, README, TOPOLOGY, READINESS - [x] 🔧 Build / CI / tooling ## 📌 New pins - `dashboard-check.yml` runs in `ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff`. This is the digest `idris-abi.yml` already uses; it is new to this workflow. - `agda-bin=2.6.3-1build1` (Ubuntu noble), installed in that container, the version every local check here used. **Assumption to confirm in CI:** that the pinned pack image is the noble build. pack publishes noble and jammy; `latest` is noble. I could not read the image config from this session. ## Checklist - [x] Commits are signed, each with a `gpgsig` header. Note: the merge commit `4a89651` lacks the session trailer lines; it carries no content of its own. - [x] Project checks pass locally (above). No Rust source changed. - [x] New files carry SPDX identifiers. - [x] Docs updated. The dashboard numbers come from the ledger via `dashboard-check`, not written by hand. - [x] No soundness hole introduced: bypass census 32/32, enforced by a TESTED ledger row. ## Notes for reviewers - **Expected review questions, answered here:** - **`seqOp` keeps the first op's kind tag.** `ReversibleOp` has no sequence kind, and nothing depends on the tag. Documented at the definition. - **`LibHandle` vs `Types.Handle` are two notions, deliberately.** `LibHandle` is the wire handle with ownership. `Types.Handle` is the L7 aliasing model. - **Owner decision still needed: `generated/idrisiser/`.** Regenerate it with capitalised module names, or remove it. It is outside the gate and still does not typecheck. - **Not claimed:** "data loss is architecturally impossible" (the README caution stays); hash one-wayness and physical erasure (X-1, ASSUMED); the FFI-bridge homomorphism (G-3, OPEN). - **Not touched:** `STATE.a2ml` `[test-coverage]`, a dated 2026-04 snapshot that still says `idris2-proofs = "30"`, and its `idris2-in-ci` blocker. `dashboard-check` does not reconcile those fields. Owner's call. - Each red check will be examined once CI reports. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- _Generated by [Claude Code](https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| @@ -0,0 +1,32 @@ | |||
| # SPDX-License-Identifier: MPL-2.0 | |||
| permissions: | ||
| contents: read | ||
| jobs: | ||
| proofs: |
hyperpolymath
pushed a commit
that referenced
this pull request
Oct 14, 2026
…ESIGNED Two CodeRabbit findings on #149 (merged before they could ride it), plus one stale status line: - ffi/zig/include/januskey.h: the header said Foreign.idr is "checked by the ABI package typecheck". The typecheck does not compare the two files. On this stack the comparison is scripts/check-abi-layout.sh (symbols, status codes, enums, sizes; ledger row A-3), and the comment now names it. - scripts/check-abi-tree.sh: a dangling symlink at src/idris-abi passed `[ -e ]`, so the retired farm could come back as a broken link unnoticed. The check is now `-e || -L`. Reproduced: with `ln -s does-not-exist src/idris-abi` the old gate exits 0 and the new one exits 1 with "src/idris-abi exists (retired symlink farm)". - .github/workflows/agda-proofs.yml: "DESIGNED until its first green run" is no longer true; its first run on #150 was green under Agda 2.6.4.3 with both fixtures refused for their stated reasons. Checks: check-abi-tree OK, check-abi-layout PASS, workflow YAML parses. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9
7 of 8 tasks
hyperpolymath
pushed a commit
that referenced
this pull request
Oct 14, 2026
Hypatia flagged two warnings on #150, both for the same thing: job `proofs` in agda-proofs.yml had no `timeout-minutes`, so a hung apt install or sibling fetch could hold a runner for the 360-minute default. The job takes about 35 s; 15 minutes matches idris-abi.yml. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9
hyperpolymath
added a commit
that referenced
this pull request
Oct 14, 2026
… Hypatia on #150) (#152) ## Summary Small follow-ups to the JNK-01 stack (#149, #150, #151, now on `main` as `ad85593` and `bf54181`). These findings posted after their PRs merged. - **`ffi/zig/include/januskey.h` (CodeRabbit, #149).** The header said `Foreign.idr` is "checked by the ABI package typecheck", but the typecheck never compares the two files. The comparison is `scripts/check-abi-layout.sh` (symbols, status codes, enums, sizes; ledger row A-3), and the comment now names it. - **`scripts/check-abi-tree.sh` (CodeRabbit, #149).** A dangling symlink at `src/idris-abi` passed `[ -e ]`, so the retired farm could come back as a broken link unnoticed. The check is now `-e || -L`. - **`.github/workflows/agda-proofs.yml` (Hypatia WH006 and missing_timeout_minutes, #150).** Job `proofs` had no `timeout-minutes`, so a hang would hold a runner for the 360-minute default. It now has 15 minutes, matching `idris-abi.yml`; the job takes about 35 s. - **`.github/workflows/agda-proofs.yml`.** The header still said "DESIGNED until its first green run". Its first run on #150 was green under Agda 2.6.4.3, with both fixtures refused for their stated reasons. ## Type of change - [x] 🐛 Bug fix: the tree gate missed a dangling link - [x] 🔧 Build / CI / tooling: job timeout - [x] 📖 Documentation: two comments made true ## 📌 New pins None. ## How has this been verified? - **Reproduction:** with `ln -s does-not-exist src/idris-abi`, the old `check-abi-tree.sh` exits 0 and the new one exits 1 with `FAIL: src/idris-abi exists (retired symlink farm)`. - `bash scripts/check-abi-tree.sh` → `OK: one ABI tree (4 modules, 1 package)`. - `bash scripts/check-abi-layout.sh` → `PASS`. The edited header line contains nothing the layout gate parses. - `agda-proofs.yml` parses, `jobs.proofs.timeout-minutes` is 15, and its SPDX header stays on line 1. ## Checklist - [x] Commits are signed. - [x] Project checks pass locally (above). - [ ] New files carry SPDX identifiers: n/a, no new files. - [x] Docs updated (the two comments). - [x] No soundness hole introduced: the gate is stricter, nothing else changes. ## Notes for reviewers The red checks that are already red on `main` (the #135 set) will show here too; #149 has their causes. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --------- Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
JNK-01, stacked PR B of 3. The base is A, #149; review only the three commits below. Its content is independent of A: only the Justfile recipe context overlaps. C stacks on top because its claims ledger runs this PR's artefact.
8c30b17feat(proofs): handoff patch 0002, unchanged.verification/proofs/agda/Reversibility.agdaruns under--safe --without-Kand grades januskey's steps in resource-algebra'sLossinstance, pinned atcf9235c532712a783a404c359a1055f40134794abyscripts/fetch-siblings.sh. It proves:all-lossless-traceandlossless-trace-all: a trace is lossless iff every step is.obliterate-absorbsandobliterated-not-lossless: aninfstep annihilates on both sides.wrap-unwrap-𝟙andwrap-unwrap-id, with the cancellation law as an explicit premise.The gate is
scripts/check-agda.sh(just test-agda) and the new workflow isagda-proofs.yml. Expected rejections live intests/reject-agda/.5f17a45test(proofs), found while verifying:-- expect: <text>and the gate checks for it.crates/reversible-core/tests/property_tests.rs(wrap/unwrap round trip)", but there is no wrap/unwrap API or test in the Rust (unwrap_safety_test.rsis about.unwrap()). The premise isexecute/undo(ReversibleExecutor,crates/reversible-core/src/lib.rs), tested bycrates/januskey-cli/tests/property_tests.rs::execute_then_undo_is_identity, already a TESTED ledger row. Only comments change; no definition does.dca00f8ci(proofs): the job'sdebian:trixie-slimcontainer is pinned by digest, asidris-abi.ymlpins its image.agda-proofs.ymlis DESIGNED until its first green run on the 2.6.4.3 pinLocally I checked with Agda 2.6.3 (Ubuntu noble), the same version the handoff used. The workflow pins Debian trixie's
agda-bin=2.6.4.3-1+b2. I could not reach the Debian archive from this session to confirm that exact version string, so the first run on this PR is the evidence either way.Type of change
📌 New pins
hyperpolymath/resource-algebra@cf9235c532712a783a404c359a1055f40134794a(scripts/fetch-siblings.sh)debian:trixie-slim@sha256:a29215f6a35e51e22adffa17f89e9d2ef06214e64a2bad10d765c46aea49f11f(resolved 2026-10-13)agda-bin=2.6.4.3-1+b2(Debian trixie)actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1(v7.0.1, same asidris-abi.yml)How has this been verified?
Agda 2.6.3, with flags
--safe --without-K --no-libraries --ignore-interfaces --double-check, on this head:The logs show the refusals at the intended claims:
HiddenLoss.agdaat therefl,1 != 0 of type Nat;ReviveAfterObliterate.agdaat therefl,inf != fin 0 of type Grade.Negative controls for the hardened gate, run locally and not committed. Each one fails the gate:
Checklist
IsCNO↔ AgdaReversiblePairlink is ASSUMED; the bridge homomorphism is OPEN.Notes for reviewers
🤖 Generated with Claude Code
https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9
Generated by Claude Code