Context
src/abi/EchidnaABI/TacticRecord.idr (introduced in commit 4118893 on branch feat/idris2-abi-tactic-record) defines a fixed-point confidence ABI for the GNN→Chapel cross-FFI tactic-record contract. The module proves the total-order properties (reflexivity, antisymmetry) but explicitly defers two round-trip lemmas. The deferral requires an LTE-weakening step on the nat side that was intentionally left out as honest proof debt rather than closing with believe_me or assert_total. The file body documents this at lines 88-93 and 191-196.
Deferred lemmas
natToFinToNat : (n : Nat) -> (prf : LT n (S MaxConfidence)) -> finToNat (natToFinLT n {prf}) = n
clampRoundtripInRange : (n : Nat) -> (prf : LT n (S MaxConfidence)) -> finToNat (clampConfidence n) = nConstraint
Zero believe_me, zero postulates, zero admits — same standard as the rest of src/abi/.
References
Filed via session 2026-05-30 TacticRecord landing arc.
Context
src/abi/EchidnaABI/TacticRecord.idr(introduced in commit 4118893 on branchfeat/idris2-abi-tactic-record) defines a fixed-point confidence ABI for the GNN→Chapel cross-FFI tactic-record contract. The module proves the total-order properties (reflexivity, antisymmetry) but explicitly defers two round-trip lemmas. The deferral requires an LTE-weakening step on the nat side that was intentionally left out as honest proof debt rather than closing withbelieve_meorassert_total. The file body documents this at lines 88-93 and 191-196.Deferred lemmas
Constraint
Zero
believe_me, zero postulates, zero admits — same standard as the rest ofsrc/abi/.References
src/abi/EchidnaABI/TacticRecord.idrFiled via session 2026-05-30 TacticRecord landing arc.