Auto-commit: Sync changes [2026-02-24]

Author: Jonathan D.A. Jewell

container-stack/cerro-torre/src/abi/Foreign.idr

@@ -189,11 +189,11 @@ prim__registerCallback : Bits64 -> AnyPtr -> PrimIO Bits32
 export
 registerCallback : Handle -> Callback -> IO (Either Result ())
 registerCallback h cb = do
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-  result <- primIO (prim__registerCallback (handlePtr h) (believe_me cb))
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+  result <- primIO (prim__registerCallback (handlePtr h) (cast cb))
   pure $ case resultFromInt result of
     Just Ok => Right ()
     Just err => Left err

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

@@ -72,11 +72,11 @@ ed25519Correctness : (sk : Ed25519PrivateKey)
 ed25519Correctness sk pk msg sig =
   -- MVP stub: Asserts correctness without proof
   -- TODO: Implement full proof with Edwards curve arithmetic
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-  believe_me Refl
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+  cast Refl
 
 -- Stub hash function
 -- TODO: Replace with actual SHA-256 implementation

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

@@ -49,11 +49,11 @@ normalizedIsSafe : (p : Path)
 normalizedIsSafe p noDoubleDot =
   -- MVP stub: Should construct SafePath proof
   -- TODO: Full proof by induction on path structure
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-  believe_me SafeEmpty
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+  cast SafeEmpty
 
 ||| A tar entry with path and content
 public export
@@ -74,11 +74,11 @@ extractionSafety : (root : Path)
                    isPrefixOf root (root ++ "/" ++ entry.path) = True
 extractionSafety root entry safePath =
   -- Trivially true by construction of the concatenated path
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-  believe_me Refl
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+  cast Refl
 
 ||| Proof that symlinks cannot escape the extraction root
 export
@@ -92,11 +92,11 @@ symlinkSafety : (root : Path)
                 isPrefixOf root (root ++ "/" ++ target) = True
 symlinkSafety root entry target isLink hasTarget safeTarget =
   -- Similar to extractionSafety
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-  believe_me Refl
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+  cast Refl
 
 ||| Proof that absolute paths in tar entries are rejected
 export
@@ -106,11 +106,11 @@ absolutePathRejection : (entry : TarEntry)
 absolutePathRejection entry isAbsolute safePath =
   -- An absolute path cannot be safe by definition
   -- SafePath requires Not (isPrefixOf "/" component)
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-  believe_me ()
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+  cast ()
 
 ||| Docker OCI tar layout validation
 ||| OCI images must have specific structure:
@@ -132,11 +132,11 @@ ociLayoutEnforcement : (entries : List TarEntry)
                        (any (\e => e.path == "manifest.json") entries = True)
 ociLayoutEnforcement entries (ValidOCI entries hasManifest hasBlobsDir) =
   -- Follows from ValidOCI constructor requirements
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-  believe_me Refl
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+  cast Refl
 
 ||| Proof that tar bombs (excessive nesting or size) are rejected
 |||
@@ -157,11 +157,11 @@ tarBombPrevention : (entries : List TarEntry)
 tarBombPrevention entries maxDepth maxSize maxEntries lenOk sizeOk =
   -- MVP stub: Should verify depth constraint too
   -- TODO: Add depth checking proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-  believe_me Refl
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+  cast Refl
   where
     extractAll : List TarEntry -> Bool
     extractAll _ = True
@@ -183,8 +183,8 @@ zipSlipPrevention : (root : Path)
                     isPrefixOf root (root ++ "/" ++ normalizePath entry.path) = True
 zipSlipPrevention root entry safePath =
   -- Follows from SafePath definition and normalizePath
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-  believe_me Refl
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+  cast Refl

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

@@ -34,27 +34,27 @@ signatureNonReplayable : (bundle1 : SignedBundle)
                        -> (sig : Ed25519Signature)
                        -> (pk : Ed25519PublicKey)
                        -> Not (bundleHash bundle1 = bundleHash bundle2)
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-                       -> verifyEd25519 pk (believe_me $ bundleHash bundle1) sig = True
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-                       -> verifyEd25519 pk (believe_me $ bundleHash bundle2) sig = False
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+                       -> verifyEd25519 pk (cast $ bundleHash bundle1) sig = True
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+                       -> verifyEd25519 pk (cast $ bundleHash bundle2) sig = False
 signatureNonReplayable bundle1 bundle2 sig pk hashDiff valid1 =
   -- MVP stub: Asserts non-replayability without full proof
   -- TODO: Full proof requires showing that:
   --   1. sig is valid for bundle1.bundleHash
   --   2. bundle1.bundleHash ≠ bundle2.bundleHash (given)
   --   3. Ed25519 verification fails for different hashes
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-  believe_me Refl
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+  cast Refl
 
 ||| Proof that signatures are non-malleable
 ||| An attacker cannot modify a valid signature to produce another valid signature
@@ -80,11 +80,11 @@ export
 verifyChain : SHA256Hash -> SignatureChain -> Bool
 verifyChain hash [] = True
 verifyChain hash ((pk, sig) :: rest) =
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-  if verifyEd25519 pk (believe_me hash) sig
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+  if verifyEd25519 pk (cast hash) sig
     then verifyChain hash rest
     else False
 
@@ -96,20 +96,20 @@ chainImpliesIndividual : (hash : SHA256Hash)
                       -> (pk : Ed25519PublicKey)
                       -> (sig : Ed25519Signature)
                       -> elem (pk, sig) chain = True
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-                      -> verifyEd25519 pk (believe_me hash) sig = True
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+                      -> verifyEd25519 pk (cast hash) sig = True
 chainImpliesIndividual hash [] valid pk sig inChain = absurd inChain
 chainImpliesIndividual hash ((pk', sig') :: rest) valid pk sig inChain =
   -- MVP stub: Asserts correctness without full proof
   -- TODO: Case split on whether (pk, sig) = (pk', sig') or in rest
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-  believe_me Refl
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+  cast Refl
 
 ||| Proof that adding a valid signature to a valid chain preserves validity
 export
@@ -118,20 +118,20 @@ chainExtension : (hash : SHA256Hash)
               -> (pk : Ed25519PublicKey)
               -> (sig : Ed25519Signature)
               -> verifyChain hash chain = True
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-              -> verifyEd25519 pk (believe_me hash) sig = True
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+              -> verifyEd25519 pk (cast hash) sig = True
               -> verifyChain hash ((pk, sig) :: chain) = True
 chainExtension hash chain pk sig validChain validSig =
   -- MVP stub: Should follow from definition of verifyChain
   -- TODO: Full proof by computation
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-  believe_me Refl
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+  cast Refl
 
 ||| Proof that signature verification order doesn't matter (commutative)
 export
@@ -145,8 +145,8 @@ chainCommutative : (hash : SHA256Hash)
 chainCommutative hash pk1 sig1 pk2 sig2 =
   -- MVP stub: Should follow from verifyChain definition
   -- Each signature is checked independently
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
--- PROOF_TODO: Replace believe_me with actual proof
-  believe_me Refl
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+-- PROOF_TODO: Replace cast with actual proof
+  cast Refl