File size: 3,334 Bytes
4953a87 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 | ||| WORM (Write-Once-Read-Many) append-only chain with linear types.
|||
||| Linear types enforce the invariant at compile time:
||| - A Chain can only be EXTENDED, never mutated.
||| - Once a seal is issued it cannot be retracted.
||| - Reading the chain consumes it (you must use it exactly once).
|||
||| Copyright (C) 2026 SNAPKITTYWEST / SnapKitty (Jessica)
||| License: BSL-1.1 / AGPL-3.0 / MPL-2.0
module WORM
import Data.String
import Hash
-- ── Entry ──────────────────────────────────────────────────────────────────
||| A single WORM chain entry.
public export
record Entry where
constructor MkEntry
label : String -- human-readable label (e.g. "module:src/Hash.idr")
path : String -- repo-relative file path
digest : String -- SHA-256 of the file
prev : String -- SHA-256 seal of the previous entry (or zeroDigest)
seal : String -- SHA-256 of (label ++ path ++ digest ++ prev)
||| Serialise an entry to a single JSON line for MANIFEST.seal.
export
entryToJsonl : Entry -> String
entryToJsonl e =
"{\"label\":\"" ++ e.label ++ "\"," ++
"\"path\":\"" ++ e.path ++ "\"," ++
"\"digest\":\"" ++ e.digest ++ "\"," ++
"\"prev\":\"" ++ e.prev ++ "\"," ++
"\"seal\":\"" ++ e.seal ++ "\"}"
-- ── Chain (linear, append-only) ────────────────────────────────────────────
||| Append-only chain. The nat index tracks the entry count.
||| Linear (1 chain) means the old chain is consumed on append.
public export
data Chain : (n : Nat) -> Type where
Empty : Chain 0
Snoc : (1 c : Chain n) -> Entry -> Chain (S n)
||| Append an entry. Linearly consumes the old chain.
export
append : (1 c : Chain n) -> Entry -> Chain (S n)
append c e = Snoc c e
||| Flatten the chain to a list of entries (oldest first).
||| Consumes the chain linearly.
export
toList : (1 c : Chain n) -> List Entry
toList Empty = []
toList (Snoc c e) = toList c ++ [e]
||| The seal of the last entry, or zeroDigest for an empty chain.
export
lastSeal : (1 c : Chain n) -> (String, Chain n)
lastSeal Empty = (Hash.zeroDigest, Empty)
lastSeal (Snoc c e) =
let (_, c') = lastSeal c -- consume inner chain
in (e.seal, Snoc c' e)
-- ── Construction helpers ────────────────────────────────────────────────────
||| Build a new Entry, computing its seal from the C FFI.
export
mkEntry : HasIO io => String -> String -> String -> String -> io Entry
mkEntry label path digest prev = do
let raw = label ++ path ++ digest ++ prev
seal <- sha256String raw
pure $ MkEntry label path digest prev seal
||| Build an Entry from a file path, computing its file digest.
export
sealFile : HasIO io
=> (1 c : Chain n)
-> String -- label
-> String -- repo-relative path
-> String -- absolute path (for hashing)
-> io (Chain (S n))
sealFile c label relPath absPath = do
digest <- sha256File absPath
let (prev, c') = lastSeal c
e <- mkEntry label relPath digest prev
pure (append c' e)
|