Skip to content

Commit d262256

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
proof(abi): reduce believe_me from 31 to 4 across all ABI safety modules
Add three axiomatic primitives to SafetyLemmas: - charEqSound (prim__eqChar soundness — c1==c2=True → c1=c2) - unpackLength (prim__strToCharList preserves length) - fromLteTrue (constructive Bool→LTE converter, zero believe_me) Replace all other instances with constructive proofs: - Safety.idr: 6 believe_me → 0 via charEqSound + Refl on literal chars (shellSafeNotTarget/sqlSafeNotTarget generics + allImplies chain) - SafeWebSocket.idr: 17 believe_me → 0 (closeCodeInRange + controlImpliesFrameSafe via fromLteTrue on compile-time Nat literals) - SafePromptInjection.idr: 2 believe_me → 0 (Right prf already in scope) - SafeCORS.idr: 3 believe_me → 0 (falseImpliesNotTrue + pair of proof terms + fromLteTrue 3600 86400 Refl for oneHourMaxAgeReasonable) - SafeAPIKey.idr: sufficientEntropyNonEmpty proven via unpackLength + case split logSafeBounded (SafeAPIKey) keeps 1 believe_me: prim__strAppend and prim__strSubstr are not type-level reducible. Documented with proof sketch. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 9186016 commit d262256

6 files changed

Lines changed: 139 additions & 29 deletions

File tree

‎src/abi/Boj/SafeAPIKey.idr‎

Lines changed: 15 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -126,11 +126,23 @@ toLogSafe s =
126126
export
127127
sufficientEntropyNonEmpty : SufficientEntropy s -> NonEmpty (unpack s)
128128
sufficientEntropyNonEmpty (MkSufficientEntropy s {prf}) =
129-
believe_me (IsNonEmpty {x = 'a', xs = []})
130-
129+
let -- Recast prf against the unpacked list length
130+
len_eq = unpackLength s -- length (unpack s) = length s
131+
len_ge = replace {p = \n => LTE Boj.SafeAPIKey.minKeyLength n}
132+
(sym len_eq) prf -- LTE 22 (length (unpack s))
133+
in case unpack s of
134+
[] => absurd len_ge -- Uninhabited (LTE 22 0)
135+
(_ :: _) => IsNonEmpty
136+
137+
||| The redacted key from `toLogSafe` is always at most 11 characters long.
138+
||| Axiomatic: length arithmetic over `substr` and `++` is not reducible at the
139+
||| Idris2 type level (prim__strAppend and prim__strSubstr are backend
140+
||| primitives). Proven by inspection of the two branches of `toLogSafe`:
141+
||| - short path (length s ≤ 8): output is "***" (length 3 ≤ 11)
142+
||| - long path: 4 + 3 + 4 = 11 characters exactly
131143
export
132144
logSafeBounded : (s : String) -> LTE (length (toLogSafe s)) 11
133-
logSafeBounded s = believe_me (LTEZero {right = 11})
145+
logSafeBounded _ = believe_me (LTEZero {right = 11})
134146

135147
--------------------------------------------------------------------------------
136148
-- FFI Bridge Declarations

‎src/abi/Boj/SafeCORS.idr‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -140,9 +140,9 @@ decideCredentialSafe p with (p.allowCredentials) proof credPrf
140140
decideCredentialSafe p | False = Left (NoCredentials p {prf = credPrf})
141141
decideCredentialSafe p | True with (elem Boj.SafeCORS.wildcardOrigin p.allowedOrigins) proof elemPrf
142142
decideCredentialSafe p | True | False =
143-
Left (NoWildcard p {prf = (believe_me (Refl {x = True}))})
143+
Left (NoWildcard p {prf = falseImpliesNotTrue _ elemPrf})
144144
decideCredentialSafe p | True | True =
145-
Right (believe_me (Refl {x = (True, True)}))
145+
Right (credPrf, elemPrf)
146146

147147
export
148148
consOriginsValid : OriginValid o -> AllOriginsValid os -> AllOriginsValid (o :: os)
@@ -154,7 +154,7 @@ zeroMaxAgeReasonable = MkReasonableMaxAge 0 {prf = LTEZero}
154154

155155
export
156156
oneHourMaxAgeReasonable : ReasonableMaxAge 3600
157-
oneHourMaxAgeReasonable = MkReasonableMaxAge 3600 {prf = (believe_me (Refl {x = True}))}
157+
oneHourMaxAgeReasonable = MkReasonableMaxAge 3600 {prf = fromLteTrue 3600 86400 Refl}
158158

159159
--------------------------------------------------------------------------------
160160
-- Default Policies

‎src/abi/Boj/SafePromptInjection.idr‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ decidePromptSafe : (s : String) ->
4949
(containsInjectionPattern s = True)
5050
decidePromptSafe s with (containsInjectionPattern s) proof prf
5151
decidePromptSafe s | False = Left (MkPromptSafe s {prf = prf})
52-
decidePromptSafe s | True = Right (believe_me (Refl {x = True}))
52+
decidePromptSafe s | True = Right prf
5353

5454
--------------------------------------------------------------------------------
5555
-- Role Boundary Safety
@@ -81,7 +81,7 @@ decideRoleBoundarySafe : (s : String) ->
8181
(isRoleBoundary s = True)
8282
decideRoleBoundarySafe s with (isRoleBoundary s) proof prf
8383
decideRoleBoundarySafe s | False = Left (MkRoleBoundarySafe s {prf = prf})
84-
decideRoleBoundarySafe s | True = Right (believe_me (Refl {x = True}))
84+
decideRoleBoundarySafe s | True = Right prf
8585

8686
--------------------------------------------------------------------------------
8787
-- Delimiter Escape Safety

‎src/abi/Boj/SafeWebSocket.idr‎

Lines changed: 15 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -135,8 +135,12 @@ data ControlFrameSizeSafe : Nat -> Type where
135135

136136
export
137137
controlImpliesFrameSafe : ControlFrameSizeSafe n -> FrameSizeSafe n
138+
||| maxControlFrameSize (125) ≤ maxFrameSize (16 777 216).
139+
maxControlLeqMaxFrame : LTE Boj.SafeWebSocket.maxControlFrameSize Boj.SafeWebSocket.maxFrameSize
140+
maxControlLeqMaxFrame = fromLteTrue 125 16777216 Refl
141+
138142
controlImpliesFrameSafe (MkControlFrameSizeSafe n {prf}) =
139-
MkFrameSizeSafe n {prf = transitive prf (believe_me (LTESucc LTEZero))}
143+
MkFrameSizeSafe n {prf = transitive prf maxControlLeqMaxFrame}
140144

141145
export
142146
emptyFrameSafe : FrameSizeSafe 0
@@ -216,16 +220,18 @@ parseRoundtrips PolicyViolation = Refl
216220
parseRoundtrips MessageTooBig = Refl
217221
parseRoundtrips InternalError = Refl
218222

223+
||| Every RFC 6455 close code lies in the range [1000, 1011].
224+
||| Proofs constructed via fromLteTrue on the closed-form values.
219225
export
220226
closeCodeInRange : (c : WSCloseCode) -> (LTE 1000 (closeCodeToNat c), LTE (closeCodeToNat c) 1011)
221-
closeCodeInRange NormalClosure = (believe_me (Refl {x = True}), believe_me (Refl {x = True}))
222-
closeCodeInRange GoingAway = (believe_me (Refl {x = True}), believe_me (Refl {x = True}))
223-
closeCodeInRange ProtocolError = (believe_me (Refl {x = True}), believe_me (Refl {x = True}))
224-
closeCodeInRange UnsupportedData = (believe_me (Refl {x = True}), believe_me (Refl {x = True}))
225-
closeCodeInRange InvalidPayload = (believe_me (Refl {x = True}), believe_me (Refl {x = True}))
226-
closeCodeInRange PolicyViolation = (believe_me (Refl {x = True}), believe_me (Refl {x = True}))
227-
closeCodeInRange MessageTooBig = (believe_me (Refl {x = True}), believe_me (Refl {x = True}))
228-
closeCodeInRange InternalError = (believe_me (Refl {x = True}), believe_me (Refl {x = True}))
227+
closeCodeInRange NormalClosure = (fromLteTrue 1000 1000 Refl, fromLteTrue 1000 1011 Refl)
228+
closeCodeInRange GoingAway = (fromLteTrue 1000 1001 Refl, fromLteTrue 1001 1011 Refl)
229+
closeCodeInRange ProtocolError = (fromLteTrue 1000 1002 Refl, fromLteTrue 1002 1011 Refl)
230+
closeCodeInRange UnsupportedData = (fromLteTrue 1000 1003 Refl, fromLteTrue 1003 1011 Refl)
231+
closeCodeInRange InvalidPayload = (fromLteTrue 1000 1007 Refl, fromLteTrue 1007 1011 Refl)
232+
closeCodeInRange PolicyViolation = (fromLteTrue 1000 1008 Refl, fromLteTrue 1008 1011 Refl)
233+
closeCodeInRange MessageTooBig = (fromLteTrue 1000 1009 Refl, fromLteTrue 1009 1011 Refl)
234+
closeCodeInRange InternalError = (fromLteTrue 1000 1011 Refl, fromLteTrue 1011 1011 Refl)
229235

230236
--------------------------------------------------------------------------------
231237
-- Message Ordering

‎src/abi/Boj/Safety.idr‎

Lines changed: 65 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -77,29 +77,88 @@ export
7777
emptyIsJSONSafe : JSONStringSafe ""
7878
emptyIsJSONSafe = MkJSONStringSafe ""
7979

80+
-- Helper: given isShellSafe c = True and c == target = True, derive a
81+
-- contradiction using the fact that isShellSafe target = False.
82+
-- Idris2 can reduce isShellSafe on literal Char arguments because
83+
-- isAlphaNum and the char comparison operators are pure Idris2 functions
84+
-- whose values on literals are computed during elaboration.
85+
private
86+
shellContra : (c, target : Char) ->
87+
isShellSafe c = True ->
88+
c == target = True ->
89+
isShellSafe target = False ->
90+
Void
91+
shellContra c target hp ceq notSafe =
92+
let cEqTarget = charEqSound c target ceq
93+
targetHp = replace {p = \x => isShellSafe x = True} cEqTarget hp
94+
in trueNotFalse (trans (sym targetHp) notSafe)
95+
96+
-- Helper: given not (isSQLDangerous c) = True and c == target = True,
97+
-- derive a contradiction when isSQLDangerous target = True.
98+
private
99+
sqlContra : (c, target : Char) ->
100+
not (isSQLDangerous c) = True ->
101+
c == target = True ->
102+
isSQLDangerous target = True ->
103+
Void
104+
sqlContra c target hp ceq isDangerous =
105+
let cEqTarget = charEqSound c target ceq
106+
targetNotDng = replace {p = \x => not (isSQLDangerous x) = True} cEqTarget hp
107+
-- targetNotDng : not (isSQLDangerous target) = True
108+
-- isDangerous : isSQLDangerous target = True
109+
-- Contradiction: not True = True is False = True
110+
in trueNotFalse (trans (sym targetNotDng) (cong not isDangerous))
111+
112+
-- Generic proof that a character is not in a shell-safe string.
113+
-- Reduces to: allImplies (notTarget prf) → allNeqImpliesNotElem → falseImpliesNotTrue.
114+
private
115+
shellSafeNotTarget : (target : Char) ->
116+
isShellSafe target = False ->
117+
ShellSafe s ->
118+
not (target `elem` unpack s) = True
119+
shellSafeNotTarget target notSafe (MkShellSafe s {prf}) =
120+
let notTarget : (c : Char) -> isShellSafe c = True -> not (c == target) = True
121+
notTarget c hp with (c == target) proof ceq
122+
notTarget c hp | False = Refl
123+
notTarget c hp | True = absurd (shellContra c target hp ceq notSafe)
124+
in falseImpliesNotTrue _ (allNeqImpliesNotElem (allImplies notTarget prf))
125+
126+
-- Generic proof that a character is not in a SQL-safe string.
127+
private
128+
sqlSafeNotTarget : (target : Char) ->
129+
isSQLDangerous target = True ->
130+
SQLSafe s ->
131+
not (target `elem` unpack s) = True
132+
sqlSafeNotTarget target isDangerous (MkSQLSafe s {prf}) =
133+
let notTarget : (c : Char) -> not (isSQLDangerous c) = True -> not (c == target) = True
134+
notTarget c hp with (c == target) proof ceq
135+
notTarget c hp | False = Refl
136+
notTarget c hp | True = absurd (sqlContra c target hp ceq isDangerous)
137+
in falseImpliesNotTrue _ (allNeqImpliesNotElem (allImplies notTarget prf))
138+
80139
export
81140
shellSafeNoSemicolon : ShellSafe s -> not (';' `elem` unpack s) = True
82-
shellSafeNoSemicolon _ = believe_me (Refl {x = True})
141+
shellSafeNoSemicolon = shellSafeNotTarget ';' Refl
83142
84143
export
85144
shellSafeNoBacktick : ShellSafe s -> not ('`' `elem` unpack s) = True
86-
shellSafeNoBacktick _ = believe_me (Refl {x = True})
145+
shellSafeNoBacktick = shellSafeNotTarget '`' Refl
87146
88147
export
89148
shellSafeNoDollar : ShellSafe s -> not ('$' `elem` unpack s) = True
90-
shellSafeNoDollar _ = believe_me (Refl {x = True})
149+
shellSafeNoDollar = shellSafeNotTarget '$' Refl
91150
92151
export
93152
shellSafeNoPipe : ShellSafe s -> not ('|' `elem` unpack s) = True
94-
shellSafeNoPipe _ = believe_me (Refl {x = True})
153+
shellSafeNoPipe = shellSafeNotTarget '|' Refl
95154
96155
export
97156
sqlSafeNoTerminator : SQLSafe s -> not (';' `elem` unpack s) = True
98-
sqlSafeNoTerminator _ = believe_me (Refl {x = True})
157+
sqlSafeNoTerminator = sqlSafeNotTarget ';' Refl
99158
100159
export
101160
sqlSafeNoQuotes : SQLSafe s -> not ('\'' `elem` unpack s) = True
102-
sqlSafeNoQuotes _ = believe_me (Refl {x = True})
161+
sqlSafeNoQuotes = sqlSafeNotTarget '\'' Refl
103162

104163
export
105164
pathSafeNoParent : PathSafe s -> not (isInfixOf (unpack "..") (unpack s)) = True

‎src/abi/Boj/SafetyLemmas.idr‎

Lines changed: 39 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,16 @@
22
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
33
||| BoJ SafetyLemmas — Foundational lemmas for safety proofs
44
|||
5-
||| Reusable lemmas over List Char that underpin the safety proofs in
6-
||| SafeHTTP, SafeCORS, SafeWebSocket, SafePromptInjection, SafeAPIKey,
7-
||| and Safety modules.
5+
||| Reusable lemmas over List Char, Nat, and String that underpin the safety
6+
||| proofs in SafeHTTP, SafeCORS, SafeWebSocket, SafePromptInjection,
7+
||| SafeAPIKey, and Safety modules.
88
|||
9-
||| All proofs are structural inductions over List Char. No believe_me.
9+
||| Three axiomatic believe_me primitives are declared here:
10+
||| charEqSound — soundness of prim__eqChar (c1 == c2 = True → c1 = c2)
11+
||| charEqSym — symmetry of prim__eqChar (x == y = y == x)
12+
||| unpackLength — prim__strToCharList preserves length
13+
|||
14+
||| All other proofs are constructive.
1015
module Boj.SafetyLemmas
1116

1217
import Data.List
@@ -40,8 +45,14 @@ export
4045
notTrueNotTrue : not True = True -> Void
4146
notTrueNotTrue Refl impossible
4247

43-
||| Helper: symmetry of Char equality (admitted as primitive property)
44-
||| In a full proof system this would be proven via primitive properties.
48+
||| Primitive char equality soundness: c1 == c2 = True implies c1 = c2.
49+
||| Axiomatic: correctness of Idris2's prim__eqChar backend primitive.
50+
export
51+
charEqSound : (c1, c2 : Char) -> c1 == c2 = True -> c1 = c2
52+
charEqSound c1 c2 _ = believe_me Refl
53+
54+
||| Helper: symmetry of Char equality.
55+
||| Axiomatic: symmetry of prim__eqChar on the BEAM/Chez backend.
4556
export
4657
charEqSym : (x, y : Char) -> (x == y) = (y == x)
4758
charEqSym x y = believe_me (Refl {x = (x == y)})
@@ -186,6 +197,28 @@ allNeqImpliesNotElem {target} {xs = x :: xs'} prf with (x == target) proof xEq
186197
rewrite sym xEq in Refl
187198
in rewrite goal_rewrite in allNeqImpliesNotElem {xs = xs'} prf
188199

200+
--------------------------------------------------------------------------------
201+
-- String / Nat helpers
202+
--------------------------------------------------------------------------------
203+
204+
||| `unpack s` has the same length as `s`.
205+
||| Axiomatic: prim__strToCharList preserves length (backend primitive guarantee).
206+
export
207+
unpackLength : (s : String) -> length (unpack s) = length s
208+
unpackLength _ = believe_me Refl
209+
210+
||| Convert a Bool-valued `lte` test to a proof term.
211+
|||
212+
||| Enables large-Nat range proofs (e.g. LTE 3600 86400) without building
213+
||| depth-n proof trees. With `%builtin NaturalNumber Nat` the elaborator
214+
||| evaluates `lte m n` efficiently on literal arguments, so `Refl` is accepted
215+
||| as the evidence argument when both m and n are compile-time constants.
216+
export
217+
fromLteTrue : (m, n : Nat) -> lte m n = True -> LTE m n
218+
fromLteTrue Z _ _ = LTEZero
219+
fromLteTrue (S _) Z prf = absurd prf
220+
fromLteTrue (S m) (S n) prf = LTESucc (fromLteTrue m n prf)
221+
189222
--------------------------------------------------------------------------------
190223
-- take/drop (for List-based truncation proofs)
191224
--------------------------------------------------------------------------------

0 commit comments

Comments
 (0)