Skip to content

Commit dcf5ed5

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
proof(SafeOTP): annotate 5 bodyless decls as OWED (Refs standards#158) (#50)
## Summary Converts the **5** bodyless declarations in `src/Proven/SafeOTP/Proofs.idr` from terse `Postulated:` comments (or no justification at all) to the estate's **OWED-with-justification** convention established 2026-05-20 across SafeChecksum / Buffer / CryptoAccel / HKDF / Bloom / FPGA, and continued in sibling PRs #37 (SafeAPIKey), #38 (SafeCORS), #39 (SafeCSV), #40 (SafeSemVer), #41 (SafeHtml), #46 (SafeMath): - Triple-pipe `|||` doc-comment stating the claim - `0 ` (erased multiplicity) so the postulate is not runtime-callable - Bare signature, no `postulate` keyword (estate-wide choice) - Explicit Idris2 0.8.0 blocker + discharge condition Refs hyperpolymath/standards#158. ## The 5 OWED items ### 1. `constantTimeCompareRefl` **Claim:** `constantTimeCompare s s = True` for every `String s`. **Why OWED:** witnessed operationally — the `length as /= length bs` guard collapses to `False`, then `go` folds `acc && (x == y)` with `x == y` true at every position. However, Idris2 0.8.0 does not reduce `unpack s` (FFI-bound) at the type level, nor does it expose a `c == c = True` Refl lemma for `prim__eq_Char`. Same blocker family as boj-server's `Boj.SafetyLemmas.charEqSym` (discharged there as a class-(J) `%unsafe believe_me` axiom). **Discharge:** a `Data.String` / `Data.Char` reflective tactic, or a class-(J) `charEqRefl` axiom plus per-list induction over `go`. ### 2. `constantTimeCompareSym` **Claim:** `constantTimeCompare a b = constantTimeCompare b a`. **Why OWED:** symmetric componentwise — length equality is symmetric, Char equality is symmetric — but `prim__eq_Char` does not expose `(x == y) = (y == x)` as a Refl lemma, and `unpack` does not reduce. Same blocker family as `constantTimeCompareRefl`. **Discharge:** as above, plus a class-(J) `charEqSym` axiom. ### 3. `codeValidatesAgainstSelf` **Claim:** `validateTOTPCode code [code] = True`. **Why OWED:** direct downstream corollary of `constantTimeCompareRefl` — definitional unfolding gives `constantTimeCompare code.code code.code || False`. Cannot be discharged until `constantTimeCompareRefl` is. **Discharge:** immediate `rewrite` step once `constantTimeCompareRefl` is in scope. ### 4. `codeInListValidates` **Claim:** if `any (\e => constantTimeCompare code.code e.code) codes = True` then `validateTOTPCode code codes = True`. **Why OWED:** this is literally the function's body equality, but Idris2 0.8.0 does not eta-reduce the lambda inside `any` at the type level for an abstract `codes`, and the `constantTimeCompare` underneath inherits the String FFI opacity. **Discharge:** induction on `codes` (one-line `Refl` for `[]`, `rewrite` step for `_ :: _`) — can be inlined here, or pulled in once a `Data.List.any` extensionality lemma lands in `contrib`. ### 5. `identicalHOTPValid` **Claim:** `validateHOTPCode code code = True`. **Why OWED:** direct downstream corollary of `constantTimeCompareRefl` — `validateHOTPCode submitted expected = constantTimeCompare submitted.code expected.code` reduces to `constantTimeCompare code.code code.code` for identical inputs. **Discharge:** immediate once `constantTimeCompareRefl` is in scope. ## Safety posture - Zero `believe_me` - Zero `postulate` - Zero `idris_crash` - All `0`-erased — postulates cannot leak into runtime - All discoverable as named declarations (vs silent / commented-out) ## Scope - Touches only `src/Proven/SafeOTP/Proofs.idr` - The 10 Refl-discharged proofs in the file (divisors, default-period, defaults, secret guards, empty-list rejection, etc.) are untouched ## Why draft Estate CI is currently jammed on base-package dependency resolution (see sibling SafeHtml PR #41 thread). DRAFT until CI is unjammed, at which point owner can flip to ready-for-review. ## Test plan - [ ] Idris2 0.8.0 `--check` on `src/Proven/SafeOTP/Proofs.idr` once CI is unjammed - [ ] Verify no downstream module shadows these names (grep was clean at edit time) - [ ] Owner review of OWED reasons against SafeChecksum + SafeHtml + SafeAPIKey precedents Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 891ed45 commit dcf5ed5

1 file changed

Lines changed: 76 additions & 20 deletions

File tree

‎src/Proven/SafeOTP/Proofs.idr‎

Lines changed: 76 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -31,16 +31,41 @@ digits8Divisor = Refl
3131
-- Constant-Time Comparison Properties
3232
--------------------------------------------------------------------------------
3333

34-
||| Constant-time comparison is reflexive.
35-
||| Postulated: requires showing (c == c) = True for all Char
36-
||| and that the accumulated && folds to True, which involves
37-
||| Char primitives not reducible in Idris 2.
34+
||| OWED: `constantTimeCompare` is reflexive — `constantTimeCompare s s
35+
||| = True` for every `String s`. Witnessed operationally by the
36+
||| implementation: the `length as /= length bs` guard collapses to
37+
||| `False`, then the inner `go` helper folds `(acc && x == y)` over
38+
||| the unpacked list with `x == y` true at every position.
39+
|||
40+
||| Held back by Idris2 0.8.0 not reducing two stacked String/Char
41+
||| primitives at the type level: (1) `unpack` is FFI-bound, so
42+
||| `unpack s = unpack s` does not type-level normalise for abstract
43+
||| `s` (same blocker family as SafeChecksum's String-FFI OWED set);
44+
||| (2) `(==) : Char -> Char -> Bool` is a primitive whose `c == c =
45+
||| True` lemma is not exposed as a definitional Refl in Idris2 0.8.0
46+
||| (same blocker family as `Boj.SafetyLemmas.charEqSym` in boj-server,
47+
||| where it is discharged as a class-(J) axiom `%unsafe believe_me`).
48+
||| Discharge once a `Data.String` / `Data.Char` reflective tactic is
49+
||| available, or by introducing a class-(J) `charEqRefl` axiom and a
50+
||| per-list induction lemma over `go`.
3851
export
39-
constantTimeCompareRefl : (s : String) -> constantTimeCompare s s = True
40-
41-
||| Constant-time comparison is symmetric.
52+
0 constantTimeCompareRefl : (s : String) -> constantTimeCompare s s = True
53+
54+
||| OWED: `constantTimeCompare` is symmetric —
55+
||| `constantTimeCompare a b = constantTimeCompare b a` for all
56+
||| Strings. Witnessed operationally by the implementation: both the
57+
||| `length as /= length bs` guard and the per-position `x == y`
58+
||| comparison in `go` are themselves symmetric (length equality is
59+
||| symmetric; `Char` equality is symmetric).
60+
|||
61+
||| Held back by Idris2 0.8.0 not reducing `unpack` at the type level
62+
||| (FFI-bound primitive), and by `prim__eq_Char` not exposing a
63+
||| `charEqSym : (x, y : Char) -> (x == y) = (y == x)` Refl lemma.
64+
||| Same blocker family as `constantTimeCompareRefl`. Discharge once a
65+
||| `Data.String` reflective tactic is available, or via a class-(J)
66+
||| `charEqSym` axiom paired with a per-list induction over `go`.
4267
export
43-
constantTimeCompareSym : (a, b : String) -> constantTimeCompare a b = constantTimeCompare b a
68+
0 constantTimeCompareSym : (a, b : String) -> constantTimeCompare a b = constantTimeCompare b a
4469

4570
||| Empty strings compare equal.
4671
public export
@@ -51,22 +76,53 @@ emptyStringsEqual = Refl
5176
-- TOTP Validation Properties
5277
--------------------------------------------------------------------------------
5378

54-
||| An OTP code validates against a list containing itself.
55-
||| Follows from constantTimeCompareRefl.
79+
||| OWED: an OTP code validates against a singleton list containing
80+
||| itself — `validateTOTPCode code [code] = True`. By definitional
81+
||| unfolding, `validateTOTPCode code [code]` reduces to
82+
||| `any (\e => constantTimeCompare code.code e.code) [code]` and
83+
||| then to `constantTimeCompare code.code code.code || False`, which
84+
||| is `True` iff `constantTimeCompare` is reflexive.
85+
|||
86+
||| Held back by the same blockers as `constantTimeCompareRefl`
87+
||| (String/Char primitive opacity in Idris2 0.8.0): this claim is a
88+
||| direct downstream corollary and cannot be discharged until
89+
||| `constantTimeCompareRefl` is. Discharge follows immediately once
90+
||| `constantTimeCompareRefl` is in scope, by `rewrite` on the head of
91+
||| the `||`.
5692
export
57-
codeValidatesAgainstSelf : (code : OTPCode) -> validateTOTPCode code [code] = True
93+
0 codeValidatesAgainstSelf : (code : OTPCode) -> validateTOTPCode code [code] = True
5894

59-
||| An OTP code validates against a list if it appears anywhere in the list.
60-
||| TOTP validation checks all valid time windows (any returns True
61-
||| if at least one match exists).
95+
||| OWED: TOTP validation accepts a code if it matches anywhere in
96+
||| the candidate list. By definition `validateTOTPCode code codes =
97+
||| any (\e => constantTimeCompare code.code e.code) codes`, so this
98+
||| is literally the hypothesis — a statement of the function's
99+
||| extensional equality with its body.
100+
|||
101+
||| Held back by Idris2 0.8.0 not eta-reducing the lambda inside `any`
102+
||| at the type level for an abstract `codes : List OTPCode` —
103+
||| `any p xs = True` does not normalise to its body without case
104+
||| analysis on `xs`. Compounded by the same String-FFI opacity in
105+
||| `constantTimeCompare` underneath. Discharge by induction on
106+
||| `codes` (a one-line `Refl` for the `[]` impossibility plus a
107+
||| `rewrite` step for `_ :: _`), once a `Data.List.any` extensionality
108+
||| lemma is in `contrib` — or inline the induction here.
62109
export
63-
codeInListValidates : (code : OTPCode) -> (codes : List OTPCode) ->
64-
any (\e => constantTimeCompare code.code e.code) codes = True ->
65-
validateTOTPCode code codes = True
66-
67-
||| HOTP validation of identical codes succeeds.
110+
0 codeInListValidates : (code : OTPCode) -> (codes : List OTPCode) ->
111+
any (\e => constantTimeCompare code.code e.code) codes = True ->
112+
validateTOTPCode code codes = True
113+
114+
||| OWED: HOTP validation of identical codes succeeds —
115+
||| `validateHOTPCode code code = True`. By definition
116+
||| `validateHOTPCode submitted expected = constantTimeCompare
117+
||| submitted.code expected.code`, so identical inputs reduce to
118+
||| `constantTimeCompare code.code code.code`, which is `True` by
119+
||| `constantTimeCompareRefl`.
120+
|||
121+
||| Held back by the same blockers as `constantTimeCompareRefl`
122+
||| (String/Char primitive opacity in Idris2 0.8.0). Discharge
123+
||| follows immediately once `constantTimeCompareRefl` is in scope.
68124
export
69-
identicalHOTPValid : (code : OTPCode) -> validateHOTPCode code code = True
125+
0 identicalHOTPValid : (code : OTPCode) -> validateHOTPCode code code = True
70126

71127
||| Validation against empty list always fails.
72128
public export

0 commit comments

Comments
 (0)