docs/verify: session merkle is built over aflock ActionRecords, not Claude JSONL (paper §4.4 wording vs implementation)

[manzil-infinity180]

Problem

Paper §4.4 (Materials Binding) describes the session merkle tree as built over Claude Code's session JSONL:

The materialsFrom directive binds the policy to external artifacts. The session merkle tree is particularly important: by constructing a merkle tree over the session JSONL, we can prove:

• Order: Turn n came after turns 0 through n−1
• Completeness: No turns were omitted
• Distance: Turns are contiguous (no gaps)

Code reality: aflock builds the merkle over aflock.ActionRecord — our own per-tool-call decision log (PreToolUse / PostToolUse records aflock chose to write). It is not the Claude session JSONL transcript.

Concretely:

• internal/state/session.go:214 ComputeSessionMerkleRoot iterates state.Actions (slice of aflock.ActionRecord).
• internal/verify/verifier.go verifySessionMerkle re-marshals the same ActionRecords and compares.
• The actual Claude JSONL transcript lives in ~/.claude/projects/<repo>/<session-uuid>.jsonl and is not input to either function.

Why this matters

The merkle root we publish today proves what aflock observed, not what Claude actually did. Concrete divergences:

1. security: aflock enforcement bypassable via claude-code general-purpose subagent (native Bash/Write) #100 native-Agent bypass: a subagent spawned via Claude Code's general-purpose Agent tool uses native Bash/Write that bypass aflock-uds. Those tool calls land in the JSONL transcript but never in aflock.Actions — the merkle root and verify pipeline are silent on them.
2. Conceptual gap: even when aflock is fully on the call path, aflock records only decision/reason snapshots, not the full assistant message / tool result content. An auditor following the paper's claim would expect the merkle to bind to the JSONL line content; today it binds to a derived summary.

Paper reference

paper/aflock.tex §4.4 "Materials Binding". Also referenced by the §7 capability table row "Session ordering proofs: Merkle".

Proposed fix

Pick one — both are scoped, neither blocks the other:

Option A — Docs (smallest, recommended for v1)

Update the paper §4.4 wording to match implementation:

"by constructing a merkle tree over aflock's per-action record log..."

And note in §4.4 (and the §7 table caption) that the proof is bound to aflock's view of the session, with #100 as the known gap. This should land alongside or inside #65 (docs alignment) so we're not documenting a moving target.

Option B — Implementation (paper-90, larger)

Extend ComputeSessionMerkleRoot to also fold the Claude session JSONL lines into the tree:

• Locate the session JSONL via ~/.claude/projects/<digest>/<session-uuid>.jsonl (already discovered by internal/usage in PR feat(usage): track JSONL tokens + cost, gated by api_key auth, with subagent rollup #127).
• Hash each JSONL line (or each turn boundary) as an additional leaf alongside ActionRecords.
• At verify time, require the JSONL to be present and re-hash it.
• This closes the conceptual gap and, partially, the security: aflock enforcement bypassable via claude-code general-purpose subagent (native Bash/Write) #100 bypass — a JSONL turn that didn't produce an aflock.Action would now leave a detectable footprint in the merkle.

Acceptance for closing this issue

• Either: paper text + §7 caption updated to describe the merkle's actual scope (Option A), or
• ComputeSessionMerkleRoot extended to include Claude JSONL leaves and verify enforces the binding (Option B).
• If A, add a follow-up tracking issue for B (or close as "by design").