| ||| Manifest.seal read/write and per-file gate verification. |
| ||| |
| ||| Copyright (C) 2026 SNAPKITTYWEST / SnapKitty (Jessica) |
| ||| License: BSL-1.1 / AGPL-3.0 / MPL-2.0 |
| module Manifest |
|
|
| import Data.String |
| import Data.List |
| import Data.Maybe |
| import System.File |
| import System.File.ReadWrite |
| import Hash |
| import WORM |
|
|
| -- ── Registered modules ───────────────────────────────────────────────────── |
|
|
| ||| Every file the clone gate tracks. |
| ||| All zeros = UNSEALED. Run `clone_gate seal` to populate. |
| export |
| registeredModules : List String |
| registeredModules = |
| [ "clone_gate/src/Hash.idr" |
| , "clone_gate/src/WORM.idr" |
| , "clone_gate/src/Manifest.idr" |
| , "clone_gate/src/Main.idr" |
| , "clone_gate/cbits/hash_shim.c" |
| , "crates/engine/src/recurrence.rs" |
| , "crates/engine/src/microbit.rs" |
| , "crates/engine/src/cad_kernel.rs" |
| , "crates/engine/src/icp_model.rs" |
| , "crates/engine/src/mmep_relaxation.rs" |
| , "crates/kani-verification/src/lib.rs" |
| , "crates/kani-verification/src/arithmetic_loop.rs" |
| , "lean/Multiplicity/Dynamics/Contraction.lean" |
| , "lean/Multiplicity/Dynamics/GTHZHarmony.lean" |
| , "lean/WalkAA/WalkAmplitudeAmplification.lean" |
| , "lean/WalkAA/WormholeWalk.lean" |
| , "agda/MultiplicityInvariants.agda" |
| , "agda/PrimitiveShattering.agda" |
| , "agda/GTHZHarmony.agda" |
| , "haskell/JohnsonWalk.hs" |
| , "haskell/JohnsonWalkStorable.hs" |
| , "haskell/JohnsonWalkParallel.hs" |
| , "haskell/WormholeWalkF2.hs" |
| , "circuits/MicrobitFullAdder.circom" |
| , "circuits/MicrobitAdderAndDrift.circom" |
| , "hardware/microbit_interlock.sv" |
| , "tools/f2_solver.py" |
| ] |
|
|
| -- ── MANIFEST.seal path ───────────────────────────────────────────────────── |
|
|
| export |
| manifestPath : String |
| manifestPath = "MANIFEST.seal" |
|
|
| -- ── Seal all registered modules ──────────────────────────────────────────── |
|
|
| ||| Hash every registered module and write MANIFEST.seal. |
| ||| Returns the number of entries sealed. |
| export |
| sealAll : HasIO io => String -> io Nat |
| sealAll repoRoot = do |
| let go : (1 c : Chain n) -> List String -> io (n : Nat ** Chain n) |
| go c [] = pure (_ ** c) |
| go c (rel :: rest) = do |
| let abs = repoRoot ++ "/" ++ rel |
| let lbl = "module:" ++ rel |
| c' <- sealFile c lbl rel abs |
| go c' rest |
| (_ ** chain) <- go Empty registeredModules |
| let entries = toList chain |
| let jsonl = unlines (map entryToJsonl entries) |
| Right _ <- writeFile manifestPath jsonl |
| | Left err => do |
| putStrLn $ "[clone_gate] ERROR writing " ++ manifestPath ++ ": " ++ show err |
| pure 0 |
| putStrLn $ "[clone_gate] Sealed " ++ show (length entries) ++ " modules -> " ++ manifestPath |
| pure (length entries) |
|
|
| -- ── Parse MANIFEST.seal ──────────────────────────────────────────────────── |
|
|
| -- Minimal JSON field extractor (no external JSON library needed) |
| extractField : String -> String -> Maybe String |
| extractField key line = |
| let needle = "\"" ++ key ++ "\":\"" |
| in case strIndex line (cast (length needle)) of |
| _ => case split (== needle) line of |
| [_, rest] => Just (takeWhile (/= '"') rest) |
| _ => Nothing |
|
|
| parseEntry : String -> Maybe Entry |
| parseEntry line = do |
| label <- extractField "label" line |
| path <- extractField "path" line |
| digest <- extractField "digest" line |
| prev <- extractField "prev" line |
| seal <- extractField "seal" line |
| pure $ MkEntry label path digest prev seal |
|
|
| -- ── Verify all registered modules ────────────────────────────────────────── |
|
|
| data VerifyResult = OK String | Fail String String String | Missing String |
|
|
| export |
| verifyAll : HasIO io => String -> io Bool |
| verifyAll repoRoot = do |
| Right contents <- readFile manifestPath |
| | Left _ => do |
| putStrLn "[clone_gate] MANIFEST.seal not found. Run: clone_gate seal" |
| pure False |
| let sealed : List Entry |
| sealed = mapMaybe parseEntry (lines contents) |
| let sealedMap : List (String, Entry) |
| sealedMap = map (\e => (e.path, e)) sealed |
| results <- traverse (checkOne repoRoot sealedMap) registeredModules |
| let ok = all isOk results |
| traverse_ printResult results |
| pure ok |
| where |
| isOk : VerifyResult -> Bool |
| isOk (OK _) = True |
| isOk _ = False |
|
|
| checkOne : HasIO io => String -> List (String, Entry) -> String -> io VerifyResult |
| checkOne root sealedMap rel = |
| case lookup rel sealedMap of |
| Nothing => pure (Missing rel) |
| Just e => do |
| actual <- sha256File (root ++ "/" ++ rel) |
| if actual == e.digest |
| then pure (OK rel) |
| else pure (Fail rel e.digest actual) |
|
|
| printResult : HasIO io => VerifyResult -> io () |
| printResult (OK rel) = putStrLn $ " [OK] " ++ rel |
| printResult (Missing rel) = putStrLn $ " [MISSING] " ++ rel |
| printResult (Fail rel exp act) = do |
| putStrLn $ " [FAIL] " ++ rel |
| putStrLn $ " expected: " ++ take 32 exp ++ "..." |
| putStrLn $ " actual : " ++ take 32 act ++ "..." |
|
|
| -- ── Per-file gate (import-time check) ────────────────────────────────────── |
|
|
| ||| Call at the top of any sovereign module to verify it hasn't been tampered. |
| ||| On failure: prints an error and exits with code 1. |
| export |
| gate : HasIO io => String -> String -> io () |
| gate repoRoot relPath = do |
| Right contents <- readFile (repoRoot ++ "/" ++ manifestPath) |
| | Left _ => do |
| putStrLn $ "[clone_gate] WARNING: " ++ relPath ++ " — MANIFEST.seal not found (unsealed)" |
| pure () |
| let sealed = mapMaybe parseEntry (lines contents) |
| case find (\e => e.path == relPath) sealed of |
| Nothing => putStrLn $ "[clone_gate] WARNING: " ++ relPath ++ " not in manifest" |
| Just e => |
| if isUnsealed e.digest |
| then putStrLn $ "[clone_gate] WARNING: " ++ relPath ++ " UNSEALED" |
| else do |
| actual <- sha256File (repoRoot ++ "/" ++ relPath) |
| when (actual /= e.digest) $ do |
| putStrLn $ "\n[clone_gate] INTEGRITY FAILURE: " ++ relPath |
| putStrLn $ " expected: " ++ e.digest |
| putStrLn $ " actual : " ++ actual |
| putStrLn $ " => File modified since last seal. Run: clone_gate seal" |
| exitFailure |
|
|
