Idris2 0.9.0 dependency: SafeCrypto.modernIsSecure / standardIsSecure (case-rewrite eta-expansion) #83

Activity

1. hyperpolymath

   added

   enhancementNew capability or improvement to existing behaviourNew capability or improvement to existing behaviour

   on May 27, 2026
2. hyperpolymath

   added 2 commits that reference this issue on May 27, 2026

   docs: Phase 2 Days 11-21 complete — totality tickets + Tier C audit +…

   ...

   e28b863

   docs: Phase 2 Days 11-21 — totality tickets + Tier C audit + long-tai…

   ...

   984163f
3. hyperpolymath commented on Aug 27, 2026

   

   hyperpolymath

   on Aug 27, 2026

   OwnerAuthor

   More actions

   The premise is dead: both proofs are discharged on Idris2 0.7.0, no 0.9.0 required

   This issue tracks the Idris2 0.9.0 release timeline. It does not need to. Both OWED sites were
   discharged on 2026-08-27 against Idris2 0.7.0 — an older compiler than the 0.8.0 the issue
   names as limited — and the cures are in PR #206.

   What was actually blocking

   The issue diagnoses an elaborator limitation:

   case is not eta-expanded under rewrite in Idris2 0.8.0. … the elaborator fails to unfold the
   case scrutinee after the rewrite step.

   That is accurate only while alg is abstract — and alg does not have to stay abstract.
   HashAlg is a finite 11-constructor enum, and securityLevel is a top-level pattern match over
   all 11. Case-split on the enum and, for each concrete constructor, both securityLevel and
   isSecure reduce; Refl closes the goal directly. No rewrite, so nothing needs eta-expanding.

   The non-matching constructors are refuted by the hypothesis itself via impossible — they are
   not assumed away, not believe_me'd, and not axiomatised.

   modernIsSecure : (alg : HashAlg) -> securityLevel alg = Modern -> isSecure alg = True
   modernIsSecure MD5_ALG      Refl impossible
   modernIsSecure SHA1_ALG     Refl impossible
   modernIsSecure SHA224_ALG   Refl impossible
   modernIsSecure SHA256_ALG   Refl impossible
   modernIsSecure SHA384_ALG   Refl impossible
   modernIsSecure SHA512_ALG   Refl impossible
   modernIsSecure SHA3_256_ALG _ = Refl
   modernIsSecure SHA3_512_ALG _ = Refl
   modernIsSecure BLAKE2b_ALG  _ = Refl
   modernIsSecure BLAKE2s_ALG  _ = Refl
   modernIsSecure BLAKE3_ALG   _ = Refl

   standardIsSecure is the same shape: the four SHA-2 constructors reduce to True, the other seven
   are refuted.

   The three tracked actions, resolved

   • Test the discharge attempt against Idris2 0.9.0 once it ships — not required;
     discharged on 0.7.0.
   • If 0.9.0 fixes the eta-expansion: discharge the 2 proofs locally — done, and it was
     not the eta-expansion that mattered.
   • If 0.9.0 does NOT fix it: file an upstream Idris2 bug and reclassify as OWED-AXIOM —
     no upstream bug exists to file, and no axiom was needed.

   The issue's own Workaround section (hand-written inversion via with blocks, "~2–3h … not
   pattern-worthy") was also unnecessary. The actual cure is a plain total case split and is
   pattern-worthy: a proof over a finite enum rarely needs rewrite at all — it needs the scrutinee
   to stop being abstract.

   Verification

   idris2 -p contrib --source-dir src --check src/Proven/SafeCrypto/Proofs.idr → rc=0, 0 errors,
   on Idris2 0.7.0. Zero new believe_me / assert_total / postulate markers introduced — the
   trusted base is unchanged, which is the point: the obligation was discharged, not relocated.

   Disposition

   Leaving this open deliberately. It should close when PR #206 merges, not before — closing it
   now would mark the work done while the cure is still unmerged. Recommend adding Closes #83 to
   that PR rather than closing here.

   Idris2 0.7.0 (source/CI target 0.8.0), measured on the local working tree of PR #206's branch.
4. hyperpolymath

   closed this as completedin 3b118cbon Sep 13, 2026