Skip to content

Commit df6b0a1

Browse files
hyperpolymathhyperpolymath
authored
proof(SafeEnv): annotate 7 bodyless decls as OWED (Refs standards#158) (#51)
## Summary Annotates the seven bodyless declarations in `src/Proven/SafeEnv/Proofs.idr` as **OWED-with-justification**, per the convention established 2026-05-20 by SafeChecksum, SafeBuffer, SafeCryptoAccel, SafeHKDF, SafeBloom, SafeFPGA and the matching sibling PRs #37 (SafeAPIKey), #41 (SafeHtml), #46 (SafeMath). Refs hyperpolymath/standards#158. ## What each decl claims & why it's OWED ### Name validation (2) 1. **`digitStartInvalid`** — claim: prepending any `isDigit c = True` character to any string yields a name `isValidEnvName` rejects. Blocker: Idris2 0.8.0 does not reduce the `unpack . pack` round-trip on `(c :: unpack s)` by Refl — `pack`/`unpack` are FFI string primitives. Discharge: `Data.String` reflective tactic, or a `packUnpackInverse` equation lemma. 2. **`wellKnownValid`** — claim: every name in `Types.wellKnownVars` (PATH, HOME, USER, SHELL, ...) passes `isValidEnvName`. Blocker: `elem name wellKnownVars = True` cannot be case-split over the literal list because each comparison bottoms out in `prim__eq_String`, a Class-J FFI primitive (same primitive whose commutativity is axiomatised in `gossamer` as `stringNotEqCommut`). The point-checks `pathValid`/`homeValid`/`userValid` already discharge specific witnesses by Refl; this is the universally-quantified form. Discharge: Bool-Prop reflection lemma for `prim__eq_String`, or refactor `wellKnownVars` to a `DecEq`-checked names list. ### Value bounds (1) 3. **`emptyBounded`** — claim: the empty string is `BoundedValue maxLen ""` for every `maxLen`. The auto-prf witness `length (unpack "") <= maxLen = True` should reduce to `0 <= maxLen = True`. Blocker: Idris2 0.8.0 does not reduce `unpack ""` to `[]` by Refl — `unpack` is an FFI string primitive whose empty-string case is not exposed as a definitional equation. Discharge: an `unpackEmpty : unpack "" = []` lemma in `Data.String`, or refactor `BoundedValue` to use primitive `String` length. ### Sensitivity classification (2) 4. **`publicClassification`** — claim: when `isSensitiveName name = False`, `classifyByName name = Public`. Blocker: Idris2 0.8.0 will not lift the False-hypothesis through `classifyByName`'s `if`-on-`isSensitiveName` scrutinee, whose `isInfixOf`-fold over the PASSWORD/SECRET/TOKEN/KEY pattern list bottoms out in `prim__eq_String`. Discharge: `boolElim`-style rewrite tactic, or refactor `classifyByName` to `case isSensitiveName name of ...`. 5. **`sensitiveClassification`** — mirror of 4 with `= True ... = Sensitive`. Same blocker, same discharge path. ### Type-conversion soundness (2) 6. **`validBoolParses`** — claim: any string drawn from `["true","false","yes","no","1","0","on","off"]` parses to `Just _` via `parseBool`. Blocker: `parseBool` lower-cases its argument via `toLower` and then case-splits; Idris2 0.8.0 does not reduce `toLower s` for opaque `s : String`, even though every literal in the precondition list is already lower-case. Discharge: Bool-Prop reflection lemma for `toLower` on lower-case-only strings, or pre-lower-case the comparison list. 7. **`validIntParses`** — claim: any string whose every character is an ASCII digit parses to `Just _` via `parseInteger {a=Integer}`. Blocker: Prelude `parseInteger` is an FFI string-to-integer conversion whose success criterion (the all-digits invariant) is not stated as a definitional equation. Compounded by `unpack` opacity. Discharge: a `parseIntegerOfDigits` lemma exposed by Prelude, or refactor to a hand-rolled digit-folder. ## Form (matches SafeChecksum convention) - Triple-pipe docblock stating claim + blocker + discharge condition - Leading `0 ` (erased-multiplicity, runtime-stripped) - Original bare type signature, otherwise unchanged - No `postulate` keyword (estate-wide choice) - No `believe_me`, no `idris_crash` See `src/Proven/SafeChecksum/Proofs.idr` L24-L100 for the reference pattern. ## Scope - Touches only `src/Proven/SafeEnv/Proofs.idr` (96 insertions, 36 deletions) - Seven declarations annotated; the other 24 proofs in the file (already discharged by `Refl` or `= ()`) are untouched - No semantic change: each annotated decl was already bodyless on `main`, this PR only adds erased multiplicity and replaces the existing two-line "Depends on ..." docblocks with the full OWED-with-justification form ## Why draft Per the sibling-PR convention: CI is jammed estate-wide (concurrency-pool exhaustion, see standards#92 / Refs MEMORY). Owner to promote from DRAFT once the pool clears and `idris2 --build proven.ipkg` runs green. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
1 parent 5bd2b36 commit df6b0a1

1 file changed

Lines changed: 96 additions & 36 deletions

File tree

‎src/Proven/SafeEnv/Proofs.idr‎

Lines changed: 96 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -34,19 +34,35 @@ export
3434
emptyNameInvalid : isValidEnvName "" = False
3535
emptyNameInvalid = Refl
3636

37-
||| Depends on isValidEnvName + pack/unpack round-trip behaviour for digit-prefixed strings.
38-
||| These are FFI string operations whose reduction is opaque to the type checker.
37+
||| OWED: prepending a digit character to any string yields a name that
38+
||| `isValidEnvName` rejects. The implementation checks
39+
||| `not (isDigit (head chars))` where `chars = unpack s`. Held back by
40+
||| Idris2 0.8.0 not reducing the `unpack . pack` round-trip on
41+
||| `(c :: unpack s)` to `(c :: unpack s)` by Refl alone — `pack`/`unpack`
42+
||| are FFI string primitives, opaque to the type-level reducer. Same
43+
||| blocker family as the SafeChecksum Luhn/ISBN OWED items. Discharge
44+
||| once a `Data.String` reflective tactic (or a `packUnpackInverse`
45+
||| equation lemma) is available.
3946
export
40-
digitStartInvalid : (s : String) ->
41-
(c : Char) -> isDigit c = True ->
42-
isValidEnvName (pack (c :: unpack s)) = False
43-
44-
||| Depends on elem over the well-known variable list and isValidEnvName
45-
||| agreeing that each listed name passes validation. Opaque due to string ops.
47+
0 digitStartInvalid : (s : String) ->
48+
(c : Char) -> isDigit c = True ->
49+
isValidEnvName (pack (c :: unpack s)) = False
50+
51+
||| OWED: every name in the curated `Types.wellKnownVars` list
52+
||| (PATH, HOME, USER, SHELL, …) passes `isValidEnvName`. Held back by
53+
||| Idris2 0.8.0 not reducing `elem name wellKnownVars = True` to a
54+
||| concrete case-split over the literal-string entries of the list —
55+
||| each comparison thunks through `prim__eq_String`, a Class-J FFI
56+
||| primitive. The point-checks `pathValid`/`homeValid`/`userValid` above
57+
||| already discharge specific members by Refl; the universally-quantified
58+
||| form is what's owed. Discharge once a Bool↔Prop reflection lemma for
59+
||| `prim__eq_String` is available (same Class-J primitive whose
60+
||| commutativity is axiomatised in `gossamer` as `stringNotEqCommut`),
61+
||| or refactor `wellKnownVars` to a sum-of-`DecEq`-checked names list.
4662
export
47-
wellKnownValid : (name : String) ->
48-
Prelude.elem name Types.wellKnownVars = True ->
49-
isValidEnvName name = True
63+
0 wellKnownValid : (name : String) ->
64+
Prelude.elem name Types.wellKnownVars = True ->
65+
isValidEnvName name = True
5066

5167
||| Theorem: PATH is valid
5268
export
@@ -74,10 +90,18 @@ data BoundedValue : Nat -> String -> Type where
7490
{auto prf : length (unpack value) <= maxLen = True} ->
7591
BoundedValue maxLen value
7692

77-
||| Empty string has zero length, so length (unpack "") <= maxLen holds for all maxLen.
78-
||| Depends on unpack "" reducing to [] and length [] reducing to 0 (FFI string op).
93+
||| OWED: the empty string is bounded by every `maxLen` — the auto-prf
94+
||| witness `length (unpack "") <= maxLen = True` should reduce to
95+
||| `0 <= maxLen = True`, which is Refl for all `maxLen`. Held back by
96+
||| Idris2 0.8.0 not reducing `unpack ""` to `[]` by Refl alone — `unpack`
97+
||| is an FFI string primitive whose empty-string case is not exposed as
98+
||| a definitional equation. Same blocker family as the SafeChecksum
99+
||| `extractDigits`/`unpack` OWED items. Discharge once a
100+
||| `unpackEmpty : unpack "" = []` equation lemma is available in
101+
||| `Data.String`, or refactor `BoundedValue` to take `length value`
102+
||| (a primitive String length) instead of `length (unpack value)`.
79103
export
80-
emptyBounded : (maxLen : Nat) -> BoundedValue maxLen ""
104+
0 emptyBounded : (maxLen : Nat) -> BoundedValue maxLen ""
81105

82106
||| Theorem: Bounded value check prevents overflow
83107
export
@@ -123,19 +147,36 @@ export
123147
keySensitive : isSensitiveName "AWS_ACCESS_KEY" = True
124148
keySensitive = Refl
125149

126-
||| When isSensitiveName returns False, classifyByName should return Public.
127-
||| Depends on classifyByName branching on isSensitiveName (opaque string matching).
150+
||| OWED: when `isSensitiveName name = False`, `classifyByName name`
151+
||| returns `Public`. `classifyByName` is defined as
152+
||| `if isSensitiveName name then Sensitive else Public` — so this
153+
||| should follow by rewriting the `if`-head with the False hypothesis.
154+
||| Held back by Idris2 0.8.0 not lifting a Bool-equality hypothesis
155+
||| through an `if` whose scrutinee is an `isInfixOf`-fold over the
156+
||| sensitive-pattern list (PASSWORD/SECRET/TOKEN/KEY) — the fold itself
157+
||| reduces through `prim__eq_String`, a Class-J FFI primitive.
158+
||| Discharge once a `boolElim`-style rewrite tactic is available for
159+
||| `if`-on-`Bool`-hypotheses, or refactor `classifyByName` to
160+
||| `case isSensitiveName name of False => Public; True => Sensitive`.
128161
export
129-
publicClassification : (name : String) ->
130-
isSensitiveName name = False ->
131-
classifyByName name = Public
132-
133-
||| When isSensitiveName returns True, classifyByName should return Sensitive.
134-
||| Depends on classifyByName branching on isSensitiveName (opaque string matching).
162+
0 publicClassification : (name : String) ->
163+
isSensitiveName name = False ->
164+
classifyByName name = Public
165+
166+
||| OWED: when `isSensitiveName name = True`, `classifyByName name`
167+
||| returns `Sensitive`. Mirror of `publicClassification` above. Same
168+
||| blocker — Idris2 0.8.0 will not lift the True-hypothesis through
169+
||| `classifyByName`'s `if`-on-`isSensitiveName` scrutinee, whose fold
170+
||| over the sensitive-pattern list bottoms out in `prim__eq_String`.
171+
||| Same discharge path: `boolElim`-style tactic, or refactor
172+
||| `classifyByName` to `case isSensitiveName name of …`. The point-check
173+
||| OWEDs `passwordSensitive`/`tokenSensitive`/`secretSensitive`/
174+
||| `keySensitive` already cover specific witnesses; this is the
175+
||| universally-quantified form.
135176
export
136-
sensitiveClassification : (name : String) ->
137-
isSensitiveName name = True ->
138-
classifyByName name = Sensitive
177+
0 sensitiveClassification : (name : String) ->
178+
isSensitiveName name = True ->
179+
classifyByName name = Sensitive
139180

140181
--------------------------------------------------------------------------------
141182
-- Access Control Proofs
@@ -174,19 +215,38 @@ blockedPatternsPreventsAccess opts name blocked = ()
174215
-- Type Conversion Proofs
175216
--------------------------------------------------------------------------------
176217

177-
||| Valid boolean string literals ("true","false","yes","no","1","0","on","off")
178-
||| are recognised by parseBool. Depends on toLower (FFI string primitive) agreeing
179-
||| with elem membership over the recognised-boolean list.
218+
||| OWED: any string drawn from the recognised-boolean list
219+
||| (`true`/`false`/`yes`/`no`/`1`/`0`/`on`/`off`) parses to `Just _`
220+
||| via `parseBool`. `parseBool` first lower-cases its argument via
221+
||| `toLower` and then case-splits on the result. Held back by
222+
||| Idris2 0.8.0 not reducing `toLower s` for an opaque `s : String` —
223+
||| `toLower` is an FFI string primitive (Class-J), even though every
224+
||| literal in the precondition list is already lower-case. Same blocker
225+
||| family as the `wellKnownValid` `prim__eq_String` axiomatisation
226+
||| precedent set in `gossamer`. Discharge once a Bool↔Prop reflection
227+
||| lemma for `toLower` on lower-case-only strings is available, or
228+
||| refactor `parseBool` to compare against a pre-lower-cased list
229+
||| without invoking `toLower`.
180230
export
181-
validBoolParses : (s : String) ->
182-
s `elem` ["true", "false", "yes", "no", "1", "0", "on", "off"] = True ->
183-
isJust (parseBool s) = True
184-
185-
||| Depends on parseInteger implementation (FFI string-to-integer conversion).
231+
0 validBoolParses : (s : String) ->
232+
s `elem` ["true", "false", "yes", "no", "1", "0", "on", "off"] = True ->
233+
isJust (parseBool s) = True
234+
235+
||| OWED: any string whose every character is an ASCII digit parses to
236+
||| `Just _` via `parseInteger {a=Integer}`. Held back by Idris2 0.8.0
237+
||| not exposing the internals of the Prelude `parseInteger` — it is an
238+
||| FFI string-to-integer conversion whose success criterion (the
239+
||| all-digits invariant) is not stated as a definitional equation.
240+
||| Compounded by `unpack` being an FFI primitive (same blocker as
241+
||| `digitStartInvalid` / `emptyBounded` above). Discharge once
242+
||| `parseInteger`'s success condition is exposed as a lemma
243+
||| (`parseIntegerOfDigits : all isDigit (unpack s) = True -> isJust (parseInteger s) = True`),
244+
||| or refactor `validIntParses` to call a hand-rolled digit-folder
245+
||| whose proof is straightforward induction over `unpack s`.
186246
export
187-
validIntParses : (s : String) ->
188-
all Prelude.Types.isDigit (unpack s) = True ->
189-
isJust (parseInteger {a=Integer} s) = True
247+
0 validIntParses : (s : String) ->
248+
all Prelude.Types.isDigit (unpack s) = True ->
249+
isJust (parseInteger {a=Integer} s) = True
190250

191251
||| Theorem: Valid ports are in range
192252
export

0 commit comments

Comments
 (0)