Skip to content

Commit 456a1da

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
proof(SafeCrypto): annotate 15 bodyless decls as OWED (Refs standards#158) (#60)
## Summary Converts the **15 bodyless declarations** in `src/Proven/SafeCrypto/Proofs.idr` from the legacy `export <sig>` postulate form (with prose-only `-- |` comments) into the estate **OWED-with-justification** convention established by `Proven.SafeChecksum.Proofs` (and now SafeAPIKey #37, SafeMath #46, SafeTOML #52, SafeOTP #50, SafeCSRF #53, SafeString #54, ...): triple-pipe `||| OWED:` docstring + `0 ` erased-multiplicity + bare sig. No `postulate`, no `believe_me`, no `idris_crash`. Refs hyperpolymath/standards#158. ## Classification **SafeCrypto's prompt flagged that this is a crypto module — many decls may be permanent class-J hardness axioms. Audit result: 0/15.** | Category | Count | Notes | |---|---:|---| | Pure cryptographic-hardness axioms (class-J, *never* in pure Idris2 — collision resistance, preimage resistance, etc.) | **0** | None present. Would live in a separate `Assumptions.idr` parallel to proof-of-work's I6 `sha256CollisionResistant`. | | `Data.Bits` primitive opacity (xor / xor-commutativity / xor-cancellation / shiftR-cast round-trip — real discharge path via stdlib lemma) | **6** | `constantTimeRefl`, `constantTimeSym`, `digestEqRefl`, `digestEqSym`, `differentDigestsUnequal`, `counterNonceUnique` | | `String` FFI opacity (pack/unpack/length — same family as SafeChecksum Luhn/ISBN, SafeBuffer pack) | **3** | `tokenLengthApprox`, `uuidLength`, `hexEncodeEvenLength` | | Random-generation FFI opacity (OS entropy `getEntropy`/`/dev/urandom`) | **4** | `randomBytesLength`, `randomNatBounded`, `randomRangeBounded`, `freshNonceSize` | | `case`-on-abstract-algorithm reduction wall (`isSecure alg = case securityLevel alg of ...` won't reduce for abstract `alg` even with rewrite in scope) | **2** | `modernIsSecure`, `standardIsSecure` | Every entry has a **named blocker** and a **named discharge condition** in its `||| OWED:` docstring — discoverable by `grep "OWED" src/`, not silent. ## Per-decl summary ### Constant-time / digest comparison (5) - `constantTimeRefl : (d : ByteVector n) -> digestEq d d = True` — needs `Data.Bits` `xor x x = 0` lemma. - `constantTimeSym : (d1, d2 : ByteVector n) -> digestEq d1 d2 = digestEq d2 d1` — needs `Data.Bits` `xorCommutative`. - `digestEqRefl` / `digestEqSym` — same claims as `constantTime*` (API-discoverability duplicates); discharge together. - `differentDigestsUnequal : ... Not (d1 = d2) -> digestEq d1 d2 = False` — needs the `Data.Bits` cancellation lemma `xor x y = 0 -> x = y`, plus an induction over `Vect n`. ### Security-level case-analysis (2) - `modernIsSecure : ... securityLevel alg = Modern -> isSecure alg = True` - `standardIsSecure : ... securityLevel alg = Standard -> isSecure alg = True` Both block on the same `case`-under-abstract-scrutinee reduction wall: `isSecure alg = case securityLevel alg of ...` will not reduce under an abstract `alg : HashAlg` even after `rewrite` substitutes the scrutinee, because the `case` was not eta-expanded to a generalised motive at elaboration. **Real fix:** refactor `isSecure` in `SafeCrypto.Hash` to a top-level pattern-match dispatch on `securityLevel` — then both proofs close by `Refl` after `rewrite`. ### Random-generation FFI bounds (3) - `randomBytesLength`, `randomNatBounded`, `randomRangeBounded` — all hit the OS entropy FFI (`getEntropy` / `/dev/urandom`) which is opaque to 0.8.0's type-level reducer. `randomNat` further hits the `Integral Nat` `mod` blocker that `SafeChecksum.Proofs` already documents for `sumChecksum`. ### Nonce + UUID (3) - `counterNonceUnique` — encoding injectivity through Bits64 → 4-byte big-endian; needs `Data.Bits` `shiftR`/`cast` round-trip lemmas. - `freshNonceSize` — literally `randomBytesLength` lifted through the `freshNonce = randomBytes` rename; discharge together. - `uuidLength` — `pack [...]` over a fixed-shape list; needs `String` pack/length lemma. ### Token + hex even-length (2) - `tokenLengthApprox` — base64 expansion bound over `String` FFI `pack`/`unpack`/`Bits8 -> Char`. - `hexEncodeEvenLength` — even-length output of a parametric hex encoder; blocked both by the parametric signature (no per-byte hypothesis available) and by `String` FFI opacity even when specialised. Discharge requires (a) tightening the sig to the concrete `Proven.SafeCrypto.bytesToHex` AND (b) the `String`-FFI reflective tactic. ## Form (matches SafeChecksum / sibling PRs convention) ```idris ||| OWED: <claim restated> ||| <Idris2 0.8.0 blocker, by name> ||| Discharge once <unblocker>. public export 0 <name> : <original signature> ``` - Triple-pipe doc block - Leading `0 ` (erased-multiplicity, runtime-stripped) - Original bare signature otherwise unchanged - No `postulate`, no `believe_me`, no `idris_crash` - Matches `Proven.SafeChecksum.Proofs` L24–L100 reference pattern ## Phase 1 attempt Each OWED docstring names the *specific* blocker that prevents a real `Refl`/`rewrite` discharge today, and the *specific* unblocking condition. Highlights: - `modernIsSecure` / `standardIsSecure` are the closest to dischargeable today — the only structural obstacle is that `isSecure` is defined as an internal `case` rather than a top-level pattern-match; a 3-line refactor in `SafeCrypto.Hash` would let both close by `Refl` after the supplied rewrite. Filed as the named discharge condition rather than as a parallel change in this PR (keeps the diff to `Proofs.idr`-only per the campaign rule "Do NOT touch other files"). - The Bits-family and Random-family blockers re-verify the same `Data.Bits` and entropy-FFI opacity that `SafeChecksum` already documents; no new defect surfaced. ## Verification ``` $ idris2 -p base -p contrib --source-dir src --check src/Proven/SafeCrypto/Proofs.idr 1/4: Building Proven.Core (src/Proven/Core.idr) 2/4: Building Proven.SafeCrypto.Hash (src/Proven/SafeCrypto/Hash.idr) 3/4: Building Proven.SafeCrypto.Random (src/Proven/SafeCrypto/Random.idr) 4/4: Building Proven.SafeCrypto.Proofs (src/Proven/SafeCrypto/Proofs.idr) $ echo $? 0 ``` `Proven.SafeCrypto.Proofs` builds green together with its dependencies under Idris2 0.8.0. ## Scope - Touches **only** `src/Proven/SafeCrypto/Proofs.idr`. - 15 declarations annotated; the 9 already-discharged `Refl` proofs in the file (`sha256OutputSize`, `sha512OutputSize`, `sha3_256OutputSize`, `blake3OutputSize`, `sha256Secure`, `sha512Secure`, `sha3_256Secure`, `md5NotSecure`, `sha1NotSecure`, `hexEncodeDeterministic`) are untouched. - No callers outside this file; the other `constantTimeRefl`/`constantTimeSym` matches across the tree are namespaced-local distinct symbols in `SafeDigest` / `SafePassword`. ## Why draft Filed DRAFT per the convention (estate-wide proven CI queue jam, cf. sibling PRs #46/#52/#53). Owner to promote from DRAFT once the pool clears. ## Test plan - [x] `idris2 -p base -p contrib --source-dir src --check src/Proven/SafeCrypto/Proofs.idr` -> exit 0. - [x] No callers regression: grep clean for all 15 names outside Proofs.idr. - [x] Branch rebased on latest `origin/main` (after #51/#52/#53/#54 landed). - [ ] Owner-side: ratify against any in-flight SafeCrypto edits before merging. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 76951a8 commit 456a1da

1 file changed

Lines changed: 211 additions & 94 deletions

File tree

‎src/Proven/SafeCrypto/Proofs.idr‎

Lines changed: 211 additions & 94 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,26 @@
22
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
33
||| Proofs for SafeCrypto operations
44
|||
5-
||| This module contains proofs verifying properties of cryptographic operations.
6-
||| Non-trivial proofs are declared as postulates pending formal verification.
5+
||| This module contains proofs verifying properties of cryptographic
6+
||| operations. Items that reduce type-level by `Refl` under Idris2 0.8.0
7+
||| are stated as real proofs; items that hit a `Data.Bits` / `String`
8+
||| FFI / case-on-abstract-algorithm reduction wall are stated as
9+
||| **OWED-with-justification** in the SafeChecksum convention:
10+
|||
11+
||| * Triple-pipe `||| OWED:` docstring naming the claim, the Idris2
12+
||| 0.8.0 blocker, and the discharge condition.
13+
||| * `0 ` erased-multiplicity, bare signature, no body, no
14+
||| `postulate` keyword (estate convention — `Proven.SafeChecksum`
15+
||| and `Proven.SafeBuffer` set the pattern).
16+
||| * No `believe_me`, no `idris_crash`.
17+
|||
18+
||| None of the bodyless items below are pure cryptographic-hardness
19+
||| axioms (collision resistance, preimage resistance, etc.); they are
20+
||| structural properties (reflexivity, symmetry, length, bounds) that
21+
||| are gated by FFI/Bits/String opacity in 0.8.0, with a real
22+
||| in-language discharge path. The crypto-hardness assumption family
23+
||| (parallel to `proof-of-work`'s I6 `sha256CollisionResistant`)
24+
||| would live in a separate `Assumptions.idr` and is not present here.
725
|||
826
||| Updated for Idris 2 0.8.0 compatibility:
927
||| - `/=` returns Bool, not Type; replaced with `Not (x = y)` in signatures
@@ -26,20 +44,30 @@ import Data.Vect
2644
-- Constant-Time Properties
2745
--------------------------------------------------------------------------------
2846

29-
-- | Constant-time digest comparison is reflexive.
30-
-- | Postulated: digestEq uses a where-local accumulator loop over Vect;
31-
-- | proving reflexivity requires showing xor x x = 0 for all Bits8 and
32-
-- | that the accumulated .|. folds to 0, which involves Bits8 arithmetic
33-
-- | not reducible in Idris 2's type theory.
34-
export
35-
constantTimeRefl : (d : ByteVector n) -> digestEq d d = True
36-
37-
-- | Constant-time digest comparison is symmetric.
38-
-- | Postulated: requires showing xor is commutative for Bits8, which is
39-
-- | a primitive operation not reducible in Idris 2.
40-
export
41-
constantTimeSym : (d1, d2 : ByteVector n) ->
42-
digestEq d1 d2 = digestEq d2 d1
47+
||| OWED: constant-time `digestEq` is reflexive — `digestEq d d = True`
48+
||| for every `ByteVector n`. The implementation folds a where-local
49+
||| `go` over the Vect, accumulating `acc .|. (x `xor` x)` and then
50+
||| comparing `acc == 0`. Reducing this to `True` by `Refl` requires
51+
||| two `Data.Bits` lemmas not exposed as definitional equalities by
52+
||| Idris2 0.8.0's Prelude+contrib: (a) `xor x x = 0` for all `Bits8`,
53+
||| and (b) `0 .|. 0 = 0` reductively under arbitrary fold depth.
54+
||| Same blocker family as `Proven.SafeChecksum.Proofs` XOR-involution
55+
||| (FFI-opaque Bits primitives). Discharge once a `Data.Bits`
56+
||| reflective tactic / Prelude lemma is available.
57+
public export
58+
0 constantTimeRefl : (d : ByteVector n) -> digestEq d d = True
59+
60+
||| OWED: constant-time `digestEq` is symmetric —
61+
||| `digestEq d1 d2 = digestEq d2 d1`. Reduces to showing that
62+
||| `foldl (\a, (x,y) => a .|. (x xor y)) 0 (zip xs ys)` is invariant
63+
||| under `zip` argument swap, which in turn reduces to commutativity
64+
||| of `xor` on `Bits8`. `xor` is a primitive in Idris2 0.8.0 and does
65+
||| not reduce by `Refl` (no `Data.Bits` commutativity lemma in the
66+
||| stdlib). Same blocker family as `constantTimeRefl`. Discharge
67+
||| once `Data.Bits` exposes `xorCommutative : (x, y : Bits8) -> x \`xor\` y = y \`xor\` x`.
68+
public export
69+
0 constantTimeSym : (d1, d2 : ByteVector n) ->
70+
digestEq d1 d2 = digestEq d2 d1
4371

4472
--------------------------------------------------------------------------------
4573
-- Hash Output Size Properties
@@ -94,101 +122,177 @@ public export
94122
sha1NotSecure : isSecure SHA1_ALG = False
95123
sha1NotSecure = Refl
96124

97-
||| Modern algorithms are secure
98-
export
99-
modernIsSecure : (alg : HashAlg) ->
100-
securityLevel alg = Modern ->
101-
isSecure alg = True
102-
103-
||| Standard algorithms are secure
104-
export
105-
standardIsSecure : (alg : HashAlg) ->
106-
securityLevel alg = Standard ->
125+
||| OWED: any algorithm whose `securityLevel` is `Modern` is `isSecure`.
126+
||| `isSecure` is defined as a `case securityLevel alg of` with a
127+
||| wildcard `_ => True` arm covering `Modern` (and `Standard`). With
128+
||| the hypothesis `securityLevel alg = Modern` in scope we need to
129+
||| rewrite the scrutinee under the `case`, but Idris2 0.8.0 will not
130+
||| reduce `isSecure alg` for an abstract `alg : HashAlg` even after
131+
||| `rewrite` substitutes `securityLevel alg`, because the `case` was
132+
||| not eta-expanded to a generalised motive at elaboration time.
133+
||| Discharge by either (a) refactoring `isSecure` to a top-level
134+
||| pattern-match dispatch on `securityLevel`, or (b) hand-proving via
135+
||| `with (securityLevel alg) proof prf` once the 0.8.0 `with`/`rewrite`
136+
||| interaction is improved.
137+
public export
138+
0 modernIsSecure : (alg : HashAlg) ->
139+
securityLevel alg = Modern ->
107140
isSecure alg = True
108141

142+
||| OWED: any algorithm whose `securityLevel` is `Standard` is
143+
||| `isSecure`. Same blocker as `modernIsSecure` — the abstract `alg`
144+
||| prevents `isSecure alg` from reducing under the `case` even with
145+
||| the `securityLevel alg = Standard` rewrite in scope. Discharge
146+
||| together with `modernIsSecure` by the same refactor.
147+
public export
148+
0 standardIsSecure : (alg : HashAlg) ->
149+
securityLevel alg = Standard ->
150+
isSecure alg = True
151+
109152
--------------------------------------------------------------------------------
110153
-- Digest Comparison Properties
111154
--------------------------------------------------------------------------------
112155

113-
||| Digest equality is reflexive
114-
export
115-
digestEqRefl : (d : ByteVector n) -> digestEq d d = True
116-
117-
||| Digest equality is symmetric
118-
export
119-
digestEqSym : (d1, d2 : ByteVector n) -> digestEq d1 d2 = digestEq d2 d1
156+
||| OWED: digest equality is reflexive — `digestEq d d = True`. This
157+
||| is the same claim as `constantTimeRefl` above (they share the
158+
||| same implementation; the duplication is for API discoverability)
159+
||| and inherits the same `Data.Bits` `xor x x = 0` reductive blocker.
160+
||| Discharge together with `constantTimeRefl`.
161+
public export
162+
0 digestEqRefl : (d : ByteVector n) -> digestEq d d = True
120163

121-
-- | Different digests compare unequal (probabilistic property).
122-
-- | Uses `Not (d1 = d2)` instead of `d1 /= d2` because in Idris 2 0.8.0
123-
-- | the `/=` operator returns Bool, not a Type suitable for use in
124-
-- | type signatures.
125-
export
126-
differentDigestsUnequal : (d1, d2 : ByteVector n) ->
127-
Not (d1 = d2) ->
128-
digestEq d1 d2 = False
164+
||| OWED: digest equality is symmetric — `digestEq d1 d2 = digestEq d2 d1`.
165+
||| Same claim as `constantTimeSym` above; same `Data.Bits` `xor`
166+
||| commutativity blocker. Discharge together with `constantTimeSym`.
167+
public export
168+
0 digestEqSym : (d1, d2 : ByteVector n) -> digestEq d1 d2 = digestEq d2 d1
169+
170+
||| OWED: distinct `ByteVector`s compare unequal under `digestEq`.
171+
||| Stated with `Not (d1 = d2)` (propositional inequality) because
172+
||| Idris2 0.8.0's `/=` returns `Bool`, not `Type`. Discharge requires
173+
||| injectivity of the constant-time `xor`-fold comparator — i.e.,
174+
||| if the fold yields `0`, the input Vects are pointwise equal.
175+
||| Blocked on the same `Data.Bits` reductive lemmas as `constantTimeRefl`
176+
||| (`xor x y = 0 -> x = y`), plus an inductive over `Vect n`.
177+
||| Discharge once `Data.Bits` exposes the cancellation lemma OR once
178+
||| `digestEq` is refactored to recurse via `decEq` element-wise.
179+
public export
180+
0 differentDigestsUnequal : (d1, d2 : ByteVector n) ->
181+
Not (d1 = d2) ->
182+
digestEq d1 d2 = False
129183

130184
--------------------------------------------------------------------------------
131185
-- Random Generation Properties
132186
--------------------------------------------------------------------------------
133187

134-
||| Random bytes generates correct length output
135-
export
136-
randomBytesLength : (n : Nat) ->
137-
case randomBytes n of
138-
Right (MkByteVec v) => length v = n
139-
Left _ => ()
140-
141-
||| Random generation within bounds
142-
export
143-
randomNatBounded : (max : Nat) -> {auto ok : IsSucc max} ->
144-
case randomNat max of
145-
Right n => LT n max
146-
Left _ => ()
147-
148-
||| Random range respects min and max bounds
149-
export
150-
randomRangeBounded : (mn, mx : Nat) -> {auto ok : LTE mn mx} ->
151-
case randomNatRange mn mx of
152-
Right n => (LTE mn n, LTE n mx)
188+
||| OWED: when `randomBytes n` succeeds it returns a `ByteVec` whose
189+
||| underlying `Vect` has length `n`. This is true *by construction*
190+
||| of `MkByteVec : Vect n Byte -> ByteVec n` — `length v = n` is
191+
||| witnessed by the dependent index. However, `randomBytes` threads
192+
||| through the entropy-source FFI (`Proven.SafeCrypto.Random`'s OS
193+
||| `getEntropy` / `/dev/urandom` foreign call) which is opaque to
194+
||| Idris2 0.8.0's type-level reducer. The whole-program FFI block
195+
||| prevents `Refl` from closing the `case ... of Right (MkByteVec v) => length v = n`
196+
||| arm even though the dependent type already encodes the claim.
197+
||| Same blocker family as the boj-server I7 FFI-correctness
198+
||| assumption. Discharge by (a) reflecting `lengthFin` on the Vect
199+
||| index, or (b) refactoring the return type so the length witness
200+
||| is exposed without case-pattern reduction.
201+
public export
202+
0 randomBytesLength : (n : Nat) ->
203+
case randomBytes n of
204+
Right (MkByteVec v) => length v = n
205+
Left _ => ()
206+
207+
||| OWED: when `randomNat max` succeeds (with `IsSucc max`) the
208+
||| returned `Nat` is strictly less than `max`. The bound holds by
209+
||| construction in `Random.idr`'s `mod`-based implementation, but
210+
||| the FFI entropy source plus `mod max` reduction in Idris2 0.8.0
211+
||| (same `Integral Nat` `mod` blocker that `SafeChecksum.Proofs`
212+
||| documents for `sumChecksum`) prevents the `case` from reducing
213+
||| to `LT n max` by `Refl`. Discharge once the FFI entropy path is
214+
||| modelled propositionally and `modLT : (a, b : Nat) -> IsSucc b -> LT (a \`mod\` b) b`
215+
||| is available in `Data.Nat`.
216+
public export
217+
0 randomNatBounded : (max : Nat) -> {auto ok : IsSucc max} ->
218+
case randomNat max of
219+
Right n => LT n max
153220
Left _ => ()
154221

222+
||| OWED: when `randomNatRange mn mx` succeeds (with `LTE mn mx`) the
223+
||| result lies in `[mn, mx]`. Built atop `randomNat (S (minus mx mn))`
224+
||| then offset-added by `mn`, so inherits the `randomNatBounded`
225+
||| blocker plus needs `plusLteLeftCancel`/`plusLteMonotoneRight`
226+
||| reasoning. Same FFI + `Data.Nat` blocker family. Discharge
227+
||| together with `randomNatBounded`.
228+
public export
229+
0 randomRangeBounded : (mn, mx : Nat) -> {auto ok : LTE mn mx} ->
230+
case randomNatRange mn mx of
231+
Right n => (LTE mn n, LTE n mx)
232+
Left _ => ()
233+
155234
--------------------------------------------------------------------------------
156235
-- Nonce Properties
157236
--------------------------------------------------------------------------------
158237

159-
-- | Counter nonces are unique for different counters.
160-
-- | Uses `Not (c1 = c2)` instead of `c1 /= c2` for Idris 2 0.8.0
161-
-- | compatibility.
162-
export
163-
counterNonceUnique : (pfx : ByteVec 8) -> (c1, c2 : Bits64) ->
164-
Not (c1 = c2) ->
165-
Not (counterNonce pfx c1 = counterNonce pfx c2)
166-
167-
||| Fresh nonces have correct size
168-
export
169-
freshNonceSize : (n : Nat) ->
170-
case freshNonce n of
171-
Right (MkByteVec v) => length v = n
172-
Left _ => ()
238+
||| OWED: counter nonces are injective in the counter — for a fixed
239+
||| 8-byte prefix, distinct `Bits64` counters yield distinct 12-byte
240+
||| nonces. The implementation encodes the counter big-endian into
241+
||| the trailing 4 bytes by repeated `shiftR`+`prim__cast_Bits64Bits8`.
242+
||| Proving injectivity reduces to injectivity of that encoding, which
243+
||| in turn needs `Data.Bits` lemmas (`shiftR`+`cast` is a bijection
244+
||| on its range) that Idris2 0.8.0 does not expose. Same `Data.Bits`
245+
||| primitive opacity blocker as the constant-time family. Stated with
246+
||| `Not (c1 = c2)` for 0.8.0 (`/=` returns `Bool`). Discharge once
247+
||| `Data.Bits` exposes the requisite cast/shift round-trip lemmas.
248+
public export
249+
0 counterNonceUnique : (pfx : ByteVec 8) -> (c1, c2 : Bits64) ->
250+
Not (c1 = c2) ->
251+
Not (counterNonce pfx c1 = counterNonce pfx c2)
252+
253+
||| OWED: `freshNonce n` returns a `ByteVec` of length `n` on success.
254+
||| Definitionally `freshNonce = randomBytes`, so this is precisely
255+
||| `randomBytesLength` lifted through the rename. Same FFI entropy
256+
||| opacity blocker; discharge together with `randomBytesLength`.
257+
public export
258+
0 freshNonceSize : (n : Nat) ->
259+
case freshNonce n of
260+
Right (MkByteVec v) => length v = n
261+
Left _ => ()
173262

174263
--------------------------------------------------------------------------------
175264
-- Token Generation Properties
176265
--------------------------------------------------------------------------------
177266

178-
-- | Random token has expected length (base64 expansion).
179-
-- | Uses `LTE` instead of `<=` for Idris 2 0.8.0 compatibility
180-
-- | (the `<=` operator returns Bool, not a Type).
181-
export
182-
tokenLengthApprox : (bytes : Nat) ->
183-
case randomToken bytes of
184-
Right s => LTE (length s) ((bytes * 4 `div` 3) + 3)
185-
Left _ => ()
186-
187-
||| UUID v4 has correct format (36 chars with hyphens)
188-
export
189-
uuidLength : case randomUUID of
190-
Right s => length s = 36
191-
Left _ => ()
267+
||| OWED: `randomToken bytes` produces a base64 string whose length
268+
||| is bounded by the standard expansion `(bytes * 4 / 3) + 3`. Built
269+
||| as `map toBase64 (randomByteList bytes)`, so reduces to a bound
270+
||| on `length (toBase64 (...))`. `toBase64` operates over `String`
271+
||| via `pack`/`unpack` FFI primitives and `Bits8 -> Char` indexing,
272+
||| neither of which Idris2 0.8.0 can reduce at type level. Stated
273+
||| with `LTE` (0.8.0 `<=` returns `Bool`). Same `String` FFI
274+
||| opacity blocker as `Proven.SafeChecksum.Proofs` Luhn/ISBN family
275+
||| and `Proven.SafeBuffer.Proofs` pack/unpack family. Discharge
276+
||| once a `String`-FFI reflective tactic or pack/unpack length
277+
||| lemma is available.
278+
public export
279+
0 tokenLengthApprox : (bytes : Nat) ->
280+
case randomToken bytes of
281+
Right s => LTE (length s) ((bytes * 4 `div` 3) + 3)
282+
Left _ => ()
283+
284+
||| OWED: `randomUUID` produces a 36-character UUID-v4 string
285+
||| (`XXXXXXXX-XXXX-XXXX-XXXX-XXXXXXXXXXXX`, 32 hex chars + 4 hyphens).
286+
||| Built by `pack`-ing a fixed-shape list of hex digits and hyphens
287+
||| from `randomBytes 16`. Reducing `length (pack [...]) = 36` by
288+
||| `Refl` requires `pack`/`length` interaction lemmas that Idris2
289+
||| 0.8.0 does not provide for FFI `String`. Same `String` FFI
290+
||| opacity blocker as `tokenLengthApprox`. Discharge together with
291+
||| `tokenLengthApprox` once the pack/unpack length lemma lands.
292+
public export
293+
0 uuidLength : case randomUUID of
294+
Right s => length s = 36
295+
Left _ => ()
192296

193297
--------------------------------------------------------------------------------
194298
-- Sensitive Data Properties
@@ -211,9 +315,22 @@ hexEncodeDeterministic : (f : List Bits8 -> String) -> (bs : List Bits8) ->
211315
f bs = f bs
212316
hexEncodeDeterministic _ _ = Refl
213317

214-
-- | Hex encoding produces even-length string.
215-
-- | Postulated: depends on internals of bytesToHex which operates via
216-
-- | pack/unpack FFI boundaries.
217-
export
218-
hexEncodeEvenLength : (bytesToHex : List Bits8 -> String) -> (bs : List Bits8) ->
219-
mod (length (bytesToHex bs)) 2 = 0
318+
||| OWED: any `bytesToHex`-like encoder produces an even-length
319+
||| `String`. The intuition is that each input byte produces exactly
320+
||| two hex digits, so the output has length `2 * length bs`, which
321+
||| is divisible by 2. The signature here takes the encoder as a
322+
||| parameter (`bytesToHex : List Bits8 -> String`) to keep it
323+
||| abstract over the concrete implementation in `Proven.SafeCrypto`,
324+
||| but that means we cannot reduce `length (bytesToHex bs)` at all
325+
||| without inducting on `bs` and using a per-byte hypothesis on the
326+
||| parameter — which the parametric sig does not give us. Even when
327+
||| specialised to the concrete `Proven.SafeCrypto.bytesToHex`, the
328+
||| body goes through `concat`+`pack`+`map byteToHex` over the
329+
||| `String` FFI boundary, which Idris2 0.8.0 cannot reduce. Same
330+
||| `String` FFI opacity blocker as `tokenLengthApprox` and
331+
||| `uuidLength`. Discharge by (a) tightening the signature to the
332+
||| concrete `bytesToHex`, AND (b) the `String`-FFI reflective
333+
||| tactic / pack-length lemma.
334+
public export
335+
0 hexEncodeEvenLength : (bytesToHex : List Bits8 -> String) -> (bs : List Bits8) ->
336+
mod (length (bytesToHex bs)) 2 = 0

0 commit comments

Comments
 (0)