---
title: "fak proof: journal hash-chain tamper-evidence"
description: "Proof that fak's append-only decision journal makes any post-hoc row mutation break Verify and durably flushes each audit row before returning."
---

# C1 · journal

> **Update — witness pass (2026-06-20, commit `3cb8ff9`).** 1 OPEN obligation(s) below were CLOSED to ✅ PROVEN by new deterministic tests added in `internal/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](README.md)** 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.
