ledger.adoc40.2 KBhistory comment on this file

verify

the formal-stocktake verdict ledger

This is the deliverable of the formal-stocktake exercise. Each row is one invariant claim extracted from docs/abstractions.adoc and docs/spec/*.adoc, paraphrased faithfully with key phrases quoted. Every verdict stays OPEN until the paper exercise discharges the claim against a formal model. The code is ground truth: crates/kernel/ents-gate-rules is the compiled Datalog rule set, and the encoded-in-ents-gate-rules? column classifies each claim against its seven denial rules (ff_violation, genesis_violation, second_root_violation, unsigned_violation, dangling_anchor_violation, dangling_context_violation, effect_admin_violation) and its two deliberately-marked gaps (abstraction 1’s granularity rule, abstraction 6’s monotone exactly-once effect dedup). The harness is Rust-native, and the model column names which check discharges each claim: search is crates/verify/ents-verify/src/search.rs’s exhaustive bounded search calling gate() directly; stateright is crates/verify/ents-verify’s receive.rs/effects.rs/durability.rs protocol-over-time skeletons; proptest is crates/kernel/ents-gate-rules/tests/prop.rs’s cheap sampled floor; alloy-paper marks a claim demoted to verify/alloy/*.als as a paper-only design tool, no longer run in CI; and — means no model is assigned yet. A row that turns FALSIFIED or DIVERGED lands a concrete counterexample as a test in crates/kernel/ents-gate-rules/tests/ledger.rs first, before anything else. The ledger carries 163 rows; exactly one is non-OPEN — the refname-binding claim, marked DIVERGED.

claim source model encoded-in-ents-gate-rules? verdict assumption-or-counterexample

claim	source	model	encoded-in-ents-gate-rules?	verdict	assumption-or-counterexample
A ref under `refs/meta/*` is simultaneously the unit of storage, sync, authorization, and history.	abstractions.adoc, §1 Meta-ref, ~L14-19	alloy-paper	gap-unmarked	OPEN	—
Granularity rule: one ref per independently-authored entity; entities different actors write concurrently must not share a ref; writes stay conflict-free.	abstractions.adoc, §1 Meta-ref, ~L21-23	—	gap-marked	OPEN	—
Trees stay pure struct representations — no version marker entry.	abstractions.adoc, §2 Typed tree, ~L39	alloy-paper	gap-unmarked	OPEN	—
"Refname binding needs no stored metadata at all: the refname is a total function of signed content, recomputed at verification."	abstractions.adoc, §2 Typed tree, L42 (normative twin: meta-ref.identity-binding)	search, proptest	gap-unmarked	DIVERGED	Cross-ref replay: an admin-signed parentless comment commit (anchor+context resolving) replayed as creation of refs/meta/effects/x passes genesis, unsigned, effect_admin (ff vacuous). Missing rule: binding_violation. Pinned by crates/kernel/ents-gate-rules/tests/ledger.rs; Alloy witness verify/alloy/gate_rules.als check binding_refname_recomputed.
Tip invariant: the tip of a meta-ref is always readable by the binary that owns the entity type; non-owning binary degrades to generic display, never an error (redaction is the sole qualification).	abstractions.adoc, §2 Typed tree, ~L44-45	—	gap-unmarked	OPEN	—
Retention invariant: the tree storing an anchor embeds the anchored blob plus a context blob; anchored content is reachable from `refs/meta/*` and survives force-push/branch-deletion/gc, with no gc special-casing and no pinned ancestry.	abstractions.adoc, §3 Anchor, ~L51-53	alloy-paper	dangling_anchor_violation, dangling_context_violation	OPEN	—
Gitlinks are not reachability edges and retain nothing; embedding is the only mechanism that works.	abstractions.adoc, §3 Anchor, L53	alloy-paper	gap-unmarked	OPEN	—
Redaction is the sole deliberate exception to retention.	abstractions.adoc, §3 Anchor, L54	alloy-paper	gap-unmarked	OPEN	—
Anchor data is never mutated.	abstractions.adoc, §3 Anchor, L55	alloy-paper	gap-unmarked	OPEN	—
Anchors project onto newer commits at read time via blame plus fuzzy matching; when the anchored commit is gc’d, projection degrades to context matching instead of breaking.	abstractions.adoc, §3 Anchor, L55-56	—	gap-unmarked	OPEN	—
Every meta-ref mutation is an author-signed commit.	abstractions.adoc, §4 Signed commit, L62	search, proptest	unsigned_violation	OPEN	—
The signature is a data artifact, not a transport artifact: it replicates with the repo and verifies offline in every clone, so verification evidence is itself repository state.	abstractions.adoc, §4 Signed commit, L63	search	gap-unmarked	OPEN	—
Push certificates are demoted to transport concerns; they carry no meta-ref semantics.	abstractions.adoc, §4 Signed commit, L64	search	gap-unmarked	OPEN	—
Refname binding is recomputed from the commit’s own signed content; a mismatch refuses (without this a signed commit could be replayed as the tip of a different meta-ref).	abstractions.adoc, §4 Signed commit, L69	alloy-paper	gap-unmarked	OPEN	—
Anti-replay: meta-refs advance fast-forward-only (new tip descends from old), enforced by atomic CAS; parent hash is the freshness binding, no nonce needed.	abstractions.adoc, §4 Signed commit, L70	search	ff_violation (FF part only; CAS mechanism itself not a Datalog rule)	OPEN	—
Tip invariant: the tip of a meta-ref is signed by a member authorized for that refname; checkable after the fact by anyone with a clone.	abstractions.adoc, §4 Signed commit, L72-73	search, proptest	unsigned_violation (partial: enrolled-member only, not refname-specific authorization)	OPEN	—
Adoption is always a merge, never rewrite: when author and placer differ, the authorized member merges the contributor’s commit onto the canonical ref, even trivially; the merge commit satisfies the tip invariant.	abstractions.adoc, §4 Signed commit, L75-76,78	stateright	gap-unmarked	OPEN	—
Cherry-picking is forbidden as an adoption mechanism: it creates a new commit object and destroys the author’s signature.	abstractions.adoc, §4 Signed commit, L77	stateright	gap-unmarked	OPEN	—
Same-actor divergence: two of a member’s own machines racing a single-writer ref is resolved by merging own heads, never erroring; typed trees merge schema-aware, not textually.	abstractions.adoc, §4 Signed commit, L80-81	stateright	gap-unmarked	OPEN	—
Principled split: content signatures carry authorization only where mutations are author-signed single-writer appends (granularity-guaranteed); `refs/heads/*` keeps transport-level auth instead.	abstractions.adoc, §4 Signed commit, L83-84	search	gap-unmarked	OPEN	—
Gate’s four-part verification: tip signed by authorized member; refname recomputes from signed content; new tip descends from old tip; update commits via atomic CAS.	abstractions.adoc, §5 Gate, L92-95	search	ff_violation (descent part); rest gap-unmarked	OPEN	—
Because members/refname rules live under `refs/meta/*`, policy is repository state: any frontend evaluates the actual policy offline, staleness bounded by last fetch.	abstractions.adoc, §5 Gate, L97	stateright	gap-unmarked	OPEN	—
Verification epoch: gate applies the tip invariant from an epoch recorded in `refs/meta/config`; history before is archival; epoch-setting commit is the first gated tip of the config ref.	abstractions.adoc, §5 Gate, L99-100	stateright	gap-unmarked	OPEN	—
Gate is a property of the store: hosted runs the gate at CAS time and aborts on failure (mandatory); local accepts any write and runs the gate as an annotating verdict (advisory).	abstractions.adoc, §5 Gate, L104-106	stateright	gap-unmarked	OPEN	—
The moment a verdict predicts rejection, sync offers to route the commit to the inbox instead — not only after actual rejection.	abstractions.adoc, §5 Gate, L108	stateright	gap-unmarked	OPEN	—
One function, three call sites: hosted CAS, local UI verdict, push pre-flight.	abstractions.adoc, §5 Gate, L110	stateright	gap-unmarked	OPEN	—
A verdict is never a bare pass/fail: on failure it carries which rule failed and for which refname.	abstractions.adoc, §5 Gate, L111	—	gap-unmarked	OPEN	—
Local web UI signs as the user with the user’s own member key; server-key signing is a hosted-only necessity, must not be imported locally.	abstractions.adoc, §5 Gate, L114-115	—	gap-unmarked	OPEN	—
Results location is derived by convention; an effect cannot choose where its verdicts land.	abstractions.adoc, §6 Effect, L132	alloy-paper	gap-unmarked	OPEN	—
Trigger semantics: the trigger denotes a set of commits; the effect fires once per commit that enters the set.	abstractions.adoc, §6 Effect, L134	stateright	gap-marked	OPEN	—
Meta-refs are outside `rev()’s domain by definition.	abstractions.adoc, §6 Effect, L138	stateright	gap-unmarked	OPEN	—
`meta(glob)` can never match effect-written namespaces (`refs/meta/results/`, `refs/meta/index/`); those are reachable only through `results(…)`.	abstractions.adoc, §6 Effect, L140-141	stateright	gap-unmarked	OPEN	—
`RefPattern` survives as the degenerate query `rev(<glob>)`; nothing shipped changes meaning.	abstractions.adoc, §6 Effect, L144	stateright	gap-unmarked	OPEN	—
Monotone, entry-only: a force-push can shrink a set, but a commit leaving the set retracts nothing — results are immutable history.	abstractions.adoc, §6 Effect, L147	stateright	gap-marked	OPEN	—
No pipeline state: the work set is `trigger − results(self, any)` — the results ref is the sole materialization marker.	abstractions.adoc, §6 Effect, L150	stateright	gap-marked	OPEN	—
Dedup key `(effect, oid)` over an at-least-once queue yields exactly-once outcomes with zero state outside the repository.	abstractions.adoc, §6 Effect, L151	stateright	gap-marked	OPEN	—
Result taxonomy: a result is `pass`, `fail`, or `error`; exit status is always a result.	abstractions.adoc, §6 Effect, L153-154	stateright	gap-unmarked	OPEN	—
Infrastructure failure is not a result; only retry exhaustion writes a terminal `error`, signed by the worker’s key like any other.	abstractions.adoc, §6 Effect, L155	stateright	gap-unmarked	OPEN	—
Retry bounds are deployment configuration, never effect data.	abstractions.adoc, §6 Effect, L156	alloy-paper	gap-unmarked	OPEN	—
A transient outage can neither retry forever nor permanently discharge an obligation.	abstractions.adoc, §6 Effect, L157	stateright	gap-unmarked	OPEN	—
Recursion is structure: downstream-of-effects is syntactically visible; because `rev()`/`meta()` cannot name an effect-written ref, an accidental fork bomb is unreachable by construction.	abstractions.adoc, §6 Effect, L159-160	stateright	gap-unmarked	OPEN	—
`post-receive` remains a dumb matcher: ref footprint is statically extractable; set entry computed incrementally from `old..new`, bounded by generation numbers.	abstractions.adoc, §6 Effect, L165-166	stateright	gap-unmarked	OPEN	—
Pushes are never blocked; the durable enqueue is the entire synchronous cost.	abstractions.adoc, §6 Effect, L167	stateright	gap-unmarked	OPEN	—
A worker dequeues, materializes toolchains, executes in a sandbox; host-direct requires explicit `--unsandboxed`.	abstractions.adoc, §6 Effect, L168-169	—	gap-unmarked	OPEN	—
Results return only as signed commits pushed to one ref per tested commit (`refs/meta/results/<effect>/<short-oid>`), so concurrent results never conflict.	abstractions.adoc, §6 Effect, L170	alloy-paper	gap-marked	OPEN	—
Identity discipline: the runner is a member, not an ambient authority; official results are official only because canonical refs are writable solely by designated worker keys.	abstractions.adoc, §6 Effect, L172-173	alloy-paper	gap-unmarked	OPEN	—
Any member may self-run any effect; results land in `refs/meta/self/<member>/*` or the inbox, adoptable by merge with the trust decision explicit.	abstractions.adoc, §6 Effect, L174	alloy-paper	gap-unmarked	OPEN	—
No content predicates beyond `results(…, status)`, no time atoms, no external-event atoms.	abstractions.adoc, §6 Effect, L177	stateright	gap-unmarked	OPEN	—
Admin-only write rule on `refs/meta/effects/*` bounds who can schedule execution on canonical infrastructure.	abstractions.adoc, §6 Effect, L181	search, proptest	effect_admin_violation	OPEN	—
Abstractions 4/5/6 close: all state changes, human or machine, flow through one verified, audited channel; the repository is the message bus.	abstractions.adoc, "The loop", L188-189	stateright	gap-unmarked	OPEN	—
No code knows where it is running; an `if hosted` branch inside the library is the design failing.	abstractions.adoc, "Composition", L196-197	—	gap-unmarked	OPEN	—
Crates that extend git carry the `gix-` prefix, import nothing from the forge, and stay upstream-shaped by construction.	abstractions.adoc, "Composition", L209-210	—	gap-unmarked	OPEN	—
The unit the library exposes is `receive(refs, objects, events, proposal)`: gate evaluation, effect matching, enqueue live inside it.	abstractions.adoc, "Composition", L213	stateright	gap-unmarked	OPEN	—
Local and hosted do not share a push path; they share `receive`, with only trait impls swapped — the correctness anchor for writes.	abstractions.adoc, "Composition", L215-216	stateright	gap-unmarked	OPEN	—
Dependencies point one way; a lower layer never depends on a higher one, checked mechanically.	abstractions.adoc, "Layering", L238	—	gap-unmarked	OPEN	—
A package depends on kernel crates freely and on other packages never (`ents-forge`/`ents-kiln` never depend on each other).	abstractions.adoc, "Layering", L247	—	gap-unmarked	OPEN	—
`ents-web’s generic rendering path must never match on which concrete entity type it was handed.	abstractions.adoc, "Layering", L252-253	—	gap-unmarked	OPEN	—
`ents-web` never depends back on `git-ents`.	abstractions.adoc, "Layering", L254	—	gap-unmarked	OPEN	—
A kernel crate must not depend on a package crate in any form (normal, dev, build, or feature-flagged).	abstractions.adoc, "Layering", L256	—	gap-unmarked	OPEN	—
`ents-testutil` must not know a package’s types.	abstractions.adoc, "Layering", L257	—	gap-unmarked	OPEN	—
Every ref namespace is minted by one function in `ents_model::namespace`; a package calls that function rather than inventing its own layout.	abstractions.adoc, "Layering", L259	alloy-paper	gap-unmarked	OPEN	—
Fanout index: a stale or absent index degrades to scanning ref tips, never to wrong answers.	abstractions.adoc, "Derived", L280	stateright	gap-unmarked	OPEN	—
Redacted bytes are withheld from the store and generated packs; the oid stays in history as evidence; signatures and the tip invariant are untouched because verification never reads withheld bytes.	abstractions.adoc, "Derived", L282	alloy-paper	gap-unmarked	OPEN	—
Redaction is enforced at ingest so content addressing cannot let anyone refill the hole exactly.	abstractions.adoc, "Derived", L283	stateright	gap-unmarked	OPEN	—
Readers surface a redaction marker, never an error.	abstractions.adoc, "Derived", L284	alloy-paper	gap-unmarked	OPEN	—
Embeddable server: keeping authorization/effect-matching logic in the library, never smeared across subprocess boundaries.	abstractions.adoc, "Derived", L289-290	—	gap-unmarked	OPEN	—
`git effect run` shares the identical materialization and sandbox path with the hosted worker.	abstractions.adoc, "Command surface", L324	stateright	gap-unmarked	OPEN	—
Every mutation frontend shares the identical `receive` with the hosted server.	abstractions.adoc, "Command surface", L324	stateright	gap-unmarked	OPEN	—
Revocation is a state on the member entity, not deletion; a revoked key must be explicitly rejected.	abstractions.adoc, "Command surface", L341	stateright	gap-unmarked	OPEN	—
Pushes to `refs/meta/*` never touch the working tree, so metadata behaves identically in both deployment modes.	abstractions.adoc, "Deployment", L363	—	gap-unmarked	OPEN	—
Worktree update happens only after `receive` accepts; core never touches a worktree.	abstractions.adoc, "Deployment", L361	—	gap-unmarked	OPEN	—
Bootstrap gap: an empty member list admits every push so the first member can enroll.	abstractions.adoc, "Deployment", L365	stateright	gap-unmarked	OPEN	—
An anchor MUST identify the exact content it was captured against (commit, path, blob oid, optional 1-based inclusive range); creation MUST validate path and range against the revision’s actual content.	docs/spec/anchor.adoc, [#anchor.definition], ~L9-17	alloy-paper	gap-unmarked	OPEN	—
Anchored text MUST be fully derivable from the blob and line range, derived at read time, never stored redundantly; the anchored commit’s id is recorded only as a plain data field, and MAY be gc’d.	docs/spec/anchor.adoc, [#anchor.immutable], ~L19-28	alloy-paper	gap-unmarked	OPEN	—
The anchoring document MUST embed the anchored blob "referenced by the existing blob’s own object id rather than copied" plus a context blob "written fresh", as ordinary tree entries, keeping content reachable "for as long as the document’s ref exists".	docs/spec/anchor.adoc, [#anchor.retention], ~L30-45	alloy-paper	dangling_anchor_violation, dangling_context_violation	OPEN	—
Projection MUST report one of exactly four outcomes (current/relocated/outdated/deleted), MUST follow renames, and MUST work between any two commits — forwards, backwards, or across unrelated history — while the anchor’s own commit exists.	docs/spec/anchor.adoc, [#anchor.projection], ~L48-61	—	gap-unmarked	OPEN	—
After the anchored commit is gc’d, fuzzy fallback recovers the same four outcomes approximately; "an outdated or deleted projection MUST NOT lose the anchor".	docs/spec/anchor.adoc, [#anchor.fuzzy-fallback], ~L63-74	—	gap-unmarked	OPEN	—
A working-tree anchor survives its content being "committed, amended, or discarded"; it records HEAD only as a "best-effort, never-load-bearing" field; projection MUST support the working tree as target.	docs/spec/anchor.adoc, [#anchor.working-tree], ~L76-93	alloy-paper	gap-unmarked	OPEN	—
An effect definition MUST be rejected before storage when a toolchain name is not a valid ref-path segment or the trigger fails to parse (including `rev()` naming `refs/meta/*` or `meta()` naming an effect-written namespace).	docs/spec/effect.adoc, [#effect.validation], ~L41-50	search	gap-unmarked	OPEN	—
Host-direct execution MUST require an explicit `--unsandboxed` flag and MUST be "available only locally, never on canonical hosted infrastructure".	docs/spec/effect.adoc, [#effect.execution], ~L54-68	—	gap-unmarked	OPEN	—
An effect’s stored data MUST NOT select its own executor, demand `--unsandboxed`, or set retry bounds; those are deployment configuration, "never a field an effect definition can carry".	docs/spec/effect.adoc, [#effect.deployment-property], ~L70-78	—	gap-unmarked	OPEN	—
A member running `git effect run` locally MUST see "the same outcome a canonical worker would record"; only the queue is skipped, and the queue carries no correctness content.	docs/spec/effect.adoc, [#effect.local-run], ~L80-89	stateright	gap-unmarked	OPEN	—
Result write-back MUST be "an ordinary receive client, never a privileged write outside the gate".	docs/spec/effect.adoc, [#effect.results-writeback], ~L93-106	stateright	gap-unmarked	OPEN	—
Only the sandbox MAY touch a toolchain’s extracted bytes; declared components MUST be resolved during effect execution, "never by any other code path".	docs/spec/effect.adoc, [#effect.toolchains], ~L161-168	—	gap-unmarked	OPEN	—
A fanout index MUST be rebuilt only by an effect and written back only as a worker-signed commit, "never by any privileged out-of-band writer".	docs/spec/effect.adoc, [#effect.fanout-index], ~L174-184	stateright	gap-unmarked	OPEN	—
Verification MUST depend only on the read half of the RefStore seam, never on write access or on any state outside `refs/meta/*`.	docs/spec/gate.adoc, intro (also [#arch.refstore-read-cas-split]), ~L3-5	search	gap-unmarked	OPEN	—
Authorization is judged against the member entity in force at acceptance time — the member ref’s tip in the same snapshot the gate reads.	docs/spec/gate.adoc, [#gate.tip-signed], ~L12-23	stateright	unsigned_violation (partial: enrolled-membership only, not snapshot-scoped refname authorization)	OPEN	—
A gate-owned hash-identified entity’s creation MUST strictly decode as its type, an unknown tree entry refusing; the gate-owned entity structs MUST stay pairwise disjoint under this decode.	docs/spec/gate.adoc, [#gate.identity-binding], ~L36-40	alloy-paper	gap-unmarked	OPEN	—
When an object the binding needs is withheld by redaction, the binding MUST be vouched by the admin-signed redaction record, and a redacted object MUST NOT be re-admitted.	docs/spec/gate.adoc, [#gate.identity-binding], ~L47-51	stateright	gap-unmarked	OPEN	—
Advancing a hash-identified entity’s ref is authorized only for the genesis signer or an admin; a review ref advances only under the signature of the member its refname names.	docs/spec/gate.adoc, [#gate.owner-mutation], ~L54-67	search	gap-unmarked	OPEN	—
A pre-flight verdict "is a prediction that can only go stale; it MUST NOT diverge from the rules the hosted store will actually apply".	docs/spec/gate.adoc, [#gate.call-sites], ~L188-196	stateright	gap-unmarked	OPEN	—
Transport-auth evidence MUST be threaded through uninterpreted — "never substituted for the tip invariant on a `refs/meta/` update"; no advisory call site MAY render a `refs/heads/` verdict meanwhile.	docs/spec/gate.adoc, [#gate.branch-acl-undefined], ~L267-284	stateright	gap-unmarked	OPEN	—
With no `refs/meta/member/*` ref, first enrollment is self-admitting; but a member set whose keys are all revoked "MUST fail closed: revoking every key MUST NOT reopen this self-admitting window".	docs/spec/gate.adoc, [#gate.bootstrap], ~L288-296	stateright	gap-unmarked	OPEN	—
`git ents lsp` MUST NOT bind a network socket, MUST NOT add a git-serving transport, and MUST receive its signing identity by injection from the composition root.	docs/spec/lens.adoc, [#lens.serve], ~L13-24	—	gap-unmarked	OPEN	—
Lens ranges are derived at request time via projection and "never cached across mutations of the comment’s ref"; non-`open` comments omitted unless asked.	docs/spec/lens.adoc, [#lens.lenses], ~L26-39	—	gap-unmarked	OPEN	—
Comment diagnostics "MUST NEVER use warning or error severity" and MUST be suppressible without affecting the lenses.	docs/spec/lens.adoc, [#lens.diagnostics], ~L41-50	—	gap-unmarked	OPEN	—
Composing MUST require no client-specific extension; a richer input surface "MUST be sugar over the same create operation, never a second mechanism".	docs/spec/lens.adoc, [#lens.compose], ~L61-75	—	gap-unmarked	OPEN	—
Editor-composed comments MUST anchor to the working tree’s content when it differs from HEAD — "exactly the bytes the author was reading".	docs/spec/lens.adoc, [#lens.working-tree], ~L77-87	alloy-paper	gap-unmarked	OPEN	—
Every lens operation MUST be the same library call the `git ents comment` porcelain exposes; the CLI listing MUST offer a machine-readable form sufficient for an agent with no editor attached.	docs/spec/lens.adoc, [#lens.parity], ~L89-101	—	gap-unmarked	OPEN	—
All forge state MUST live under `refs/meta/`; retention pins under `refs/meta/pins/` are "the sole exception" to tree-is-the-entity, carrying the empty tree, never an entity.	docs/spec/meta-ref.adoc, [#meta-ref.namespace], ~L15-27	alloy-paper	gap-unmarked	OPEN	—
Inbox routing preserves the canonical ref’s entire path below `refs/meta/` so "two different entity kinds can never collide under the same inbox id"; `<member>` is the leading segment so authorization keys off the refname alone.	docs/spec/meta-ref.adoc, [#meta-ref.inbox], ~L45-61	alloy-paper	gap-unmarked	OPEN	—
A member is authorized only for its own `refs/meta/inbox/<member>/*` segment; "no member, including an admin-registered one, MAY write into another member’s inbox segment".	docs/spec/meta-ref.adoc, [#meta-ref.inbox], ~L62-68	search	gap-unmarked	OPEN	—
An inbox ref MUST NOT be deleted on adoption or at any other time — it remains the contributor’s audit trail.	docs/spec/meta-ref.adoc, [#meta-ref.inbox], ~L69-71	stateright	gap-unmarked	OPEN	—
`self` is its own top-level namespace, keeping the canonical results glob and the self-run glob "disjoint by construction"; both namespaces hold the same typed trees as canonical, only the refname rule differs.	docs/spec/meta-ref.adoc, [#meta-ref.inbox], ~L72-85	alloy-paper	gap-unmarked	OPEN	—
For a hash-identified entity, "every parentless commit reachable from the proposed tip MUST be that genesis" — the reachability form makes doppelgänger replay impossible and holds across divergence merges.	docs/spec/meta-ref.adoc, [#meta-ref.identity-binding], ~L117-124	alloy-paper	genesis_violation, second_root_violation	OPEN	—
The parentless-roots walk MUST NOT be applied to pins: a pin’s ancestry deliberately reaches into code history.	docs/spec/meta-ref.adoc, [#meta-ref.identity-binding], ~L132-135	alloy-paper	gap-unmarked	OPEN	—
Who authored a state, and when, MUST come from the commit itself, never from duplicated tree fields: "each datum has exactly one signed home".	docs/spec/meta-ref.adoc, [#meta-ref.identity-binding], ~L144-147	alloy-paper	gap-unmarked	OPEN	—
Within a meta-ref’s history a commit parent means exactly one thing — the prior state of the same entity (pin retained-commit parents sole exception); a cross-entity relationship MUST be tree data, never a parent edge.	docs/spec/meta-ref.adoc, [#meta-ref.identity-binding], ~L147-150	alloy-paper	gap-unmarked	OPEN	—
A genesis commit is frozen by the identity derived from it, so hash-identified/composite-keyed structs MUST evolve additively only — "new fields optional, required fields never added, renamed, or removed".	docs/spec/meta-ref.adoc, [#meta-ref.identity-binding], ~L149-153	alloy-paper	gap-unmarked	OPEN	—
A struct change is a migration committed on top of the old tip; history keeps the old encoding, and a struct change "MUST NOT rewrite or delete a prior commit on the ref".	docs/spec/meta-ref.adoc, [#meta-ref.migration], ~L172-180	alloy-paper	gap-unmarked	OPEN	—
The gate and `receive` are content-agnostic: verification depends on "signature, refname, trailer, and DAG descent, never on tree contents", so a stock server MUST carry entity types it cannot parse.	docs/spec/model.adoc, [#model.extensibility], ~L8-22	search	gap-unmarked	OPEN	—
A facet shape MUST be compile-time-defined: runtime-readable, never runtime-constructible.	docs/spec/model.adoc, [#model.extensibility], ~L13-15	—	gap-unmarked	OPEN	—
A member’s id binds to its key-carrying entity’s refname final segment; enrollment occurs as a signed commit — the member is forge state "with no user database separate from the repository".	docs/spec/model.adoc, [#model.member-identity], ~L31-40	alloy-paper	gap-unmarked	OPEN	—
Admission consults the member entity currently in force, so a revoked key’s new pushes are refused "from the moment the revocation lands, regardless of any committer timestamp the pushed commit claims".	docs/spec/model.adoc, [#model.member-revocation], ~L47-50	stateright	gap-unmarked	OPEN	—
A ref accepted before the revocation landed remains valid: "acceptance is never re-judged".	docs/spec/model.adoc, [#model.member-revocation], ~L51-52	stateright	gap-unmarked	OPEN	—
Unrevoking returns the key to authorizing new signatures "without altering the record of the period it was revoked".	docs/spec/model.adoc, [#model.member-revocation], ~L60-61	stateright	gap-unmarked	OPEN	—
A self-attested member MUST NOT be authorized for canonical refs — writes limited to its own inbox and self-run namespaces — until an admin-registered member promotes it.	docs/spec/model.adoc, [#model.member-provenance], ~L64-75	search	gap-unmarked (effect_admin_violation covers only the effects namespace, not the provenance tier generally)	OPEN	—
A machine actor is an ordinary Member entity, revocable like any human key; "a privileged write path for a machine actor MUST NOT exist outside this model".	docs/spec/model.adoc, [#model.member-worker], ~L77-86	stateright	gap-unmarked	OPEN	—
A comment’s identity is the oid of its genesis commit and "MUST NEVER change afterward: edits advance the ref, they do not rename it".	docs/spec/model.adoc, [#model.comment], ~L99-102	alloy-paper	gap-unmarked	OPEN	—
A comment about nothing MUST be refused at creation by the writing tool, "though never by the gate, which stays content-agnostic".	docs/spec/model.adoc, [#model.comment], ~L93-98	—	gap-unmarked	OPEN	—
A new comment’s state is `open`; resolving records `resolved` as an ordinary mutation commit — "never a deletion, so the conversation stays auditable" — and reopening is supported the same way.	docs/spec/model.adoc, [#model.comment-state], ~L109-121	—	gap-unmarked	OPEN	—
A state-changing mutation by an enrolled key MUST carry a `Key-for-<member-id>` trailer whose value is the member ref’s tip oid at mutation time, pinning the enrolled record across later rotation or revocation.	docs/spec/model.adoc, [#model.comment-provenance], ~L123-129	—	gap-unmarked	OPEN	—
An entity’s thread MUST be an aggregation query over comment refs; a context entity MUST NOT store its comment list, so concurrent commenters "never race a shared ref".	docs/spec/model.adoc, [#model.comment-context], ~L132-142	alloy-paper	gap-marked (instance of abstraction 1’s granularity rule)	OPEN	—
A reply’s parent MUST exist when the reply is created; aboutness is inherited from the thread root; no comment stores a list of its replies.	docs/spec/model.adoc, [#model.comment-thread], ~L144-154	alloy-paper	gap-unmarked	OPEN	—
An issue’s identity is its genesis oid — no sequential counter exists — and machine-readable output (including `--porcelain`) MUST carry the full id.	docs/spec/model.adoc, [#model.issue], ~L158-177	alloy-paper	gap-unmarked	OPEN	—
A review binds by composite key `reviews/<target>/<member>`; at genesis the reviewed-commit tree field equals the `<target>` segment and binds it; re-reviewing advances the field while the refname stays keyed by genesis.	docs/spec/model.adoc, [#model.review], ~L181-198	alloy-paper	gap-unmarked	OPEN	—
Every review MUST occupy exactly two refs: the entity ref and its retention pin.	docs/spec/model.adoc, [#model.review], ~L191-193	alloy-paper	gap-unmarked	OPEN	—
A review’s verdict MUST be a hard enum — `approve`, `request-changes`, or `comment`: "a verdict gates decisions, so its vocabulary is platform, not schema".	docs/spec/model.adoc, [#model.review], ~L199-202	—	gap-unmarked	OPEN	—
A pin’s tip is a reviewer-signed commit whose parents include the reviewed commit, so that commit and its ancestry "survive force-push, branch deletion, and gc for as long as the review exists".	docs/spec/model.adoc, [#model.review-pin], ~L213-224	alloy-paper	gap-unmarked	OPEN	—
Re-reviewing MUST advance the pin fast-forward with parents = previous pin tip + newly reviewed commit, so every reviewed round stays retained and the pin’s history is the audit trail.	docs/spec/model.adoc, [#model.review-pin], ~L225-229	alloy-paper	gap-unmarked	OPEN	—
A result MUST carry the effect’s name and the judged commit’s full oid as tree fields from which the refname derives — "a result MUST mean something with the refname stripped away" (a signed `pass` cannot be replayed against another effect/commit).	docs/spec/model.adoc, [#model.result-identity], ~L260-270	alloy-paper	gap-unmarked	OPEN	—
Result fields are not parent edges: a result ref’s parents stay prior states of the same result, and a result MUST NOT retain the judged commit’s ancestry the way a pin does.	docs/spec/model.adoc, [#model.result-identity], ~L271-274	alloy-paper	gap-unmarked	OPEN	—
A toolchain is a hash-pinned ~1KB manifest carrying its own provenance, "a resource an effect declares as a dependency … never a trigger condition in its own right".	docs/spec/model.adoc, [#model.toolchain], ~L279-289	—	gap-unmarked	OPEN	—
A Redaction entity carries the target oid, a reason, and the admin signature; it "MUST NOT carry the redacted content itself".	docs/spec/model.adoc, [#model.redaction], ~L294-300	alloy-paper	gap-unmarked	OPEN	—
Authentication state MUST live in the repository as ordinary forge state; "a session database or token table MUST NOT back it".	docs/spec/model.adoc, [#model.account], ~L308-313	—	gap-unmarked	OPEN	—
The library MUST NOT define its own ObjectStore trait — gitoxide’s `Find`/`Exists`/`Write` ARE the seam; a new trait exists only where gitoxide is silent.	docs/spec/overview.adoc, [#arch.no-object-store-trait], ~L180-189	—	gap-unmarked	OPEN	—
The gate’s pure verify function MUST live in a crate separate from `receive`; advisory call sites MUST be answerable without linking effect-matching and enqueue logic.	docs/spec/overview.adoc, [#arch.gate-receive-split], ~L191-199	—	gap-unmarked	OPEN	—
The query algebra MUST live apart from executor code; `receive` MUST NOT depend on the effect crate, "so no push path links executor code".	docs/spec/overview.adoc, [#arch.query-effect-split], ~L201-208	—	gap-unmarked	OPEN	—
A concrete store implementation is wired only inside a composition root, never a library crate, and is not promoted to a shared library crate until a second root consumes it.	docs/spec/overview.adoc, [#arch.store-composition-root], ~L211-219	—	gap-unmarked	OPEN	—
A loose-ref RefStore MUST write refs through its own CAS discipline and MUST NOT shell out to `git update-ref`, so local mutations honor the same CAS guarantee as hosted.	docs/spec/overview.adoc, [#arch.loose-cas-discipline], ~L239-245	stateright	gap-unmarked	OPEN	—
A CommitQuery MUST parse per the fixed grammar; `\|`/`&`/`-` denote union/intersection/difference, left-associative at a single precedence level, parentheses the only override.	docs/spec/query.adoc, [#query.grammar] (+ [#query.set-ops]), ~L12-35	stateright	gap-unmarked	OPEN	—
Unsupported rev syntax (`~n`/`^n`, `A…B`, `@{…}`, abbreviated hex) and any `refs/meta/*` pattern MUST be rejected as malformed — "never silently evaluated to the empty set or to the wrong set".	docs/spec/query.adoc, [#query.rev], ~L39-58	stateright	gap-unmarked	OPEN	—
Membership in `results(effect, status)` is decided solely by existence of a matching results ref — never by reachability from `refs/heads/*` or any ref outside the query’s footprint — and resolution is a refname scan, never a history walk.	docs/spec/query.adoc, [#query.results], ~L61-79	stateright	gap-unmarked	OPEN	—
The fanout index "MUST NOT be addressable by any query atom at all".	docs/spec/query.adoc, [#query.meta], ~L82-91	stateright	gap-unmarked	OPEN	—
`self` in the work set is evaluation-time notation, "not a keyword an author may write in a trigger"; work-set evaluation inherits incremental bounds and refname-scan resolution, never a full-history walk.	docs/spec/query.adoc, [#query.workset], ~L159-173	stateright	gap-marked (work-set/dedup materialization is the declared cross-transaction gap)	OPEN	—
Replicating refs a trusted remote already admitted MAY apply directly (re-verification on fetch is opt-in audit); commits the replicating machinery authors itself — divergence and adoption merges — are origination, not replication.	docs/spec/receive.adoc, [#receive.unit], ~L10-27	stateright	gap-unmarked	OPEN	—
Gate evaluation MUST be checkable against exactly the proposal shape, frontend-independent; meta-ref admission "MUST ignore [transport-auth evidence] entirely and MUST NOT consult it in place of the tip invariant".	docs/spec/receive.adoc, [#receive.proposal-shape], ~L29-47	stateright	gap-unmarked	OPEN	—
An entity declared across multiple refs MUST write them in a single Proposal through one `receive` call; the atomic multi-ref CAS admits or refuses the whole batch, "so such an entity is never observable with only some of its refs written".	docs/spec/receive.adoc, [#receive.multi-ref-atomicity], ~L49-66	stateright	gap-unmarked	OPEN	—
A `receive` inside a git hook reads existing state through the common object directory, never git’s quarantine directory: quarantined objects "MUST NOT be treated as stored until the transaction commits".	docs/spec/receive.adoc, [#receive.object-access], ~L93-105	stateright	gap-unmarked	OPEN	—
Pending obligations MUST be derivable from repository state alone; an EventSink MAY lose events on crash provided the root reconciles at startup before serving pushes; "a durable queue MUST be treated as a performance optimization, never a correctness requirement".	docs/spec/receive.adoc, [#receive.reconstructible], ~L134-146	stateright	gap-marked (cross-transaction queue/materialization state is the declared dedup gap)	OPEN	—
A push to `refs/meta/redactions/*` MUST be rejected unless the member is admin-registered, regardless of any other role rule, statable as a single refname glob.	docs/spec/receive.adoc, [#receive.redaction-admin-only], ~L148-158	search	gap-unmarked (effect_admin_violation covers only `refs/meta/effects/*`; no redactions-namespace rule exists)	OPEN	—
The local root wires loose refs, the odb, Docker, null EventSink, and the advisory gate; `git ents serve` MUST NOT expose git’s smart-HTTP wire protocol; local effect execution is pull, "never a daemon watching refs".	docs/spec/roots.adoc, [#roots.local], ~L20-32	—	gap-unmarked	OPEN	—
The single-node hosted root’s hooks call the gate and reconcile around receive-pack’s own ref update, "never through this crate’s own `RefStore::transaction, to avoid a double-write race".	docs/spec/roots.adoc, [#roots.single-node-hosted], ~L34-52	stateright	gap-unmarked	OPEN	—
The worker MUST NOT share in-process state with `receive`.	docs/spec/roots.adoc, [#roots.hosted], ~L55-63	stateright	gap-unmarked	OPEN	—
Wiring the scale-out root (Postgres/Tigris/durable queue) MUST require zero modification to any library crate — the seam design’s honesty test, proven by an actual production migration.	docs/spec/roots.adoc, [#roots.honesty-test], ~L66-75	—	gap-unmarked	OPEN	—
Configuration selects trait implementations only at the composition root and MUST NOT leak past it.	docs/spec/roots.adoc, [#roots.config-isolation], ~L78-83	—	gap-unmarked	OPEN	—
`ents-web` receives its signing identity by injection and MUST NOT assume a network; in-process webview embedding remains a supported deployment.	docs/spec/roots.adoc, [#roots.web-agnostic], ~L96-103	—	gap-unmarked	OPEN	—
A hosted web session is held only in server memory; every state-changing request carries a per-session CSRF token verified before acting; a web edit is signed only on behalf of an authenticated session.	docs/spec/roots.adoc, [#roots.web-session], ~L141-148	—	gap-unmarked	OPEN	—
Every repository-path segment MUST be validated before filesystem or subprocess use, rejecting escapes, nesting inside an existing repository, or namespace-directory collisions.	docs/spec/roots.adoc, [#roots.path-validation], ~L151-158	—	gap-unmarked	OPEN	—
Fetch authorization MUST be refname-keyed, using the same authorization model as write authorization.	docs/spec/roots.adoc, [#roots.fetch-auth], ~L160-167	search	gap-unmarked	OPEN	—
A clone plus `refs/meta/*` MUST carry the complete audit history and the signatures needed to verify it, "with no server-side data left behind".	docs/spec/sync.adoc, [#sync.forge-transfer], ~L9-16	alloy-paper	gap-unmarked	OPEN	—
Inbox adoption and self-run adoption MUST both go through the same merge machinery as divergence resolution, "not a separate adoption code path".	docs/spec/sync.adoc, [#sync.adoption-machinery], ~L50-57	stateright	gap-unmarked	OPEN	—
"Nothing in the resulting ref-store state lets a pure verifier tell" a cherry-picked adoption from a hand-authored commit — attribution preservation binds the merge machinery, never the gate.	docs/spec/sync.adoc, [#sync.adoption-no-cherry-pick] (also gate.adoc Adoption intro ~L218-224), ~L59-73	stateright	gap-unmarked	OPEN	—

A ref under refs/meta/* is simultaneously the unit of storage, sync, authorization, and history.

abstractions.adoc, §1 Meta-ref, ~L14-19

alloy-paper

gap-unmarked

OPEN

—

Granularity rule: one ref per independently-authored entity; entities different actors write concurrently must not share a ref; writes stay conflict-free.

abstractions.adoc, §1 Meta-ref, ~L21-23

—

gap-marked

OPEN

—

Trees stay pure struct representations — no version marker entry.

abstractions.adoc, §2 Typed tree, ~L39

alloy-paper

gap-unmarked

OPEN

—

"Refname binding needs no stored metadata at all: the refname is a total function of signed content, recomputed at verification."

abstractions.adoc, §2 Typed tree, L42 (normative twin: meta-ref.identity-binding)

search, proptest

gap-unmarked

DIVERGED

Cross-ref replay: an admin-signed parentless comment commit (anchor+context resolving) replayed as creation of refs/meta/effects/x passes genesis, unsigned, effect_admin (ff vacuous). Missing rule: binding_violation. Pinned by crates/kernel/ents-gate-rules/tests/ledger.rs; Alloy witness verify/alloy/gate_rules.als check binding_refname_recomputed.

Tip invariant: the tip of a meta-ref is always readable by the binary that owns the entity type; non-owning binary degrades to generic display, never an error (redaction is the sole qualification).

abstractions.adoc, §2 Typed tree, ~L44-45

—

gap-unmarked

OPEN

—

Retention invariant: the tree storing an anchor embeds the anchored blob plus a context blob; anchored content is reachable from refs/meta/* and survives force-push/branch-deletion/gc, with no gc special-casing and no pinned ancestry.

abstractions.adoc, §3 Anchor, ~L51-53

alloy-paper

dangling_anchor_violation, dangling_context_violation

OPEN

—

Gitlinks are not reachability edges and retain nothing; embedding is the only mechanism that works.

abstractions.adoc, §3 Anchor, L53

alloy-paper

gap-unmarked

OPEN

—

Redaction is the sole deliberate exception to retention.

abstractions.adoc, §3 Anchor, L54

alloy-paper

gap-unmarked

OPEN

—

Anchor data is never mutated.

abstractions.adoc, §3 Anchor, L55

alloy-paper

gap-unmarked

OPEN

—

Anchors project onto newer commits at read time via blame plus fuzzy matching; when the anchored commit is gc’d, projection degrades to context matching instead of breaking.

abstractions.adoc, §3 Anchor, L55-56

—

gap-unmarked

OPEN

—

Every meta-ref mutation is an author-signed commit.

abstractions.adoc, §4 Signed commit, L62

search, proptest

unsigned_violation

OPEN

—

The signature is a data artifact, not a transport artifact: it replicates with the repo and verifies offline in every clone, so verification evidence is itself repository state.

abstractions.adoc, §4 Signed commit, L63

gap-unmarked

OPEN

—

Push certificates are demoted to transport concerns; they carry no meta-ref semantics.

abstractions.adoc, §4 Signed commit, L64

gap-unmarked

OPEN

—

Refname binding is recomputed from the commit’s own signed content; a mismatch refuses (without this a signed commit could be replayed as the tip of a different meta-ref).

abstractions.adoc, §4 Signed commit, L69

alloy-paper

gap-unmarked

OPEN

—

Anti-replay: meta-refs advance fast-forward-only (new tip descends from old), enforced by atomic CAS; parent hash is the freshness binding, no nonce needed.

abstractions.adoc, §4 Signed commit, L70

ff_violation (FF part only; CAS mechanism itself not a Datalog rule)

OPEN

—

Tip invariant: the tip of a meta-ref is signed by a member authorized for that refname; checkable after the fact by anyone with a clone.

abstractions.adoc, §4 Signed commit, L72-73

search, proptest

unsigned_violation (partial: enrolled-member only, not refname-specific authorization)

OPEN

—

Adoption is always a merge, never rewrite: when author and placer differ, the authorized member merges the contributor’s commit onto the canonical ref, even trivially; the merge commit satisfies the tip invariant.

abstractions.adoc, §4 Signed commit, L75-76,78

stateright

gap-unmarked

OPEN

—

Cherry-picking is forbidden as an adoption mechanism: it creates a new commit object and destroys the author’s signature.

abstractions.adoc, §4 Signed commit, L77

stateright

gap-unmarked

OPEN

—

Same-actor divergence: two of a member’s own machines racing a single-writer ref is resolved by merging own heads, never erroring; typed trees merge schema-aware, not textually.

abstractions.adoc, §4 Signed commit, L80-81

stateright

gap-unmarked

OPEN

—

Principled split: content signatures carry authorization only where mutations are author-signed single-writer appends (granularity-guaranteed); refs/heads/* keeps transport-level auth instead.

abstractions.adoc, §4 Signed commit, L83-84

gap-unmarked

OPEN

—

Gate’s four-part verification: tip signed by authorized member; refname recomputes from signed content; new tip descends from old tip; update commits via atomic CAS.

abstractions.adoc, §5 Gate, L92-95

ff_violation (descent part); rest gap-unmarked

OPEN

—

Because members/refname rules live under refs/meta/*, policy is repository state: any frontend evaluates the actual policy offline, staleness bounded by last fetch.

abstractions.adoc, §5 Gate, L97

stateright

gap-unmarked

OPEN

—

Verification epoch: gate applies the tip invariant from an epoch recorded in refs/meta/config; history before is archival; epoch-setting commit is the first gated tip of the config ref.

abstractions.adoc, §5 Gate, L99-100

stateright

gap-unmarked

OPEN

—

Gate is a property of the store: hosted runs the gate at CAS time and aborts on failure (mandatory); local accepts any write and runs the gate as an annotating verdict (advisory).

abstractions.adoc, §5 Gate, L104-106

stateright

gap-unmarked

OPEN

—

The moment a verdict predicts rejection, sync offers to route the commit to the inbox instead — not only after actual rejection.

abstractions.adoc, §5 Gate, L108

stateright

gap-unmarked

OPEN

—

One function, three call sites: hosted CAS, local UI verdict, push pre-flight.

abstractions.adoc, §5 Gate, L110

stateright

gap-unmarked

OPEN

—

A verdict is never a bare pass/fail: on failure it carries which rule failed and for which refname.

abstractions.adoc, §5 Gate, L111

—

gap-unmarked

OPEN

—

Local web UI signs as the user with the user’s own member key; server-key signing is a hosted-only necessity, must not be imported locally.

abstractions.adoc, §5 Gate, L114-115

—

gap-unmarked

OPEN

—

Results location is derived by convention; an effect cannot choose where its verdicts land.

abstractions.adoc, §6 Effect, L132

alloy-paper

gap-unmarked

OPEN

—

Trigger semantics: the trigger denotes a set of commits; the effect fires once per commit that enters the set.

abstractions.adoc, §6 Effect, L134

stateright

gap-marked

OPEN

—

Meta-refs are outside `rev()’s domain by definition.

abstractions.adoc, §6 Effect, L138

stateright

gap-unmarked

OPEN

—

meta(glob) can never match effect-written namespaces (refs/meta/results/*, refs/meta/index/*); those are reachable only through results(…).

abstractions.adoc, §6 Effect, L140-141

stateright

gap-unmarked

OPEN

—

RefPattern survives as the degenerate query rev(<glob>); nothing shipped changes meaning.

abstractions.adoc, §6 Effect, L144

stateright

gap-unmarked

OPEN

—

Monotone, entry-only: a force-push can shrink a set, but a commit leaving the set retracts nothing — results are immutable history.

abstractions.adoc, §6 Effect, L147

stateright

gap-marked

OPEN

—

No pipeline state: the work set is trigger − results(self, any) — the results ref is the sole materialization marker.

abstractions.adoc, §6 Effect, L150

stateright

gap-marked

OPEN

—

Dedup key (effect, oid) over an at-least-once queue yields exactly-once outcomes with zero state outside the repository.

abstractions.adoc, §6 Effect, L151

stateright

gap-marked

OPEN

—

Result taxonomy: a result is pass, fail, or error; exit status is always a result.

abstractions.adoc, §6 Effect, L153-154

stateright

gap-unmarked

OPEN

—

Infrastructure failure is not a result; only retry exhaustion writes a terminal error, signed by the worker’s key like any other.

abstractions.adoc, §6 Effect, L155

stateright

gap-unmarked

OPEN

—

Retry bounds are deployment configuration, never effect data.

abstractions.adoc, §6 Effect, L156

alloy-paper

gap-unmarked

OPEN

—

A transient outage can neither retry forever nor permanently discharge an obligation.

abstractions.adoc, §6 Effect, L157

stateright

gap-unmarked

OPEN

—

Recursion is structure: downstream-of-effects is syntactically visible; because rev()/meta() cannot name an effect-written ref, an accidental fork bomb is unreachable by construction.

abstractions.adoc, §6 Effect, L159-160

stateright

gap-unmarked

OPEN

—

post-receive remains a dumb matcher: ref footprint is statically extractable; set entry computed incrementally from old..new, bounded by generation numbers.

abstractions.adoc, §6 Effect, L165-166

stateright

gap-unmarked

OPEN

—

Pushes are never blocked; the durable enqueue is the entire synchronous cost.

abstractions.adoc, §6 Effect, L167

stateright

gap-unmarked

OPEN

—

A worker dequeues, materializes toolchains, executes in a sandbox; host-direct requires explicit --unsandboxed.

abstractions.adoc, §6 Effect, L168-169

—

gap-unmarked

OPEN

—

Results return only as signed commits pushed to one ref per tested commit (refs/meta/results/<effect>/<short-oid>), so concurrent results never conflict.

abstractions.adoc, §6 Effect, L170

alloy-paper

gap-marked

OPEN

—

Identity discipline: the runner is a member, not an ambient authority; official results are official only because canonical refs are writable solely by designated worker keys.

abstractions.adoc, §6 Effect, L172-173

alloy-paper

gap-unmarked

OPEN

—

Any member may self-run any effect; results land in refs/meta/self/<member>/* or the inbox, adoptable by merge with the trust decision explicit.

abstractions.adoc, §6 Effect, L174

alloy-paper

gap-unmarked

OPEN

—

No content predicates beyond results(…, status), no time atoms, no external-event atoms.

abstractions.adoc, §6 Effect, L177

stateright

gap-unmarked

OPEN

—

Admin-only write rule on refs/meta/effects/* bounds who can schedule execution on canonical infrastructure.

abstractions.adoc, §6 Effect, L181

search, proptest

effect_admin_violation

OPEN

—

Abstractions 4/5/6 close: all state changes, human or machine, flow through one verified, audited channel; the repository is the message bus.

abstractions.adoc, "The loop", L188-189

stateright

gap-unmarked

OPEN

—

No code knows where it is running; an if hosted branch inside the library is the design failing.

abstractions.adoc, "Composition", L196-197

—

gap-unmarked

OPEN

—

Crates that extend git carry the gix- prefix, import nothing from the forge, and stay upstream-shaped by construction.

abstractions.adoc, "Composition", L209-210

—

gap-unmarked

OPEN

—

The unit the library exposes is receive(refs, objects, events, proposal): gate evaluation, effect matching, enqueue live inside it.

abstractions.adoc, "Composition", L213

stateright

gap-unmarked

OPEN

—

Local and hosted do not share a push path; they share receive, with only trait impls swapped — the correctness anchor for writes.

abstractions.adoc, "Composition", L215-216

stateright

gap-unmarked

OPEN

—

Dependencies point one way; a lower layer never depends on a higher one, checked mechanically.

abstractions.adoc, "Layering", L238

—

gap-unmarked

OPEN

—

A package depends on kernel crates freely and on other packages never (ents-forge/ents-kiln never depend on each other).

abstractions.adoc, "Layering", L247

—

gap-unmarked

OPEN

—

`ents-web’s generic rendering path must never match on which concrete entity type it was handed.

abstractions.adoc, "Layering", L252-253

—

gap-unmarked

OPEN

—

ents-web never depends back on git-ents.

abstractions.adoc, "Layering", L254

—

gap-unmarked

OPEN

—

A kernel crate must not depend on a package crate in any form (normal, dev, build, or feature-flagged).

abstractions.adoc, "Layering", L256

—

gap-unmarked

OPEN

—

ents-testutil must not know a package’s types.

abstractions.adoc, "Layering", L257

—

gap-unmarked

OPEN

—

Every ref namespace is minted by one function in ents_model::namespace; a package calls that function rather than inventing its own layout.

abstractions.adoc, "Layering", L259

alloy-paper

gap-unmarked

OPEN

—

Fanout index: a stale or absent index degrades to scanning ref tips, never to wrong answers.

abstractions.adoc, "Derived", L280

stateright

gap-unmarked

OPEN

—

Redacted bytes are withheld from the store and generated packs; the oid stays in history as evidence; signatures and the tip invariant are untouched because verification never reads withheld bytes.

abstractions.adoc, "Derived", L282

alloy-paper

gap-unmarked

OPEN

—

Redaction is enforced at ingest so content addressing cannot let anyone refill the hole exactly.

abstractions.adoc, "Derived", L283

stateright

gap-unmarked

OPEN

—

Readers surface a redaction marker, never an error.

abstractions.adoc, "Derived", L284

alloy-paper

gap-unmarked

OPEN

—

Embeddable server: keeping authorization/effect-matching logic in the library, never smeared across subprocess boundaries.

abstractions.adoc, "Derived", L289-290

—

gap-unmarked

OPEN

—

git effect run shares the identical materialization and sandbox path with the hosted worker.

abstractions.adoc, "Command surface", L324

stateright

gap-unmarked

OPEN

—

Every mutation frontend shares the identical receive with the hosted server.

abstractions.adoc, "Command surface", L324

stateright

gap-unmarked

OPEN

—

Revocation is a state on the member entity, not deletion; a revoked key must be explicitly rejected.

abstractions.adoc, "Command surface", L341

stateright

gap-unmarked

OPEN

—

Pushes to refs/meta/* never touch the working tree, so metadata behaves identically in both deployment modes.

abstractions.adoc, "Deployment", L363

—

gap-unmarked

OPEN

—

Worktree update happens only after receive accepts; core never touches a worktree.

abstractions.adoc, "Deployment", L361

—

gap-unmarked

OPEN

—

Bootstrap gap: an empty member list admits every push so the first member can enroll.

abstractions.adoc, "Deployment", L365

stateright

gap-unmarked

OPEN

—

An anchor MUST identify the exact content it was captured against (commit, path, blob oid, optional 1-based inclusive range); creation MUST validate path and range against the revision’s actual content.

docs/spec/anchor.adoc, [#anchor.definition], ~L9-17

alloy-paper

gap-unmarked

OPEN

—

Anchored text MUST be fully derivable from the blob and line range, derived at read time, never stored redundantly; the anchored commit’s id is recorded only as a plain data field, and MAY be gc’d.

docs/spec/anchor.adoc, [#anchor.immutable], ~L19-28

alloy-paper

gap-unmarked

OPEN

—

The anchoring document MUST embed the anchored blob "referenced by the existing blob’s own object id rather than copied" plus a context blob "written fresh", as ordinary tree entries, keeping content reachable "for as long as the document’s ref exists".

docs/spec/anchor.adoc, [#anchor.retention], ~L30-45

alloy-paper

dangling_anchor_violation, dangling_context_violation

OPEN

—

Projection MUST report one of exactly four outcomes (current/relocated/outdated/deleted), MUST follow renames, and MUST work between any two commits — forwards, backwards, or across unrelated history — while the anchor’s own commit exists.

docs/spec/anchor.adoc, [#anchor.projection], ~L48-61

—

gap-unmarked

OPEN

—

After the anchored commit is gc’d, fuzzy fallback recovers the same four outcomes approximately; "an outdated or deleted projection MUST NOT lose the anchor".

docs/spec/anchor.adoc, [#anchor.fuzzy-fallback], ~L63-74

—

gap-unmarked

OPEN

—

A working-tree anchor survives its content being "committed, amended, or discarded"; it records HEAD only as a "best-effort, never-load-bearing" field; projection MUST support the working tree as target.

docs/spec/anchor.adoc, [#anchor.working-tree], ~L76-93

alloy-paper

gap-unmarked

OPEN

—

An effect definition MUST be rejected before storage when a toolchain name is not a valid ref-path segment or the trigger fails to parse (including rev() naming refs/meta/* or meta() naming an effect-written namespace).

docs/spec/effect.adoc, [#effect.validation], ~L41-50

gap-unmarked

OPEN

—

Host-direct execution MUST require an explicit --unsandboxed flag and MUST be "available only locally, never on canonical hosted infrastructure".

docs/spec/effect.adoc, [#effect.execution], ~L54-68

—

gap-unmarked

OPEN

—

An effect’s stored data MUST NOT select its own executor, demand --unsandboxed, or set retry bounds; those are deployment configuration, "never a field an effect definition can carry".

docs/spec/effect.adoc, [#effect.deployment-property], ~L70-78

—

gap-unmarked

OPEN

—

A member running git effect run locally MUST see "the same outcome a canonical worker would record"; only the queue is skipped, and the queue carries no correctness content.

docs/spec/effect.adoc, [#effect.local-run], ~L80-89

stateright

gap-unmarked

OPEN

—

Result write-back MUST be "an ordinary receive client, never a privileged write outside the gate".

docs/spec/effect.adoc, [#effect.results-writeback], ~L93-106

stateright

gap-unmarked

OPEN

—

Only the sandbox MAY touch a toolchain’s extracted bytes; declared components MUST be resolved during effect execution, "never by any other code path".

docs/spec/effect.adoc, [#effect.toolchains], ~L161-168

—

gap-unmarked

OPEN

—

A fanout index MUST be rebuilt only by an effect and written back only as a worker-signed commit, "never by any privileged out-of-band writer".

docs/spec/effect.adoc, [#effect.fanout-index], ~L174-184

stateright

gap-unmarked

OPEN

—

Verification MUST depend only on the read half of the RefStore seam, never on write access or on any state outside refs/meta/*.

docs/spec/gate.adoc, intro (also [#arch.refstore-read-cas-split]), ~L3-5

gap-unmarked

OPEN

—

Authorization is judged against the member entity in force at acceptance time — the member ref’s tip in the same snapshot the gate reads.

docs/spec/gate.adoc, [#gate.tip-signed], ~L12-23

stateright

unsigned_violation (partial: enrolled-membership only, not snapshot-scoped refname authorization)

OPEN

—

A gate-owned hash-identified entity’s creation MUST strictly decode as its type, an unknown tree entry refusing; the gate-owned entity structs MUST stay pairwise disjoint under this decode.

docs/spec/gate.adoc, [#gate.identity-binding], ~L36-40

alloy-paper

gap-unmarked

OPEN

—

When an object the binding needs is withheld by redaction, the binding MUST be vouched by the admin-signed redaction record, and a redacted object MUST NOT be re-admitted.

docs/spec/gate.adoc, [#gate.identity-binding], ~L47-51

stateright

gap-unmarked

OPEN

—

Advancing a hash-identified entity’s ref is authorized only for the genesis signer or an admin; a review ref advances only under the signature of the member its refname names.

docs/spec/gate.adoc, [#gate.owner-mutation], ~L54-67

gap-unmarked

OPEN

—

A pre-flight verdict "is a prediction that can only go stale; it MUST NOT diverge from the rules the hosted store will actually apply".

docs/spec/gate.adoc, [#gate.call-sites], ~L188-196

stateright

gap-unmarked

OPEN

—

Transport-auth evidence MUST be threaded through uninterpreted — "never substituted for the tip invariant on a refs/meta/* update"; no advisory call site MAY render a refs/heads/* verdict meanwhile.

docs/spec/gate.adoc, [#gate.branch-acl-undefined], ~L267-284

stateright

gap-unmarked

OPEN

—

With no refs/meta/member/* ref, first enrollment is self-admitting; but a member set whose keys are all revoked "MUST fail closed: revoking every key MUST NOT reopen this self-admitting window".

docs/spec/gate.adoc, [#gate.bootstrap], ~L288-296

stateright

gap-unmarked

OPEN

—

git ents lsp MUST NOT bind a network socket, MUST NOT add a git-serving transport, and MUST receive its signing identity by injection from the composition root.

docs/spec/lens.adoc, [#lens.serve], ~L13-24

—

gap-unmarked

OPEN

—

Lens ranges are derived at request time via projection and "never cached across mutations of the comment’s ref"; non-open comments omitted unless asked.

docs/spec/lens.adoc, [#lens.lenses], ~L26-39

—

gap-unmarked

OPEN

—

Comment diagnostics "MUST NEVER use warning or error severity" and MUST be suppressible without affecting the lenses.

docs/spec/lens.adoc, [#lens.diagnostics], ~L41-50

—

gap-unmarked

OPEN

—

Composing MUST require no client-specific extension; a richer input surface "MUST be sugar over the same create operation, never a second mechanism".

docs/spec/lens.adoc, [#lens.compose], ~L61-75

—

gap-unmarked

OPEN

—

Editor-composed comments MUST anchor to the working tree’s content when it differs from HEAD — "exactly the bytes the author was reading".

docs/spec/lens.adoc, [#lens.working-tree], ~L77-87

alloy-paper

gap-unmarked

OPEN

—

Every lens operation MUST be the same library call the git ents comment porcelain exposes; the CLI listing MUST offer a machine-readable form sufficient for an agent with no editor attached.

docs/spec/lens.adoc, [#lens.parity], ~L89-101

—

gap-unmarked

OPEN

—

All forge state MUST live under refs/meta/*; retention pins under refs/meta/pins/* are "the sole exception" to tree-is-the-entity, carrying the empty tree, never an entity.

docs/spec/meta-ref.adoc, [#meta-ref.namespace], ~L15-27

alloy-paper

gap-unmarked

OPEN

—

Inbox routing preserves the canonical ref’s entire path below refs/meta/ so "two different entity kinds can never collide under the same inbox id"; <member> is the leading segment so authorization keys off the refname alone.

docs/spec/meta-ref.adoc, [#meta-ref.inbox], ~L45-61

alloy-paper

gap-unmarked

OPEN

—

A member is authorized only for its own refs/meta/inbox/<member>/* segment; "no member, including an admin-registered one, MAY write into another member’s inbox segment".

docs/spec/meta-ref.adoc, [#meta-ref.inbox], ~L62-68

gap-unmarked

OPEN

—

An inbox ref MUST NOT be deleted on adoption or at any other time — it remains the contributor’s audit trail.

docs/spec/meta-ref.adoc, [#meta-ref.inbox], ~L69-71

stateright

gap-unmarked

OPEN

—

self is its own top-level namespace, keeping the canonical results glob and the self-run glob "disjoint by construction"; both namespaces hold the same typed trees as canonical, only the refname rule differs.

docs/spec/meta-ref.adoc, [#meta-ref.inbox], ~L72-85

alloy-paper

gap-unmarked

OPEN

—

For a hash-identified entity, "every parentless commit reachable from the proposed tip MUST be that genesis" — the reachability form makes doppelgänger replay impossible and holds across divergence merges.

docs/spec/meta-ref.adoc, [#meta-ref.identity-binding], ~L117-124

alloy-paper

genesis_violation, second_root_violation

OPEN

—

The parentless-roots walk MUST NOT be applied to pins: a pin’s ancestry deliberately reaches into code history.

docs/spec/meta-ref.adoc, [#meta-ref.identity-binding], ~L132-135

alloy-paper

gap-unmarked

OPEN

—

Who authored a state, and when, MUST come from the commit itself, never from duplicated tree fields: "each datum has exactly one signed home".

docs/spec/meta-ref.adoc, [#meta-ref.identity-binding], ~L144-147

alloy-paper

gap-unmarked

OPEN

—

Within a meta-ref’s history a commit parent means exactly one thing — the prior state of the same entity (pin retained-commit parents sole exception); a cross-entity relationship MUST be tree data, never a parent edge.

docs/spec/meta-ref.adoc, [#meta-ref.identity-binding], ~L147-150

alloy-paper

gap-unmarked

OPEN

—

A genesis commit is frozen by the identity derived from it, so hash-identified/composite-keyed structs MUST evolve additively only — "new fields optional, required fields never added, renamed, or removed".

docs/spec/meta-ref.adoc, [#meta-ref.identity-binding], ~L149-153

alloy-paper

gap-unmarked

OPEN

—

A struct change is a migration committed on top of the old tip; history keeps the old encoding, and a struct change "MUST NOT rewrite or delete a prior commit on the ref".

docs/spec/meta-ref.adoc, [#meta-ref.migration], ~L172-180

alloy-paper

gap-unmarked

OPEN

—

The gate and receive are content-agnostic: verification depends on "signature, refname, trailer, and DAG descent, never on tree contents", so a stock server MUST carry entity types it cannot parse.

docs/spec/model.adoc, [#model.extensibility], ~L8-22

gap-unmarked

OPEN

—

A facet shape MUST be compile-time-defined: runtime-readable, never runtime-constructible.

docs/spec/model.adoc, [#model.extensibility], ~L13-15

—

gap-unmarked

OPEN

—

A member’s id binds to its key-carrying entity’s refname final segment; enrollment occurs as a signed commit — the member is forge state "with no user database separate from the repository".

docs/spec/model.adoc, [#model.member-identity], ~L31-40

alloy-paper

gap-unmarked

OPEN

—

Admission consults the member entity currently in force, so a revoked key’s new pushes are refused "from the moment the revocation lands, regardless of any committer timestamp the pushed commit claims".

docs/spec/model.adoc, [#model.member-revocation], ~L47-50

stateright

gap-unmarked

OPEN

—

A ref accepted before the revocation landed remains valid: "acceptance is never re-judged".

docs/spec/model.adoc, [#model.member-revocation], ~L51-52

stateright

gap-unmarked

OPEN

—

Unrevoking returns the key to authorizing new signatures "without altering the record of the period it was revoked".

docs/spec/model.adoc, [#model.member-revocation], ~L60-61

stateright

gap-unmarked

OPEN

—

A self-attested member MUST NOT be authorized for canonical refs — writes limited to its own inbox and self-run namespaces — until an admin-registered member promotes it.

docs/spec/model.adoc, [#model.member-provenance], ~L64-75

gap-unmarked (effect_admin_violation covers only the effects namespace, not the provenance tier generally)

OPEN

—

A machine actor is an ordinary Member entity, revocable like any human key; "a privileged write path for a machine actor MUST NOT exist outside this model".

docs/spec/model.adoc, [#model.member-worker], ~L77-86

stateright

gap-unmarked

OPEN

—

A comment’s identity is the oid of its genesis commit and "MUST NEVER change afterward: edits advance the ref, they do not rename it".

docs/spec/model.adoc, [#model.comment], ~L99-102

alloy-paper

gap-unmarked

OPEN

—

A comment about nothing MUST be refused at creation by the writing tool, "though never by the gate, which stays content-agnostic".

docs/spec/model.adoc, [#model.comment], ~L93-98

—

gap-unmarked

OPEN

—

A new comment’s state is open; resolving records resolved as an ordinary mutation commit — "never a deletion, so the conversation stays auditable" — and reopening is supported the same way.

docs/spec/model.adoc, [#model.comment-state], ~L109-121

—

gap-unmarked

OPEN

—

A state-changing mutation by an enrolled key MUST carry a Key-for-<member-id> trailer whose value is the member ref’s tip oid at mutation time, pinning the enrolled record across later rotation or revocation.

docs/spec/model.adoc, [#model.comment-provenance], ~L123-129

—

gap-unmarked

OPEN

—

An entity’s thread MUST be an aggregation query over comment refs; a context entity MUST NOT store its comment list, so concurrent commenters "never race a shared ref".

docs/spec/model.adoc, [#model.comment-context], ~L132-142

alloy-paper

gap-marked (instance of abstraction 1’s granularity rule)

OPEN

—

A reply’s parent MUST exist when the reply is created; aboutness is inherited from the thread root; no comment stores a list of its replies.

docs/spec/model.adoc, [#model.comment-thread], ~L144-154

alloy-paper

gap-unmarked

OPEN

—

An issue’s identity is its genesis oid — no sequential counter exists — and machine-readable output (including --porcelain) MUST carry the full id.

docs/spec/model.adoc, [#model.issue], ~L158-177

alloy-paper

gap-unmarked

OPEN

—

A review binds by composite key reviews/<target>/<member>; at genesis the reviewed-commit tree field equals the <target> segment and binds it; re-reviewing advances the field while the refname stays keyed by genesis.

docs/spec/model.adoc, [#model.review], ~L181-198

alloy-paper

gap-unmarked

OPEN

—

Every review MUST occupy exactly two refs: the entity ref and its retention pin.

docs/spec/model.adoc, [#model.review], ~L191-193

alloy-paper

gap-unmarked

OPEN

—

A review’s verdict MUST be a hard enum — approve, request-changes, or comment: "a verdict gates decisions, so its vocabulary is platform, not schema".

docs/spec/model.adoc, [#model.review], ~L199-202

—

gap-unmarked

OPEN

—

A pin’s tip is a reviewer-signed commit whose parents include the reviewed commit, so that commit and its ancestry "survive force-push, branch deletion, and gc for as long as the review exists".

docs/spec/model.adoc, [#model.review-pin], ~L213-224

alloy-paper

gap-unmarked

OPEN

—

Re-reviewing MUST advance the pin fast-forward with parents = previous pin tip + newly reviewed commit, so every reviewed round stays retained and the pin’s history is the audit trail.

docs/spec/model.adoc, [#model.review-pin], ~L225-229

alloy-paper

gap-unmarked

OPEN

—

A result MUST carry the effect’s name and the judged commit’s full oid as tree fields from which the refname derives — "a result MUST mean something with the refname stripped away" (a signed pass cannot be replayed against another effect/commit).

docs/spec/model.adoc, [#model.result-identity], ~L260-270

alloy-paper

gap-unmarked

OPEN

—

Result fields are not parent edges: a result ref’s parents stay prior states of the same result, and a result MUST NOT retain the judged commit’s ancestry the way a pin does.

docs/spec/model.adoc, [#model.result-identity], ~L271-274

alloy-paper

gap-unmarked

OPEN

—

A toolchain is a hash-pinned ~1KB manifest carrying its own provenance, "a resource an effect declares as a dependency … never a trigger condition in its own right".

docs/spec/model.adoc, [#model.toolchain], ~L279-289

—

gap-unmarked

OPEN

—

A Redaction entity carries the target oid, a reason, and the admin signature; it "MUST NOT carry the redacted content itself".

docs/spec/model.adoc, [#model.redaction], ~L294-300

alloy-paper

gap-unmarked

OPEN

—

Authentication state MUST live in the repository as ordinary forge state; "a session database or token table MUST NOT back it".

docs/spec/model.adoc, [#model.account], ~L308-313

—

gap-unmarked

OPEN

—

The library MUST NOT define its own ObjectStore trait — gitoxide’s Find/Exists/Write ARE the seam; a new trait exists only where gitoxide is silent.

docs/spec/overview.adoc, [#arch.no-object-store-trait], ~L180-189

—

gap-unmarked

OPEN

—

The gate’s pure verify function MUST live in a crate separate from receive; advisory call sites MUST be answerable without linking effect-matching and enqueue logic.

docs/spec/overview.adoc, [#arch.gate-receive-split], ~L191-199

—

gap-unmarked

OPEN

—

The query algebra MUST live apart from executor code; receive MUST NOT depend on the effect crate, "so no push path links executor code".

docs/spec/overview.adoc, [#arch.query-effect-split], ~L201-208

—

gap-unmarked

OPEN

—

A concrete store implementation is wired only inside a composition root, never a library crate, and is not promoted to a shared library crate until a second root consumes it.

docs/spec/overview.adoc, [#arch.store-composition-root], ~L211-219

—

gap-unmarked

OPEN

—

A loose-ref RefStore MUST write refs through its own CAS discipline and MUST NOT shell out to git update-ref, so local mutations honor the same CAS guarantee as hosted.

docs/spec/overview.adoc, [#arch.loose-cas-discipline], ~L239-245

stateright

gap-unmarked

OPEN

—

A CommitQuery MUST parse per the fixed grammar; |/&/- denote union/intersection/difference, left-associative at a single precedence level, parentheses the only override.

docs/spec/query.adoc, [#query.grammar] (+ [#query.set-ops]), ~L12-35

stateright

gap-unmarked

OPEN

—

Unsupported rev syntax (~n/^n, A…B, @{…}, abbreviated hex) and any refs/meta/* pattern MUST be rejected as malformed — "never silently evaluated to the empty set or to the wrong set".

docs/spec/query.adoc, [#query.rev], ~L39-58

stateright

gap-unmarked

OPEN

—

Membership in results(effect, status) is decided solely by existence of a matching results ref — never by reachability from refs/heads/* or any ref outside the query’s footprint — and resolution is a refname scan, never a history walk.

docs/spec/query.adoc, [#query.results], ~L61-79

stateright

gap-unmarked

OPEN

—

The fanout index "MUST NOT be addressable by any query atom at all".

docs/spec/query.adoc, [#query.meta], ~L82-91

stateright

gap-unmarked

OPEN

—

self in the work set is evaluation-time notation, "not a keyword an author may write in a trigger"; work-set evaluation inherits incremental bounds and refname-scan resolution, never a full-history walk.

docs/spec/query.adoc, [#query.workset], ~L159-173

stateright

gap-marked (work-set/dedup materialization is the declared cross-transaction gap)

OPEN

—

Replicating refs a trusted remote already admitted MAY apply directly (re-verification on fetch is opt-in audit); commits the replicating machinery authors itself — divergence and adoption merges — are origination, not replication.

docs/spec/receive.adoc, [#receive.unit], ~L10-27

stateright

gap-unmarked

OPEN

—

Gate evaluation MUST be checkable against exactly the proposal shape, frontend-independent; meta-ref admission "MUST ignore [transport-auth evidence] entirely and MUST NOT consult it in place of the tip invariant".

docs/spec/receive.adoc, [#receive.proposal-shape], ~L29-47

stateright

gap-unmarked

OPEN

—

An entity declared across multiple refs MUST write them in a single Proposal through one receive call; the atomic multi-ref CAS admits or refuses the whole batch, "so such an entity is never observable with only some of its refs written".

docs/spec/receive.adoc, [#receive.multi-ref-atomicity], ~L49-66

stateright

gap-unmarked

OPEN

—

A receive inside a git hook reads existing state through the common object directory, never git’s quarantine directory: quarantined objects "MUST NOT be treated as stored until the transaction commits".

docs/spec/receive.adoc, [#receive.object-access], ~L93-105

stateright

gap-unmarked

OPEN

—

Pending obligations MUST be derivable from repository state alone; an EventSink MAY lose events on crash provided the root reconciles at startup before serving pushes; "a durable queue MUST be treated as a performance optimization, never a correctness requirement".

docs/spec/receive.adoc, [#receive.reconstructible], ~L134-146

stateright

gap-marked (cross-transaction queue/materialization state is the declared dedup gap)

OPEN

—

A push to refs/meta/redactions/* MUST be rejected unless the member is admin-registered, regardless of any other role rule, statable as a single refname glob.

docs/spec/receive.adoc, [#receive.redaction-admin-only], ~L148-158

gap-unmarked (effect_admin_violation covers only refs/meta/effects/*; no redactions-namespace rule exists)

OPEN

—

The local root wires loose refs, the odb, Docker, null EventSink, and the advisory gate; git ents serve MUST NOT expose git’s smart-HTTP wire protocol; local effect execution is pull, "never a daemon watching refs".

docs/spec/roots.adoc, [#roots.local], ~L20-32

—

gap-unmarked

OPEN

—

The single-node hosted root’s hooks call the gate and reconcile around receive-pack’s own ref update, "never through this crate’s own `RefStore::transaction, to avoid a double-write race".

docs/spec/roots.adoc, [#roots.single-node-hosted], ~L34-52

stateright

gap-unmarked

OPEN

—

The worker MUST NOT share in-process state with receive.

docs/spec/roots.adoc, [#roots.hosted], ~L55-63

stateright

gap-unmarked

OPEN

—

Wiring the scale-out root (Postgres/Tigris/durable queue) MUST require zero modification to any library crate — the seam design’s honesty test, proven by an actual production migration.

docs/spec/roots.adoc, [#roots.honesty-test], ~L66-75

—

gap-unmarked

OPEN

—

Configuration selects trait implementations only at the composition root and MUST NOT leak past it.

docs/spec/roots.adoc, [#roots.config-isolation], ~L78-83

—

gap-unmarked

OPEN

—

ents-web receives its signing identity by injection and MUST NOT assume a network; in-process webview embedding remains a supported deployment.

docs/spec/roots.adoc, [#roots.web-agnostic], ~L96-103

—

gap-unmarked

OPEN

—

A hosted web session is held only in server memory; every state-changing request carries a per-session CSRF token verified before acting; a web edit is signed only on behalf of an authenticated session.

docs/spec/roots.adoc, [#roots.web-session], ~L141-148

—

gap-unmarked

OPEN

—

Every repository-path segment MUST be validated before filesystem or subprocess use, rejecting escapes, nesting inside an existing repository, or namespace-directory collisions.

docs/spec/roots.adoc, [#roots.path-validation], ~L151-158

—

gap-unmarked

OPEN

—

Fetch authorization MUST be refname-keyed, using the same authorization model as write authorization.

docs/spec/roots.adoc, [#roots.fetch-auth], ~L160-167

gap-unmarked

OPEN

—

A clone plus refs/meta/* MUST carry the complete audit history and the signatures needed to verify it, "with no server-side data left behind".

docs/spec/sync.adoc, [#sync.forge-transfer], ~L9-16

alloy-paper

gap-unmarked

OPEN

—

Inbox adoption and self-run adoption MUST both go through the same merge machinery as divergence resolution, "not a separate adoption code path".

docs/spec/sync.adoc, [#sync.adoption-machinery], ~L50-57

stateright

gap-unmarked

OPEN

—

"Nothing in the resulting ref-store state lets a pure verifier tell" a cherry-picked adoption from a hand-authored commit — attribution preservation binds the merge machinery, never the gate.

docs/spec/sync.adoc, [#sync.adoption-no-cherry-pick] (also gate.adoc Adoption intro ~L218-224), ~L59-73

stateright

gap-unmarked

OPEN

—

verify/ledger.adoc

verify