Skip to content

Commit 542d462

Browse files
hyperpolymathhyperpolymath
authored
proof(SafeCSRF): annotate 6 bodyless decls as OWED (Refs standards#158) (#53)
## Summary Annotates the 6 bodyless declarations in `src/Proven/SafeCSRF/Proofs.idr` as **OWED-with-justification**, per the convention set 2026-05-20 by sibling PRs #37 (SafeAPIKey), #38 (SafeCORS), #39 (SafeCSV), #40 (SafeSemVer), #41 (SafeHtml), and the SafeChecksum/SafeArgs in-repo reference files. Refs hyperpolymath/standards#158. ## Form (matches the convention) - Triple-pipe `||| OWED:` doc-block stating **claim + Idris2 0.8.0 blocker + concrete discharge path** for each declaration - Leading `0 ` (erased-multiplicity, runtime-stripped) - `public export` visibility upgraded from `export` to match the SafeChecksum/SafeCSV reference dominant form - Original type signature unchanged otherwise - **No** `postulate` keyword, **no** `believe_me`, **no** `idris_crash` ## Decls + claims + reasons 1. **`constantTimeEqRefl`** — `constantTimeEqual s s = True` Blocker: `String.unpack` FFI opacity + missing `prim__eq_Char x x = True` reflective lemma + `andTrueNeutral` not exposed as Refl identity in Idris2 0.8.0 stdlib. Same family as SafeChecksum Luhn/ISBN + gossamer `stringNotEqCommut` class-J axiom. Discharge: `Data.String` reflective tactic + `Data.Bool` `andTrueNeutral` + `prim__eq_Char` reflective lemma; alternatively refactor `constantTimeEqual` to `Vect n Char`. 2. **`constantTimeEqSym`** — `constantTimeEqual a b = constantTimeEqual b a` Blocker: `prim__eq_Char` commutativity not exposed as Refl-reducible — symmetric to `Boj.SafetyLemmas.charEqSym` class-J axiom already shipped in boj-server; upstream `/=` length guard also FFI-opaque. Discharge: `Data.Char` reflective `eqCharSym` lemma. 3. **`differentLengthUnequal`** — `Not (length a = length b) -> constantTimeEqual a b = False` Blocker: Bool-Prop reflection gap — hypothesis is propositional `Not (length a = length b)` over `String.length`, but the comparison branches on Boolean `(length as /= length bs)` over `List Char` (after `unpack`). Same family as `SafeArgs.boolParsingComplete`. Discharge: `Data.String` `lengthUnpackEq` + `Data.Nat` `decEqToNeq` Bool reflection, or refactor to `LengthEq`-tagged input. 4. **`tokenValidatesSelf`** — `validateToken tok (tokenString tok) = True` Blocker: same as `constantTimeEqRefl` (chain `constantTimeEqRefl → tokenValidatesSelf`). Discharge: one-line `constantTimeEqRefl (tokenString tok)` once parent discharges. 5. **`identicalDoubleSubmitValid`** — `validateDoubleSubmit (MkDoubleSubmit val val) = True` Blocker: same `constantTimeEqRefl` chain. Discharge: one-line `constantTimeEqRefl val` once parent discharges. 6. **`fullValidationRequiresToken`** — `validateToken tok submitted = False -> fullValidation tok submitted origins origin = False` Blocker: `validateToken`'s definitional opacity through the `tokenString` record-field accessor. The sibling `wrongSessionFails` (already proved by `rewrite prf in Refl` in this file) closes the symmetric pattern only because its hypothesis is stated directly over `constantTimeEqual`; here `prf` is wrapped through `validateToken` and the wrapper does not reduce. Discharge: refactor `validateToken` to take `String` directly (skipping the `CSRFToken`-record indirection), at which point `rewrite prf in Refl` closes it — cf. `wrongSessionFails`. ## Scope - Touches only `src/Proven/SafeCSRF/Proofs.idr` - The two `Refl`-discharged proofs (`mkTokenRejectsEmpty`, `hexTokenEmpty`) and the one `rewrite`-discharged proof (`wrongSessionFails`) are untouched - No bindings, no FFI, no source `.idr` outside `Proofs.idr` ## Why draft Mirrors the sibling-PR cadence: draft → CI gate → human review + non-`--admin` merge. Local `idris2 --build proven.ipkg` is not green on my machine because the installed `base` package has no compatible TTC binaries (`Found version 0.8.0 of package base installed with no compatible binaries for the current Idris2 compiler`) — same toolchain state as on the sibling SafeCSV/SafeSemVer/SafeHtml PRs. CI is the oracle. Refs hyperpolymath/standards#158
1 parent e035ff1 commit 542d462

1 file changed

Lines changed: 155 additions & 34 deletions

File tree

‎src/Proven/SafeCSRF/Proofs.idr‎

Lines changed: 155 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,17 @@
44
|||
55
||| Verifies properties of constant-time comparison, token validation,
66
||| and double-submit cookie pattern correctness.
7+
|||
8+
||| Six declarations in this file are stated as OWED-with-justification
9+
||| per the convention set 2026-05-20 by SafeChecksum/SafeArgs/SafeCSV:
10+
||| triple-pipe `||| OWED:` doc-block + `0 ` erased-multiplicity + bare
11+
||| signature, no `postulate` keyword, no `believe_me`. Each entry
12+
||| names the specific Idris2 0.8.0 blocker (chiefly `unpack`/Char-FFI
13+
||| primitive equality opacity and Bool-Prop reflection gaps over
14+
||| `String.length` / `constantTimeEqual`) and a concrete discharge
15+
||| path. The blocker family is the same as the SafeChecksum Luhn /
16+
||| ISBN String-FFI OWED set and the gossamer `stringNotEqCommut`
17+
||| class-J axiom.
718
module Proven.SafeCSRF.Proofs
819

920
import Proven.SafeCSRF
@@ -16,49 +27,159 @@ import Data.List
1627
-- Constant-Time Comparison Properties
1728
--------------------------------------------------------------------------------
1829

19-
||| Constant-time comparison is reflexive: any string equals itself.
20-
||| Postulated: constantTimeEqual uses a where-local accumulator fold
21-
||| over unpack results; proving reflexivity requires showing
22-
||| (c == c) = True for all Char and that the accumulated && folds
23-
||| to True, which involves Char comparison not reducible in Idris 2.
24-
export
25-
constantTimeEqRefl : (s : String) -> constantTimeEqual s s = True
30+
||| OWED: `constantTimeEqual s s = True` for every `s : String`.
31+
||| Operationally true because `constantTimeEqual` first compares
32+
||| `length (unpack s) /= length (unpack s)` (always `False`), then
33+
||| folds `acc && (c == c)` over the zipped character lists, and
34+
||| `c == c = True` for every `Char c`.
35+
|||
36+
||| Held back by Idris2 0.8.0 not type-level reducing `String.unpack`
37+
||| (an opaque C FFI primitive) and not exposing a reflective
38+
||| `prim__eq_Char x x = True` lemma. The `where`-local `go` fold
39+
||| further compounds the issue: induction on the abstract
40+
||| `unpack s` is unavailable without `unpack` reducing, and even if
41+
||| we had a concrete cons-list the inductive step requires
42+
||| `acc && True = acc` (`andTrueNeutral` — not exposed as a Refl
43+
||| identity in Idris2 0.8.0's stdlib). Same blocker family as
44+
||| `SafeChecksum.luhnValidatesKnownGood` (String FFI) and the
45+
||| gossamer `stringNotEqCommut` class-J axiom.
46+
|||
47+
||| Discharge once: (a) a `Data.String` reflective tactic exposes
48+
||| `unpack`/`pack` reductively, (b) `Data.Bool` ships
49+
||| `andTrueNeutral` as a Refl-reducible identity (or it is added
50+
||| locally as a helper lemma over `List Char`), and (c) a
51+
||| `prim__eq_Char` reflective lemma is available. Alternative:
52+
||| refactor `constantTimeEqual` to operate on a `Vect n Char`
53+
||| directly so the length-equality and per-character comparison are
54+
||| both type-level structural.
55+
public export
56+
0 constantTimeEqRefl : (s : String) -> constantTimeEqual s s = True
2657

27-
||| Constant-time comparison is symmetric.
28-
||| Postulated: requires showing Char (==) is commutative, which
29-
||| is a primitive operation.
30-
export
31-
constantTimeEqSym : (a, b : String) -> constantTimeEqual a b = constantTimeEqual b a
58+
||| OWED: `constantTimeEqual a b = constantTimeEqual b a` for every
59+
||| `a, b : String`. Operationally true because the length-inequality
60+
||| guard `length as /= length bs` is symmetric in its two arguments
61+
||| and the per-character fold reduces to `acc && (x == y)` which
62+
||| commutes via `Char` primitive equality commutativity.
63+
|||
64+
||| Held back by Idris2 0.8.0 not exposing
65+
||| `prim__eq_Char x y = prim__eq_Char y x` as a Refl-reducible lemma
66+
||| — `Char` equality bottoms out in a runtime FFI primitive, exactly
67+
||| the same blocker as the gossamer `stringNotEqCommut` class-J
68+
||| axiom (which had to introduce `%unsafe`+`believe_me ()` over
69+
||| `prim__eq_String` to land). The `/=` length check is also routed
70+
||| through opaque `String.length`/`unpack` so the upstream guard
71+
||| does not reduce either.
72+
|||
73+
||| Discharge once a `Data.Char` reflective `eqCharSym` lemma is
74+
||| available — symmetric to the `Boj.SafetyLemmas.charEqSym` class-J
75+
||| axiom already shipped in boj-server. Until then, recording this
76+
||| as a stated OWED (parallel to the `SafeChecksum` String-FFI set)
77+
||| keeps the obligation discoverable rather than silent.
78+
public export
79+
0 constantTimeEqSym : (a, b : String) -> constantTimeEqual a b = constantTimeEqual b a
3280

33-
||| Different-length strings always compare unequal.
34-
||| This follows from the length check at the top of constantTimeEqual.
35-
export
36-
differentLengthUnequal : (a, b : String) ->
37-
Not (length a = length b) ->
38-
constantTimeEqual a b = False
81+
||| OWED: if `Not (length a = length b)` then
82+
||| `constantTimeEqual a b = False`. Operationally true because the
83+
||| `constantTimeEqual` definition first computes
84+
||| `length as /= length bs` (with `as = unpack a`, `bs = unpack b`)
85+
||| and returns `False` immediately when this `Bool` is `True`.
86+
|||
87+
||| Held back by a Bool-Prop reflection gap: the hypothesis is the
88+
||| *propositional* inequality `Not (length a = length b)` over
89+
||| `String.length`, but `constantTimeEqual` branches on the
90+
||| *Boolean* `length as /= length bs` over `List Char` (i.e. after
91+
||| `unpack`). To bridge the two we need both (a) a lemma
92+
||| `length s = length (unpack s)` (not exposed as Refl in Idris2
93+
||| 0.8.0 because `unpack` is an opaque FFI primitive) and (b) a
94+
||| `Bool ↔ Prop` reflection from `Not (m = n)` to `(m /= n) = True`
95+
||| on `Nat` (not in the stdlib at this version). Same family as
96+
||| `SafeArgs.boolParsingComplete`.
97+
|||
98+
||| Discharge once `Data.String` exposes `lengthUnpackEq` and
99+
||| `Data.Nat` (or `Decidable.Equality`) ships the
100+
||| `decEqToNeq` Bool reflection lemma, or once `constantTimeEqual`
101+
||| is refactored to take a `LengthEq`-tagged input (push the
102+
||| length equality into the type and remove the runtime guard).
103+
public export
104+
0 differentLengthUnequal : (a, b : String) ->
105+
Not (length a = length b) ->
106+
constantTimeEqual a b = False
39107

40108
--------------------------------------------------------------------------------
41109
-- Token Validation Properties
42110
--------------------------------------------------------------------------------
43111

44-
||| A token validates against its own string representation.
45-
||| Follows from constantTimeEqRefl.
46-
export
47-
tokenValidatesSelf : (tok : CSRFToken) -> validateToken tok (tokenString tok) = True
112+
||| OWED: `validateToken tok (tokenString tok) = True` for every
113+
||| `tok : CSRFToken`. By unfolding,
114+
||| `validateToken tok (tokenString tok)
115+
||| = constantTimeEqual (tokenString tok) (tokenString tok)`, which
116+
||| is the `constantTimeEqRefl` instance at `s = tokenString tok`.
117+
|||
118+
||| Held back by the same blocker as `constantTimeEqRefl` above —
119+
||| once that OWED lemma is discharged this proof becomes a one-line
120+
||| `constantTimeEqRefl (tokenString tok)`. Recorded as a separate
121+
||| OWED entry rather than collapsing into `constantTimeEqRefl` so
122+
||| that callers reading `validateToken`-shaped obligations can find
123+
||| the named identity directly. Same blocker family as
124+
||| `SafeChecksum.verifyCRC32Definition` would be without
125+
||| `verifyCRC32` reducing definitionally.
126+
|||
127+
||| Discharge once `constantTimeEqRefl` is discharged (the chain is
128+
||| `constantTimeEqRefl → tokenValidatesSelf`); the proof body is
129+
||| then `constantTimeEqRefl (tokenString tok)`.
130+
public export
131+
0 tokenValidatesSelf : (tok : CSRFToken) -> validateToken tok (tokenString tok) = True
48132

49-
||| Double-submit validation succeeds when both values are identical.
50-
||| Follows from constantTimeEqRefl.
51-
export
52-
identicalDoubleSubmitValid : (val : String) ->
53-
validateDoubleSubmit (MkDoubleSubmit val val) = True
133+
||| OWED: `validateDoubleSubmit (MkDoubleSubmit val val) = True` for
134+
||| every `val : String`. By unfolding,
135+
||| `validateDoubleSubmit (MkDoubleSubmit val val)
136+
||| = constantTimeEqual val val`, which is the `constantTimeEqRefl`
137+
||| instance at `s = val`.
138+
|||
139+
||| Held back by the same blocker as `constantTimeEqRefl` above —
140+
||| once that OWED lemma is discharged this proof becomes a one-line
141+
||| `constantTimeEqRefl val`. Recorded as a separate OWED entry so
142+
||| the double-submit-cookie pattern's reflexivity claim is
143+
||| discoverable as a named obligation in the safety surface.
144+
|||
145+
||| Discharge once `constantTimeEqRefl` is discharged; the proof
146+
||| body is then `constantTimeEqRefl val`.
147+
public export
148+
0 identicalDoubleSubmitValid : (val : String) ->
149+
validateDoubleSubmit (MkDoubleSubmit val val) = True
54150

55-
||| fullValidation fails if token validation fails.
56-
||| The && short-circuits: if the first conjunct is False, result is False.
57-
export
58-
fullValidationRequiresToken : (tok : CSRFToken) -> (submitted : String) ->
59-
(origins : List String) -> (origin : String) ->
60-
validateToken tok submitted = False ->
61-
fullValidation tok submitted origins origin = False
151+
||| OWED: if `validateToken tok submitted = False` then
152+
||| `fullValidation tok submitted origins origin = False`.
153+
||| Operationally true because
154+
||| `fullValidation tok submitted origins origin
155+
||| = validateToken tok submitted && validateOrigin origins origin`,
156+
||| and `False && _ = False` by the `Bool` `&&` definition.
157+
|||
158+
||| Although the `&&` `False`-short-circuit is in principle a Refl
159+
||| identity (`False && b = False`), discharging this lemma still
160+
||| requires `validateToken` to be reduced to its `constantTimeEqual`
161+
||| form so that `rewrite prf` can fire — which in turn requires
162+
||| `String.unpack` / `List.length` / `Char` primitive equality to
163+
||| reduce at the type level, all of which are FFI-opaque in
164+
||| Idris2 0.8.0. The sibling `wrongSessionFails` (already proved in
165+
||| this file by `rewrite prf in Refl`) discharges the symmetric
166+
||| pattern only because its `prf` is stated directly over
167+
||| `constantTimeEqual` rather than over the wrapped `validateToken`
168+
||| — for `fullValidationRequiresToken` the same trick is blocked by
169+
||| `validateToken`'s definitional opacity at the level of `tok`'s
170+
||| record-field accessor `tokenString`.
171+
|||
172+
||| Discharge once either (a) `validateToken` is refactored to
173+
||| operate directly on `String` (rather than via the `tokenString`
174+
||| accessor through the `CSRFToken` record), at which point
175+
||| `rewrite prf in Refl` would close it (cf. `wrongSessionFails`),
176+
||| or (b) a Bool-Prop reflective tactic exposes `validateToken`'s
177+
||| reduction. Recorded as OWED until one of those lands.
178+
public export
179+
0 fullValidationRequiresToken : (tok : CSRFToken) -> (submitted : String) ->
180+
(origins : List String) -> (origin : String) ->
181+
validateToken tok submitted = False ->
182+
fullValidation tok submitted origins origin = False
62183

63184
--------------------------------------------------------------------------------
64185
-- Token Construction Properties

0 commit comments

Comments
 (0)