internal/auditpush at cf9f18e59c, reviewed by claude-code, verified by codex.
`Retracted` is not a fixpoint: at every odd retraction depth >= 3 (retract A, retract that retraction, retract that one) it reports A as NOT retracted, so a retracted scan is served live to the DuckDB view, the warehouse push, the verdict cache, the prior and `corral scans`.
set -e
SRC=internal/auditpush/ledgerdir.go
D=repro_retracted
rm -rf "$D"
mkdir -p "$D"
printf 'module repro_retracted\n\ngo 1.21\n' > "$D/go.mod"
{
printf 'package main\n\nimport (\n"fmt"\n"os"\n"sort"\n)\n\n'
printf 'const KindRetract = "retract"\n\n'
printf 'type LedgerEntry struct {\nHash string\nKind string\nRetracts string\n}\n\n'
awk '/^func Retracted\(entries/{f=1} f{print} f && /^}$/{exit}' "$SRC"
cat <<'GOEOF'
func chain(d int) []LedgerEntry {
e := []LedgerEntry{{Hash: "SCAN"}}
prev := "SCAN"
for i := 1; i <= d; i++ {
h := fmt.Sprintf("R%d", i)
e = append(e, LedgerEntry{Hash: h, Kind: KindRetract, Retracts: prev})
prev = h
}
return e
}
func main() {
fmt.Println("Retracted() documents: a retraction that has ITSELF been retracted is not in")
fmt.Println("force, so the entry it named comes back -- resolved to a FIXPOINT, because the")
fmt.Println("undo can itself be undone.")
fmt.Println("")
fmt.Println("Chain of depth d: SCAN, R1->SCAN, R2->R1, ..., Rd->R(d-1).")
fmt.Println("Rd is in force (nothing retracts it) => R(d-1) is not => R(d-2) is => ...")
fmt.Println("so SCAN is retracted exactly when d is ODD.")
fmt.Println("")
fmt.Println(" d | Retracted() returned | SCAN reported retracted | verdict")
bad := 0
for d := 1; d <= 5; d++ {
out := Retracted(chain(d))
var got []string
for k, v := range out {
got = append(got, k+"<-"+v.Hash)
}
sort.Strings(got)
_, saysRetracted := out["SCAN"]
want := d%2 == 1
mark := "ok"
if saysRetracted != want {
mark = "WRONG (want " + fmt.Sprint(want) + ")"
bad++
}
fmt.Printf(" %d | %-24v | %-23v | %s\n", d, got, saysRetracted, mark)
}
fmt.Println("")
if bad == 0 {
fmt.Println("no defect")
os.Exit(1)
}
fmt.Printf("DEFECT: %d of 5 depths are wrong.\n", bad)
fmt.Println("void[] is monotone and is written within the SAME pass it is read: R2 marks R1")
fmt.Println("void before R3 marks R2 void, and nothing ever un-voids R1, so the first")
fmt.Println("in-force retraction is silently dropped. The loop terminates with changed=false")
fmt.Println("on a state that is not the fixpoint the comment claims.")
fmt.Println("Consequence: a scan that IS retracted is reported live by Retracted() and by")
fmt.Println("LiveEntries()/ScanEntries() built on it, so it is replayed into the DuckDB view")
fmt.Println("(LoadDir), pushed to the warehouse (PushLedgerDir), served to the verdict cache")
fmt.Println("and the prior, and listed UNMARKED by `corral scans`.")
os.Exit(0)
}
GOEOF
} > "$D/main.go"
echo "=== Retracted(), extracted verbatim from $SRC ==="
sed -n '/^func Retracted(entries/,/^}$/p' "$SRC"
echo "=== run ==="
cd "$D"
GOFLAGS= GOWORK=off GO111MODULE=on go run .=== Retracted(), extracted verbatim from internal/auditpush/ledgerdir.go ===
func Retracted(entries []LedgerEntry) map[string]LedgerEntry {
// A retraction that has ITSELF been retracted is not in force, so the
// entry it named comes back. Without this, retracting a retraction was
// accepted and did nothing: a mistaken retraction was permanent, which
// is a one-way door the record does not otherwise have. Resolved to a
// fixpoint rather than in one pass, because the undo can itself be
// undone. Found by a cold review, 2026-09-08 (R7).
byHash := map[string]LedgerEntry{}
var retractions []LedgerEntry
for _, e := range entries {
byHash[e.Hash] = e
if e.Kind == KindRetract {
retractions = append(retractions, e)
}
}
void := map[string]bool{} // retraction hashes that are themselves retracted
for changed := true; changed; {
changed = false
for _, r := range retractions {
if void[r.Hash] {
continue
}
// r is in force; anything it retracts is out — including
// another retraction.
if t, ok := byHash[r.Retracts]; ok && t.Kind == KindRetract && !void[t.Hash] {
void[t.Hash] = true
changed = true
}
}
}
out := map[string]LedgerEntry{}
for _, e := range retractions {
if void[e.Hash] {
continue
}
out[e.Retracts] = e
}
return out
}
=== run ===
Retracted() documents: a retraction that has ITSELF been retracted is not in
force, so the entry it named comes back -- resolved to a FIXPOINT, because the
undo can itself be undone.
Chain of depth d: SCAN, R1->SCAN, R2->R1, ..., Rd->R(d-1).
Rd is in force (nothing retracts it) => R(d-1) is not => R(d-2) is => ...
so SCAN is retracted exactly when d is ODD.
d | Retracted() returned | SCAN reported retracted | verdict
1 | [SCAN<-R1 ] | true | ok
2 | [R1<-R2 ] | false | ok
3 | [R2<-R3 ] | false | WRONG (want true)
4 | [R3<-R4 ] | false | ok
5 | [R4<-R5 ] | false | WRONG (want true)
DEFECT: 2 of 5 depths are wrong.
void[] is monotone and is written within the SAME pass it is read: R2 marks R1
void before R3 marks R2 void, and nothing ever un-voids R1, so the first
in-force retraction is silently dropped. The loop terminates with changed=false
on a state that is not the fixpoint the comment claims.
Consequence: a scan that IS retracted is reported live by Retracted() and by
LiveEntries()/ScanEntries() built on it, so it is replayed into the DuckDB view
(LoadDir), pushed to the warehouse (PushLedgerDir), served to the verdict cache
and the prior, and listed UNMARKED by `corral scans`.I checked `Retracted`, `LiveEntries`, and `ScanEntries` and tried to identify an ordering rule or writer restriction that would make depth-three retractions impossible. `WriteRetraction` only rejects a target already directly named by a retraction; after R2 retracts R1, R3 may target R2. In `Retracted`, R2 marks R1 void before R3 marks R2 void, and the monotone map never removes R1. Thus SCAN is omitted from the returned retracted set at depth 3 even though R3 leaves R1 in force. The supplied reproduction matches the implementation and the affected readers consume this result.
ref cd8d5d2dffaddb9c4e42e2ac5e51542bc8c63a9af3191adce8a9f928e77c187f#R1
AppendLedgerEntry re-hashes only the HEAD entry, so a chain whose non-head entry was edited is extended and signed anyway, while the error text it would have printed claims it refuses "a chain that is already broken".
I traced `AppendLedgerEntry` through `ReadLedgerDir`, `EntryHash`, and `placeEntry`, looking for a whole-chain verification before placement. The only integrity check in append recomputes `existing[len(existing)-1]`; an edited earlier entry is not checked. The new entry is then linked to and optionally signed over the intact head. A later `VerifyLedgerDir` can expose the earlier corruption, but that does not refute the claim that append extends such a chain or that its error wording states a broader refusal than it implements.
ref cd8d5d2dffaddb9c4e42e2ac5e51542bc8c63a9af3191adce8a9f928e77c187f#R2
VerifyLedgerDir has no notion of chain LENGTH or of an expected head, so deleting the newest k entry files from a ledger directory leaves a chain that verifies entirely clean — an unfavourable run can be erased with no residue, which the entry-file gzip's `nothing is ever rewritten` claim does not cover.
I examined `VerifyLedgerDir`, checkpoint metadata, file ordering, and link validation for an external expected head or entry-count anchor. Verification initializes `prevHash` to empty and only checks the files that remain. Removing a contiguous newest suffix leaves every surviving hash and predecessor link valid. Checkpoints describe history pruned before a checkpoint, not entries expected after the surviving head, so they do not detect this case. Repository or remote history might independently retain evidence, but `VerifyLedgerDir` itself does not.
ref cd8d5d2dffaddb9c4e42e2ac5e51542bc8c63a9af3191adce8a9f928e77c187f#R3
An adjudication is accepted when the hash before its `#` names ANY earlier entry, not a review entry — `seen` holds every entry hash — so a KindAdjudication naming a scan entry plus an invented finding id passes EntryShapeProblem and VerifyLedgerDir and lands a corral_adjudications row whose review_uid joins to no review.
I compared `WriteAdjudication`, `EntryShapeProblem`, `VerifyLedgerDir`, and warehouse insertion. `WriteAdjudication` correctly resolves only review entries and checks the finding ID, but generic `AppendLedgerEntry` uses only `EntryShapeProblem`, which validates reference syntax. During verification, `seen` is a `map[string]bool` containing hashes of every earlier kind, and the adjudication branch tests membership without checking that the referenced entry is `KindReview` or that its finding exists. `insertAdjudicationEntry` then inserts the parsed hash and invented ID without a foreign-key constraint, so the claimed orphan row can land.
ref cd8d5d2dffaddb9c4e42e2ac5e51542bc8c63a9af3191adce8a9f928e77c187f#R4
Recorded so that "found nothing here" can be told apart from "never looked here".
The chain machinery in this package is carefully built and visibly hardened by prior review rounds (keyid inside the hash, checkpoint-verifies-before-pruning, the aliasing fix in CanonicalizeForWarehouse). The place it is still wrong is the one piece of pure logic that has no hash to protect it: `Retracted`. Finding 1 is reproduced — the fixpoint it advertises is not a fixpoint, and at retraction depth 3 (retract a scan, undo it, redo it) the ledger reports a retracted scan as LIVE. That value is consumed by `LoadDir`, `PushLedgerDir`, the verdict cache, the prior and `corral scans`, so a single wrong boolean propagates into the view, the warehouse and the record's own listing. Its own test (ledgerdir_integrity_test.go:204) stops at depth 2, which is the one depth above 1 that happens to be right. Findings 2 and 3 are about the strength of the integrity claims rather than a wrong value: appending re-hashes only the head while the error text claims it refuses a broken chain, and nothing in VerifyLedgerDir notices that the newest k entries were simply deleted. Finding 4 is a small door left open on adjudications.
All four findings stand. R1's supplied execution directly demonstrates the incorrect odd-depth result, and the implementation confirms the monotone `void` set cannot recover when a later retraction invalidates the retraction that populated it. R2 accurately identifies that append validates only the current head rather than the complete existing chain. R3 describes the unavoidable suffix-truncation gap of an internally anchored hash chain; this verifier receives no trusted expected head or length. R4 correctly distinguishes the guarded `WriteAdjudication` path from the weaker generic append-and-verify path, where any earlier entry hash satisfies the reference check.