C1 · journal
Update — witness pass (2026-06-20, commit
3cb8ff9). 1 OPEN obligation(s) below were CLOSED to ✅ PROVEN by new deterministic tests added ininternal/journal/proofs_witness_test.go. The body keeps the original analysis (the gap and the ‘to close’ plan that was then executed); the current verdict is in the master ledger and the executed closures are listed in Closures at the foot of this file.
The journal is fak’s durable, append-only, tamper-evident decision journal — the regulated-audit surface of the trust floor. It implements abi.Emitter: on every audit-relevant lifecycle event (EvDecide/EvDeny/EvQuarantine/EvVDSOHit) it appends one JSONL Row carrying a monotonic Seq, a wall-clock anchor, the tool/trace/verdict/reason, content digests of the call args and result, and a hash-chain link Hash = sha256(PrevHash ‖ content-fields). “Correct” here is a regime-C / integrity property, not a numerical one: the ledger must resist an adversary who can edit the file, by making any post-hoc mutation detectable (it does not prevent a privileged edit — it makes one break Verify), and it must be durable — a row already returned to the caller must survive a process crash. The two theorems below pin those two guarantees.
THEOREM (1) Append-only hash-chain tamper-evidence. For a file-backed journal, every committed Row N carries PrevHash = the hash of row N−1 and Hash = sha256 over PrevHash chained with N’s content fields (Seq..ResultDigest, in declaration order). Therefore mutating any byte of any already-committed row makes Verify(path) return a non-nil error at the first broken link. The chain is append-only: Seq is monotonic 1-based, and a reopen continues the same chain rather than forking it.
REGIME C — crypto / integrity (hash-chain / WORM ledger).
PROOF append() stamps row.PrevHash = j.lastHash and row.Hash = chainHash(row.PrevHash, row), then advances j.lastHash (journal.go:145-147). chainHash writes the previous hash, a 0x1f unit separator, then the content fields Seq..ResultDigest in declaration order into one SHA-256; PrevHash and Hash are excluded from the pre-image (PrevHash is the chained-in prefix, Hash is the output) and the unit separators make a concatenation collision impossible (journal.go:315-322). Verify/verifyReader re-read the file line by line (journal.go:444-482) and verifyStep enforces three independent checks on every row: monotonic sequence (row.Seq == wantSeq), prev-hash continuity (row.PrevHash == prev), and authenticity (chainHash(row.PrevHash,row) == row.Hash) (journal.go:505-516). A single mutated content byte changes the recomputed chainHash and trips the authenticity check at that row; an adversary who re-hashes to cover it produces a Hash that no longer matches the next row’s PrevHash, tripping the continuity check there. recoverHead recovers seq+lastHash from existing content on Open, so a restart continues the same chain (journal.go:409-438).
WITNESS go test ./internal/journal/ -count=1 -timeout 120s -run 'TestVerifyDetectsTampering|TestFileJournalReopensAndContinuesChain' -v
TestVerifyDetectsTampering (journal_test.go:77-106) writes two rows, asserts Verify green (n=2), then rewrites the file replacing "tool":"Bash" → "tool":"Fish" in a past row and asserts Verify(path) returns a non-nil error — the tamper-evidence property directly. TestFileJournalReopensAndContinuesChain (journal_test.go:51-75) reopens after Close, appends, and Verify returns n=2, nil — chain continuation, not fork.
VERDICT PROVEN — 2026-06-20 (Mac node, native go test). Output tail: --- PASS: TestMemoryJournalChainsRecentAndStreams / --- PASS: TestFileJournalReopensAndContinuesChain / --- PASS: TestVerifyDetectsTampering / ok github.com/anthony-chaudhary/fak/internal/journal 0.205s.
DOS bound at ship.
THEOREM (2) Per-write durable flush (a crash loses nothing already returned). For a file-backed journal, each Emit that produces an audit row flushes that row’s bytes to the OS file before returning, so a process crash (not power loss) after Emit returns loses no committed row — a Verify(path) issued without any intervening Close()/Flush() recovers every emitted row.
REGIME C — crypto / integrity (durability of the audit record).
PROOF append() calls writeRow(j.bw, row) synchronously under the lock for every committed row when j.bw != nil (journal.go:149-153). writeRow marshals the row, writes the JSONL line, and calls bw.Flush() before returning (journal.go:296-308), so the bytes leave the user-space bufio buffer into the OS page cache on every row — surviving a process crash. This is the mechanism the package header claims (journal.go:11-14). The mechanism is real, but the witness is missing. Every Verify(path)/os.ReadFile in the test file runs after a j.Close() (journal_test.go:72 after two Closes; journal_test.go:88/92 after the Close at line 85), and Close() itself flushes and fsyncs (journal.go:281-292). A green Verify there is equally explained by Close’s flush, so no test distinguishes “flushed per Emit” from “flushed only at Close”. No counterexample exists — the code does flush per row — so this is OPEN, not REFUTED.
CLOSING WITNESS Emit N rows on an Open(path) journal and, with no Close and no Flush call, invoke Verify(path) (a fresh os.Open of the same path) and assert n == N, nil. That isolates writeRow’s bw.Flush() as the sole thing that put the bytes on disk. The named frontier upgrade is a Gobra crash-safety / append-ordering proof — 00-METHOD.md §6 lists journal append ordering among the scoped-out concurrency-critical leaves where a data-race / crash-safety proof would strictly dominate a runtime test.
WITNESS go test ./internal/journal/ -count=1 -timeout 120s -run 'TestFileJournalReopensAndContinuesChain|TestVerifyDetectsTampering' -v — both PASS, but neither isolates the pre-Close flush.
VERDICT OPEN — 2026-06-20 (Mac node, native go test). The per-Emit flush is implemented (journal.go:307) but un-witnessed; the closing witness above would promote it to PROVEN.
DOS bound at ship.
Closures (witness pass 2026-06-20, commit 3cb8ff9)
Each obligation marked OPEN above was discharged by a new zero-dependency (stdlib testing/testing/quick) metamorphic/round-trip/invariant test that ASSERTS the property against an independently recomputed reference. Verified by go test -count=1 ./internal/... (45 packages green, 0 failures).
- per-write-durable-flush → ✅ PROVEN by
TestPerWriteDurableFlush_VerifyWithoutCloseRecoversEveryEmittedRow. Sound, non-vacuous, deterministic. Mechanism: Emit -> append (journal.go:131-168) -> writeRow (journal.go:296-308) whose final statement is bw.Flush(), pushing buffered bytes to the OS file on EVERY row. The test opens a file-backed journal with an injected fixed clock, then in a loop of 64 Emits checks after EACH Emit that an independent Verify(path) – which opens the file from scratch, exactly as a crash-recovery auditor would, with NO intervening j.Close()/j.Flush() – recovers EXACTLY the number of rows emitted so far (exact integer equality, not >=). This simulates ‘process crashes here, right after Emit returned’ and asserts no committed row is stranded in the bufio buffer. A second test (TestPerWriteDurableFlush_StatsMatchDurableRows) pins the companion invariant: the producer live head Seq (Stats) equals the durable on-disk row count Verify finds, again with no Close/Flush. NON-VACUITY: if the bw.Flush() in writeRow were removed, rows would sit buffered (bufio default 4KB) and the fresh-handle Verify would see fewer rows than emitted at the early steps, failing the exact-equality assertion; the final post-Close Verify==total guard also rules out a write-nothing vacuity. Both new tests PASS and the whole internal/journal package go test passes with the file present.