fix(abi): real jk_* FFI, ABI typechecks under Idris2 0.8.0, gates and claims ledger (JNK-01, C of 3) by hyperpolymath · Pull Request #151 · hyperpolymath/januskey

hyperpolymath · 2026-10-13T23:54:36Z

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

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.
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 (P1-0 (B): claims ledger — run every TESTED row, reconcile test/proof counts #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

🐛 Bug fix: the ABI did not typecheck; the FFI described a template, not ffi/zig
🕳️ Soundness fix: tautological "proofs" removed; non-discriminating fixture fixed; census enforced
📖 Documentation: PROOF-NEEDS, README, TOPOLOGY, READINESS
🔧 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

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.
Project checks pass locally (above). No Rust source changed.
New files carry SPDX identifiers.
Docs updated. The dashboard numbers come from the ledger via dashboard-check, not written by hand.
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.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9

Generated by Claude Code

…num codecs and a linear handle The previous Foreign.idr was the RSR template FFI (januskey_init, januskey_process, januskey_get_string, …) against template types (createHandle, handlePtr, Result) that Types.idr never defined. It never described ffi/zig, which exports jk_init … jk_version per ffi/zig/include/januskey.h. Now: - One %foreign declaration per exported symbol (13), C types as in the header; out-pointer parameters are caller-owned AnyPtr cells. - Status: a closed sum of the 12 header codes; statusCode / statusFromCode total; statusRoundTrip (one Refl per constructor) and statusCodeInjective (derived from the round trip, so it cannot drift from the table); statusFromInt refuses negatives and >11. decodeStatus keeps the raw int on failure; nothing is read as Ok by default. - opKindCode / algorithmCode in Types.idr's constructor order (= the header's enum order), each with a round-trip lemma. - LibHandle : LibState -> Type; closeOnce : (1 h : LibHandle Open) -> IO (LibHandle Closed) — destroy at most once, at the type. Scope stated in the docstring: linearity is a property of the binding; a handle bound by an IO <- is unrestricted, the guarantee holds for linear parameters. - Typed wrappers over the operations return Either Int Status. Not claimed: anything about the Zig implementation's behaviour (that is ffi/zig/test/integration_test.zig's job). Typechecks under Idris2 0.8.0 together with the next commit; this commit alone leaves Types/Layout/Proofs' known errors in place, so idris-abi.yml stays red until the stack lands. Refs: JNK-01 step 2 (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

…laced by theorems or removed The package had never typechecked (PR #140's "expected red"). Fixes, all semantics-preserving where the statement was true: - Types: import Data.String (isInfixOf) and Data.Nat; KeyId and ObliterationProof moved above ResultOf (forward references); MkHandle and MkTx now inhabit every state (their functions were unconstructible with a Pending/Available-only constructor); LinearFile and LinearKey keep the handle linear but their fields unrestricted (a linear field cannot be read twice or dropped); oblitMostExpensive (`So (3*n >= n)` by Oh on an open n) restated as oblitCostDominates : LTE n (3 * n) = lteAddRight n. - Layout: Aligned stated as divisibility with an explicit quotient (`mod` on Nat does not reduce, so `mod size boundary = 0` could never be Refl); bodiless copyDeleteCNO (false as stated: IsCNO for *any* op of kind Copy) replaced by copyOp + copyIsCNO, a theorem on the (path, hash) log model; canRollback (returned its argument) replaced by obliterateNotReversible. - Proofs: overwriteCoversAll via gteRefl; chainNoGaps no longer matches the index (EmptyChain has none: absurd); cnoPairCompose (Unit) replaced by seqOp + seqCNO (composition of CNOs is a CNO); tamperDetectable (Unit) replaced by tamperBreaksLink; errorCodeDeterministic now over Foreign.Status (its CError was never defined). Removed, reason recorded in source beside the replacement: memoryDefeatsGPU, timeCostMonotonic, outputIs256Bits, threePassMinimum, defaultExceedsMinimum, defaultMeetsOWASP, defaultMemoryOWASP, identityIsCNO, hashOneWay, linearFileConsumed (ill-typed; claimed LinearFile -> Void), systemForgetsOldKey. None was a statement about the thing its name claimed. Verified: idris2 --typecheck src/abi/januskey-abi.ipkg, 4/4 modules, zero warnings, Idris2 0.8.0 (bootstrap build, locally); no believe_me / assert_total / assert_smaller / %partial / holes in src/abi. Refs: JNK-01 steps 1–2 (ISSUES-2026-10-12), #145. 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

@sizeof

…us table in PROOF-NEEDS - scripts/check-abi-layout.sh (just abi-layout-check; CI step before the typecheck): Idris2 StructSize vs Zig @sizeof asserts, statusCode table vs januskey.h JK_* #defines, op-kind/algorithm tables vs the header enums, %foreign symbols vs header prototypes vs `pub export fn`s. No compiler needed. Negative control: one perturbed status code -> FAIL. - scripts/check-idris-reject.sh (just test-proofs-reject; CI step after the typecheck): each tests/reject-idris fixture is appended to a scratch copy of the package as JanusKey.ABI.Reject.<Name> and must be refused. DoubleClose ("linear name h in non-linear context"), ForgottenClose ("0 uses of linear name h"), UnknownStatusIsOk (unification) — all three refused under 0.8.0. - PROOF-NEEDS.adoc: status table A-1..A-5, C-1..C-5, G-1..G-3, X-1 in the five-status vocabulary with artefacts; the removed-placeholder list; model limits; note that README/TOPOLOGY/READINESS still carry the "does not typecheck (#145)" wording and #146 ledger counts, to be reconciled by dashboard-check when this stack lands (not hand-edited). - README.adoc: the one sentence about src/abi that became false, corrected (the caution that data-loss impossibility is not a theorem stays). Refs: JNK-01 (ISSUES-2026-10-12), #145, #146. 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

…ose now tests the second close check-idris-reject.sh counted any refusal as the expected one. Pinning each fixture to its message showed that DoubleClose was not testing what it claims: it was refused at its *first* close ("Trying to use linear name h in non-linear context", line 14 col 18), because IO's bind is not linear. A single close in IO do-notation is refused the same way, so the fixture never reached the second close. - DoubleClose puts the two closes in a linear pair (`closeOnce h # closeOnce h`) and is refused with "There are 2 uses of linear name h". Positive controls, run locally and not committed: `closeOnce h` and `closeOnce h # pure ()` both typecheck. - Each fixture carries `-- expect: <text>`. The gate fails if that line is missing, if the fixture typechecks, or if the message (Idris's echoed ` NN | ` source lines excluded, since they contain the expect comment) does not contain the text. ForgottenClose expects "There are 0 uses of linear name h"; UnknownStatusIsOk expects "Mismatch between: Just Ok and Nothing". - The gate takes optional fixture names, so one ledger row can run one fixture; a named fixture that does not exist fails. - Foreign.idr (docstring only): plain IO's bind is not linear, so a linear LibHandle cannot be closed inside IO do-notation at all; sequencing needs a linear monad (Control.Linear.LIO), not used here. Negative controls (Idris2 0.8.0, not committed): a fixture refused for a missing import -> FAIL; the old DoubleClose shape -> FAIL "refused, but not with 'There are 2 uses of linear name h'"; no expect line -> FAIL; an accepted fixture -> FAIL; an unknown fixture name -> FAIL. tests/aspect/cross_cutting_test.sh: PROOF-NEEDS cites it for a census of believe_me, assert_total, assert_smaller, partial and holes, but it checked only believe_me, assert_total, postulate and sorry. It now also checks assert_smaller, partial (also catching `%default partial`) and holes (`?name`), with comment and docstring lines stripped: 32/32. Controls: each bypass in a scratch module fails its own check; the same words in comments and docstrings do not. The "(30+ proofs)" label on the Proofs.idr existence check is dropped; that count was false. Refs: JNK-01, #145. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9

…tems 3 and 5) #145 asks that adversaryCannotKnow be deleted or restated honestly and marked OPEN, and that the misleading "No postulate" header go. The stack did neither. - Proofs.idr header: "Proves correctness properties for all JanusKey operations ... no postulate — fully total" becomes a list of what the module holds, pointing at the claims ledger for what each states and at the aspect test for the bypass census. - Types.adversaryCannotKnow (definition unchanged): its docstring said "Proof: adversary cannot recover obliterated content". It now says the type is uninhabited only because Knows has no Adversary constructor, a property of the model, and that recovery after obliteration is OPEN in the ledger (row E-1, next commit). PostObliteration's docstring ("this is an impossibility proof") is restated as what it is, a marker. - Proofs.revokedKeyUnusable removed: it was adversaryCannotKnow at KeyId and took no revocation, so its name claimed what it did not state (the same reason the stack removed systemForgetsOldKey). Nothing referenced it. - Types.systemKnowsNewKey: "but not the old" dropped from its docstring; Knows has no negative form. idris2 --typecheck src/abi/januskey-abi.ipkg: 4/4, no warnings (0.8.0). Refs: #145. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9

…conciled; dashboard-check gets the provers The fourth step of the runbook's T0: the status table in PROOF-NEEDS ("Same day, three commits later") enters the claims ledger, and the dashboards take the count dashboard-check measures, not one written by hand. Ledger (26 rows, one line each, IDs matching the status table): - PROVEN (8): A-1 statusCodeInjective, A-2 opKindRoundTrip, C-1 seqCNO, C-2 copyIsCNO, C-3 obliterateNotReversible, C-4 tamperBreaksLink, C-5 oblitAligned (command: idris2 --typecheck src/abi/januskey-abi.ipkg); G-1 lossless-trace-all (command: bash scripts/check-agda.sh). - TESTED (+5): A-3 check-abi-layout; A-4 DoubleClose and ForgottenClose; A-5 UnknownStatusIsOk; the src/abi bypass census. The execute/undo row is marked as G-1's cancellation premise. - ASSUMED: G-2 (Idris2 IsCNO <-> Agda ReversiblePair, by transcription), X-1 (hash one-wayness, physical erasure). - OPEN: G-3 (bridge homomorphism), E-1 (attacker recovery / revoked-key use; #145 item 3), the six security obligations, MPR linked to the Rust. The two #145-pointing OPEN rows are replaced: their typecheck half is now the PROVEN rows, and #145 closes with this stack. Status table: one status per row from the five-status vocabulary. A-4 "PROVEN at the type; TESTED" -> TESTED (the fixtures are the evidence); C-5 and G-1 qualifiers moved out of the status cell; X-1 "EXTERNAL" -> ASSUMED (EXTERNAL is not a ledger status); E-1 added. Census line now 32/32. Current State, Recommended Prover (Agda kernel, Idris2 ABI, per the 2026-10-12 ruling) and Priority no longer say the ABI is missing or placeholder. Dashboards: TOPOLOGY MPR line and READINESS justification, row 16, totals and debt list say the ABI typechecks and 8 proofs are checked (ABI and grade lemmas, not the security obligations). Positive control: before these edits dashboard-check reported exactly the three stale "0 proofs" claims (TOPOLOGY:80, READINESS:12, READINESS:67). dashboard-check.yml: PROVEN rows run their checker, so the job now runs in the pinned idris2-pack image idris-abi.yml uses, installs agda-bin=2.6.3-1build1 from apt (the version every local check here used) and curl for rustup; timeout 15 -> 30 min. check-abi-layout.sh prints PASS on success, which a TESTED row needs. Verified (Idris2 0.8.0, Agda 2.6.3): cargo run -p dashboard-check -- --check . -> OK, "119 tests measured, 8 PROVEN claims", every row discharged. Negative control: a scratch copy with seqCNO's proof broken fails all seven Idris PROVEN rows. Refs: JNK-01, #145, #146. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9

…age pin)

coderabbitai · 2026-10-13T23:54:46Z

Important

Review skipped

Auto reviews are disabled on base/target branches other than the default branch.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Advanced
Run ID: 059e5c63-3bc3-4614-8a71-01312438b56d

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

🔍 Trigger review

Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

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.

❤️ Share

_{Comment @coderabbitai help to get the list of available commands.}

hyperpolymath · 2026-10-13T23:57:46Z

CI on 4a89651. Every check this stack owns is green:

idris-abi: green (job). All four steps pass: tree invariants, header/Zig agreement, typecheck in idris2-pack@sha256:f0758996…, and the expected rejections. This is the first green run of the job (J1-3: make the Idris2 ABI typecheck; delete or honestly restate the six unproved security claims #145 item 6).
dashboard-check: green (job), in about 2 min. Every ledger row was discharged in CI, ending ✓ 119 tests measured, 8 PROVEN claims. agda-bin=2.6.3-1build1 resolved, which settles the open assumption in the PR body: the pinned pack image is the noble build.
agda-proofs: green under Agda 2.6.4.3.
rust-ci: green (check, clippy, fmt, test).
The inherited main set (main is red on 7 of 12 workflows; four e2e jobs die at dtolnay/rust-toolchain@v1, so the unit tests have no CI measurement #135) is red for the reasons in refactor(abi): one ABI tree — module-path layout, JanusKey casing, symlink farm retired (JNK-01, A of 3) #149: lint-workflows, governance / Workflow security linter, governance / Allowlist Preflight, Validate DEED manifests. dashboard-check.yml was already on the lint-workflows list before this PR: its first line is the actions-lock banner.

Generated by Claude Code

hyperpolymath · 2026-10-13T23:57:47Z

@coderabbitai review

Generated by Claude Code

coderabbitai · 2026-10-13T23:57:54Z

⚠️ Action not completed

Review rate limited.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.

… 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>

claude added 7 commits October 13, 2026 23:41

Merge branch 'proofs/reversibility-grade' into the C stack (Debian im…

4a89651

…age pin)

hyperpolymath mentioned this pull request Oct 13, 2026

feat(proofs): reversibility as a Loss grade — Agda kernel module pinned to resource-algebra (JNK-01, B of 3) #150

Merged

7 tasks done

hyperpolymath marked this pull request as ready for review October 13, 2026 23:57

hyperpolymath mentioned this pull request Oct 13, 2026

J1-3: make the Idris2 ABI typecheck; delete or honestly restate the six unproved security claims #145

Closed

Merge branch 'proofs/reversibility-grade' into claude/new-session-lwzjw0

5712a6c

hyperpolymath merged commit ad0c833 into proofs/reversibility-grade Oct 13, 2026
21 of 27 checks passed

hyperpolymath deleted the claude/new-session-lwzjw0 branch October 13, 2026 23:58

hyperpolymath mentioned this pull request Oct 14, 2026

fix(abi): review follow-ups from the JNK-01 stack (CodeRabbit on #149, Hypatia on #150) #152

Merged

7 of 8 tasks

Navigation Menu

Repository navigation

fix(abi): real jk_* FFI, ABI typechecks under Idris2 0.8.0, gates and claims ledger (JNK-01, C of 3) - #151

fix(abi): real jk_* FFI, ABI typechecks under Idris2 0.8.0, gates and claims ledger (JNK-01, C of 3)#151
hyperpolymath merged 8 commits into
proofs/reversibility-gradefrom
claude/new-session-lwzjw0

hyperpolymath commented Oct 13, 2026

Uh oh!

coderabbitai Bot commented Oct 13, 2026 •

edited

Loading

Review skipped

Uh oh!

hyperpolymath commented Oct 13, 2026

Uh oh!

hyperpolymath commented Oct 13, 2026

Uh oh!

coderabbitai Bot commented Oct 13, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

hyperpolymath commented Oct 13, 2026

Summary

Two findings the handoff did not have

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

This head: just test-proofs test-proofs-reject test-agda and the aspect test

cargo run -q -p dashboard-check -- --check . on this head

Status rows moved

Type of change

📌 New pins

Checklist

Notes for reviewers

Uh oh!

coderabbitai Bot commented Oct 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Review skipped

Uh oh!

hyperpolymath commented Oct 13, 2026

Uh oh!

hyperpolymath commented Oct 13, 2026

Uh oh!

coderabbitai Bot commented Oct 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

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

This head: `just test-proofs test-proofs-reject test-agda` and the aspect test

`cargo run -q -p dashboard-check -- --check .` on this head

coderabbitai Bot commented Oct 13, 2026 •

edited

Loading

coderabbitai Bot commented Oct 13, 2026 •

edited

Loading