fix(cerro-torre): String-bridge — discharge 3 ImporterProofs postulates

PROOF-NEEDS.md

@@ -94,25 +94,38 @@ These encode computational hardness assumptions unprovable in any formal system.
 | `tamperEvidence` | Theorems.idr | sha256CollisionResistant + signatureNonReplayable + list concat non-injectivity |
 | `replayPrevention` | Theorems.idr | signatureNonReplayable (different record type) |
 
-### String Primitive Limitations (6) — INFRASTRUCTURE BUILT
-
-`isPrefixOf` and `isInfixOf` are C primitives with no reduction rules. Proven List Char equivalents exist in `StringLemmas.idr` (`charsPrefixOf`, `charsInfixOf`, `charsPrefixOfAppend`). To eliminate these postulates, add a bridge postulate connecting String operations to their List Char equivalents.
-
-| Postulate | File | Proven equivalent in StringLemmas.idr |
-|-----------|------|--------------------------------------|
-| `extractionSafety` | ImporterProofs.idr | `charsPrefixOfAppend` |
-| `symlinkSafety` | ImporterProofs.idr | `charsPrefixOfAppend` |
-| `zipSlipPrevention` | ImporterProofs.idr | `charsPrefixOfAppend` |
-| `normalizedIsSafe` | ImporterProofs.idr | `dotDotNotInfix` (partial) |
-| `absolutePathRejection` | ImporterProofs.idr | Needs SafePath definition over List Char |
-| `ociLayoutEnforcement` | ImporterProofs.idr | Needs DecEq on TarEntry paths |
-
-### Path to eliminating String postulates
-
-1. Add bridge postulate: `isPrefixOf s1 s2 = charsPrefixOf (unpack s1) (unpack s2)` (1 postulate)
-2. Prove `unpack` distributes over `++`: `unpack (a ++ b) = unpack a ++ unpack b` (may need 1 more postulate)
-3. Derive extractionSafety, symlinkSafety, zipSlipPrevention from bridge + `charsPrefixOfAppend`
-4. Net: 3 postulates → 1-2 bridge postulates (improvement)
+### String Primitive Limitations — 3 of 6 ELIMINATED 2026-05-18
+
+`isPrefixOf` is a C primitive with no reduction rules. The bridge is now
+in place (`StringLemmas.idr`): two minimal documented axioms
+`isPrefixOfBridge` (`isPrefixOf s1 s2 = charsPrefixOf (unpack s1)
+(unpack s2)`) and `unpackAppend` (`unpack (a ++ b) = unpack a ++ unpack
+b`). Via these + the already-proven `charsPrefixOfAppend`, three
+postulates are now **real proofs** (full `cerro-torre.ipkg` green under
+idris2 0.8.0). Net: 3 ad-hoc string postulates → 2 fundamental,
+well-understood ones (same justified category as estate backend
+string-primitive axioms, e.g. boj-server SafetyLemmas).
+
+| Postulate | File | Status |
+|-----------|------|--------|
+| `extractionSafety` | ImporterProofs.idr | **PROVEN** (isPrefixOfBridge + unpackAppend + charsPrefixOfAppend) |
+| `symlinkSafety` | ImporterProofs.idr | **PROVEN** (idem) |
+| `zipSlipPrevention` | ImporterProofs.idr | **PROVEN** (idem) |
+| `normalizedIsSafe` | ImporterProofs.idr | postulate — needs `dotDotNotInfix` + infix bridge |
+| `absolutePathRejection` | ImporterProofs.idr | postulate — needs SafePath over List Char |
+| `ociLayoutEnforcement` | ImporterProofs.idr | postulate — needs DecEq on TarEntry paths |
+
+Remaining bridge axioms (minimal trusted base): `isPrefixOfBridge`,
+`unpackAppend` in `StringLemmas.idr`.
+
+### Path to eliminating remaining String postulates
+
+1. ~~Add `isPrefixOfBridge` + `unpackAppend`~~ — DONE 2026-05-18.
+2. ~~Derive extractionSafety / symlinkSafety / zipSlipPrevention~~ — DONE.
+3. `normalizedIsSafe`: add an `isInfixOf` bridge analogous to
+   `isPrefixOfBridge`, then derive from `dotDotNotInfix`.
+4. `absolutePathRejection`: define `SafePath` semantics over `List Char`.
+5. `ociLayoutEnforcement`: add `DecEq` on `TarEntry` paths.
 
 ## assert_total Usage (2) — ACCEPTABLE
 

container-stack/cerro-torre/verification/idris/ImporterProofs.idr

@@ -19,6 +19,7 @@ import Data.List
 import Data.List1
 import Data.Nat
 import Decidable.Equality
+import StringLemmas
 
 %default total
 
@@ -160,7 +161,10 @@ extractionSafety : (root : Path)
                 -> (entry : TarEntry)
                 -> SafePath (entry.path)
                 -> isPrefixOf root (root ++ "/" ++ entry.path) = True
-extractionSafety _ _ _ = idris_crash "extractionSafety: string-primitive postulate — type-level use only"
+extractionSafety root entry _ =
+  rewrite isPrefixOfBridge root (root ++ "/" ++ entry.path) in
+  rewrite unpackAppend root ("/" ++ entry.path) in
+  charsPrefixOfAppend (unpack root) (unpack ("/" ++ entry.path))
 
 ||| POSTULATE: Symlink Safety
 |||
@@ -178,7 +182,10 @@ symlinkSafety : (root : Path)
              -> entry.symlinkTarget = Just target
              -> SafePath target
              -> isPrefixOf root (root ++ "/" ++ target) = True
-symlinkSafety _ _ _ _ _ _ = idris_crash "symlinkSafety: string-primitive postulate — type-level use only"
+symlinkSafety root _ target _ _ _ =
+  rewrite isPrefixOfBridge root (root ++ "/" ++ target) in
+  rewrite unpackAppend root ("/" ++ target) in
+  charsPrefixOfAppend (unpack root) (unpack ("/" ++ target))
 
 ||| POSTULATE: Absolute Path Rejection
 |||
@@ -278,4 +285,7 @@ zipSlipPrevention : (root : Path)
                  -> (entry : TarEntry)
                  -> SafePath (normalizePath entry.path)
                  -> isPrefixOf root (root ++ "/" ++ normalizePath entry.path) = True
-zipSlipPrevention _ _ _ = idris_crash "zipSlipPrevention: string-primitive postulate — type-level use only"
+zipSlipPrevention root entry _ =
+  rewrite isPrefixOfBridge root (root ++ "/" ++ normalizePath entry.path) in
+  rewrite unpackAppend root ("/" ++ normalizePath entry.path) in
+  charsPrefixOfAppend (unpack root) (unpack ("/" ++ normalizePath entry.path))

container-stack/cerro-torre/verification/idris/StringLemmas.idr

@@ -14,6 +14,7 @@
 
 module StringLemmas
 
+import Data.String
 import Data.List
 import Decidable.Equality
 
@@ -74,3 +75,39 @@ dotDotNotInfix : (xs : List Char)
               -> charsInfixOf ['.', '.'] xs = False
               -> Not (charsInfixOf ['.', '.'] xs = True)
 dotDotNotInfix xs prf contra = absurd (trans (sym prf) contra)
+
+-- ============================================================================
+-- Bridge Axioms (string-primitive postulates)
+-- ============================================================================
+--
+-- These two are the *minimal* trusted base connecting Idris2's opaque C
+-- String primitives to the proven List-Char operations above. They are
+-- the same justified category as backend string-primitive axioms
+-- elsewhere in the estate (cf. boj-server SafetyLemmas charEqSound/
+-- unpackLength): not provable in Idris2 (no reduction rules for the C
+-- prims), minimal, isolated, documented. Per the repo idiom (Idris2 0.8
+-- has no `postulate` keyword) they are `partial`+`idris_crash` stubs.
+--
+-- NET EFFECT: they let ImporterProofs.idr discharge `extractionSafety`,
+-- `symlinkSafety`, `zipSlipPrevention` with real proofs — replacing 3
+-- ad-hoc string postulates with 2 fundamental, well-understood ones.
+
+||| BRIDGE AXIOM: String.isPrefixOf agrees with the proven List-Char
+||| `charsPrefixOf` under `unpack`. `isPrefixOf` is a C primitive with
+||| no reduction rules; this equivalence is a backend-semantics fact.
+partial
+public export
+isPrefixOfBridge : (s1, s2 : String)
+                -> isPrefixOf s1 s2 = charsPrefixOf (unpack s1) (unpack s2)
+isPrefixOfBridge _ _ =
+  idris_crash "isPrefixOfBridge: string-primitive axiom — type-level use only"
+
+||| BRIDGE AXIOM: `unpack` distributes over String `++`. Backend
+||| primitive guarantee (`prim__strAppend` / `prim__strToCharList`),
+||| not reducible at the Idris2 type level.
+partial
+public export
+unpackAppend : (a, b : String)
+            -> unpack (a ++ b) = unpack a ++ unpack b
+unpackAppend _ _ =
+  idris_crash "unpackAppend: string-primitive axiom — type-level use only"