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.idr typechecks.- For each of
copyDeleteCNO, memoryDefeatsGPU, timeCostMonotonic, cnoPairCompose, tamperDetectable and adversaryCannotKnow, 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-abi job 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
ULTRAPLAN J1-3, filed from the
idris-abi (expected red until J1-3)job that #142 added. That job runsidris2 --typecheck src/abi/januskey-abi.ipkgin theidris2-pack@sha256:f0758996…image and is red by design until the items below are done.Acceptance criteria
src/abi/Foreign.idr.src/abi/Types.idrtypechecks.copyDeleteCNO,memoryDefeatsGPU,timeCostMonotonic,cnoPairCompose,tamperDetectableandadversaryCannotKnow, do one of two things:chainNoGaps, or delete it.idris-abijob is green on the fix commit. Making it a required check is J1-4.Measured 2026-10-02 on
main539e6f9:src/abi/Proofs.idrhas 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