Repository navigation
J1-3: make the Idris2 ABI typecheck; delete or honestly restate the six unproved security claims #145
Description
ULTRAPLAN J1-3, filed from the idris-abi (expected red until J1-3) job that #142 added. That job runs idris2 --typecheck src/abi/januskey-abi.ipkg in the idris2-pack@sha256:f0758996… image and is red by design until the items below are done.
Acceptance criteria
- Fix the module-name case mismatch in
src/abi/Foreign.idr. src/abi/Types.idrtypechecks.- For each of
copyDeleteCNO,memoryDefeatsGPU,timeCostMonotonic,cnoPairCompose,tamperDetectableandadversaryCannotKnow, do one of two things:- delete it, or
- restate it honestly and mark it OPEN in the claims ledger (P1-0).
- Fix the FS case of
chainNoGaps, or delete it. - Remove the misleading "No postulate" header.
- The
idris-abijob is green on the fix commit. Making it a required check is J1-4.
Measured 2026-10-02 on main 539e6f9: src/abi/Proofs.idr has 26 top-level declarations (grep -cE '^[a-z][A-Za-z0-9_]* *:'), and the docs claim "30 proofs". The counts are reconciled in P1-0 (#134).
🤖 Generated with Claude Code
Activity
fix(ci): make Rust Build + rust-ci able to go green; unmask clippy/fmt (
P1-0 (B): claims ledger — run every TESTED row, reconcile test/proof …
hyperpolymath commentedon Oct 13, 2026
Closed by the JNK-01 stack: #149 (A, one ABI tree) → #150 (B, Agda kernel module) → #151 (C, real FFI, typecheck, gates, ledger).
Gate:
idris-abiis green on C's head4a89651(job): tree invariants, header/Zig agreement,idris2 --typecheck src/abi/januskey-abi.ipkginidris2-pack@sha256:f0758996…, and expected rejections.dashboard-checkon the same head discharges the ledger with 8 PROVEN rows (job).Acceptance criteria:
Januskey.ABI.Foreign→JanusKey.ABI.Foreign, andscripts/check-abi-tree.shfails on any module whose name differs from its path (refactor(abi): one ABI tree — module-path layout, JanusKey casing, symlink farm retired (JNK-01, A of 3) #149).Types.idrtypechecks, together with Layout, Foreign and Proofs: 4/4 modules, no warnings, Idris2 0.8.0 (fix(abi): real jk_* FFI, ABI typechecks under Idris2 0.8.0, gates and claims ledger (JNK-01, C of 3) #151).copyDeleteCNO→copyOp+copyIsCNO;cnoPairCompose→seqOp+seqCNO;tamperDetectable→tamperBreaksLink;memoryDefeatsGPUandtimeCostMonotonicremoved.adversaryCannotKnowis restated (it holds only becauseKnowshas no Adversary constructor) and is the OPEN ledger row E-1.revokedKeyUnusableis removed for the same reason.chainNoGapsno longer matches the index;EmptyChainis discharged byabsurd.Proofs.idris replaced by a pointer to the ledger and the bypass census.idris-abiis green on the fix commit (above). Making it a required check is J1-4.maincarries the fix once the stack merges.Generated by Claude Code
refactor(abi): one ABI tree — module-path layout, JanusKey casing, sy…
fix(abi): real jk_* FFI, ABI typechecks under Idris2 0.8.0, gates and…