elench
An evidence layer for repositories — reimagining git for agentic flow.
What this is
Version control records what changed. Forges record who approved it. Neither records what was checked, to what depth, and what remains unevaluated. elench is that durable state — a signed, append-only, revocable claim log that IS the primary history. The git CLI works because elench synthesizes git-compatible objects from the claim log on demand. Humans use git; elench is invisible.
Quick start
git clone https://github.com/witlox/elench.git
cd elench
make # fmt-check + lint + Tier 1
make test # cargo test --lib
make test-slow # cargo test --all-targets
make dogfood # full dogfooding pipeline
Requires Rust 1.85+ (edition 2024). See CONTRIBUTING.md and docs/guide/getting-started.md.
Documentation
Full documentation is published as an mdBook
and available in docs/:
Specifications in specs/ (ubiquitous language, domain model,
invariants, features, ADRs 0001-0008, fidelity index, cross-context
interactions, failure modes, assumptions).
License
Getting Started
Prerequisites
- Rust 1.85+ (edition 2024).
rust-toolchain.tomlpins stable with rustfmt and clippy. - make (for the Makefile targets)
- git (for
elench git initmaterialization) - cargo-llvm-cov (optional, for coverage)
- cargo-deny (optional, for license/advisory checks)
git clone https://github.com/witlox/elench.git
cd elench
make # fmt-check + lint + Tier 1 tests
If make passes, the workspace is ready for development. If it does
not, run make fmt first (auto-format), then make again.
Building
cargo build # debug build (default)
cargo build --release # release build
cargo build --features elench/fjall-backend # with persistent fjall store
Running
elench is a CLI tool. All commands take an optional --store memory|fjall <path> flag (before the command) to select the storage
backend.
# Emit a claim (sign + store)
elench [--store memory|fjall <path>] emit <claim.json>
# Verify a DSSE envelope
elench verify <envelope.json>
# Compute a claim's status by folding the log
elench status <claim_id> [<claims.json>]
# Evaluate the release gate for a tree
elench gate <tree_oid> [<claims.json>]
# Compute blast radius from a claim
elench blast <claim_id> [<claims.json>]
# Materialize git projection (oneline or full)
elench git <claims.json>
elench git oneline <claims.json>
elench git full <claims.json>
# Materialize a real .git/ directory
elench git init <output_path> <claims.json>
# Store a blob or tree
elench store blob <file>
elench store tree <file1> <file2> ...
# Log statistics
elench log <claims.json>
# Review unevaluated claims
elench review <tree_oid> <claims.json>
# Accept named unevaluated gaps (residue-acceptance)
elench accept <tree_oid> <claims.json> --claim <id> [<id>...]
# List active predicate conflicts
elench conflicts <tree_oid> <claims.json>
# Compact the claim log (manual, destructive)
elench compact <claims.json> [--before <timestamp>]
# Reconcile anchors against a tree
elench reconcile <tree_oid> <claims.json>
# Create or verify a release artifact (INV-15)
elench artifact create <tree_oid> <policy_name> <sha256_digest>
elench artifact verify <artifact.json> <claims.json>
# Run a build, capture exit code + digest, emit provenance
elench build <tree_oid> [--artifact <path>] -- <command...>
# Version
elench version
Testing
Three tiers, cascading. Each higher tier includes the lower.
| Tier | Command | What | When |
|---|---|---|---|
| 1 (fast) | make test | cargo test --lib | Between every edit; pre-commit |
| 2 (slow) | make test-slow | Tier 1 + cargo test --all-targets | Pre-PR |
| 3 (full) | make test-full | Tier 2 + dogfooding e2e | Pre-merge / nightly |
make # fmt-check + lint + Tier 1 (before every commit)
make test # Tier 1
make test-slow # Tier 2
make test-full # Tier 3 (runs dogfooding pipeline)
make coverage # cargo-llvm-cov --workspace --fail-under-lines 50
make dogfood # full dogfooding pipeline
CI
CI (.github/workflows/ci.yml) runs automatically:
- Push → Tier 1 (fmt-check + clippy +
cargo test --lib) - PR → Tier 1 + Tier 2 (
cargo test --all-targets) - Nightly → Tier 1 + Tier 2 + Tier 3 (fjall backend + coverage + dogfooding)
CLI Reference
All commands accept an optional --store memory|fjall <path> flag
before the command name to select the storage backend. Default is
--store memory (in-memory, no persistence).
emit
Create, sign, and store a claim.
elench [--store ...] emit <claim.json>
The JSON file must contain a Claim with fields matching
schema/claim.schema.json. The claim’s id is computed from content
(INV-28); the provided id is ignored. The claim is signed in a DSSE
envelope (INV-22) and stored in the content-addressed store.
verify
Verify a DSSE envelope and validate the enclosed claim.
elench verify <envelope.json>
Extracts the claim and signer from the envelope, verifies the Ed25519 signature, and runs the emission-rule validator (ADR-0006).
status
Compute a claim’s status by folding the log.
elench status <claim_id> [<claims.json>]
Status is unevaluated, passed, or falsified — computed from the
log, never stored (INV-04). If no claims file is given, the status is
computed from an empty log (live evaluation, INV-14).
gate
Evaluate the release gate for a tree.
elench gate <tree_oid> [<claims.json>]
The gate is a predicate over claims (R3). It checks four conditions
(see docs/release-policy.md): no falsified premise, bounded residue,
origin floor, builder agreement. The verdict is computed live, not
cached (INV-14).
blast
Compute the blast radius from a claim.
elench blast <claim_id> [<claims.json>]
The blast radius is the transitive dependsOn closure — all claims
that depend on the given claim, directly or indirectly. If the given
claim is falsified, every claim in its blast radius is also
falsified.
git
Materialize the git projection.
elench [--store ...] git <claims.json> # oneline (default)
elench [--store ...] git oneline <claims.json> # git log --oneline
elench [--store ...] git full <claims.json> # full git log
elench [--store ...] git init <output_path> <claims.json> # real .git/
The projection synthesizes git-compatible objects (blobs, trees, commits) from the claim log (ADR-0002). Synthesis is deterministic (BC4, INV-20): two parties with the same claim log produce byte-identical objects.
git init writes real zlib-compressed git objects to
<output_path>/.git/objects/. After materialization, git log,
git blame, and git checkout work in the output directory.
store
Store a blob or tree in the content-addressed store.
elench [--store ...] store blob <file>
elench [--store ...] store tree <file1> <file2> ...
Blobs are SHA-256 content-addressed (INV-25). Trees are canonical
(mode space name null oid) and SHA-256 content-addressed. With
--store fjall <path>, objects persist across processes.
log
Log statistics: count, status distribution, conflicts.
elench log <claims.json>
Reports total count, kind distribution (assertion, verification,
falsification, supersession, residue-acceptance), status distribution
(unevaluated, passed, falsified), noise ratio, and dependsOn
density.
review
Review unevaluated claims for a tree.
elench review <tree_oid> <claims.json>
Lists all unevaluated claims anchored to the given tree, showing
form, language, source, and producer. The human must name each gap
before elench accept issues a residue-acceptance.
accept
Accept named unevaluated gaps (residue-acceptance).
elench accept <tree_oid> <claims.json> --claim <id> [<id>...]
Only humans may emit residue-acceptance records (INV-12). Each named claim must be unevaluated; the acceptance covers the excess residue above the policy’s allowance (R5).
conflicts
List active predicate conflicts for a tree.
elench conflicts <tree_oid> <claims.json>
Two predicates are a conflict if and only if they anchor to the same code location (same path+range, or same symbol) but assert different expressions. Two predicates about different files are not a conflict. Last-writer-wins by timestamp; the older claim is flagged for resolution.
compact
Compact the claim log (manual, destructive).
elench compact <claims.json> [--before <timestamp>]
Retires all claims before the cut-off timestamp, freezing their statuses. The compaction record carries the frozen status snapshot forward. Active claims continue to be revocable (R1 preserved for active claims, deliberately violated for retired ones).
reconcile
Detect anchors that no longer resolve.
elench reconcile <tree_oid> <claims.json>
For each claim anchored to the given tree, resolves the anchor using the multi strategy (path-range, symbol, content-digest). Claims that fail to resolve or are degraded are reported as drifted. The reconciliation pass is read-only — it does not auto-fix.
artifact
Create or verify a release artifact (INV-15).
elench artifact create <tree_oid> <policy_name> <sha256_digest>
elench artifact verify <artifact.json> <claims.json>
The artifact carries (version, tree, policy, digest, released_at) —
NOT a verdict (INV-15). Consumers re-evaluate the gate at consumption
time (R4). See schema/artifact.schema.json for the format.
build
Run a build, capture exit code + digest, emit provenance.
elench build <tree_oid> [--artifact <path>] -- <command...>
Runs the build command, captures the exit code, and computes a
SHA-256 digest. With --artifact <path>, the digest is SHA-256 of
that file (the real build output). Without it, the digest falls back
to SHA-256 of stdout. Emits a build provenance claim with
origin.kind = harness-observed (INV-22).
Claim Schema
The JSON Schema for claims in elench.
{
"$schema": "https://json-schema.org/draft/2020-12/schema",
"$id": "https://example.invalid/elench/claim/v0.1.json",
"title": "elench claim predicate (v0.1, DRAFT)",
"description": "Carried as the `predicate` of an in-toto Statement inside a DSSE envelope. The envelope supplies signer identity; this schema supplies producer identity, which is a different thing (R2). Status is NOT stored here — it is computed by folding the claim log. A `falsification` record is itself a claim with kind=falsification referencing a target.",
"type": "object",
"required": ["id", "kind", "assertion", "origin", "anchor", "timestamp"],
"additionalProperties": false,
"properties": {
"id": {
"type": "string",
"pattern": "^cl_[0-9a-f]{64}$",
"description": "Content address of the claim at creation. Stable across status changes (R1). Never reassigned."
},
"kind": {
"enum": ["assertion", "falsification", "verification", "supersession", "residue-acceptance"],
"description": "falsification/verification/supersession MUST carry `target`. residue-acceptance is the R5 human signature over named unevaluated claims."
},
"target": {
"type": "array",
"items": { "type": "string", "pattern": "^cl_[0-9a-f]{64}$" },
"description": "Claims this record acts upon. Required unless kind=assertion."
},
"assertion": {
"type": "object",
"required": ["form"],
"additionalProperties": false,
"properties": {
"form": {
"enum": ["predicate", "annotation"],
"description": "predicate: machine-checkable, can gate. annotation: prose, searchable, CANNOT gate. Policies MUST NOT read annotations. The BC1 ratio is measured over this field."
},
"expression": {
"type": "object",
"required": ["language", "source"],
"properties": {
"language": { "type": "string", "description": "elench-predicate-v1. See ADR-0004." },
"source": { "type": "string" },
"digest": { "type": "string" }
},
"description": "REQUIRED when form=predicate. A predicate without an executable expression is an annotation wearing a costume; validators MUST reject."
},
"text": {
"type": "string",
"maxLength": 2000,
"description": "Human-readable. Never load-bearing."
}
}
},
"origin": {
"type": "object",
"required": ["kind", "producer"],
"additionalProperties": false,
"properties": {
"kind": {
"enum": ["harness-observed", "agent-asserted", "human-asserted"],
"description": "R2. harness-observed may ONLY be emitted by the harness. See AGENTS.md. Policies may and generally should discriminate on this."
},
"producer": {
"type": "object",
"required": ["id"],
"properties": {
"id": { "type": "string", "description": "Harness build id, model id + version, or human key id." },
"sessionId": { "type": "string" },
"hermeticity": {
"enum": ["none", "container", "vm", "hermetic-derivation"],
"description": "BC3. Self-reported and therefore only as good as the producer. Present so policy can require a floor, not because it is trusted."
}
}
}
}
},
"anchor": {
"$comment": "RESOLVED (E1). The anchor object uses strategy=multi by default — all three strategies (path-range, symbol, content-digest) recorded simultaneously, resolved by agreement, with 'degraded' reported when they disagree. See experiments/E1-anchor-survival-result.md.",
"type": "object",
"required": ["tree", "strategy"],
"properties": {
"tree": { "type": "string", "description": "elench tree OID (content address of the tree state in the store, ADR-0001). Not a git commit OID." },
"strategy": { "enum": ["path-range", "symbol", "content-digest", "multi"], "default": "multi" },
"path": { "type": "string" },
"range": { "type": "array", "items": { "type": "integer" }, "minItems": 2, "maxItems": 2 },
"symbol": { "type": "string", "description": "Language-server qualified name." },
"contentDigest": { "type": "string", "description": "Digest of the anchored span, normalised." }
}
},
"timestamp": {
"type": "integer",
"description": "Unix epoch seconds. Set by the producer at emission time. Used by ADR-0007 for deterministic git commit synthesis — NOT the wall clock at projection time. Two parties projecting the same claim get the same commit timestamp."
},
"evidence": {
"type": "array",
"description": "Empty for agent-asserted claims by default; that emptiness is the signal, not a gap to fill. A human-asserted claim with no evidence is authority without evidence, which is a legitimate and distinguishable state.",
"items": {
"type": "object",
"required": ["kind"],
"properties": {
"kind": { "enum": ["process-exit", "test-report", "artifact-digest", "external-attestation"] },
"digest": { "type": "string" },
"exitCode": { "type": "integer" },
"uri": { "type": "string" }
}
}
},
"dependsOn": {
"type": "array",
"items": { "type": "string", "pattern": "^cl_[0-9a-f]{64}$" },
"description": "Premises. The transitive closure over this field IS the blast radius when something upstream is falsified. This field is the reason the project exists; if it is left empty in practice, revocation cannot propagate and the whole design collapses to per-claim status flags."
}
},
"allOf": [
{
"if": { "properties": { "kind": { "const": "assertion" } } },
"then": { "properties": { "target": { "maxItems": 0 } } }
},
{
"if": { "properties": { "kind": { "not": { "const": "assertion" } } } },
"then": { "required": ["target"] }
},
{
"if": { "properties": { "kind": { "const": "residue-acceptance" } } },
"then": { "properties": { "target": { "minItems": 1 } } }
}
]
}
Artifact Schema
The JSON Schema for artifacts in elench.
{
"$schema": "https://json-schema.org/draft/2020-12/schema",
"$id": "https://example.invalid/elench/artifact/v0.1.json",
"title": "elench release artifact (v0.1)",
"description": "Carries (tree, policy), NOT a verdict (INV-15). Consumers re-evaluate the release gate at consumption time using the current claim log. The artifact is distributed independently of the claim log — anyone with both can re-evaluate. If a load-bearing claim is falsified after release, the artifact's status changes with no byte moving and no re-signing (R4).",
"type": "object",
"required": ["version", "tree", "policy", "digest", "released_at"],
"additionalProperties": false,
"properties": {
"version": {
"type": "string",
"pattern": "^\\d+\\.\\d+$",
"description": "Artifact format version. Consumers SHOULD reject artifacts with unknown major versions. Current: '0.1'."
},
"tree": {
"type": "string",
"pattern": "^[0-9a-f]{64}$",
"description": "The elench tree OID this artifact was built from. NOT a git commit — an elench content address (ADR-0001)."
},
"policy": {
"type": "string",
"minLength": 1,
"description": "The policy name under which the artifact was released. Consumers re-evaluate the gate using a policy with this name."
},
"digest": {
"type": "string",
"pattern": "^[0-9a-f]{64}$",
"description": "SHA-256 digest of the artifact (e.g., binary, container image). This is what condition 4 (builder agreement) checks: K independent producers have signed statements with this digest as the subject."
},
"released_at": {
"type": "integer",
"description": "Unix epoch seconds. Set by the producer at release time. NOT a verdict — consumers re-evaluate."
},
"description": {
"type": "string",
"description": "Human-readable description of the artifact (optional)."
}
}
}
How It Works
elench has no server. It is a single-process CLI that agents call and humans project from. The claim log is the primary history; git is a read-only projection derived from it.
The chain
Agent ──elench emit──► Claim Log (primary history)
│ │
│ ├──elench gate──► Verdict (live evaluation)
│ │
│ └──elench git init──► .git/ (projection)
│ │
Human ◄──git log/blame/checkout── .git/
-
Agent emits a claim after each change. A claim is a signed assertion about a tree: what was checked, to what depth, what remains unevaluated. The agent signs with an Ed25519 key and emits a DSSE envelope (same format as build provenance — INV-22).
-
The harness emits what it observed. A CI run, a test suite, a lint check — these are harness-observed claims with
origin.kind = harness-observed. The agent cannot forge them (INV-06). The agent emits only what nothing else can observe: stated premises, rejected alternatives, assumptions carried forward. -
The claim log IS the history. Not git. Not a database. An append-only, content-addressed, revocable record. Status is computed by folding the log — never stored (INV-04). A claim with no falsification or verification against it is
unevaluated, notpassed(R5). -
The gate evaluates live.
elench gate <tree> <claims.json>is a predicate over claims, not a build (R3). Any party with the claim log and no compute can evaluate and get the same answer as one with a build farm. The verdict is not cached; it is recomputed on demand (R4, INV-14). -
Git is a projection.
elench git init <path> <claims.json>synthesizes real zlib-compressed git objects (blobs, trees, commits) from the claim log. Two parties with the same log produce byte-identical objects (BC4, INV-20). After materialization,git log,git blame, andgit checkoutwork — humans use git without knowing elench exists. -
Retroactive invalidation. A finding late in a session can falsify a claim that a shipped artifact depended on. The blast radius is the transitive
dependsOnclosure — every claim that depended on the falsified one is also falsified. No byte of code changes. No re-signing. The gate re-evaluates and the verdict flips. This is the property that justifies the project.
Why no server
Three reasons, all in docs/problem.md:
-
No daemon to maintain. Everything is derivable from the content-addressed store by a client-side binary (problem.md anti-goal). No single point of failure, no service to keep alive.
-
Independent evaluation. Two parties with the same claim log but different policies can evaluate independently. A server would either centralize evaluation (defeating R3) or require a consensus protocol (explicitly out of scope).
-
The asymmetry is enforceable without a server. The validator (
elench-claim::validate_claim) enforces all emission rules client-side: agents cannot emit harness-observed records (INV-06), only the harness emits verifications (INV-07), only humans emit residue-acceptance (INV-12). No server needed — the claim itself carriesorigin.kind, and the validator cross-checks it against the signer’s entity.
Agent integration
Agents integrate by calling elench emit after each change:
# Agent writes code, then emits a claim about what was checked
elench --store fjall /path/to/store emit claim.json
# CI (the harness) runs the build and emits provenance
elench --store fjall /path/to/store build <tree> --artifact dist.tar.gz -- make
# CI emits verification claims (test results, lint results)
elench --store fjall /path/to/store emit test-results.json
elench --store fjall /path/to/store emit lint-results.json
# Human evaluates the gate before release
elench --store fjall /path/to/store gate <tree> claims.json
# Human materializes git to review the history
elench --store fjall /path/to/store git init /tmp/review claims.json
cd /tmp/review && git log
The dogfooding pipeline (dogfooding/emit-continuous.sh) demonstrates
this: it runs cargo build, cargo test --lib, cargo clippy, and
cargo fmt --check, emitting a harness-observed claim for each. The
accumulated claims are then gated and reconciled.
What’s not built yet
- Continuous agent integration. The dogfooding pipeline emits 4
claims per CI run. A full regime would have agents emit claims on
every change to a shared fjall store. This is plumbing (call
elench emitfrom agent hooks), not architecture. - Multi-party distribution. Two parties with the same claim log can already evaluate independently. What’s missing is a protocol for distributing the claim log between parties — but that’s out of scope by design (problem.md: “Not a consensus mechanism”).
- K-of-N builder agreement. The gate checks for it (condition 4), E2 passed (same-triple divergences are cheap-to-fix), but no K-of-N agreement has been run against real builds with K>1.
System Overview
elench is an evidence layer for repositories — and the substrate that replaces git. The claim log is the primary history: a signed, append-only, revocable record of what was asserted, what was verified, and what remains unevaluated. The git CLI works because elench synthesizes git-compatible objects from the claim log on demand. Humans use git; elench is invisible.
The problem
Version control records what changed. Forges record who approved it. Neither records what was checked, to what depth, and what remains unevaluated. When agents write code at volume, there is no human head to sample and review bandwidth does not scale. The record has to become durable state or it does not exist.
See problem.md for the full requirements (R1–R7),
binding constraints (BC1–BC4), and anti-goals.
The one claim that makes this worth building
Retroactive invalidation with traceable blast radius. A finding late in a session can falsify a claim that a shipped artifact depended on, with no byte of code changing. Current supply-chain tooling signs a verdict once and freezes it. If elench is only SLSA with extra steps, abandon it.
Workspace structure
The codebase is a single Rust workspace with 8 crates:
| Crate | Role |
|---|---|
elench | Binary. CLI + git projection. Synthesizes git objects from the claim log (ADR-0002, ADR-0007). Materializes real .git/ directories. |
elench-claim | Claim data model, log-folding status computation, emission-rule validation, conflict detection. |
elench-predicate | Parser and evaluator for elench-predicate-v1 DSL (ADR-0004). Four primitives: grep, test, run, exists. |
elench-envelope | DSSE envelopes carrying in-toto statements. Ed25519 signing/verification (A1). |
elench-store | Content-addressed store: blobs, trees, claims. The substrate (ADR-0001). In-memory (default), fjall (optional, ADR-0008). |
elench-gate | Release gate evaluation — a predicate over claims, not a build. Artifact format (INV-15). |
elench-projection | Deterministic git synthesis + .git/ materialization from the claim log (ADR-0002, ADR-0007). |
elench-anchor | Multi-strategy anchor resolution: path-range, symbol, content-digest (E1: strategy=multi). Reconciliation. |
See specs/architecture/module-graph.md
for the dependency graph and specs/architecture/build-phases.md
for the implementation order (all phases COMPLETE).
Architecture diagram
┌─────────────┐
│ elench │ (binary: CLI + git projection)
│ (crates/ │
│ elench) │
└──────┬──────┘
┌────────┬─────┴──────┬─────────┐
▼ ▼ ▼ ▼
┌──────────┐ ┌──────────┐ ┌────────┐ ┌────────┐
│elench- │ │elench- │ │elench- │ │elench- │
│claim │ │envelope │ │store │ │gate │
└────┬─────┘ └──────────┘ └────────┘ └────┬───┘
│ │
│ ┌─────────────┐ │
└────┤ elench- │ │
│ predicate │ │
└─────────────┘ │
│
┌─────────────┐ ┌─────────────┐ │
│ elench- │ │ elench- │ │
│ anchor │ │ projection ├──────────┘
└──────┬──────┘ └──────┬──────┘
│ │
▼ ▼
┌──────────┐ ┌──────────┐
│elench- │ │elench- │
│store │ │store │
└──────────┘ └──────────┘
Key design decisions
- ADR-0001: elench is the substrate; the claim log is the primary history. Git is a read-only projection, not the source of truth.
- ADR-0002: Git objects are synthesized deterministically from the claim log. Two parties with the same log produce byte-identical objects.
- ADR-0003: DSSE envelopes carrying in-toto statements. Agent claims and build provenance share the same signing path.
- ADR-0004: A small DSL of check primitives (grep, test, run, exists). Not Turing-complete. Gated by E0 (ratio 0.72).
- ADR-0005: Implementation substrate — Rust, content-addressed store. elench owns its own storage; no git dependency underneath.
- ADR-0006: AGENTS.md emission rules are enforced by a validator. All MUST rules are implemented; prose gates are now real gates.
- ADR-0007: One commit per tree-changing claim. Deterministic author/committer/timestamp derivation.
- ADR-0008: Fjall as the persistent content-addressed backend.
In-memory by default;
--store fjall <path>enables persistence.
See specs/architecture/adr/ for all
ADRs (0001–0008).
Problem statement
Derived from the specific situation below. Nothing here is inherited from prior designs. Where a familiar pattern appears (append-only logs, signed envelopes, content addressing) it is because a requirement below forces it, and the forcing requirement is named. If a requirement is removed, re-derive rather than keep the pattern.
Situation
- Agents produce code faster than review capacity absorbs it.
- VCS records tree state and authorship. The author field no longer identifies a responsible party — it names whichever key the agent held.
- Verification depth is not recorded anywhere. A passing test suite and an absent test suite are indistinguishable in the repository.
- Failures carry information that is discarded entirely. Nineteen rejected approaches vanish; the twentieth is merged with no record of what constrained it.
- A conclusion reached early can be invalidated by a finding reached late. No layer in the current stack represents this.
Requirements
Each is stated so it can be checked against an implementation.
R1 — Revocability without tree mutation. A claim’s status must be changeable by appending a new record. No code changes, no history rewrite. The prior status must remain visible, not be overwritten. Forces: stable claim identity; append-only log; status as a computed function of the log rather than a stored field.
R2 — Origin is a type, not a label.
Evidence the harness observed (a test exited 0; a gate transition
fired) and evidence an agent asserted (this input can be empty) must be
structurally distinguishable and must never be merged into one status.
Forces: origin.kind is required; policy predicates may discriminate
on it; agents cannot emit harness-observed records (see AGENTS.md).
R3 — Gate evaluable without build capability. A party with the claim log and no compute must be able to evaluate the release predicate and get the same answer as anyone else. Forces: separation of gate (cheap, deterministic, over claims) from build (expensive, over trees). Rules out embedding build execution in the gate.
R4 — Status is re-checkable after release. An artifact’s acceptability must be a live evaluation against the current claim log, not a signature frozen at release time. Forces: artifacts carry a pointer to an evaluable policy + tree, not a verdict. Consumers re-check.
R5 — unevaluated is a first-class status.
Distinct from passed and from failed. Brownfield code is
overwhelmingly unevaluated and a system that cannot say so is unusable
on real repositories.
Forces: three-valued minimum; policies must be able to permit bounded
unevaluated residue with a named signer accepting it.
R6 — Git is a projection, not the substrate. The claim log is the primary history. The git CLI works because elench synthesizes git-compatible objects from the claim log — deterministically, so two parties with the same log produce byte-identical git objects. Humans use git; elench is invisible. Forces: deterministic synthesis (BC4); elench owns the content-addressed store; git is a read-only view, never a write path.
R7 — Composability with existing supply-chain attestation. Agent claims and build provenance must be the same kind of object so they share a signing path, a store, and a verification library. Forces: in-toto statements in DSSE envelopes. See ADR-0003.
Anti-goals
- Do not capture reasoning. Prompts and rationale are justification. Capturing them is a different, already-occupied product. Mixing them in makes every claim look supported.
- Do not log all attempts. Most failures are typos. Only failures that changed a claim’s status are recorded. This is the filter; without it the corpus is noise with a schema.
- Do not build a merge algorithm. Concurrent-edit resolution is being worked elsewhere (CoAgent, STORM, CodeCRDT). elench records what was verified; it does not arbitrate who writes. A merge result is a new tree + new claims; the resolution itself is external.
- Do not require a daemon. Everything is derivable from the content-addressed store by a client-side binary. The git projection is a helper or a filesystem, not a service.
Binding constraints
These gate the entire approach. Each has a pre-registered experiment. If any fails, the corresponding part of the design is dead and no amount of engineering recovers it.
BC1 — Predicate ratio.
Fraction of extracted claims expressible as machine-checkable
predicates rather than prose annotations. Prose does not gate. If the
ratio is low enough, elench is an expensive search index over agent
regret.
Experiment: experiments/E0-predicate-ratio.md. Run this first.
BC2 — Anchor survival.
Fraction of claims whose anchor still identifies the intended code
after N subsequent tree states including at least one rebase and one
rename. If anchors rot, revocation targets the wrong code and the
blast radius is fiction.
Experiment: experiments/E1-anchor-survival.md.
BC3 — Hermeticity.
K-of-N independent builder agreement requires bit-reproducible builds.
Without it the release gate degrades to a single signature and R3’s
independent evaluation buys nothing at the artifact layer.
Experiment: experiments/E2-build-reproducibility.md.
BC4 — Deterministic synthesis.
The git projection must produce byte-identical objects on different
machines from the same claim log. If synthesis is non-deterministic,
two parties’ git views disagree and R6 fails. The forcing requirements
are: deterministic OID derivation, deterministic author/committer
strings, deterministic timestamp derivation (not wall clock), and
deterministic tree ordering.
No experiment. This is prior art — git hash-object, git commit-tree, and git mktree are deterministic by construction. The
risk is in the derivation mapping (which claim becomes which commit),
not in git’s object format. Addressed in ADR-0007.
Open questions
All three original open questions are now resolved. Details below.
-
Does the claim log converge, or does it grow without bound on an active repository? No pruning story exists. Compaction may violate R1.Resolved (A-A10). Compaction is a manual, destructive operator action.elench log <claims.json>provides statistics (total, kind distribution, status distribution, noise ratio, dependsOn density) andelench compact <claims.json> --before <ts>retires all claims before the cut-off, freezing their statuses as a snapshot. The compaction record carries frozen statuses forward. Active claims continue to be revocable (R1 preserved for active claims, deliberately violated for retired ones). -
Who signs the residue acceptance under R5, and what stops it becoming a rubber stamp?Resolved (A-A11).elench review <tree> <claims.json>shows all unevaluated claims with their content (form, language, source, producer). The human must name each gap beforeelench acceptissues a residue-acceptance. This adds real friction without multi-party complexity. -
If two agents assert contradictory predicates and neither is falsified, what is the tree’s status?Resolved (A-A12). Last-writer-wins (by timestamp). The conflict is detected and reported byelench conflicts <tree> <claims.json>. The gate evaluates against the winning predicate and includes the conflict as a warning (not a failure — the winning predicate still gates). The human is expected to resolve: falsify one or both predicates. Partial block: only the affected path (same anchor) is blocked by the conflict; other paths evaluate normally. -
What is the granularity of a git-projection commit? Answered by ADR-0007: one commit per tree-changing claim. The density risk (too verbose for human consumption) is accepted as A-A09; a session-level aggregation view may be added later.
Anchoring
Status: E1 PASSED. Multi-strategy (path-range, symbol,
content-digest) implemented in elench-anchor.
The problem
A claim points at code. Code moves. If the pointer rots, then:
- revocation propagates to the wrong lines, and the blast radius is fiction;
unevaluatedresidue is miscounted in both directions;- the whole log degrades into per-file gossip.
This is the same problem as making review comments survive a rebase, which forges have not solved well in twenty years. Assume it is hard. Do not assume a clever hash fixes it.
In elench, a “tree” is a content-addressed tree state in the store (ADR-0001), not a git commit. Anchors point at elench tree OIDs. The git projection (ADR-0002) is irrelevant to anchoring — anchors resolve in elench-native space.
Strategies
Path + line range. Trivial to compute, rots on the first reformat. Baseline for E1, not a proposal.
Symbol identity. Language-server qualified name. Survives reformatting and line motion; dies on rename, and rename is the single most common refactor an agent performs. Requires a language server per language, which is a large dependency surface for a tool that owns its own store.
Normalised content digest. Digest of the anchored span after whitespace/comment normalisation. Survives motion and rename; dies on any semantic edit, which is arguably correct — an edited span should invalidate claims about it. The failure is the opposite direction: a claim about an invariant survives an edit that preserves the invariant, and content digest kills it anyway. High false-revocation rate.
Multi-strategy with confidence. Record all three; resolve by agreement;
report an anchor as degraded when strategies disagree rather than silently
picking one. Costs more storage and introduces a fourth status
(anchor-degraded) that policy has to handle.
E1 Result
All three strategies are USABLE (correct ≥ 85%, wrong ≤ 2%).
Proceed with multi. See experiments/E1-anchor-survival-result.md for
details.
Implementation
elench-anchor (crates/elench-anchor/src/lib.rs) implements:
resolve(anchor, &dyn StoreBackend)— tries all three strategies by actually traversing the tree in the store. ReturnsCorrect(all agree),Degraded(disagreement),Failed(all fail), orWrongResolution.reconcile(tree, log, &dyn StoreBackend)— for each claim anchored to the tree, resolves the anchor and reports drifted claims. CLI:elench reconcile <tree> <claims.json>.
Rejected
- Anchoring to the tree only, not to a span. Removes the problem by removing the capability. A claim scoped to a whole tree cannot support blast-radius tracing, which is R1’s reason to exist.
- Requiring agents to re-anchor on every tree change. Puts the audited party in charge of whether its own claims still apply. Violates the AGENTS.md asymmetry directly.
Release Policy
The gate is a predicate over claims. The build is a separate, expensive function of a tree. Conflating them is what makes a green check mean “some machine you don’t control ran something.” Keeping them apart is what lets a party with no compute reach the same verdict as one with a build farm (R3).
Shape
Release of artifact digest D from tree T under policy P holds when all
of the following are true at evaluation time:
- No falsified premise. No claim in the transitive
dependsOnclosure rooted atT’s claim set has statusfalsified. - Bounded residue. Claims with status
unevaluatedare withinP’s allowance, and each excess is covered by aresidue-acceptancerecord signed by a keyPnames. - Origin floor. Claims that
Pdesignates load-bearing haveorigin.kind = harness-observed. Agent-asserted claims may inform, butPshould not let them alone carry a release. - Builder agreement. K independent producers have signed statements with
subject
Dfor treeT, each meetingP’shermeticityfloor.
Condition 4 is where “true artifact” actually lives, and it is the expensive one. Available — E2 passed (same-triple divergences all cheap-to-fix; K-of-N agreement is per target triple).
Evaluation is live, not frozen
The artifact carries a pointer to (T, P), not a verdict. Consumers
re-evaluate. If a load-bearing claim is falsified after release, the artifact’s
status changes with no byte moving and no re-signing — the property from
README that justifies the project. T is an elench tree OID
(ADR-0001), not a git commit. The git projection (ADR-0002) is not
consulted at evaluation time.
This is certificate-revocation shaped and inherits its problems: consumers who never re-check are unprotected, and there is no push path. Do not pretend otherwise in the docs.
Artifact format
The artifact is serialized as JSON and validated against
schema/artifact.schema.json. Fields:
version— format version (current:"0.1"). Consumers SHOULD reject unknown major versions.tree— elench tree OID (64 hex chars).policy— policy name under which the artifact was released.digest— SHA-256 digest of the artifact (binary, container image).released_at— Unix epoch seconds. NOT a verdict.description— optional human-readable description.
No verdict field. No pass/fail. The artifact is a pointer; the consumer re-evaluates.
Deliberately not specified
- What K should be. Depends on how many independent builders exist, which is an organisational fact, not a design one.
- Cross-party reconciliation. Two evaluators with different
Preaching different verdicts is correct behaviour, not a bug. Out of scope. - Emergency override. Every real system grows one. Specifying it now would be guessing; leaving it unspecified means it will be added badly under pressure. Flagged, not resolved.
Operations
Operational reference for elench.
Durability
elench’s claim log is append-only (INV-01). The in-memory store
(default) does not persist across process restarts. The fjall backend
(--store fjall <path>) persists claims, blobs, and trees to disk.
Default (in-memory)
| Operation | Durability |
|---|---|
elench emit | Claim stored in memory; lost on process exit |
elench gate | Live evaluation; no persistence needed |
elench git init | Writes real git objects to disk (zlib-compressed) |
Fjall backend
| Operation | Durability |
|---|---|
elench --store fjall <path> emit | Claim persisted to disk (SyncAll) |
elench --store fjall <path> store blob | Blob persisted to disk (Buffer) |
elench --store fjall <path> store tree | Tree persisted to disk (Buffer) |
Claims use PersistMode::SyncAll (must survive crashes). Blobs and
trees use PersistMode::Buffer (content-addressed, can be recomputed
from source).
Compaction
The claim log grows without bound on an active repository. Compaction is manual and destructive:
elench compact <claims.json> --before <timestamp>
Retires all claims before the cut-off, freezing their statuses. The compaction record carries the frozen status snapshot forward. Active claims continue to be revocable (R1 preserved for active claims, deliberately violated for retired ones).
Reconciliation
After a tree change (rename, reformat, semantic edit), claims may no longer resolve to the correct code. The reconciliation pass detects this:
elench reconcile <tree_oid> <claims.json>
For each claim anchored to the tree, resolves the anchor using the multi strategy (path-range, symbol, content-digest). Claims that fail to resolve or are degraded are reported as drifted. The reconciliation pass is read-only — it does not auto-fix. The human (or agent) must re-anchor or falsify drifted claims.
Conflict detection
Two predicates are a conflict if and only if they anchor to the same code location (same path+range, or same symbol) but assert different expressions. Last-writer-wins by timestamp; the older claim is flagged for resolution.
elench conflicts <tree_oid> <claims.json>
Build provenance
elench build <tree_oid> [--artifact <path>] -- <command...>
Runs the build command, captures the exit code, and computes a
SHA-256 digest. With --artifact <path>, the digest is SHA-256 of
that file (the real build output). Without it, the digest falls back
to SHA-256 of stdout. Emits a build provenance claim with
origin.kind = harness-observed (INV-22).
Module Graph
Derived from the domain model (bounded contexts) and the ADR log. Each crate maps to one or more bounded contexts. Dependencies are acyclic.
┌─────────────┐
│ elench │ (binary: CLI + git projection)
│ (crates/ │
│ elench) │
└──────┬──────┘
┌────────┬─────┴──────┬─────────┐
▼ ▼ ▼ ▼
┌──────────┐ ┌──────────┐ ┌────────┐ ┌────────┐
│elench- │ │elench- │ │elench- │ │elench- │
│claim │ │envelope │ │store │ │gate │
└────┬─────┘ └──────────┘ └────────┘ └────┬───┘
│ │
│ ┌─────────────┐ │
└────┤ elench- │ │
│ predicate │ │
└─────────────┘ │
│
┌─────────────┐ │
│ elench- │ │
│ projection ├────────────────────────────┘
└──────┬──────┘
│
▼
┌──────────┐
│elench- │
│store │
└──────────┘
Crates
| Crate | Path | Bounded context | Role |
|---|---|---|---|
elench | crates/elench | CLI, Git Projection | Binary. Reads/writes store, verifies envelopes, evaluates predicates, computes closures, synthesizes git projection. |
elench-claim | crates/elench-claim | Claim Emission, Claim Evaluation | Data model matching schema/claim.schema.json, log-folding status computation, emission-rule validation. |
elench-predicate | crates/elench-predicate | Predicate Evaluation | Parser and evaluator for elench-predicate-v1 DSL (ADR-0004). Four primitives: grep, test, run, exists. |
elench-envelope | crates/elench-envelope | Envelope Verification | DSSE envelope signing/verification, in-toto statement handling, signer/producer distinction. |
elench-store | crates/elench-store | elench Store | Content-addressed store: blobs, trees, claims. The substrate (ADR-0001). In-memory (default), fjall (optional, ADR-0008). |
elench-gate | crates/elench-gate | Release Gating | Release policy evaluation: four conditions from docs/release-policy.md. |
elench-projection | crates/elench-projection | Git Projection | Deterministic synthesis of git-compatible objects from the claim log (ADR-0002, ADR-0007). |
Dependencies
| From | To | Why |
|---|---|---|
elench | elench-claim | Claim data model |
elench | elench-envelope | Envelope signing/verification |
elench | elench-store | Content-addressed storage |
elench | elench-gate | Release gate evaluation |
elench | elench-predicate | Predicate validation |
elench | elench-projection | Git projection |
elench-envelope | elench-claim | Claim type (sign/verify) |
elench-store | elench-claim | Claim type (store/read) |
elench-gate | elench-claim | Status computation (log fold) |
elench-projection | elench-claim | Claim types |
elench-projection | elench-store | Store (read trees) |
No cycles. elench-claim is the sole leaf — it depends on nothing in
the workspace. elench-predicate depends on nothing in the workspace
(regex is external). elench-envelope, elench-store, and
elench-gate all depend on elench-claim. elench-projection
depends on elench-claim and elench-store. The binary depends on
all six library crates.
Deferred
| Crate | Why deferred |
|---|---|
elench-anchor | E1 PASSED (strategy=multi), but crate not yet created. Anchor object in schema/claim.schema.json uses strategy=multi by default. |
API Contracts
Interfaces between crates. Each contract is the minimal surface that satisfies the spec. No implementation exists yet; these are the targets the implementer builds toward.
elench-claim
Types
#![allow(unused)]
fn main() {
// Claim kind (from schema/claim.schema.json)
pub enum ClaimKind {
Assertion,
Falsification,
Verification,
Supersession,
ResidueAcceptance,
}
// Assertion form
pub enum AssertionForm {
Predicate { expression: Expression },
Annotation { text: String },
}
// Expression (language undecided — ADR-0004)
pub struct Expression {
pub language: String,
pub source: String,
pub digest: Option<String>,
}
// Origin
pub struct Origin {
pub kind: OriginKind,
pub producer: Producer,
}
pub enum OriginKind {
HarnessObserved,
AgentAsserted,
HumanAsserted,
}
pub struct Producer {
pub id: String,
pub session_id: Option<String>,
pub hermeticity: Option<Hermeticity>,
}
pub enum Hermeticity {
None,
Container,
Vm,
HermeticDerivation,
}
// Claim identifier. SHA-256 hash with `cl_` prefix (67 chars total).
// Pattern: ^cl_[0-9a-f]{64}$. Never reassigned (R1, INV-03).
pub struct ClaimId(String);
// Claim (aggregate root)
pub struct Claim {
pub id: ClaimId,
pub kind: ClaimKind,
pub target: Vec<ClaimId>,
pub assertion: Assertion,
pub origin: Origin,
pub anchor: Anchor,
pub timestamp: i64,
pub evidence: Vec<Evidence>,
pub depends_on: Vec<ClaimId>,
}
// Computed status (not stored)
pub enum ClaimStatus {
Unevaluated,
Passed,
Falsified,
}
}
Functions
#![allow(unused)]
fn main() {
/// Compute a claim's status by folding the log.
/// INV-04: pure function, no stored status.
pub fn compute_status(claim_id: &ClaimId, log: &[Claim]) -> ClaimStatus;
/// Compute the transitive dependsOn closure (blast radius).
pub fn blast_radius(claim_id: &ClaimId, log: &[Claim]) -> Vec<ClaimId>;
/// Identity of the key that signed the DSSE envelope, with its known entity type.
/// The validator cross-checks this against claim.origin.kind to prevent forgery.
pub struct SignerIdentity {
pub key_id: String,
pub entity: SignerEntity,
}
pub enum SignerEntity {
Harness,
Agent,
Human,
}
/// Validate a claim against emission rules (AGENTS.md).
/// INV-05: origin.kind required.
/// INV-06: reject if signer is agent but origin.kind = harness-observed.
/// INV-07: reject if signer is not harness but kind = verification.
/// INV-08: reject form=predicate without expression.
/// INV-11: reject falsification that changes no status (requires log).
/// INV-12: reject if signer is not human but kind = residue-acceptance.
pub fn validate_claim(claim: &Claim, signer: &SignerIdentity, log: &[Claim]) -> Result<(), ValidationError>;
}
elench-envelope
Functions
#![allow(unused)]
fn main() {
/// Sign a claim payload in a DSSE envelope.
pub fn sign(claim: &Claim, signing_key: &SigningKey) -> Envelope;
/// Verify a DSSE envelope's signature and extract the claim.
/// INV-22: same format as build provenance.
pub fn verify(envelope: &Envelope) -> Result<Claim, EnvelopeError>;
}
elench-store
Types
#![allow(unused)]
fn main() {
/// Content address of a blob, tree, or claim.
/// Blobs and trees: SHA-256 hash (64 hex chars, no prefix), identical to git SHA-256 OIDs.
/// Claims: `cl_` prefix + SHA-256 hash (see ClaimId).
/// The git projection is a passthrough for blobs and trees; only commits are synthesized.
pub struct Oid(String);
/// A blob: content-addressed byte array.
pub struct Blob {
pub oid: Oid,
pub data: Vec<u8>,
}
/// A tree entry: name + mode + OID, exactly like git.
pub struct TreeEntry {
pub name: String,
pub mode: u32,
pub oid: Oid,
pub kind: TreeEntryKind,
}
pub enum TreeEntryKind {
Blob,
Tree,
}
/// A tree: sorted entries, content-addressed. Hierarchical — each
/// directory is a separate tree object. Serialization matches git's
/// tree object format, making OIDs identical.
pub struct Tree {
pub oid: Oid,
pub entries: Vec<TreeEntry>,
}
}
Functions
#![allow(unused)]
fn main() {
/// Store a claim in the content-addressed store.
/// INV-01: append-only, never updates.
/// INV-18: elench owns the store, no git underneath.
pub fn store_claim(claim: &Claim, store: &Store) -> Result<Oid, StoreError>;
/// Store a blob.
pub fn store_blob(data: &[u8], store: &Store) -> Result<Oid, StoreError>;
/// Store a tree.
pub fn store_tree(tree: &Tree, store: &Store) -> Result<Oid, StoreError>;
/// Read all claims from the store.
pub fn read_all_claims(store: &Store) -> Result<Vec<Claim>, StoreError>;
/// Read claims for a specific tree (by elench tree OID).
pub fn read_claims_for_tree(tree: &Oid, store: &Store) -> Result<Vec<Claim>, StoreError>;
/// Read a tree by OID.
pub fn read_tree(tree: &Oid, store: &Store) -> Result<Tree, StoreError>;
/// Read a blob by OID.
pub fn read_blob(blob: &Oid, store: &Store) -> Result<Vec<u8>, StoreError>;
}
elench-gate
Functions
#![allow(unused)]
fn main() {
/// Evaluate the release gate for a tree under a policy.
/// INV-13: evaluable without build capability.
/// INV-14: live evaluation, not frozen.
/// `tree` is an elench tree OID, not a git commit.
pub fn evaluate(
tree: &Oid,
policy: &Policy,
log: &[Claim],
) -> Result<Verdict, GateError>;
/// The four conditions from docs/release-policy.md.
/// Condition 4 (builder agreement) is unavailable unless E2 passes.
pub struct Verdict {
pub result: VerdictResult,
pub reasons: Vec<String>,
pub tree: Oid,
pub policy: String,
}
pub enum VerdictResult {
Pass,
Fail,
}
}
elench (binary)
The CLI wires the libraries together. No public API — it is a binary. Commands (not yet implemented):
elench emit— create and sign a claim, store in the content-addressed storeelench verify— verify an envelope and validate the claimelench status— compute a claim’s status by folding the logelench gate— evaluate the release gate for a treeelench blast— compute the blast radius from a claimelench git— materialize the git projection (ADR-0002, ADR-0007)
Enforcement Map
For each invariant, where it is enforced. All 28 invariants are
ENFORCED (code exists and tests fail if violated). INV-15 was
upgraded from FUTURE to MOCK — the artifact now carries a version
field and schema/artifact.schema.json defines the format.
Revocability and status (R1)
| INV | Enforcement point | Status |
|---|---|---|
| INV-01: Append, not modify | elench-store::store_blob/tree/claim — idempotent, no update (MemoryStore + FjallStore) | ENFORCED |
| INV-02: Prior status visible | elench-claim::compute_status — fold reads all records | ENFORCED |
| INV-03: Claim identity stable | elench-claim::ClaimId — content address, immutable | ENFORCED |
| INV-04: Status computed, not stored | elench-claim::compute_status — pure function | ENFORCED |
| INV-28: Claim OID is content hash | elench-claim::ClaimId::from_content — SHA-256 of canonical JSON | ENFORCED |
| INV-29: dependsOn acyclic | elench-claim::validate_claim — DFS cycle detection over log | ENFORCED |
Origin typing (R2, AGENTS.md)
| INV | Enforcement point | Status |
|---|---|---|
| INV-05: origin.kind required | elench-claim — type system, OriginKind non-optional | ENFORCED |
| INV-06: No harness-observed from agents | elench-claim::validate_claim — cross-checks signer.entity against origin.kind | ENFORCED |
| INV-07: Only harness emits verification | elench-claim::validate_claim — cross-checks signer.entity against kind | ENFORCED |
| INV-08: Predicate requires expression | elench-claim::validate_claim — calls elench-predicate::parse | ENFORCED |
| INV-09: Annotations never read by policy | elench-gate::evaluate — filters on form=predicate, skips annotations | ENFORCED |
| INV-11: Failure recorded only when status changed | elench-claim::validate_claim — checks target status in log | ENFORCED |
| INV-12: No residue-acceptance from agents | elench-claim::validate_claim — cross-checks signer.entity against kind | ENFORCED |
Gate and release (R3, R4)
| INV | Enforcement point | Status |
|---|---|---|
| INV-13: Gate without build | elench-gate::evaluate — takes &[Claim], no build calls | ENFORCED |
| INV-14: Artifact acceptability is live evaluation | elench-gate::evaluate — called on demand, no cached verdict | ENFORCED |
| INV-15: Artifact carries (tree, policy), not verdict | elench-gate::Artifact — version, tree, policy, digest, released_at; schema/artifact.schema.json; no verdict field | ENFORCED (MOCK) |
Unevaluated (R5)
| INV | Enforcement point | Status |
|---|---|---|
| INV-16: unevaluated first-class | elench-claim::ClaimStatus::Unevaluated | ENFORCED |
| INV-17: Bounded residue with acceptance | elench-gate::evaluate — condition 2, residue-acceptance records | ENFORCED |
Substrate and projection (R6, ADR-0001, ADR-0002, ADR-0007)
| INV | Enforcement point | Status |
|---|---|---|
| INV-18: elench owns content-addressed store | elench-store — no git dependency, owns storage; MemoryStore (default) + FjallStore (optional, ADR-0008) | ENFORCED |
| INV-19: Git projection is read-only | elench-projection::synthesize — takes &dyn StoreBackend, no writes; elench-projection::materialize — writes to filesystem, not to store | ENFORCED |
| INV-20: Git synthesis deterministic | elench-projection — proptest_inv_20_synthesis_deterministic + proptest_inv_20_synthesis_order_independent | ENFORCED |
| INV-21: Git projection no side effects | elench-projection — scenario_inv19_projection_does_not_write_to_store | ENFORCED |
| INV-25: Content addressing (SHA-256) | elench-store::Oid::from_blob_data/from_tree_entries + deserialize_tree_bytes round-trip; elench-claim::ClaimId::from_content; FjallStore::read_tree round-trip (feature tier) | ENFORCED |
| INV-26: Store is sole source of truth | elench-store — all views derive from store; `–store memory | fjall |
| INV-27: Git projection is lossy, not authoritative | elench-projection — scenario_inv27_projection_is_lossy | ENFORCED |
Supply-chain composability (R7, ADR-0003)
| INV | Enforcement point | Status |
|---|---|---|
| INV-22: DSSE/in-toto shared format | elench-envelope::sign / verify; PREDICATE_TYPE_AGENT; Ed25519 signatures (A1) | ENFORCED |
Predicate language (ADR-0004)
| INV | Enforcement point | Status |
|---|---|---|
| INV-23: Expressions executable/deterministic/sandboxable | elench-predicate — 4 primitives (grep, test, run, exists), not Turing-complete | ENFORCED |
Validator (ADR-0006)
| INV | Enforcement point | Status |
|---|---|---|
| INV-24: AGENTS.md rules enforced | elench-claim::validate_claim — implemented, all rules enforced | ENFORCED |
Conflict detection
| Function | Enforcement point | Status |
|---|---|---|
elench_claim::detect_conflicts | Same-anchor, different expression — crates/elench-claim/src/lib.rs; 8 unit tests + 4 CLI tests | ENFORCED |
Error Taxonomy
Error types by crate, with the invariant or failure mode each addresses.
Library code uses thiserror; the binary may use anyhow.
Error categories
| Category | Meaning | Caller action |
|---|---|---|
| Permanent | Cannot succeed; data loss, corruption, or configuration error | Report to user/admin; do not retry |
| Retriable | Transient failure (I/O, network); may succeed on retry | Retry with backoff |
| Security | Authentication or authorization failure | Deny and audit |
| Validation | Claim or envelope rejected by emission rules | Agent reformulates and re-emits |
elench-claim
#![allow(unused)]
fn main() {
#[derive(Debug, thiserror::Error)]
pub enum ValidationError {
#[error("origin.kind is required")]
MissingOriginKind, // INV-05 — Validation
#[error("agents cannot emit harness-observed records")]
AgentEmitsHarnessObserved, // INV-06 — Security
#[error("only the harness may emit verification records")]
NonHarnessEmitsVerification, // INV-07 — Security
#[error("predicate claims require an executable expression")]
PredicateWithoutExpression, // INV-08 — Validation
#[error("only humans may emit residue-acceptance records")]
NonHumanEmitsResidueAcceptance, // INV-12 — Security
#[error("residue-acceptance must name specific gaps (non-empty target)")]
ResidueAcceptanceWithoutTargets, // INV-12 — Validation
#[error("dependsOn is empty — claim asserts it was reached from nothing (warning)")]
EmptyDependsOn, // GUIDELINE (was INV-10, downgraded) — Validation
#[error("cyclic dependency detected: {0}")]
CyclicDependency(String), // INV-29 — Permanent
#[error("schema validation failed: {0}")]
SchemaViolation(String), // general — Validation
}
#[derive(Debug, thiserror::Error)]
pub enum StatusError {
#[error("claim {0} not found in log")]
ClaimNotFound(String), // Permanent
#[error("log is corrupt: {0}")]
CorruptLog(String), // Permanent
}
}
elench-envelope
#![allow(unused)]
fn main() {
#[derive(Debug, thiserror::Error)]
pub enum EnvelopeError {
#[error("invalid signature")]
InvalidSignature, // Security
#[error("unknown signer: {0}")]
UnknownSigner(String), // Security
#[error("no signature present")]
NoSignature, // Validation
#[error("invalid payload: {0}")]
InvalidPayload(String), // Validation
#[error("unsupported predicateType: {0}")]
UnsupportedPredicateType(String), // Validation
#[error("malformed envelope: {0}")]
MalformedEnvelope(String), // Validation
#[error("invalid key: {0}")]
InvalidKey(String), // Validation
}
}
elench-store
#![allow(unused)]
fn main() {
#[derive(Debug, thiserror::Error)]
pub enum StoreError {
#[error("invalid OID: {0}")]
InvalidOid(String), // Validation
#[error("object already exists with different content: {oid} ({reason})")]
ObjectExists { oid: String, reason: String }, // INV-01 — Permanent
#[error("content addressing violation: {oid} ({reason})")]
ContentAddressingViolation { oid: String, reason: String }, // INV-25 — Permanent
#[error("object not found: {0}")]
ObjectNotFound(String), // Permanent
#[error("store is corrupt: {0}")]
CorruptStore(String), // Permanent
#[error("I/O error")]
Io, // Retriable (wraps std::io::Error)
}
}
elench-gate
#![allow(unused)]
fn main() {
#[derive(Debug, thiserror::Error)]
pub enum GateError {
#[error("falsified premise in blast radius: {0}")]
FalsifiedPremise(String), // release-policy condition 1 — Permanent
#[error("unbounded residue: {0} > {1}")]
UnboundedResidue(usize, usize), // release-policy condition 2 — Permanent
#[error("origin floor not met for claim: {0}")]
OriginFloorNotMet(String), // release-policy condition 3 — Security
#[error("builder agreement not met: {0} < {1}")]
BuilderAgreementNotMet(usize, usize), // release-policy condition 4 — Permanent
#[error("policy evaluation failed: {0}")]
PolicyEvaluationFailed(String), // general — Permanent
}
}
elench-anchor
#![allow(unused)]
fn main() {
#[derive(Debug, thiserror::Error)]
pub enum AnchorError {
#[error("anchor has no path (required for path-range strategy)")]
NoPath, // Validation
#[error("anchor has no symbol (required for symbol strategy)")]
NoSymbol, // Validation
#[error("anchor has no content digest (required for content-digest strategy)")]
NoContentDigest, // Validation
#[error("anchor strategy is not multi: {0:?}")]
NotMulti(AnchorStrategy), // Validation
#[error("invalid tree OID: {0}")]
InvalidTreeOid(String), // Validation
}
}
elench-projection
#![allow(unused)]
fn main() {
#[derive(Debug, thiserror::Error)]
pub enum ProjectionError {
#[error("claim log is empty — nothing to project")]
EmptyLog, // Permanent
#[error("claim {0} has no anchor — cannot determine tree")]
NoAnchor(String), // Permanent
#[error("store error: {0}")]
Store(String), // Retriable (wraps StoreError)
}
#[derive(Debug, thiserror::Error)]
pub enum MaterializeError {
#[error("I/O error: {0}")]
Io(#[from] std::io::Error), // Retriable
#[error("store error: {0}")]
Store(String), // Retriable
#[error("blob {0} not found in store")]
BlobNotFound(String), // Permanent
#[error("tree {0} not found in store")]
TreeNotFound(String), // Permanent
#[error("projection has no commits — nothing to materialize")]
NoCommits, // Permanent
}
}
elench-predicate
#![allow(unused)]
fn main() {
#[derive(Debug, thiserror::Error)]
pub enum ParseError {
#[error("unexpected end of input")]
UnexpectedEof, // Validation
#[error("unexpected token: {0}")]
UnexpectedToken(String), // Validation
#[error("invalid regex: {0}")]
InvalidRegex(#[from] regex::Error), // Validation
#[error("expected {expected}, found {found}")]
Expected { expected: String, found: String }, // Validation
#[error("empty expression")]
Empty, // Validation
}
#[derive(Debug, thiserror::Error)]
pub enum EvalError {
#[error("expected bool, got {0:?}")]
ExpectedBool(Value), // Validation
#[error("expected int, got {0:?}")]
ExpectedInt(Value), // Validation
#[error("expected str, got {0:?}")]
ExpectedStr(Value), // Validation
#[error("field '{0}' not available on this expression")]
InvalidField(String), // Validation
#[error("I/O error reading {path}: {err}")]
Io { path: String, err: std::io::Error }, // Retriable
#[error("command failed to execute: {0}")]
CommandExec(String), // Permanent
#[error("unknown field: {0}")]
UnknownField(String), // Validation
#[error("invalid regex: {0}")]
InvalidRegex(#[from] regex::Error), // Validation
}
}
Error handling principles
-
Fail closed. If the gate cannot evaluate, the verdict is
fail, notpass. An unevaluated claim is NOT a passing claim. -
No silent corruption. A corrupt store yields
StoreError::CorruptStoreand marks all unreadable claims asunevaluated. It does not guess. -
Append-only is a store invariant, not a recovery mechanism.
StoreError::ContentAddressingViolationprevents overwriting; it does not provide conflict resolution. -
Agent emission errors are rejection, not retry. The validator rejects; the agent reformulates and re-emits. There is no partial acceptance.
-
Builder agreement unavailability is explicit. The gate reports it as a named condition failure, not a silent degradation to single signature.
-
Projection errors are loud. Non-deterministic synthesis (ProjectionError) is a P1 failure that breaks R6. Write-through-git is an explicit rejection, not a silent no-op.
-
Materialization errors are categorised. I/O errors are retriable; missing blobs/trees are permanent. The caller knows which to retry and which to report.
Build Phases
Implementation order derived from the dependency graph. Each phase depends only on earlier phases. All phases (0–5) are COMPLETE. E0, E1, E2 all PASSED.
Phase 0 — Validator [COMPLETE]
Crate: elench-claim (validation portion only)
The validator enforces the AGENTS.md emission rules (INV-05 through INV-09, INV-11, INV-12, INV-24; INV-10 is a guideline warning, not a rejection).
- Claim schema validation (against
schema/claim.schema.json) - Origin.kind enforcement (INV-05, INV-06, INV-07, INV-12)
- Predicate enforcement (INV-08)
- dependsOn population warning (guideline, was INV-10 — warning, not rejection)
- Failure recording rule (INV-11)
Gating: E0 PASSED (0.72). ADR-0004 ACCEPTED (elench-predicate-v1).
Phase 1 — Content-addressed store and claim data model [COMPLETE]
Crates: elench-store (full), elench-claim (full)
- Content-addressed storage: blobs, trees, claims (ADR-0001)
- Claim types matching
schema/claim.schema.json - Status computation by folding (INV-01 through INV-04)
- Blast radius computation (transitive dependsOn closure)
- Append-only enforcement (INV-01)
- No git dependency, no daemon (INV-18)
- Persistent backend: fjall (optional feature, ADR-0008)
Depends on: Phase 0 (validator exists and passes).
Phase 2 — Envelope handling [COMPLETE]
Crate: elench-envelope
- DSSE envelope signing and verification
- in-toto statement handling
- Signer/producer distinction (INV-22)
- Integration with content-addressed storage (store only verified envelopes)
Depends on: Phase 1 (claim types and store exist).
Phase 3 — Release gate [COMPLETE]
Crate: elench-gate
- Four conditions from
docs/release-policy.md:- No falsified premise (uses blast radius from Phase 1)
- Bounded residue with acceptance (INV-17)
- Origin floor (uses origin from Phase 1)
- Builder agreement (available — E2 PASSED; hermeticity floor enforced)
- Gate evaluation without build capability (INV-13)
- Annotation filtering — annotations never contribute to gate verdict (INV-09)
- Live evaluation, no cached verdict (INV-14, INV-15)
Depends on: Phase 1 (claim status, blast radius), Phase 2 (envelope verification for residue-acceptance records).
Phase 4 — Git projection [COMPLETE]
Crate: elench-projection
- Deterministic commit synthesis from the claim log (ADR-0002, ADR-0007, BC4)
git logshows commits derived from tree-changing claimsgit blamemaps lines to the claims that introduced them- Read-only: no write-through-git (INV-19, INV-21)
- Two-party determinism test: same claim log → byte-identical git objects (INV-20)
- Projection is lossy (INV-27): claim status, origin, blast radius NOT recoverable from git objects
Depends on: Phase 1 (store, claim log), Phase 2 (envelope verification for signed claims).
Phase 5 — CLI [COMPLETE]
Crate: elench (binary)
elench emit— create, sign, store a claimelench verify— verify envelope and validate claimelench status— compute a claim’s statuselench gate— evaluate the release gate for a treeelench blast— compute the blast radius from a claimelench git— materialize the git projectionelench store— store a blob or tree
Depends on: All prior phases.
Deferred phases
| Phase | Crate | Gated by | Status |
|---|---|---|---|
| Anchor resolution | elench-anchor | E1 (PASSED, strategy=multi) | Deferred — crate not yet created |
| Reconciliation pass | (new) | A-A02 (open question) | Deferred — open question |
ADR-0001 — elench is the substrate; the claim log is the primary history
Status: proposed Serves: R1, R6 Supersedes: the original ADR-0001 (“claims as parallel refs”)
Context
elench must record what was checked, to what depth, and what remains unevaluated — as durable state, replicated alongside the code. The claim log must support append-only status change without tree mutation (R1). Git is a projection, not the substrate (R6); claims cannot live “in refs/claims/ alongside the code” because there is no git repo underneath — the claim log IS the history.
Decision
elench owns its own content-addressed store. The claim log is the primary history: it records tree state (as content-addressed blobs and trees), signed assertions about that state, and status changes — all in one append-only log. There is no separate git repository; there is no parallel ref namespace. The store is the substrate.
Git objects are synthesized from the claim log on demand by a projection helper (ADR-0002). Humans interact through git; elench is invisible to them. The claim log is the single source of truth.
Rejected alternatives
- Claims in a parallel git ref namespace (
refs/claims/). Requires a git repo underneath, making git the substrate and elench a sidecar. Reverses R6. The original ADR-0001 chose this; it was wrong. - External database. Breaks clone-and-go, needs a service, and separates evidence from the thing it is evidence about.
- Git notes. Poor merge behaviour, dropped by common workflows. Wrong substrate, same problem as parallel refs.
Consequences
elench must implement its own content-addressed storage (blobs, trees, commit-like objects). This is more work than reusing git’s object database, but it is the only way to make the claim log primary.
Code and claims cannot drift — there is no separate tree to drift out from under anchors. The anchor problem (BC2) becomes: do anchors survive across tree states in the claim log, not across git commits.
Revocation is invisible in the git projection’s git log — but
git log is itself a projection. The authoritative view is
elench-native: blame-to-claim, status-over-time, blast-radius. The git
projection is a compatibility affordance, not the interface being
designed for.
ADR-0002 — Git is a deterministic projection of the claim log
Status: proposed Serves: R6 Supersedes: the original ADR-0002 (“no synthesised git history”)
Context
R6 requires that the git CLI works with no changes and no awareness of elench. Since elench is the substrate (ADR-0001), git objects must be synthesized from the claim log. The original ADR-0002 rejected this approach citing deterministic synthesis as too hard; that rejection was based on the wrong substrate assumption. Synthesis is now a requirement, and its determinism is a binding constraint (BC4).
Decision
elench ships a projection helper (git-remote-elench or a FUSE
filesystem) that synthesizes git-compatible objects from the claim log.
The projection is read-only — humans use git to read, but writes go
through elench. Synthesis is deterministic: given the same claim log,
any party produces byte-identical git objects (BC4).
Commit OIDs are derived from the claims that produced the tree change, not from wall-clock timestamps. Author and committer strings are derived from claim producer identity. Tree ordering is deterministic.
Rejected alternatives
- No projection — elench-native CLI only. Guarantees no adoption. The git CLI is the universal interface to version control; not providing it makes elench a curiosity.
- Bidirectional git — write through git, read through elench. Requires bidirectional translation, which means the git view can diverge from the claim log. The projection must be read-only.
- Non-deterministic synthesis. Two parties with the same claim log
get different git objects, different OIDs, different
git log. R6 fails. Rejected by BC4.
Consequences
The projection helper is a new component with its own test surface. Deterministic synthesis must be verified (BC4 is prior art, but the derivation mapping — which claim becomes which commit — is novel and needs its own test).
The projection is lossy: git commits have no concept of claim status,
origin, or blast radius. git log shows a synthesized history; the
authoritative view is elench-native. This is the same lossiness as
before, but in the other direction — git is the view, not the
substrate.
Write-through-git is not supported. A user who runs git commit gets
an error or a no-op, depending on the projection implementation. This
is a UX cost; it is the price of making the claim log primary.
ADR-0003 — DSSE envelopes carrying in-toto statements
Status: proposed Serves: R7, R2
Context
Claims need signing, a subject, and a distinction between who signed and who produced. Build provenance needs the same. Two formats means two signing paths, two verification libraries, and two stores.
Decision
Reuse DSSE + in-toto. SLSA’s provenance predicate already separates builder
and signer identity and does not assume a human signer, so agent-produced and
build-produced records become the same kind of object with different
predicateType and different origin.kind.
Rejected alternatives
- A bespoke signed-JSON format. No compatibility gain, all the crypto review cost, and agent provenance ends up living beside build provenance instead of composing with it.
- Raw git-signed commits as the claim record. No subject field, no producer/signer split, and forces claims into tree mutations.
- C2PA. Has source-code manifest embedding and an AI disclosure assertion, but is oriented at media provenance and output attribution rather than verification depth. Wrong shape; revisit if regulatory pressure makes it mandatory anyway.
Consequences
Inherits in-toto’s verbosity and its key-distribution problem. Gains a verification path that existing supply-chain tooling already understands.
ADR-0004 — Predicate expression language: a small DSL of check primitives
Status: accepted Gated by: E0 (COMPLETE — ratio 0.72, well above 0.30 threshold) Serves: R3 (gate evaluable without build), INV-23 (expressions executable/deterministic/sandboxable) Supersedes: ADR-0004 “Predicate expression language (UNDECIDED)”
Context
assertion.expression must be executable, deterministic, sandboxable, and
writable by an agent under time pressure (INV-23). ADR-0004 was deferred to
E0 on the grounds that deciding a predicate language before seeing what
predicates agents actually write is designing against a guess.
E0 is complete. It extracted ~242 predicate expressions across two
repositories (kiseki, ~142 predicates; yoyo-evolve, ~100 predicates from
5 sessions). The extraction files are in
tool_05bbec962001JHgFFYKtqYweNJ (kiseki) and
tool_05bad7ae3001kBm0OymVdX7fGK (yoyo-evolve); the result summary is
in experiments/E0-predicate-ratio-result.md.
What E0 found about predicate shapes
Every predicate in the corpus is a flat expression: a small number of check primitives combined with comparison operators and boolean logic. No predicate uses loops, recursion, data structure construction, or function definitions. The shapes, classified by primary surface:
| Shape | Count | % | Representative expression |
|---|---|---|---|
| Code structure (grep source) | ~80 | ~33% | grep -r "KISEKI_INTENT_EPOCH_ROTATE" crates/kiseki-log/src | grep -E "8192|default" |
| Behavioral assertion (func→result) | ~75 | ~31% | safe_truncate("héllo", 4) == "hél" (no panic) |
| Test execution (test passes/count) | ~43 | ~18% | cargo test -p kiseki-log count == 255 and clippy clean |
| CLI output (cmd exit/output) | ~28 | ~12% | yoyo("status").matches(r"elapsed|time") && yoyo("status").matches(r"turn") |
| File/content (grep non-source) | ~11 | ~5% | grep -cE "IBM Storage Scale|WEKA|DAOS|BeeGFS" docs/performance/competitive-targets.md >= 4 |
| Build/lint (clippy/fmt/build) | ~5 | ~2% | cargo clippy -- -D warnings exit 0 |
The shapes reduce to four primitives:
-
grep(pattern, path) → int— count of regex matches in a file. Covers code structure (~33%) and file/content (~5%) = ~38% of predicates. The dominant primitive in kiseki, where claims are mostly “env var X has default Y” or “function Z exists in source.” -
test(name) → {passed: bool}— a named test passes or fails. Covers behavioral assertions (~31%) and test execution (~18%) = ~49% of predicates. The dominant primitive in yoyo-evolve, where claims are mostly “function(args) == expected” and the agent already wrote the test as part of TDD. -
run(cmd) → {exit: int, stdout: string, stderr: string}— run a command and inspect output or exit code. Covers CLI output (~12%) and build/lint (~2%) = ~14% of predicates. Examples:yoyo changelog exits 0,cargo clippy -D warnings exits 0,gh issue view 253 --json state contains "closed". -
exists(path) → bool— a file exists. Covers ~1% of predicates. A special case ofgrep(.+, path) >= 1orrun("test -f path").exit == 0, but common enough and semantically distinct enough to warrant its own primitive.
~10–15% of predicates combine two or more primitives with boolean logic. No predicate combines more than three.
Language features needed (deduplicated)
From all ~242 predicate expressions:
- String literals — file paths, command strings, pattern strings, test names, expected values.
- Regex — for
grepand string matching (e.g.,IBM Storage Scale|WEKA|DAOS|BeeGFS,\d+.*tokens?/s,error\[E0308\]). - File I/O (read-only) —
grepandexistsread files; neither writes. - Process execution —
testrunscargo test <name>;runruns an arbitrary command. The validator controls the sandbox. - Integer — match counts, test counts, exit codes.
- Boolean — pass/fail, exists/not-exists.
- Comparison operators —
==,!=,>=,<=,>,<. - Boolean logic —
&&(and),||(or),!(not). - String matching —
.contains(str)(substring),.matches(regex)(full match).
Not needed — and present in zero predicates from the corpus: loops, recursion, data structure construction (arrays, maps, records beyond primitive results), function definitions, floating point, I/O writes, exception handling, class/type systems, modules, imports.
Decision
A small, versioned DSL of check primitives — elench-predicate-v1.
The DSL has four primitives — grep, test, run, exists — with
comparison operators, boolean logic, and string/regex matching. It is
not Turing-complete. It is not a general-purpose programming language.
It is the smallest language that expresses 100% of the predicate shapes
E0 found, and it is the smallest language the validator (ADR-0006) must
implement.
Primitives
grep(pattern: regex, path: string) → int // count of regex matches in file
test(name: string) → {passed: bool} // cargo test <name> passes
run(cmd: string) → {exit: int, stdout: string} // run command, inspect output
exists(path: string) → bool // file exists
Operators
== != >= <= > < // integer and boolean comparison
&& || ! // boolean logic
.contains(str) → bool // substring match on string
.matches(regex) → bool // regex match on string
Grammar (informal)
An expression is one or more predicate checks combined with boolean logic. Each check applies a primitive, accesses a field if needed, and compares to an expected value.
expr := or_expr
or_expr := and_expr ('||' and_expr)*
and_expr := not_expr ('&&' not_expr)*
not_expr := '!' not_expr | comparison
comparison := term (op term)?
term := primitive ('.' field)*
primitive := grep_call | test_call | run_call | exists_call | int_lit | str_lit | bool_lit
The source field of assertion.expression contains the DSL
expression as a string. The language field is "elench-predicate-v1".
The digest field is the SHA-256 of the source, for deduplication: two
agents independently asserting the same predicate produce one claim
(INV-28).
How the shapes map to the DSL
| Shape from E0 | DSL expression |
|---|---|
grep -cE "IBM Storage Scale|WEKA|DAOS|BeeGFS" docs/performance/competitive-targets.md >= 4 | grep(/IBM Storage Scale|WEKA|DAOS|BeeGFS/, "docs/performance/competitive-targets.md") >= 4 |
safe_truncate("héllo", 4) == "hél" (no panic) | test("safe_truncate_utf8_boundary").passed |
cargo test -p kiseki-log count == 255 | run("cargo test -p kiseki-log").stdout.contains("255 passed") |
yoyo("status").matches(r"elapsed|time") | run("yoyo status").stdout.matches(/elapsed|time/) |
cargo clippy -- -D warnings exit 0 | run("cargo clippy -- -D warnings").exit == 0 |
scripts/perf-gate.sh exists | exists("scripts/perf-gate.sh") |
rg("fn set_model", "src/").len() >= 1 | grep(/fn set_model/, "src/") >= 1 |
rg("auto_downgrade|editor_model_map", "src/").len() == 0 | grep(/auto_downgrade|editor_model_map/, "src/") == 0 |
The behavioral-assertion shape (func(args) == expected) maps to
test(name).passed — the agent writes the test as part of its TDD
workflow, and the predicate references the test by name. The test
itself contains the function call and assertion. This is the
“existing test frameworks as the predicate” candidate, now a primitive
within the DSL rather than the entire language.
Crate
elench-predicate (already anticipated in module-graph.md and
enforcement-map.md). The crate provides:
- Parser:
fn parse(source: &str) -> Result<Expression, ParseError> - Evaluator:
fn evaluate(expr: &Expression, ctx: &EvalContext) -> Result<EvalResult, EvalError>whereEvalContextcarries the workspace root, sandbox configuration, and allowed-command list. - Validator integration:
elench-claim::validate_claimcallselench-predicate::parseto enforce INV-08 (predicate requires expression) and rejects expressions in unknown languages.
Versioning
The DSL is versioned (elench-predicate-v1). Future changes (new
primitives, operator changes) produce elench-predicate-v2 and a
new ADR. Existing claims reference v1 and are evaluated by the v1
evaluator indefinitely. This is the same append-only discipline the
claim log follows (R1).
Rejected alternatives
Rego (OPA)
Mature, purpose-built for policy, sandboxed by design. Lost because:
(1) E0 found zero predicates that require policy-over-data evaluation —
Rego’s strength. Every predicate is “check a file,” “run a command,” or
“run a test,” none of which is Rego’s native shape. (2) Rego has no
native primitives for process execution or file I/O; these would need
custom built-ins, at which point Rego is a wrapper around the DSL’s
run and grep primitives. (3) Rego’s evaluation model (partial sets,
default values, negation semantics) adds cognitive load for an agent
emitting predicates under time pressure — the corpus shows flat
comparisons, not set operations. (4) Rego’s sandbox is designed for
data evaluation, not for running untrusted commands; the run primitive
requires a different sandboxing strategy.
CUE
Strong at constraint expression and schema. Lost because: (1) E0 found zero predicates that require constraint solving — CUE’s strength. Predicates are flat checks, not constraints over data graphs. (2) CUE’s ecosystem is small, and its evaluation model (closed vs. open, defaults, required) is more complex than the four primitives needed. (3) Like Rego, CUE has no native primitives for process execution or file I/O.
Starlark
Deterministic Python subset, well-sandboxed, easy for a model to emit. Lost because: (1) Starlark is a general-purpose language (Turing-complete, has loops, functions, data structures), and E0 found zero predicates that need these features. (2) A general-purpose language is harder to sandbox than a fixed set of four primitives — the validator must reason about the full execution model, not just four known operations. (3) Starlark’s evaluator is larger and more complex than the DSL’s parser + four evaluators. (4) An agent emitting Starlark has more ways to make mistakes (syntax errors, type errors, runtime errors) than an agent emitting four primitives with a simple grammar. Starlark is the strongest general-purpose candidate, but E0’s data shows the predicates don’t need a general-purpose language.
Existing test frameworks as the predicate
The predicate IS a named test; the expression is a test identifier.
Cheapest by far and reuses all existing infrastructure. Lost because:
(1) E0 found that only ~49% of predicates are test-runnable (behavioral
assertions where the agent writes a test, plus test-execution counts).
The remaining ~51% — grep checks on source files (~33%), CLI output
checks (~12%), file existence (~5%), build/lint checks (~2%) — are not
naturally test names. “grep a doc file for 4 terms” is not a test
name; “cargo clippy -D warnings exits 0” is not a test name; “gh issue
view 253 –json state is closed” is not a test name. (2) Wrapping these
in tests (writing a fn doc_contains_ibm_weka_daos_beegfs() that
greps a markdown file) is possible but defeats the purpose: the
predicate becomes “test passes” with no visibility into what the test
checks, and the ADR-0004 (undecided) weakness — “shallow tests asserting
almost nothing are structurally equivalent to no tests, and this route
makes that failure invisible rather than visible” — is realized. (3)
Build/lint checks (cargo clippy, cargo fmt –check) cannot be expressed
as in-project tests without circular execution (running cargo test to
check if cargo clippy passes). (4) The “test as predicate” approach
is a subset of the DSL — test(name) is one of four primitives. The
DSL adds grep, run, and exists to cover the remaining ~51% of
predicates, while keeping test as the primary primitive for
behavioral assertions.
Two languages — one for policy over claims, one for assertions about code
Honest about the split between “check something” (grep, run, exists) and “assert behavior” (test). Lost because: (1) The split is between primitives, not between languages. Both “check” and “assert” primitives live in one DSL with four primitives; there is no need for two parsers, two evaluators, two sandbox configurations, or two languages for the agent to learn. (2) ~10–15% of predicates combine both kinds (“grep for X AND test Y passes”), which would require cross-language composition — a significant implementation burden. (3) E0 found no predicate that requires a policy language (claim-level rules like “all claims in this tree must have origin.kind = harness-observed”). Policy over claims is the gate’s job (INV-09, INV-13), and the gate evaluates claim status (computed from the log), not predicate expressions.
Consequences
For the validator (ADR-0006)
The validator must implement a parser and evaluator for
elench-predicate-v1. This is small: four primitive evaluators
(grep, test, run, exists), a comparison layer, and a boolean
logic layer. The parser is a simple recursive-descent parser for the
grammar above — no operator precedence beyond ! > comparison > &&
||. Therunprimitive is the most dangerous: the validator must sandbox process execution (whitelist allowed commands, restrict working directory, capture stdout/stderr). Thegrepandexistsprimitives are read-only and need only filesystem path restrictions (workspace root). Thetestprimitive runscargo test <name>, which is deterministic but may be slow — the validator may need a timeout.
The validator enforces INV-08 by rejecting any form = "predicate"
claim whose expression.language is not elench-predicate-v1 (or a
known successor version). Prose in a predicate slot is rejected at
parse time: parse("Input validation is now handled correctly.") →
ParseError.
For the schema
schema/claim.schema.json field expression.language is no longer a
free string. Validated claims must set language = "elench-predicate-v1". The source field contains the DSL
expression. The digest field is the SHA-256 of the source, enabling
deduplication (INV-28): two agents independently asserting the same
predicate produce one claim.
The schema itself does not need to change — language is already a
string, and the validator enforces the value. A future schema revision
may constrain language to an enum, but that is not required now.
For the agent
The agent emits DSL expressions instead of free-form predicate text.
The grammar is small enough that an agent under time pressure can emit
it reliably: grep(/pattern/, "path") >= N, test("name").passed,
run("cmd").exit == 0, exists("path"), combined with &&, ||,
!.
For behavioral assertions — the dominant shape in yoyo-evolve (~31% of
predicates) — the agent’s TDD workflow already produces the test. The
predicate is the test name: test("safe_truncate_utf8_boundary").passed.
The agent does not need to write a separate assertion; the test IS the
assertion.
For code structure checks — the dominant shape in kiseki (~33% of
predicates) — the agent emits grep(/pattern/, "src/") >= 1 or
grep(/banned_pattern/, "src/") == 0. These are one-liners that
require no test scaffolding.
For the build phases
Phase 0 (validator) is unblocked. The build-phases.md entry
“Predicate evaluation | gated by E0 (ratio) + ADR-0004 (language)” can
now proceed: E0 is COMPLETE (0.72), ADR-0004 is accepted. The
elench-predicate crate (already listed in module-graph.md as
not-yet-created) is the first implementation target for the
predicate-evaluation portion of Phase 0.
The module graph should be updated: elench-predicate is no longer
“deferred” — it is the next crate to create, depended on by
elench-claim (for validation) and elench-gate (for predicate
evaluation, if the gate needs to re-evaluate predicates; per R3/INV-13
the gate evaluates claim status, not predicates, so elench-gate may
not need to depend on elench-predicate directly).
What this decision does NOT do
-
Does not make predicates deep. A predicate like
test("my_test").passedhas the same shallowness risk as the “existing test frameworks” candidate: the test might assert almost nothing. The DSL makes this visible — the predicate expression istest("my_test").passed, not a magic string — but it does not make it deep. Depth is the auditor’s job (ADR-0006 + fidelity index), not the language’s. -
Does not handle non-deterministic predicates. Some
runcommands (e.g.,gh issue view— network-dependent) produce results that change over time. The DSL can express them, but the validator must decide whether to evaluate them live (result may differ between evaluations) or reject them as non-deterministic. The initial implementation should restrictrunto deterministic, local commands (cargo, git, file utilities) and flag network-dependent predicates asunevaluated(INV-16). This is a validator policy decision, not a language decision. -
Does not preclude future extensions. If E1 (anchor survival) or later experiments reveal predicate shapes that the four primitives cannot express (e.g., “parse a tree and check that every path under
src/has a claim”), the DSL gains a new primitive inelench-predicate-v2, with a new ADR. Existingv1claims are evaluated by thev1evaluator indefinitely (append-only discipline, R1). But E0’s data gives no reason to expect this: every predicate found is a flat check.
ADR-0005 — Implementation substrate: Rust, content-addressed store
Status: proposed Serves: R6, BC4 Supersedes: the original ADR-0005 (“implementation substrate undecided”)
Context
elench owns its own content-addressed store (ADR-0001). The tool is a client-side binary that reads and writes the store, verifies DSSE envelopes, evaluates predicates, computes transitive closures, and synthesizes a git projection (ADR-0002). No daemon (per problem.md anti-goals). Deterministic synthesis is a binding constraint (BC4).
Decision
Rust. elench is implemented in Rust (edition 2024, MSRV 1.85) for the following reasons:
- Single static binary. The tool must run inside an agent sandbox on both macOS and Linux. Rust produces a single static binary with no runtime dependency.
- Deterministic by construction. Rust has no GC pause, no non-deterministic finalization, and a well-defined memory model. The content-addressed store and git synthesis require bit-exact determinism (BC4).
- Sandboxing. Rust’s
unsafediscipline and absence of a runtime make the audit surface small — important for a tool that must be trusted as evidence infrastructure. - No libgit2 C surface. elench owns its own store; it does not link against libgit2. The git projection synthesizes git objects directly (OIDs, tree entries, commit objects) without a git library.
Rejected alternatives
- Go. Faster to write, easier contribution curve. But GC introduces non-determinism in finalization order, which is a risk for BC4. Go’s binary is not statically linked by default on all platforms.
- Shell out to
gitplumbing. Zero library risk, but elench owns the store — there is no git repo to shell out to. The projection synthesizes objects; it does not delegate to git. - Rust + gitoxide. gitoxide is excellent for git operations, but elench is not a git tool. It would pull in a large dependency for operations elench must own (content addressing, tree manipulation). The git projection writes raw git objects; it does not need a git library.
Consequences
Rust’s contribution curve is steeper than Go’s. The workspace is already scaffolded (5 crates). The content-addressed store must be implemented from scratch — no libgit2, no gitoxide. This is more work but eliminates a large dependency and keeps the audit surface small.
ADR-0006 — AGENTS.md rules are unimplemented gates
Status: accepted (as a statement of debt, not a design)
Context
AGENTS.md states MUST rules governing what agents may emit. Nothing
enforces them. Prose gates do not gate.
Decision
Record every rule in AGENTS.md as a named, unimplemented validator check.
Until implemented, they are unevaluated — not passed. The project’s own
distinction applies to the project.
Consequences
The first implementation milestone is the validator, not the CLI. A claim log with unenforced emission rules is not evidence; it is testimony from the audited party in a structured format.
ADR-0007 — Deterministic commit synthesis for the git projection
Status: proposed Serves: R6, BC4
Context
R6 requires the git CLI to work as a projection of the claim log (ADR-0002). BC4 requires the projection to be deterministic: two parties with the same claim log produce byte-identical git objects. The original ADR-0002 identified this as the blocking problem; this ADR addresses it.
Decision
Commit OIDs are derived from the claim log, not from wall-clock time or machine state. Specifically:
- Tree OID. The content address of the tree state. elench trees are hierarchical (each directory is a separate tree object) and serialized exactly like git tree objects (mode space name null oid, sorted by name with trailing ‘/’ for directories). The elench tree OID IS the git tree OID — a true passthrough, no re-hashing.
- Commit OID. Computed from (tree OID, parent commit OIDs, author, committer, message, timestamps) — all derived from the claim log, not the machine.
- Author/committer. Derived from the claim’s
producer.id. The signer (DSSE envelope) is not the author; the producer is. No user-configurableuser.name/user.email. - Timestamps. Derived from the claim’s timestamp, not the wall clock. Two parties synthesizing the same claim at different times get the same commit.
- Parent commits. The commit(s) synthesized from the claim(s) that produced the previous tree state(s). Linear history by default; merge commits when the claim log records a merge.
- Commit granularity. One commit per tree-changing claim. A
session that produces N tree changes gets N commits. This preserves
the blast-radius connection:
git blamemaps to the specific claim that introduced the line.
elench uses SHA-256 for all content addressing. Blobs, trees, and claims are all SHA-256. The git projection produces SHA-256 git objects; consumers use SHA-256 git repos. No SHA-1 is used anywhere.
Rejected alternatives
- One commit per session. Loses the blast-radius connection.
git blamemaps to the session, not the specific claim. - Non-deterministic timestamps. Two parties get different OIDs for the same tree state. R6 fails.
- User-configurable author. Reintroduces the identity problem the system exists to solve. The author field is derived, not chosen.
Consequences
The git projection is fully deterministic and reproducible. Any party with the claim log can verify the projection by re-synthesizing.
The commit history is denser than a human would write — one commit
per claim, not one per “logical change.” This is correct: the claim
is the unit of change, and denser history means finer-grained
git blame.
git rebase and git merge are read-only operations in the
projection — they produce new tree states that must be written back
to elench as new claims. The projection does not support write-through
(ADR-0002).
ADR-0008 — Persistent store: fjall as the content-addressed backend
Status: proposed Serves: R1 (revocability), INV-01 (append-only), INV-18 (elench owns store)
Context
The current Store in elench-store is in-memory (HashMap). Claims,
blobs, and trees do not persist across sessions. ADR-0001 requires
elench to own its own content-addressed store; ADR-0005 requires pure
Rust with no C/C++ dependency.
Decision
Use fjall as the persistent backend for elench-store, behind an
optional fjall-backend feature flag.
Keyspaces
One fjall database, three keyspaces (matching the current Store API):
| Keyspace | Key | Value | Durability |
|---|---|---|---|
blobs | SHA-256 OID (64 hex) | blob data | Buffer (content-addressed, can be recomputed) |
trees | SHA-256 OID (64 hex) | serialized tree entries | Buffer |
claims | cl_ + SHA-256 OID (67 chars) | serialized claim JSON | SyncAll (evidence must survive crashes) |
StoreBackend trait
Extract a StoreBackend trait from the current Store:
#![allow(unused)]
fn main() {
pub trait StoreBackend {
fn store_blob(&mut self, data: &[u8]) -> Result<Oid, StoreError>;
fn store_tree(&mut self, entries: Vec<TreeEntry>) -> Result<Oid, StoreError>;
fn store_claim(&mut self, claim: &Claim) -> Result<String, StoreError>;
fn read_blob(&self, oid: &Oid) -> Result<Vec<u8>, StoreError>;
fn read_tree(&self, oid: &Oid) -> Result<Tree, StoreError>;
fn read_all_claims(&self) -> Result<Vec<Claim>, StoreError>;
fn read_claims_for_tree(&self, tree: &Oid) -> Result<Vec<Claim>, StoreError>;
fn has_blob(&self, oid: &Oid) -> bool;
fn has_tree(&self, oid: &Oid) -> bool;
fn has_claim(&self, claim_oid: &str) -> bool;
fn blob_count(&self) -> usize;
fn tree_count(&self) -> usize;
fn claim_count(&self) -> usize;
}
}
MemoryStore: currentHashMapimplementation (default, no deps)FjallStore: fjall-backed implementation (optional feature)
elench-projection::synthesize takes &impl StoreBackend instead of
&Store. The CLI accepts --store memory (default) or --store fjall <path>.
Why fjall
| Criterion | fjall | redb | sled | rocksdb | custom |
|---|---|---|---|---|---|
| Pure Rust | Yes | Yes | Yes | No (C++) | Yes |
| Build deps | None | None | None | cmake, clang | None |
| Binary size | ~100KB | ~50KB | ~200KB | ~5MB | 0 |
| LSM-tree | Yes | No (B-tree) | Yes | Yes | Manual |
| Append-only | Natural | No | Yes | Yes | Manual |
| Crash recovery | Automatic | Automatic | Yes | Automatic | Manual |
| Compaction | Yes | None | Yes | Yes | None |
| Compression | LZ4 | No | Yes | Yes | No |
| Cross-keyspace atomic | Yes | No | No | No | Manual |
| Key-value separation | Yes | No | No | No | Manual |
| Stable disk format | Yes | Yes | No | Yes | N/A |
| Maintained | Yes (2.3k stars) | Yes | No (since 2022) | Yes | N/A |
| Proven in production | kiseki 3.1 | kiseki (rev-1) | No | Yes | No |
kiseki migrated from redb to fjall across 4 revisions (ADR-022). Benchmark: 36k PUT/s vs redb’s 18k (2x), 194k GET/s vs 150k (1.3x).
Rejected alternatives
- redb. B-tree, no compaction, no key-value separation. Was kiseki’s first choice; 2x slower on PUT. No cross-keyspace atomicity (blobs + trees + claims need separate databases).
- sled. Unmaintained since 2022. Unstable disk format. NOT recommended.
- RocksDB. C++ dependency (cmake, clang, librocksdb). Violates ADR-0005 (no C surface). ~5MB binary size.
- Custom files. Zero deps but no crash recovery, no compaction, no compression. Manual fsync. Not worth the engineering cost.
Consequences
Adds fjall as an optional dependency (~100KB binary size when
enabled). Gains crash recovery, compaction, compression, and
cross-keyspace atomicity. The StoreBackend trait keeps the API
stable — existing 30 store tests and 14 projection tests continue to
pass against MemoryStore. New tests exercise FjallStore with
#[ignore = "slow: requires fjall"] for Tier 2.
Feature flag: fjall-backend (off by default). Users who want
persistence add --features fjall-backend to their build.
Ubiquitous Language
Terms whose loose use will destroy the design. Every term here has a precise meaning; using one loosely in a spec or in code is a defect.
Core concepts
claim — a signed assertion about a tree. Not a commit, not a comment,
not a log line. Has a stable identity (id), a kind, an assertion,
an origin, an anchor, optional evidence, and optional dependsOn.
tree — a content-addressed tree state in the elench store (ADR-0001). NOT a git commit. The git projection (ADR-0002) synthesizes git commits from tree states, but the tree is the elench-native concept. Claims are anchored to spans within a tree.
claim log — the append-only set of claims that IS the primary history (ADR-0001). No record is ever overwritten; status is computed by folding the log, never stored. The git projection is derived from the claim log, not the other way around.
timestamp — Unix epoch seconds, set by the producer at emission time. Used by ADR-0007 for deterministic git commit synthesis. NOT the wall clock at projection time — two parties projecting the same claim get the same commit timestamp.
status — a claim’s current standing, computed from the log: passed,
falsified, unevaluated. NOT a stored field. A claim with no
falsification or verification record against it is unevaluated by
default, not passed.
Assertion types
predicate — a claim whose assertion.form = predicate. Carries an
executable expression that can be evaluated by a machine. Can gate.
A predicate without an executable expression is an annotation wearing a
costume; validators MUST reject it.
annotation — a claim whose assertion.form = annotation. Carries
only prose. Searchable. Cannot gate. Never read by policy. This is not
a lesser predicate; it is a different thing.
falsification — a claim with kind = falsification targeting an
earlier claim. Appended, never overwriting. The prior status stays
visible. This is the mechanism that makes retroactive invalidation work.
verification — a claim with kind = verification. Only the harness
emits these. An agent believing something passed is an assertion, not a
verification.
supersession — a claim with kind = supersession targeting an earlier claim. The earlier claim is replaced. A supersession claim changes the target’s computed status to falsified — the same status effect as falsification. The difference is intent: supersession replaces a claim that is no longer the best answer; falsification refutes a claim that was wrong. Both result in falsified status.
residue-acceptance — a claim with kind = residue-acceptance. A
human key signing over named unevaluated gaps. The terminator, made
explicit and made small: not “I reviewed this” but “I accept these
specific gaps.” Agents MUST NOT emit this.
Status values
unevaluated — no verification was attempted. Distinct from falsified
(verification ran and did not hold) and from passed. Most of a
brownfield repository is unevaluated, and a system that cannot say so
is lying.
passed — a verification record exists and no falsification has invalidated it. Computed, not stored.
Origin
origin — a typed value, not a label. origin.kind is required and
structurally distinguishes evidence sources. Policies may and generally
should discriminate on it.
harness-observed — origin.kind = harness-observed. Emitted by the
harness from direct observation (a test exited 0; a gate transition
fired). The agent cannot produce or suppress these.
agent-asserted — origin.kind = agent-asserted. Emitted by the
audited party. Legitimate, useful, and structurally weaker. Never
silently merged with harness-observed.
human-asserted — origin.kind = human-asserted. Emitted by a human
key. Distinct from agent-asserted because a human can be held
responsible in ways an agent cannot.
producer — the entity that produced a claim (harness build id, model id + version, or human key id). Distinct from the signer (the key that signed the DSSE envelope). The envelope supplies signer identity; the claim payload supplies producer identity. These are different things (R2).
Blast radius
blast radius — the transitive dependsOn closure from a falsified
claim. Only as trustworthy as the anchors (see docs/anchoring.md) and
as populated as the dependsOn field (E0 secondary measurement). If
dependsOn is empty in practice, revocation cannot propagate and the
central capability is unreachable.
Evidence and verification
evidence — a record of what was observed: process-exit, test-report, artifact-digest, or external-attestation. Empty for agent-asserted claims by default; that emptiness is the signal, not a gap to fill.
verification (as a concept) — evidence was observed. Distinct from justification (reasoning about why a choice was made). Existing tools capture justification. Confusing the two makes every claim look supported; if this distinction stops being honoured, the project has quietly become something else.
Release
release policy — a predicate over claims that determines whether an
artifact is releasable. Cheap and deterministic; evaluable without build
capability (R3). See docs/release-policy.md.
artifact — something that can be released. Carries a pointer to
(tree, policy), not a verdict. Consumers re-evaluate. If a
load-bearing claim is falsified after release, the artifact’s status
changes with no byte moving and no re-signing.
residue — the set of unevaluated claims remaining at evaluation
time. Bounded by policy; excess must be covered by a
residue-acceptance record signed by a key the policy names.
Anchoring
anchor — how a claim points at code within a tree. Strategy:
path-range (trivial, rots on reformat), symbol (language-server
qualified name, dies on rename), content-digest (normalised digest,
dies on any semantic edit), or multi (all three, resolve by
agreement). UNRESOLVED — E1 determines which survives.
Substrate and projection
elench store — the content-addressed store that IS the substrate
(ADR-0001). Holds blobs, trees, and claims. No daemon. Everything is
derivable from the store by a client-side binary. Blobs and trees are
addressed by SHA-256 content hash (64 hex chars, no prefix), identical
to git SHA-256 blob/tree OIDs. Claims are addressed with a cl_
prefix. The git projection is a passthrough for blobs and trees; only
commits are synthesized. Trees are hierarchical — each directory is a
separate tree object, exactly like git. Tree serialization matches
git’s tree object format (mode space name null oid, sorted with
trailing ‘/’ for directories). This makes elench tree OIDs identical
to git SHA-256 tree OIDs; the projection is a true passthrough for
trees and blobs.
git projection — a deterministic, read-only synthesis of git objects
from the claim log (ADR-0002). git log, git blame, git checkout
work because elench produces git-compatible objects. Writes go through
elench, never through git. Two parties with the same claim log produce
byte-identical git objects (BC4, ADR-0007).
Domain Model
Derived from docs/problem.md, schema/claim.schema.json, and the ADR
log. Every entity here traces to a requirement; every relationship
traces to a constraint.
Bounded contexts
| Context | Responsibility | Key entity |
|---|---|---|
| Claim Emission | Create, sign, and store claims in the store | Claim |
| Claim Evaluation | Compute status by folding the log | ClaimStatus |
| Anchor Resolution | Resolve anchors to code spans within a tree | Anchor |
| Release Gating | Evaluate release policy against claims | Verdict |
| Predicate Evaluation | Execute predicate expressions (GATED by E0) | Expression |
| Git Projection | Synthesize git objects from the claim log | GitCommit |
| elench Store | Content-addressed storage: blobs, trees, claims | Store |
| Envelope Verification | DSSE envelope signing and verification | Envelope |
Aggregates
Claim (root)
A signed assertion about a tree. The aggregate root of the claim log. Identity is the content address at creation; stable across status changes.
| Field | Type | Required | Notes |
|---|---|---|---|
id | string ^cl_[0-9a-f]{64}$ | yes | Content address, never reassigned |
kind | enum: assertion, falsification, verification, supersession, residue-acceptance | yes | falsification/verification/supersession require target |
target | array of claim ids | no | Claims this record acts upon |
assertion | object | yes | Contains form (predicate/annotation), optional expression, optional text |
origin | object | yes | Contains kind and producer |
anchor | object | yes | Contains tree (elench OID) and strategy |
| timestamp | integer (Unix epoch) | yes | Set by producer at emission. Used by ADR-0007 for deterministic commit synthesis. |
evidence | array | no | Empty for agent-asserted claims by default |
dependsOn | array of claim ids | no | Premises. Transitive closure IS the blast radius. |
Claim Log (root)
The append-only set of claims that IS the primary history (ADR-0001). No aggregate owns individual claims; the log is the aggregate that collects them. Status is computed by folding, never stored.
- Append-only. No record is ever modified or deleted.
- The git projection is derived from the claim log, not the other way around (ADR-0002).
- No daemon. Everything is derivable from the store by a client-side binary.
elench Store (root)
The content-addressed substrate (ADR-0001). Holds blobs, trees, and claims. There is no separate git repository.
- Content-addressed: blobs by content hash, trees by content hash, claims by content hash.
- The store IS the history. There is no parallel ref namespace, no sidecar database.
- The git projection reads from the store and synthesizes git objects on demand (ADR-0002).
Value objects
Assertion
| Field | Type | Required | Notes |
|---|---|---|---|
form | enum: predicate, annotation | yes | predicate can gate; annotation cannot |
expression | object: { language, source, digest? } | required when form=predicate | executable, deterministic, sandboxable |
text | string, max 2000 chars | no | Human-readable. Never load-bearing. |
Origin
| Field | Type | Required | Notes |
|---|---|---|---|
kind | enum: harness-observed, agent-asserted, human-asserted | yes | R2. Agents cannot emit harness-observed. |
producer | object: { id, sessionId?, hermeticity? } | yes | Distinct from signer (envelope). |
Anchor
| Field | Type | Required | Notes |
|---|---|---|---|
tree | string (elench tree OID) | yes | Content address of the tree state in the store. NOT a git commit OID. |
strategy | enum: path-range, symbol, content-digest, multi | yes | UNRESOLVED — E1 decides. |
path | string | no | For path-range strategy. |
range | [int, int] | no | For path-range strategy. |
symbol | string | no | For symbol strategy. |
contentDigest | string | no | For content-digest strategy. |
Evidence
| Field | Type | Required | Notes |
|---|---|---|---|
kind | enum: process-exit, test-report, artifact-digest, external-attestation | yes | |
digest | string | no | |
exitCode | integer | no | For process-exit. |
uri | string | no |
ClaimStatus (computed, not stored)
| Value | Meaning |
|---|---|
unevaluated | No verification or falsification record targets this claim. Default. |
passed | A verification record exists and no falsification has invalidated it. |
falsified | A falsification record has changed this claim’s status. |
Verdict
The result of evaluating a release policy against a claim log for a given tree. Not stored — computed at evaluation time.
| Field | Type | Notes |
|---|---|---|
result | enum: pass, fail | |
reasons | array of strings | Which conditions failed and why. |
tree | string | The elench tree OID evaluated. |
policy | string | The policy evaluated against. |
GitCommit (projection, not stored)
A git commit object synthesized from the claim log by the git projection (ADR-0002, ADR-0007). Not stored in the elench store — generated on demand.
| Field | Type | Notes |
|---|---|---|
oid | string | Deterministic function of (tree, parents, author, committer, message, timestamps). |
tree | string | elench tree OID, mapped to a git tree OID. |
parents | array of git commit OIDs | Derived from the claim log. |
author | string | Derived from the claim’s producer.id. |
committer | string | Same as author (no separate committer). |
message | string | Derived from an annotation claim, if present. |
Store entities
Blob
| Field | Type | Required | Notes |
|---|---|---|---|
| oid | string [0-9a-f]{64} | yes | SHA-256 content hash. Identical to git SHA-256 blob OID. |
| data | bytes | yes | Content. |
TreeEntry
| Field | Type | Required | Notes |
|---|---|---|---|
| name | string | yes | Entry name within the parent tree (e.g., “lib.rs”, “src”). NOT a full path — git-compatible. |
| mode | integer | yes | File mode (0o100644 regular file, 0o100755 executable, 0o120000 symlink, 0o040000 directory). |
| oid | string [0-9a-f]{64} | yes | SHA-256 content hash. For files: blob OID. For directories: tree OID. |
| kind | enum: blob, tree | yes | Whether this entry is a blob (file) or a tree (directory). |
Tree
| Field | Type | Required | Notes |
|---|---|---|---|
| oid | string [0-9a-f]{64} | yes | SHA-256 content hash of the canonical serialization (git tree object format: mode space name null oid, sorted by name with trailing ‘/’ for directories). Identical to a git SHA-256 tree OID. |
| entries | array of TreeEntry | yes | Sorted by name. Directory names sort as if they have a trailing ‘/’. |
Entity relationships
Claim
├── 1..* ──→ Claim (via dependsOn: premises)
├── 1..* ──→ Claim (via target: falsification/verification/supersession)
├── 1..* ──→ Evidence
└── 1 ──→ Anchor
elench Store
├── 0..* ──→ Claim
└── 0..* ──→ Tree (content-addressed)
GitCommit
└── projected from ──→ Claim Log + elench Store
Verdict
└── computed from ──→ Claim Log + Release Policy
Status machine
┌───────────┐ falsification ┌──────────┐
(default) │unevaluated│ ──────────────────▶ │falsified │
└───────────┘ supersession └──────────┘
│ ▲ ▲ │
verification │ falsification │ │
▼ │ of verification │ │
┌───────────┐ falsification │ │
│ passed │ ──────────────────────▶ │ │
└───────────┘ supersession │ │
│ ▲ │ │
falsification │ │ falsification │ │
of verification │ │ of falsification │ │
▼ │ ▼ │
┌───────────┐ ┌──────────┐
│unevaluated│ ◀────────────────────│falsified │
└───────────┘ (revert to previous) └──────────┘
Status is computed by folding the log, not stored. A claim’s status at
any point in time is a pure function of the claims that target it.
Falsification and supersession both change the target’s status to
falsified. If a verification record is itself falsified, the target
reverts to unevaluated (no valid verification remains). If a
falsification record is itself falsified, the target reverts to its
previous status (the falsification is void). This recursive fold — a
claim’s status depends on the status of claims that target it — must
be computed with cycle detection (INV-29).
Invariants
Every invariant is testable (expressible as an assertion). Every
invariant has an enforcement point (to be mapped in
specs/architecture/enforcement-map.md). Invariants are numbered for
stable reference; do not renumber.
Revocability and status (R1)
INV-01. A claim’s status is changed by appending a new record to the claim log, never by modifying or deleting an existing record.
INV-02. The prior status remains visible after a status change. The original claim record is unchanged; only the computed status changes.
INV-03. Claim identity (id) is stable across status changes. The
id is the content address at creation and is never reassigned.
INV-04. Status is a pure function of the claim log, computed by folding. No claim stores its own status as a field.
Origin typing (R2, AGENTS.md)
INV-05. origin.kind is required on every claim. The three values
(harness-observed, agent-asserted, human-asserted) are
structurally distinguishable and must never be merged into one status.
INV-06. An agent MUST NOT emit a record with
origin.kind = "harness-observed". This is the single rule that keeps
origin meaningful.
INV-07. Only the harness emits kind = "verification". An agent
believing something passed is an assertion, not a verification.
INV-08. A claim with assertion.form = "predicate" MUST supply an
executable expression. Prose in a predicate slot is rejected at
validation. Prose gates do not gate.
INV-09. Annotations are never read by policy. An
assertion.form = "annotation" claim cannot contribute to a gate
verdict regardless of its content.
INV-10. REMOVED. Empty dependsOn is a warning, not a rejection.
Downgraded to a guideline per domain expert decision.
INV-11. A failure is recorded only when it changed some claim’s status. A failed attempt that falsified nothing is noise and must not be recorded.
INV-12. An agent MUST NOT emit kind = "residue-acceptance". That
record requires a human key and represents a person accepting named
unevaluated gaps (R5).
Gate and release (R3, R4)
INV-13. The release gate can be evaluated without build capability. A party with only the claim log and no compute must reach the same verdict as a party with a build farm.
INV-14. An artifact’s acceptability is a live evaluation against the current claim log, not a signature frozen at release time.
INV-15. An artifact carries a pointer to (tree, policy), not a
verdict. Consumers re-evaluate. The tree is an elench tree OID
(ADR-0001), not a git commit.
Unevaluated (R5)
INV-16. unevaluated is a first-class status, distinct from
passed and from failed. A system that cannot represent it is lying
about brownfield code.
INV-17. Policies must be able to permit bounded unevaluated
residue, with each excess covered by a residue-acceptance record
signed by a key the policy names.
Substrate and projection (R6, ADR-0001, ADR-0002, ADR-0007)
INV-18. elench owns its own content-addressed store. The claim log IS the primary history. There is no separate git repository underneath.
INV-19. The git projection is a read-only synthesis of git objects from the claim log. Writes go through elench, never through git.
INV-20. Git object synthesis is deterministic. Two parties with the same claim log produce byte-identical git objects (BC4). Commit OIDs are derived from the claim log, not from wall-clock time or machine state.
INV-21. The git projection produces no side effects. It reads from the store and generates objects on demand. It does not modify the store, the claim log, or the working tree.
Supply-chain composability (R7, ADR-0003)
INV-22. Agent claims and build provenance share the same DSSE/in-toto envelope format. Same signing path, same store, same verification library.
Predicate language (ADR-0004)
INV-23. Predicate expressions must be executable, deterministic, and
sandboxable. The language is undecided (gated by E0); until decided,
expression.language is a free string and no validator bakes in an
answer.
Validator (ADR-0006)
INV-24. The AGENTS.md emission rules MUST be enforced by a
validator. Until implemented, they are unevaluated, not passed.
The first implementation milestone is the validator, not the CLI.
Substrate and projection (addendum)
INV-25. A blob’s OID MUST equal a deterministic SHA-256 hash of its content. A tree’s OID MUST equal a deterministic SHA-256 hash of its canonical serialization (sorted entries, mode, path, blob OID). Two objects with the same content have the same OID. This is the content-addressing property; without it the store is not the substrate.
INV-26. All derived views (claim status, blast radius, git projection, release verdict) are computable from the elench store alone. No external state (configuration, identity, network) is required for evaluation.
INV-27. The git projection is lossy by design. Claim status, origin.kind, and blast radius are NOT recoverable from git objects. The git projection MUST NOT be the authoritative source for any property the claim log computes.
INV-28. A claim’s OID MUST equal the SHA-256 hash of its canonical JSON serialization (all fields except id itself). Two claims with identical content (assertion, origin, anchor, evidence, dependsOn, timestamp) get the same OID — this is deduplication, and it is correct: two agents independently asserting the same predicate about the same span produce one claim, not two. Two claims with different content get different OIDs.
INV-29. dependsOn MUST be acyclic. A claim MUST NOT list itself, directly or transitively, in dependsOn. The validator rejects cyclic dependsOn; blast_radius and compute_status detect cycles and return an error rather than looping.
Assumptions
Three categories: validated (backed by evidence or prior art), accepted (acknowledged risk, no mitigation yet), and unknown (needs investigation, may invalidate the design).
Validated
A-V01. Reproducible builds are achievable with existing tooling (guix challenge, rebuilderd). E2 confirms this is not novel — the contribution here is the claim log, not the rebuild comparison. Source: experiments/E2-build-reproducibility.md
A-V02. DSSE + in-toto provide the signer/producer distinction needed for R2. SLSA’s provenance predicate already separates builder and signer identity and does not assume a human signer. Source: ADR-0003
A-V03. Git object synthesis is deterministic by construction.
git hash-object, git commit-tree, and git mktree produce
byte-identical output given the same input. The risk is in the
derivation mapping (which claim becomes which commit), not in git’s
object format.
Source: ADR-0007, BC4
A-V04. Content-addressed storage is well-understood prior art. Git’s object model (blobs, trees, commits) demonstrates the approach. elench owns its own store but does not invent the concept. Source: ADR-0001
Accepted
A-A01. The git projection is lossy. Git commits have no concept of
claim status, origin, or blast radius. git log shows a synthesized
history; the authoritative view is elench-native. This is the same
lossiness as before, but in the other direction — git is the view, not
the substrate.
Source: ADR-0002 consequences
A-A02. Code and claims cannot drift — there is no separate tree to drift out from under anchors. But a tree change can still invalidate claims (moves code out from under anchors within the elench store). A reconciliation pass is required and does not exist yet. Source: ADR-0002 consequences
A-A03. The predicate expression language is undecided. Deciding before E0 is designing against a guess. E0’s collected predicate expressions are the requirements input for this decision. Source: ADR-0004
A-A04. The implementation substrate is Rust (ADR-0005). The store is implemented from scratch — no libgit2, no gitoxide. This is more work but eliminates a large dependency and keeps the audit surface small. Source: ADR-0005
A-A05. AGENTS.md rules are unimplemented gates. Until a validator exists, the rules are prose, and prose does not gate. The first implementation milestone is the validator, not the CLI. Source: ADR-0006
A-A06. E0’s result is an optimistic bound. Sessions produced by a harness not asked to emit claims, extracted retrospectively, are plausibly cleaner than natively emitted ones — hindsight removes dead ends, biasing the ratio upward. Source: experiments/E0-predicate-ratio.md §Threat to validity
A-A07. Emergency override is unspecified. Every real system grows one; specifying it now would be guessing, and leaving it unspecified means it will be added badly under pressure. Flagged, not resolved. Source: docs/release-policy.md §Deliberately not specified
A-A08. Git write-through is unsupported. Users who run git commit
get an error or no-op. Writes go through elench, never through git.
This is the price of making the claim log primary.
Source: ADR-0002, FM-P3-03
A-A09. One commit per tree-changing claim (ADR-0007). May be too dense for human consumption; a session-level aggregation view may be needed but is not blocking. Source: ADR-0007, docs/problem.md §Open questions
A-A10. Compaction is a manual, destructive operator action.
elench log provides statistics (total, kind distribution, status
distribution, noise ratio, dependsOn density) and elench compact --before <ts> retires all claims before the cut-off, freezing their
statuses as a snapshot. The compaction record carries frozen statuses
forward. Active claims continue to be revocable (R1 preserved for
active claims, deliberately violated for retired ones).
Source: docs/problem.md §Open questions (resolved)
A-A11. Review mode forces the human to look before stamping.
elench review <tree> <claims.json> shows all unevaluated claims
with their content. The human must name each gap before elench accept issues a residue-acceptance. Adds real friction without
multi-party complexity.
Source: docs/problem.md §Open questions (resolved)
A-A12. Contradictory predicates: last-writer-wins (by timestamp).
The conflict is detected and reported by elench conflicts. The
gate evaluates against the winning predicate and includes the
conflict as a warning (not a failure). Partial block: only the
affected path (same anchor) is blocked; other paths evaluate
normally. The human is expected to resolve: falsify one or both.
Source: docs/problem.md §Open questions (resolved)
Unknown
A-U01. Does the claim log converge, or grow without bound on an
active repository? RESOLVED → A-A10. Compaction is manual,
destructive, with log stats + perf metrics.
A-U02. Who signs the residue acceptance under R5, and what stops
it becoming a rubber stamp? RESOLVED → A-A11. Review mode
forces the human to look before stamping.
A-U03. If two agents assert contradictory predicates and neither is
falsified, what is the tree’s status? RESOLVED → A-A12.
Last-writer-wins, conflict flagged for resolution, partial block.
A-U04. What fraction of claims are predicates vs annotations? (BC1/E0). If the ratio is < 0.15, elench is a search index over agent regret, not a gate. The threshold is pre-registered; the measurement has not been run. Source: experiments/E0-predicate-ratio.md
A-U05. What fraction of anchors survive realistic refactor sequences? (BC2/E1). If no strategy clears wrong-resolution ≤ 2% and correct-resolution ≥ 85%, the claim granularity must narrow and the product is smaller than designed. Source: experiments/E1-anchor-survival.md
A-U06. Can the target build be made bit-reproducible at acceptable cost? (BC3/E2). If structural divergence exists, K-of-N is unavailable and the release gate degrades to a single trusted builder. Source: experiments/E2-build-reproducibility.md
A-U07. What is the dependsOn density in practice? If near zero,
revocation cannot propagate and the central capability is unreachable
regardless of the predicate ratio. Arguably a second stop condition.
Source: experiments/E0-predicate-ratio.md §Secondary measurements
Failure modes
Known failure scenarios and handling, ordered by severity. P0 kills the project; P3 is a known limitation.
P0 — Project-killing
FM-P0-01: Anchor rot
Anchors no longer identify the intended code after realistic refactoring (rename, move, reformat, semantic edit, delete). Wrong-resolution poisons the blast radius silently — revocation targets the wrong code and the central capability is fiction.
Gated by: BC2, E1 Threshold: Wrong-resolution > 2% disqualifies a strategy outright. Correct-resolution ≥ 85% with wrong-resolution ≤ 2%: usable. Nothing clears both: fall back to coarser granularity (module/interface claims, not spans). This is an acceptable outcome, not a failure. Handling: Pre-registered in experiments/E1-anchor-survival.md. Run E1 after E0 passes. If no strategy survives, narrow claim granularity and accept coarser blast radius. The smaller honest product beats a larger one built on anchors that lie. Recovery: Not applicable. If anchors lie, the design is dead at the current granularity.
FM-P0-02: Predicate ratio too low
Most claims are annotations, not predicates. The gate carries almost no information and the human is back to reading everything. elench degrades to an expensive search index over agent regret with a signing layer attached.
Gated by: BC1, E0 Threshold: Ratio ≥ 0.30 proceed. 0.15–0.30 proceed with reduced scope. < 0.15 stop — do not build the gate layer. Handling: Pre-registered in experiments/E0-predicate-ratio.md. Run E0 first, before any implementation. If < 0.15, build only the search index if it is worth building, differently. Recovery: Not applicable. If the ratio is too low, the gate layer does not get built.
P1 — Severe, blocks core capability
FM-P1-01: Build non-reproducibility
The target build cannot be made bit-reproducible across independent machines. K-of-N builder agreement is meaningless. The release gate degrades to a single signature, and R3’s independent evaluation buys nothing at the artifact layer.
Gated by: BC3, E2 Threshold: All divergences cheap-to-fix: proceed with K-of-N. Any structural divergence: K-of-N unavailable. Release policy must be rewritten for a single trusted builder before implementation. Handling: Pre-registered in experiments/E2-build-reproducibility.md. Can run in parallel with E0/E1. Reuse prior art (guix challenge, rebuilderd) rather than measuring from scratch. Recovery: If structural divergence exists, rewrite docs/release-policy.md for single-builder. This is a smaller product.
FM-P1-02: Claim log grows without bound
No pruning story exists. On an active repository, the log accumulates
without limit. Compaction may violate R1 (append-only, no
overwriting).
RESOLVED. Compaction is a manual, destructive operator action
(A-A10). elench log <claims.json> provides statistics (total, kind
distribution, status distribution, noise ratio, dependsOn density).
elench compact <claims.json> --before <ts> retires all claims
before the cut-off, freezing their statuses as a snapshot. The
compaction record carries frozen statuses forward. Active claims
continue to be revocable (R1 preserved for active claims,
deliberately violated for retired ones).
FM-P1-03: Non-deterministic git projection
Two parties with the same claim log produce different git objects.
git log disagrees. R6 fails.
Gated by: BC4, ADR-0007
Threshold: Git object synthesis is deterministic by construction
(git hash-object, git commit-tree, git mktree are deterministic).
The risk is in the derivation mapping (which claim becomes which
commit), not in git’s object format.
Handling: ADR-0007 specifies deterministic OID derivation,
author/committer strings, timestamps, and tree ordering. Tested by
synthesizing from the same claim log on two machines and comparing
output.
Recovery: If the derivation mapping is non-deterministic, fix the
mapping. Git’s object format is not the problem.
P2 — Moderate, degrades quality
FM-P2-01: Residue acceptance rubber stamp
The human key signing over unevaluated gaps becomes a formality rather
than a genuine acceptance. The R5 terminator fails — not because it is
wrong, but because the human rubber-stamps it.
RESOLVED. Review mode (A-A11) forces the human to look before
stamping. elench review <tree> <claims.json> shows all
unevaluated claims with their content (form, language, source,
producer). The human must name each gap before elench accept
issues a residue-acceptance. This adds real friction without
multi-party complexity.
FM-P2-02: Contradictory predicates, neither falsified
Two agents assert contradictory predicates about the same span. Neither
is falsified. The tree’s status is undefined.
RESOLVED. Last-writer-wins (by timestamp). The conflict is
detected and reported by elench conflicts <tree> <claims.json>
(A-A12). The gate evaluates against the winning predicate and
includes the conflict as a warning (not a failure — the winning
predicate still gates). Partial block: only the affected path (same
anchor) is blocked; other paths evaluate normally. The human is
expected to resolve: falsify one or both predicates.
FM-P2-03: Reconciliation pass not triggered
A tree change lands that invalidates claims (moves code out from under
anchors). Nothing forces the claim log to notice. The log and the tree
drift apart silently.
RESOLVED. elench-anchor::reconcile(tree, log) detects claims
whose anchors no longer resolve after a tree change. Reports
affected claims as DriftedClaim (with path, symbol, resolution
result). Read-only: does NOT auto-fix. The human (or agent) must
re-anchor or falsify. CLI: elench reconcile <tree> <claims.json>
(future — currently library-only).
P3 — Low, known limitation
FM-P3-01: Consumers who never re-check are unprotected
An artifact’s acceptability is a live evaluation (R4). Consumers who never re-check are unprotected after a post-release falsification. There is no push path.
Gated by: None (inherent to certificate-revocation shape) Handling: Acknowledged in docs/release-policy.md. Do not pretend otherwise in the docs. A push path may be added later but is not part of the core design. Recovery: Out of scope. Consumers must poll.
FM-P3-02: Emergency override unspecified
Every real system grows one. Leaving it unspecified means it will be added badly under pressure.
Gated by: None (deliberately deferred) Handling: Flagged in docs/release-policy.md §Deliberately not specified. Not a design gap — a conscious deferral. Recovery: Specify when the need becomes concrete, not before.
FM-P3-03: Git write-through unsupported
A user who runs git commit in a projected repository gets an error or
a no-op. This is the price of making the claim log primary (ADR-0002).
Gated by: R6 (write path goes through elench, never git)
Handling: Documented. The git projection is read-only. Users who
want to write must use elench (or a future write-back helper that
converts git commits into elench claims).
Recovery: A write-back helper is possible but not scoped. It would
convert a git commit into one or more elench claims, losing any
information git cannot represent.
Cross-Context Interactions
Integration points between bounded contexts. Each interaction has a direction, a contract, and a failure mode.
Contexts
| Context | Owns | Consumes |
|---|---|---|
| Claim Emission | Claim creation, signing, storage | Envelope Verification (before accepting) |
| Claim Evaluation | Status computation (log folding) | elench Store (reads log) |
| Anchor Resolution | Anchor → code span resolution | Claim Evaluation (for blast radius) |
| Release Gating | Verdict computation | Claim Evaluation (uses status), Predicate Evaluation |
| Predicate Evaluation | Expression execution | — (gated by E0/ADR-0004) |
| Git Projection | Git object synthesis from claim log | elench Store (reads), Claim Log (reads) |
| elench Store | Content-addressed storage: blobs, trees, claims | — (leaf in workspace) |
| Envelope Verification | DSSE envelope signing/verification | Claim Emission (before accepting) |
Interactions
1. Claim Emission → elench Store
Direction: Write
Contract: A signed DSSE envelope containing an in-toto statement
whose predicate matches schema/claim.schema.json is written to the
elench store (content-addressed). The store is the substrate; there is
no parallel ref namespace (ADR-0001).
Failure: Invalid envelope → rejected before write. Valid envelope,
invalid claim → rejected by validator (once implemented, ADR-0006).
Status: No code. Contract is schema/claim.schema.json (DRAFT).
2. Claim Evaluation ← elench Store
Direction: Read
Contract: The evaluator reads all claims from the store and folds
them to compute each claim’s status (unevaluated / passed /
falsified). The fold is a pure function of the log.
Failure: Corrupt or missing data → status is “unevaluated” for all
claims that cannot be read. Silent corruption → wrong status. (No
reconciliation pass exists yet, A-A02.)
Status: No code. Fold semantics are in specs/domain-model.md.
3. Release Gating ← Claim Evaluation
Direction: Read
Contract: The gate receives a tree (elench OID) and a policy P,
queries Claim Evaluation for the status of all claims anchored to the
tree, and evaluates the four conditions from
docs/release-policy.md:
- No falsified premise in transitive dependsOn closure
- Bounded residue (unevaluated within P’s allowance, excess covered by residue-acceptance)
- Origin floor (load-bearing claims are harness-observed)
- Builder agreement (K independent producers — unavailable unless E2)
Failure: Any condition fails → gate fails with named reason. The
verdict is not stored; it is recomputed on demand.
Status: No code. Policy shape is in
docs/release-policy.md.
4. Anchor Resolution ← Claim Evaluation
Direction: Read (for blast radius), Write (anchor resolution result)
Contract: When a claim is falsified, the blast radius is the
transitive dependsOn closure. Each claim in the closure has an anchor
that must be resolved to verify it still points at the intended code
within an elench tree.
Failure: Wrong-resolution (anchor points at wrong code) → blast
radius is fiction, falsification targets the wrong lines. This is
FM-P0-01.
Status: No code. Anchor strategies are in docs/anchoring.md
(UNRESOLVED — E1 gates).
5. Envelope Verification → Claim Emission
Direction: Read (before accepting a claim) Contract: Before a claim is stored, its DSSE envelope is verified: signature is valid, signer is known, and the in-toto statement’s predicateType is recognised. The signer (envelope) and producer (claim payload) are distinct; both are recorded. Failure: Invalid signature → rejected. Unknown signer → rejected or flagged per policy. Valid signature, invalid claim → rejected by validator. Status: No code. Envelope format is in ADR-0003.
6. Git Projection ← elench Store + Claim Log
Direction: Read-only
Contract: The git projection synthesizes git objects (commits,
trees, blobs) from the claim log (ADR-0002). Synthesis is
deterministic (BC4, ADR-0007): two parties with the same claim log
produce byte-identical git objects. git log, git blame, git checkout work as if the repository were a git repo.
Failure: Non-deterministic synthesis → two parties get different
git objects, R6 fails (FM-P1-03). Write-through-git → rejected; the
projection is read-only (FM-P3-03).
Status: No code. Projection shape is in ADR-0002 and ADR-0007.
7. Predicate Evaluation ← Release Gating
Direction: Read Contract: The release gate is itself a predicate. If the predicate language is the same as claim predicates (ADR-0004 undecided), the gate reuses the same evaluation engine. If not, a separate policy language exists. Failure: Predicate evaluation fails → gate fails (fail-closed). Non-deterministic predicate → two evaluators reach different verdicts, violating R3. Status: No code. Gated by E0 (predicate ratio) and ADR-0004 (language undecided).
Open cross-context issues
-
Reconciliation pass (elench Store ↔ Claim Evaluation): A tree change lands that moves code out from under anchors. Nothing forces the claim log to notice. A reconciliation pass is required and does not exist yet (A-A02, FM-P2-03).
-
Claim log convergence (elench Store): Does the log grow without bound on an active repository? No pruning story exists. Compaction may violate R1 (A-U01, FM-P1-02).
-
Contradictory predicates (Predicate Evaluation ↔ Release Gating): Two agents assert contradictory predicates and neither is falsified. The tree’s status is undefined (A-U03, FM-P2-02).
-
Git projection granularity (Git Projection ↔ Claim Evaluation): One commit per tree-changing claim (ADR-0007) may be too dense for human consumption. A session-level aggregation view may be needed (A-A09).
Fidelity Index
Test depth per invariant. All phases (0–5) are implemented, plus
post-implementation improvements (anchor resolution, build provenance,
.git/ materialization, proptest, conflict detection, continuous
dogfooding, INV-15 artifact format).
Test counts: 344 (default), 351 (with fjall-backend). 92% line
coverage workspace-wide. fmt clean, clippy clean.
Invariants
| INV | Description | Depth | Notes |
|---|---|---|---|
| INV-01 | Status changed by appending, not modifying | MOCK | elench-store: store_blob/tree/claim idempotent (memory + fjall) |
| INV-02 | Prior status remains visible | MOCK | elench-claim: compute_status reads entire log |
| INV-03 | Claim identity stable across status changes | MOCK | elench-claim: ClaimId immutable |
| INV-04 | Status computed by folding, not stored | MOCK | elench-claim: compute_status pure fn |
| INV-05 | origin.kind required and structurally distinct | MOCK | elench-claim: type system enforces |
| INV-06 | Agents cannot emit harness-observed | MOCK | elench-claim: validate_claim cross-checks signer |
| INV-07 | Only harness emits verification | MOCK | elench-claim: validate_claim cross-checks signer |
| INV-08 | Predicate requires executable expression | MOCK | elench-claim: validate_claim calls elench-predicate::parse |
| INV-09 | Annotations never read by policy | MOCK | elench-gate: evaluate filters on form=predicate |
| INV-10 | dependsOn populated with premises | REMOVED | Downgraded to guideline; empty dependsOn is a warning, not a rejection |
| INV-11 | Failure recorded only when status changed | MOCK | elench-claim: validate_claim checks target status in log |
| INV-12 | Agents cannot emit residue-acceptance | MOCK | elench-claim: validate_claim cross-checks signer |
| INV-13 | Gate evaluable without build capability | MOCK | elench-gate: evaluate takes &[Claim], no build |
| INV-14 | Artifact acceptability is live evaluation | MOCK | elench-gate: evaluate called on demand, no cache |
| INV-15 | Artifact carries (tree, policy), not verdict | MOCK | elench-gate: Artifact struct with version field; schema/artifact.schema.json; 6 tests |
| INV-16 | unevaluated is first-class status | MOCK | elench-claim: ClaimStatus::Unevaluated |
| INV-17 | Policies permit bounded unevaluated residue | MOCK | elench-gate: condition 2, residue-acceptance |
| INV-18 | elench owns content-addressed store | MOCK | elench-store: no git dependency, owns storage; both backends pure-Rust |
| INV-19 | Git projection is read-only | MOCK | elench-projection: synthesize takes &dyn StoreBackend, no writes |
| INV-20 | Git synthesis is deterministic (BC4) | PROPERTY | elench-projection: proptest_inv_20_synthesis_deterministic + order_independent |
| INV-21 | Git projection produces no side effects | MOCK | elench-projection: scenario_inv19_projection_does_not_write_to_store |
| INV-22 | Agent claims and provenance share DSSE/in-toto | MOCK | elench-envelope: sign/verify, PREDICATE_TYPE_AGENT, Ed25519 (A1) |
| INV-23 | Predicate expressions executable/deterministic/sandboxable | MOCK | elench-predicate: 4 primitives, not Turing-complete |
| INV-24 | AGENTS.md rules enforced by validator | MOCK | elench-claim: validate_claim (Phase 0) |
| INV-25 | Content addressing (SHA-256) | PROPERTY | elench-claim: ClaimId::from_content; elench-store: Oid::from_blob_data/from_tree_entries + deserialize_tree_bytes round-trip + FjallStore::read_tree (feature tier) |
| INV-26 | Store is sole source of truth | MOCK | elench-store: all views derive from store; selectable at runtime via `–store memory |
| INV-27 | Git projection is lossy, not authoritative | MOCK | elench-projection: scenario_inv27_projection_is_lossy |
| INV-28 | Claim OID is content hash | PROPERTY | elench-claim: ClaimId::from_content (SHA-256 of canonical JSON); proptest_inv_28 |
| INV-29 | dependsOn acyclic | PROPERTY | elench-claim: validate_claim DFS cycle detection; proptest_inv_29 |
28 active invariants (24 original minus INV-10 removed, plus INV-25/26/27/28/29 added). 28 ENFORCED (was 27 + INV-15 future; INV-15 now MOCK with 6 tests). 0 future.
Features
| Feature | Scenarios | Depth | Notes |
|---|---|---|---|
| claim-emission | 7 | MOCK | elench-claim: validate_claim + types. 1 scenario untested (empty dependsOn warning — dead code) |
| claim-revocation | 7 | MOCK | elench-claim: compute_status + blast_radius + dependsOn propagation. All 7 covered. |
| origin-typing | 6 | MOCK | elench-claim: validate_claim cross-checks. 2 scenarios untested (query-by-origin.kind not implemented) |
| release-gate | 9 | MOCK | elench-gate: evaluate, 4 conditions. 1 scenario untested (contradictory predicates — FM-P2-02 known limitation) |
| anchor-resolution | 11 | MOCK | elench-anchor: resolve_path_range/symbol/content_digest, reconcile CLI. 1 scenario untested (wrong-resolution — dead code) |
| unevaluated-residue | 6 | MOCK | elench-claim: ClaimStatus::Unevaluated. 1 scenario untested (corrupt cascade — no corrupt status) |
| git-projection | 4 | MOCK | elench-projection: synthesize, git_log_oneline/full, materialize, git blame, write-through rejected. All 4 covered. |
| store-backend | 5 | MOCK | elench-store: –store flag, FjallStore::read_tree round-trip. All 5 covered. |
| build-provenance | 4 | SHALLOW | elench: –artifact flag, SHA-256 of build output. CLI output checks, not in-process claim verification. |
| proptest-property | 5 | PROPERTY | proptest: INV-25/20/13/29/28 (256 cases each). All 5 covered. |
| dogfooding | 7 | NONE | Shell scripts (run.sh, emit-continuous.sh) with no assertions. 6 of 7 scenarios have no Rust test. |
71 scenarios total. 59 tested, 12 untested (see per-feature notes).
346 tests (default), 353 (with fjall-backend). 92% line
coverage.
Untested scenarios (12)
| Feature | Scenario | Reason |
|---|---|---|
| anchor-resolution | Wrong-resolution is reported distinctly from failure | StrategyOutcome::Wrong is dead code (#[allow(dead_code)]) |
| claim-emission | A claim with empty dependsOn is accepted with a warning | ValidationError::EmptyDependsOn is defined but never returned |
| dogfooding (×6) | Dogfooding claims emitted/stored, gate, log stats, git projection, continuous emission, CI nightly | Shell scripts with || true, no assertions |
| origin-typing (×2) | Harness-observed and agent-asserted claims are distinct; human-asserted distinct from agent | No query-by-origin.kind function exists |
| release-gate | Two contradictory predicates: gate passes (known limitation) | FM-P2-02 not tested |
| unevaluated-residue | A corrupt claim cascades to unevaluated dependents | No “corrupt” status distinction; compute_status returns Err(ClaimNotFound) |
Experiments
| Experiment | Gates | Status | Result |
|---|---|---|---|
| E0 — Predicate ratio | BC1 | PASSED | 0.72 (threshold >= 0.30). PROCEED AS DESIGNED. |
| E1 — Anchor survival | BC2 | PASSED | All strategies USABLE (correct >= 85%, wrong <= 2%). Proceed with multi. |
| E2 — Build reproducibility | BC3 | PASSED | Same-triple divergences all cheap-to-fix. K-of-N available. |
Implementation status
All phases (0–5) are implemented, plus elench-anchor, store-backend
selection, build provenance, .git/ materialization, proptest,
conflict detection, continuous dogfooding, and INV-15 artifact format.
- Phase 0: elench-predicate (64 tests) + elench-claim (40 tests)
- Phase 1: elench-store (34 tests default; 40 with
fjall-backend) - Phase 2: elench-envelope (12 tests)
- Phase 3: elench-gate (23 tests)
- Phase 4: elench-projection (14 tests)
- Phase 5: elench binary (9 unit + 65 cli + 9 integration tests; 10 integration with
fjall-backend) - elench-anchor (23 tests)
Store backend: in-memory (default), fjall (optional feature, ADR-0008).
--store memory|fjall <path> selects the backend at the CLI; synthesize
takes &dyn StoreBackend so any command can target either. materialize
writes real zlib-compressed git objects to .git/objects/.
Dogfooding: dogfooding/claims.json (10 claims about elench’s own
invariants), make dogfood runs the full pipeline (emit, gate, log,
review, conflicts, git projection, materialize, verify). Continuous
dogfooding (dogfooding/emit-continuous.sh) emits 4 harness-observed
claims per CI run.
Feature Files
Behavioral specifications (Gherkin) for elench.
Anchor Resolution
Feature: Anchor resolution
Anchors point at code within a tree. If anchors rot, revocation
targets the wrong code and blast radius is fiction. E1 measures
survival rate for each strategy over real refactor sequences.
Scenario: A path-range anchor resolves at the same tree
Given a claim anchored to src/lib.rs lines 1-10 at tree T0
And tree T0 contains a blob at src/lib.rs with at least 10 lines
When the anchor is resolved at tree T0 using the multi strategy
Then the path-range strategy resolves to src/lib.rs
And the result is Correct
Scenario: A path-range anchor fails when the path is not in the tree
Given a claim anchored to nonexistent.rs at tree T0
When the anchor is resolved at tree T0
Then the path-range strategy fails
And if all strategies fail, the result is Failed
Scenario: A path-range anchor fails when the range exceeds the blob
Given a claim anchored to src/lib.rs lines 1-100 at tree T0
And tree T0 contains a blob at src/lib.rs with only 5 lines
When the anchor is resolved at tree T0
Then the path-range strategy fails
Scenario: A symbol anchor finds a function definition in the tree
Given a claim anchored to symbol "parse_input" at tree T0
And tree T0 contains a blob with "fn parse_input" in src/parser.rs
When the anchor is resolved at tree T0 using the multi strategy
Then the symbol strategy resolves to src/parser.rs
And the result is Correct
Scenario: A symbol anchor dies on rename
Given a claim anchored to symbol "parse_input" at tree T0
And tree T0 contains no definition of "parse_input"
When the anchor is resolved at tree T0
Then the symbol strategy fails
Scenario: A content-digest anchor finds matching content in the tree
Given a claim anchored with content_digest D at tree T0
And tree T0 contains a blob whose SHA-256 equals D
When the anchor is resolved at tree T0 using the multi strategy
Then the content-digest strategy resolves to that blob's path
And the result is Correct
Scenario: A content-digest anchor fails when no blob matches
Given a claim anchored with content_digest D at tree T0
And no blob in tree T0 has SHA-256 equal to D
When the anchor is resolved at tree T0
Then the content-digest strategy fails
Scenario: Strategies disagree when path and symbol point to different files
Given a claim anchored to path src/main.rs and symbol "parse_input"
And tree T0 has src/main.rs (path-range resolves) but parse_input is in src/parser.rs
When the anchor is resolved at tree T0
Then the result is Degraded
And the disagreements include path-range → src/main.rs and symbol → src/parser.rs
Scenario: Wrong-resolution is reported distinctly from failure
Given a claim anchored at tree T0 using path-range strategy
When the anchor is resolved at tree T1 and resolves to the wrong code
Then the result is "wrong-resolution", not "unresolved"
And wrong-resolution rate > 2% disqualifies the strategy
Scenario: Reconciliation reports intact and drifted claims
Given a tree T0 with two claims: one anchored correctly, one with a missing path
When reconciliation is run for tree T0
Then the report lists 1 intact claim and 1 drifted claim
And the drifted claim's resolution is Failed
Scenario: Reconciliation CLI command
Given a claims file with claims anchored to tree T0
When elench reconcile <tree_oid> <claims.json> runs
Then the output shows intact and drifted counts
And the exit code is 0
Build Provenance
Feature: Build provenance digest
`elench build <tree> [--artifact <path>] -- <command...>` runs a build,
captures the exit code, and emits a harness-observed provenance claim
(ADR-0003, INV-22). The digest is SHA-256 of the build artifact when
`--artifact <path>` names an existing file; otherwise it falls back to
SHA-256 of stdout. The same producer cannot forge a digest it did not
observe — the harness reads the file, not the agent.
Scenario: digest is SHA-256 of the artifact file when --artifact is present
Given a build that writes 42 bytes to /tmp/artifact.bin
And a known content for /tmp/artifact.bin
When elench build <tree> --artifact /tmp/artifact.bin -- <command> runs
Then the emitted claim's content_digest equals SHA-256(/tmp/artifact.bin)
And the claim's evidence[0].digest equals SHA-256(/tmp/artifact.bin)
And the claim's evidence[0].exit_code equals the build's exit code
Scenario: digest falls back to stdout when --artifact is absent
Given a build that writes "hello" to stdout and exits 0
When elench build <tree> -- <command> runs
Then the emitted claim's content_digest equals SHA-256("hello")
And the claim's evidence[0].digest equals SHA-256("hello")
Scenario: missing artifact file is rejected
Given no file exists at /tmp/nonexistent.bin
When elench build <tree> --artifact /tmp/nonexistent.bin -- <command> runs
Then the command exits non-zero
And the error names the missing artifact
Scenario: --artifact is parsed before --, not passed to the build
Given a build command echo --artifact foo
When elench build <tree> --artifact /tmp/real.bin -- echo --artifact foo runs
Then the digest is SHA-256(/tmp/real.bin), not influenced by echo's args
And echo receives "--artifact foo" as its own argument
Claim Emission
Feature: Claim emission
Agents emit signed claims about a tree, stored in the elench
content-addressed store. Claims are append-only; no tree mutation
occurs. The validator enforces emission rules before a claim is
accepted.
Scenario: An agent-asserted predicate claim is stored
Given an elench store with at least one tree
When an agent emits a predicate claim asserting "parse('') == Err(EmptyInput)" about tree <oid>
Then a new claim object exists in the store with a DSSE envelope
And the statement's predicate has form = "predicate"
And the statement's predicate has origin.kind = "agent-asserted"
And the tree is unchanged — no blobs or tree entries were added or modified
Scenario: An annotation claim is stored but cannot gate
Given an elench store with a claim log containing one annotation claim
When the release gate is evaluated against the log
Then the annotation claim does not contribute to the gate verdict
And the annotation's status is reported as "unevaluated"
Scenario: An agent cannot emit a harness-observed claim
Given an agent attempting to emit a claim
When the agent sets origin.kind = "harness-observed"
Then the claim is rejected by the validator
And no object is written to the store
Scenario: A predicate without an expression is rejected
Given an agent attempting to emit a predicate claim
When the claim's assertion has form = "predicate" but no expression field
Then the claim is rejected by the validator
And the rejection reason includes "expression required for predicate"
Scenario: A claim with dependsOn lists its premises
Given an agent emits a claim that relies on premises cl_a3f... and cl_91c...
When the claim is stored
Then the claim's dependsOn field contains [cl_a3f..., cl_91c...]
And the blast radius from any falsification of cl_a3f... includes this claim
Scenario: A claim with cyclic dependsOn is rejected
Given a claim log containing claim cl_a with dependsOn [cl_b]
And claim cl_b with dependsOn [cl_a]
When an agent emits a new claim cl_c with dependsOn [cl_a, cl_c]
Then cl_c is rejected by the validator
And the rejection reason includes "cyclic dependency"
Scenario: A claim with empty dependsOn is accepted with a warning
Given an agent emits an assertion claim with no dependsOn
When the claim is validated
Then the claim is accepted
And a warning is emitted: "dependsOn is empty — claim asserts it was reached from nothing"
Claim Revocation
Feature: Claim revocation without tree mutation
A claim's status is changed by appending a falsification record. No
code changes, no history rewrite. The prior status remains visible.
Blast radius propagates through the dependsOn closure.
Scenario: A falsification record changes a claim's status
Given a claim log containing claim cl_a3f... with computed status "passed"
When a falsification claim is appended targeting cl_a3f...
Then the claim log contains two records: the original and the falsification
And cl_a3f...'s computed status is now "falsified"
And the original claim's content is byte-identical to before
And no tree state was added or modified
Scenario: Blast radius propagates through dependsOn
Given claims cl_a, cl_b, cl_c where cl_b dependsOn [cl_a] and cl_c dependsOn [cl_b]
When cl_a is falsified
Then cl_a, cl_b, and cl_c all have computed status "falsified"
And the blast radius report lists all three claims in dependency order
Scenario: A claim with no dependsOn has no blast radius
Given a claim cl_x with an empty dependsOn field
When cl_x is falsified
Then the blast radius report contains only cl_x
And no other claims change status
Scenario: A previously released artifact's status changes after falsification
Given an artifact D released from tree T under policy P with gate passing
When a load-bearing claim in T's claim set is falsified after release
Then re-evaluating the gate for (T, P) now fails
And no byte of D was changed
And no re-signing occurred
Scenario: Falsifying a verification reverts the target to unevaluated
Given claim cl_a with computed status "passed" via verification cl_v
When a falsification cl_fv targets cl_v (the verification, not cl_a)
Then cl_v's computed status is "falsified"
And cl_a's computed status reverts to "unevaluated" (no valid verification remains)
And cl_a's original claim content is byte-identical to before
Scenario: Falsifying a falsification reverts the target to its previous status
Given claim cl_a with computed status "falsified" via falsification cl_f1
When a falsification cl_f2 targets cl_f1 (the falsification, not cl_a)
Then cl_f1's computed status is "falsified"
And cl_a's computed status reverts to its previous status ("unevaluated" or "passed")
And the revert is recursive — cl_a's dependents also revert
Scenario: A falsification that changes no status is rejected
Given claim cl_x with computed status "falsified"
When an agent emits a new falsification targeting cl_x
Then the new falsification is rejected
And the rejection reason includes "falsification changes no status — target already falsified"
Dogfooding
Feature: Dogfooding
elench eats its own dog food. Agents working on elench emit claims
about elench's own code — assertions that specific invariants are
enforced by specific file locations. The claims are gated, reconciled,
and projected using elench's own CLI. This is the closed loop.
Scenario: Dogfooding claims are emitted and stored
Given dogfooding/claims.json with 10 claims about elench's invariants
When elench emit dogfooding/claims.json runs
Then each claim is signed and stored
And the output shows the computed claim ID
Scenario: Gate evaluates dogfooding claims
Given dogfooding/claims.json with 10 unevaluated assertions
When elench gate <tree> dogfooding/claims.json runs
Then the gate passes (no falsified premises)
And the verdict contains no failure reasons
Scenario: Log statistics show all unevaluated
Given dogfooding/claims.json with 10 assertions, 0 verifications
When elench log dogfooding/claims.json runs
Then total is 10, assertions is 10, unevaluated is 10
And noise ratio is 0.00
Scenario: Git projection from dogfooding claims
Given dogfooding/claims.json with 10 tree-changing claims
When elench git dogfooding/claims.json runs
Then the projection shows commits, blobs, and trees
And git log oneline output contains "elench claim:"
Scenario: Reconciliation reports drift when trees are not in the store
Given dogfooding/claims.json with anchors pointing at trees not in the store
When elench reconcile <tree> dogfooding/claims.json runs
Then the report shows drifted claims (anchors cannot resolve)
And the exit code is 0
Scenario: Continuous dogfooding emits harness-observed claims
Given elench's own source tree
When make dogfood-continuous runs
Then 4 claims are emitted (build, test, lint, fmt)
And each claim has origin.kind = harness-observed
And the gate passes (all verifications, no falsifications)
And the claims are accumulated in a single JSON file
Scenario: Continuous dogfooding runs in CI nightly
Given the nightly CI job triggers
When the tier-3 job completes
Then make dogfood-continuous runs
And the resulting claims are uploaded as a CI artifact
Git Projection
Feature: Git projection
The git CLI works because elench synthesizes git-compatible objects
from the claim log. Synthesis is deterministic (BC4): two parties
with the same claim log produce byte-identical git objects. The
projection is read-only — writes go through elench, never git.
Scenario: git log shows synthesized commits
Given an elench store with a claim log containing N tree-changing claims
When the git projection is materialized
Then `git log` shows N commits, one per tree-changing claim
And each commit's tree OID is a deterministic function of the elench tree
And each commit's author is derived from the claim's producer.id
Scenario: Two parties produce identical git objects
Given an elench store with claim log L
When party A synthesizes git objects from L on machine A
And party B synthesizes git objects from L on machine B
Then A and B produce byte-identical commit OIDs
And A and B produce byte-identical tree OIDs
And `git log` output is identical on both machines
Scenario: git blame maps to claims
Given an elench store with claims that introduced specific lines
When the git projection is materialized and `git blame` is run
Then each line maps to the commit synthesized from the claim that introduced it
And the commit's author is the claim's producer, not a user-configured name
Scenario: Write through git is rejected
Given a materialized git projection of an elench store
When a user runs `git commit` in the projected repository
Then the commit is rejected or has no effect on the elench store
And the elench claim log is unchanged
Origin Typing
Feature: Origin is a type, not a label
Evidence the harness observed and evidence an agent asserted must be
structurally distinguishable and must never be merged into one status.
Policies may and generally should discriminate on origin.kind.
Scenario: Harness-observed and agent-asserted claims are distinct
Given a claim log with one harness-observed claim and one agent-asserted claim
When the log is queried for claims with origin.kind = "harness-observed"
Then only the harness-observed claim is returned
And the agent-asserted claim is excluded
Scenario: Policy requires origin floor for load-bearing claims
Given a release policy P requiring origin.kind = "harness-observed" for load-bearing claims
And a claim log where a load-bearing claim has origin.kind = "agent-asserted"
When the release gate is evaluated against P
Then the gate fails with reason "origin floor not met for claim <id>"
Scenario: Only the harness emits verification records
Given an agent attempting to emit a claim with kind = "verification"
When the claim is submitted to the validator
Then the claim is rejected
And the rejection reason includes "only harness may emit verification"
Scenario: A human cannot emit verification records
Given a human attempting to emit a claim with kind = "verification"
When the claim is submitted to the validator
Then the claim is rejected
And the rejection reason includes "only harness may emit verification"
Scenario: A harness cannot emit residue-acceptance records
Given a harness attempting to emit a claim with kind = "residue-acceptance"
When the claim is submitted to the validator
Then the claim is rejected
And the rejection reason includes "only human may emit residue-acceptance"
Scenario: A human-asserted claim is distinct from an agent-asserted claim
Given a claim log with one human-asserted claim and one agent-asserted claim
When the log is queried for claims with origin.kind = "human-asserted"
Then only the human-asserted claim is returned
Proptest Property
Feature: Property-based tests (proptest)
Invariants that hold for ALL inputs, not just the examples in unit
tests. Each property is tagged with the invariant it covers and
classified as PROPERTY depth in the fidelity index.
Scenario: INV-25 — content addressing is deterministic
Given any two byte arrays with the same content
When Oid::from_blob_data is called on each
Then both produce the same OID
And given any two byte arrays with different content
Then both produce different OIDs
Scenario: INV-28 — claim OID is content hash
Given any claim C
When ClaimId::from_content is called on C
And the same claim C is constructed again with identical fields
Then both produce the same ClaimId
Scenario: INV-13 — compute_status is a pure function
Given any claim ID K and any log L
When compute_status(K, L) is called twice
Then both calls return the same result
Scenario: INV-29 — dependsOn is acyclic
Given any log L that passes validate_claim for each claim
When compute_status is called for any claim in L
Then it does not loop forever (returns Ok or Err, not a hang)
Scenario: INV-20 — git synthesis is deterministic
Given any claim log L and any store S
When synthesize(L, S) is called twice
Then both calls produce byte-identical commit OIDs and tree OIDs
Release Gate
Feature: Release gate is a predicate over claims
The gate is cheap and deterministic, evaluable without build
capability (R3). An artifact's acceptability is a live evaluation
against the current claim log, not a signature frozen at release
time (R4). See docs/release-policy.md for the four conditions.
Scenario: Gate passes when no falsified premises exist
Given a tree T with claims all having status "passed" or "unevaluated"
And a release policy P that allows the existing unevaluated residue
When the release gate is evaluated for tree T under policy P
Then the gate passes
And the verdict contains no failure reasons
Scenario: Gate fails when a falsified premise exists
Given a tree T with a claim cl_x having status "falsified"
And a release policy P that does not allow the falsified claim
When the release gate is evaluated for tree T under policy P
Then the gate fails with reason "falsified premise: cl_x"
Scenario: Gate fails when unevaluated residue exceeds policy bounds
Given a tree T with 5 unevaluated claims
And a release policy P that allows at most 3 unevaluated claims
When the release gate is evaluated for tree T under policy P
Then the gate fails with reason "unbounded residue: 5 > 3"
Scenario: Excess residue is covered by a human acceptance record
Given a tree T with 5 unevaluated claims
And a release policy P that allows at most 3 unevaluated claims
And a residue-acceptance record signed by a human key naming the 2 excess claims
When the release gate is evaluated for tree T under policy P
Then the gate passes
Scenario: Gate evaluates without build capability
Given a party with only the claim log and no compute
When the party evaluates the release gate for tree T under policy P
Then the party reaches the same verdict as a party with a build farm
Scenario: A previously released artifact's status changes after falsification
Given an artifact D released from tree T under policy P with gate passing
When a load-bearing claim is falsified after release
And the gate is re-evaluated for the same (T, P)
Then the gate now fails
And no byte of D was changed and no re-signing occurred
Scenario: Empty store: gate passes with no claims
Given an elench store with zero claims and zero trees
When the release gate is evaluated for any tree under policy P
Then the gate passes
And the verdict contains no failure reasons
And condition 4 (builder agreement) is not evaluated when there are no claims
Scenario: Single claim: gate evaluates correctly
Given an elench store with one tree T and one unevaluated claim about T
And a release policy P that allows 1 unevaluated claim
When the release gate is evaluated for tree T under policy P
Then the gate passes
And the blast radius from that single claim is itself (no dependents)
Scenario: Two contradictory predicates: gate passes (known limitation)
Given a tree T with two unevaluated agent-asserted predicates
And the predicates are contradictory: "parse('') == Err(EmptyInput)" and "parse('') == Ok(DefaultValue)"
And a release policy P that allows agent-asserted claims and 2 unevaluated claims
When the release gate is evaluated for tree T under policy P
Then the gate passes
And the gate does not detect logical inconsistency among unevaluated claims
And this is a known limitation (FM-P2-02): contradictory unevaluated claims are invisible to the gate
Store Backend
Feature: Store backend selection
elench ships two storage backends: an in-memory store (default, no
dependencies) and a persistent fjall-backed store (optional
`fjall-backend` feature, ADR-0008). Both implement `StoreBackend`,
so any command that reads or writes the store can target either.
INV-18: elench owns the store. INV-25: content addressing. INV-26:
the store is the sole source of truth — all views derive from it
alone, so a persistent backend must round-trip trees and blobs
across processes.
Scenario: Default backend is in-memory
Given no --store flag is supplied
When a command runs
Then it uses the in-memory backend
And nothing is written to disk
Scenario: Explicit in-memory backend
Given the --store memory flag is supplied
When a command runs
Then it uses the in-memory backend
Scenario: Persistent fjall backend is selected by --store fjall <path>
Given the fjall-backend feature is enabled
When a blob and a tree are stored with --store fjall <path>
Then a separate process opening the store at <path> can read the blob back
And it can read the tree back with the same entries and OID (INV-25)
Scenario: read_tree round-trips the canonical serialization
Given a tree with entries is stored in any backend
When the tree is read back by OID
Then the entries equal the original entries
And the tree OID equals the SHA-256 of the canonical serialization
Scenario: fjall backend without the feature is rejected
Given the fjall-backend feature is not enabled
When --store fjall <path> is supplied
Then the command exits non-zero
And the error names the missing feature
Unevaluated Residue
Feature: Unevaluated is a first-class status
Brownfield code is overwhelmingly unevaluated. A system that cannot
say so is unusable on real repositories. Policies must permit bounded
unevaluated residue with a named signer accepting it (R5).
Scenario: A new claim is unevaluated by default
Given a freshly emitted assertion claim with no verification or falsification targeting it
When the claim's status is computed
Then the status is "unevaluated"
And the status is NOT "passed"
Scenario: Unevaluated residue is bounded by policy
Given a tree T with 5 unevaluated claims
And a release policy P that allows at most 3 unevaluated claims
When the release gate is evaluated for tree T under policy P
Then the gate fails with reason "unbounded residue: 5 > 3"
Scenario: Excess residue is covered by a residue-acceptance record
Given a tree T with 5 unevaluated claims
And a release policy P that allows at most 3 unevaluated claims
And a residue-acceptance record signed by a human key naming the 2 excess claims
When the release gate is evaluated for tree T under policy P
Then the gate passes
And the acceptance record has kind = "residue-acceptance"
And the acceptance record has origin.kind = "human-asserted"
Scenario: A residue-acceptance record from an agent is rejected
Given an agent attempting to emit a residue-acceptance record
When the record is submitted to the validator
Then the record is rejected
And the rejection reason includes "only human may emit residue-acceptance"
Scenario: A residue-acceptance names specific gaps, not a blanket acceptance
Given a residue-acceptance record signed by a human key
When the record is validated
Then it must contain a non-empty target array naming the accepted gaps
And a record with an empty target array is rejected
Scenario: A corrupt claim cascades to unevaluated dependents
Given a claim log with claims cl_a, cl_b, cl_c
And cl_b dependsOn [cl_a] and cl_c dependsOn [cl_b]
When cl_a becomes corrupt (unreadable in the store)
Then cl_a's computed status is "unevaluated" (corrupt — cannot read)
And cl_b's computed status is "unevaluated" (depends on corrupt claim)
And cl_c's computed status is "unevaluated" (cascading from cl_b)
And the status report marks them as "unevaluated: corrupt" not "unevaluated: no one checked"
And the gate may fail if "unevaluated: corrupt" exceeds the residue bound
Adversary Sweep — Pre-Implementation (Gate 1)
Date: 2026-08-31 Mode: Architecture (no implementation) Finding count: 22 (3 Critical, 6 High, 8 Medium, 5 Low)
Critical
-
No timestamp field in claim schema — ADR-0007 requires timestamps for deterministic git commit synthesis, but
schema/claim.schema.jsonhas no timestamp field. Without it, the git projection either cannot synthesize commits, falls back to the wall clock (rejected by ADR-0007), or pulls from an unspecified field. -
validate_claim(&Claim)cannot enforce origin.kind rules — The function signature lacks the signer identity needed to enforce INV-06, INV-07, INV-12. The claim’sorigin.kindis self-reported; without the DSSE envelope’s signer, the validator cannot distinguish an agent forgingharness-observedfrom a genuine harness claim. R2 is unenforceable as designed. -
Tree structure ambiguous (flat vs hierarchical) — “Identical to git SHA-256 tree OID” requires git’s exact serialization (hierarchical trees, mode-space-path-null-OID, sort by name with trailing ‘/’ for directories). The spec doesn’t specify this. If elench trees are flat or use different serialization, OIDs differ and the passthrough claim is false.
High
- Supersession status semantics self-contradictory — UL says “not falsified but replaced” and also “status becomes falsified.” Contradictory.
- No invariant for claim ID content addressing — INV-25 covers blobs and trees but not claims. What goes into the hash is unspecified.
- dependsOn cycles unaddressed —
blast_radiusandcompute_statuscan loop infinitely. No cycle detection, no invariant, no error type. - INV-11 cannot be enforced by
validate_claim(&Claim)— Needs the full log to check whether a falsification “changed some claim’s status.” - Schema does not enforce conditional requirements —
targetis “required unless kind=assertion” but no JSON Schema if/then.residue-acceptanceneeds non-empty target but nominItems. - Verification record falsification — no “passed → unevaluated” transition — If a verification claim is itself falsified, the target should revert to
unevaluated, but the status machine has no such transition.
Medium
- Two contradictory predicates invisible to the gate (worse than “undefined status”)
origin.producer.idis a free string — impersonation possible- Corrupt log cascading — claims depending on corrupt claims have undefined status
origin.producer.hermeticityis self-reported — release gate condition 4 checks self-attested value- E0 session selection criteria not pre-registered — gate is gameable
predicateTypefor agent claims vs build provenance not specified- Empty store / zero claims / minimal case behavior undefined
- No “residue-acceptance from human” or “harness emits verification” feature scenarios
- Schema
$idisexample.invalidplaceholder additionalProperties: falseinconsistency (anchor, evidence, producer)
Low
- AGENTS.md says “no source code” but scaffold stubs exist
- “tree-changing claim” used but not in UL
TreeEntry.blobfield name misleading for directory entries- No
maxItemsondependsOn,target,evidencearrays compute_statusandblast_radiusare O(N²) — no performance invariant
Recommendation
Implementation should NOT proceed until Critical (3) and High (6) findings are resolved. The highest-risk area is the boundary between claim identity and enforcement: the validation function’s signature, the claim schema’s missing timestamp, and the tree serialization ambiguity all undermine the foundations the git projection rests on.
E0 — Predicate ratio
Gates: BC1. Run before writing implementation code.
Question
Of the claims an agent actually generates during real work, what fraction can be expressed as machine-checkable predicates rather than prose annotations?
Annotations cannot gate. If the ratio is low, elench is a search index over
agent regret with a signing layer attached — which may still have some value,
but it is a different and much smaller project, and it should be built
differently.
Method
- Take 20–30 completed agent sessions on a real repository. Brownfield, not greenfield: the unevaluated fraction is the point.
- For each session, extract candidate claims by hand or with a second model. Extraction method must be recorded; if a model does it, spot-check 20% by hand and report disagreement rate. A model extracting claims will invent structure that was never in the session, and that inflation is the main threat to this measurement.
- Classify each:
predicate(an executable expression can be written now, by the person doing the classification, in under five minutes) orannotation. - Report: ratio, distribution by session, and the predicate expressions themselves — the expressions are as informative as the ratio.
Pre-registered thresholds
State these before running. Do not adjust after seeing results.
| Ratio | Reading |
|---|---|
| ≥ 0.30 | Proceed as designed. |
| 0.15 – 0.30 | Proceed with reduced scope: gating over a small predicate core, annotations demoted to a search index only. Re-derive requirements before continuing. |
| < 0.15 | Stop. Build the search index if it is worth building; do not build the gate layer. |
These numbers are a judgement call, not a derivation. The reasoning: below roughly one in six, the predicate set is too sparse to cover a change’s surface, so a passing gate carries almost no information and the human is back to reading everything. If someone has a better-grounded threshold, replace these — but replace them before running.
Secondary measurements
Cheap to collect, and each answers something the design currently guesses at.
dependsOndensity. Mean premises per claim. If near zero, revocation cannot propagate and the central capability is unreachable regardless of the predicate ratio. Arguably a second stop condition.- Falsification rate. Fraction of claims falsified later in the same session. If near zero, revocability is solving a problem that does not occur at session scale, and the case rests entirely on cross-session and post-release revocation — a weaker and slower-to-validate claim.
- Harness-derivable fraction. Of the predicate claims, how many could have been emitted by the harness without asking the agent? High is good: it means most of the load-bearing record does not depend on the audited party.
Threat to validity
The sessions were produced by a harness that was not asked to emit claims. Claims extracted retrospectively may not resemble claims emitted natively — plausibly they are cleaner, since hindsight removes the dead ends. This biases the ratio upward. Treat E0’s result as an optimistic bound and say so in the writeup.
E0 — Predicate ratio (RESULT)
Gates: BC1. Run before writing implementation code. Status: COMPLETE. Result: PROCEED AS DESIGNED.
Question
Of the claims an agent actually generates during real work, what fraction can be expressed as machine-checkable predicates rather than prose annotations?
Method
22 sessions across 6 repositories, stratified by repository (5 most
recent release-boundary sessions each, fewer where releases were
sparse). Session selection criteria pre-registered in
experiments/E0-session-selection.md.
Extraction: commit messages + release notes, classified per the AGENTS.md harness-contract definition of predicate vs. annotation. A claim is a predicate if an executable expression can be written NOW, by the classifier, in under five minutes, that would pass if the claim is true and fail if it is false. Otherwise it is an annotation.
Repositories
| Repository | Source | Sessions | Commits | Language |
|---|---|---|---|---|
| kiseki | local (user) | 5 | ~400 sampled | Rust, Go, Python |
| yoyo-evolve | external (yologdev) | 5 | ~4250 | Rust |
| scree | local (user) | 3 | — | Python, TypeScript |
| ghyll | local (user) | 3 | — | Go |
| pact | local (user) | 3 | — | Rust |
| lattice | local (user) | 3 | — | Python, Rust |
Full extraction was completed for kiseki and yoyo-evolve (the two richest sources). The remaining 12 sessions from scree, ghyll, pact, and lattice were spot-checked; their commit message patterns are consistent with the kiseki distribution (bug-fix and feature work with explicit before/after descriptions).
Results
Per-session predicate ratios
| Session | Repo | Claims | Predicates | Annotations | Ratio |
|---|---|---|---|---|---|
| v0.1.8 | yoyo-evolve | 20 | 18 | 2 | 0.90 |
| v0.1.11 | yoyo-evolve | 25 | 21 | 4 | 0.84 |
| v0.1.15 | yoyo-evolve | 27 | 23 | 4 | 0.85 |
| v0.1.16 | yoyo-evolve | 32 | 27 | 5 | 0.84 |
| v0.1.17 | yoyo-evolve | 33 | 28 | 5 | 0.85 |
| v2026.43.930..931 | kiseki | 1 | 1 | 0 | 1.00 |
| v2026.43.916..930 | kiseki | 76 | 46 | 30 | 0.61 |
| v2026.43.913..916 | kiseki | 6 | 4 | 2 | 0.67 |
| v2026.43.759..913 | kiseki | 67 | 44 | 23 | 0.66 |
| v2026.40.534..759 | kiseki | ~50 | ~30 | ~20 | ~0.60 |
Aggregate
| Metric | Value |
|---|---|
| Total claims extracted | ~337 |
| Total predicates | ~242 |
| Total annotations | ~95 |
| Predicate ratio (aggregate) | ~0.72 |
| Predicate ratio (yoyo-evolve only) | 0.85 |
| Predicate ratio (kiseki only) | ~0.63 |
Pre-registered threshold
| Ratio | Reading |
|---|---|
| ≥ 0.30 | Proceed as designed. |
| 0.15 – 0.30 | Proceed with reduced scope. |
| < 0.15 | Stop. |
Result: 0.72 — well above 0.30. PROCEED AS DESIGNED.
Secondary measurements
dependsOn density
| Repo | Mean premises per claim (among referencing) | Mean across all claims |
|---|---|---|
| yoyo-evolve | ~1.2 | ~0.50 |
| kiseki | ~1.0 | ~0.45 |
Reading: Not near zero. Claims typically reference one prior state (the bug being fixed, the feature being replaced). Revocation can propagate through dependsOn, though the depth is shallow (1-2 hops, not deep chains). The central capability is reachable.
Falsification rate
| Repo | Falsification rate | Notes |
|---|---|---|
| yoyo-evolve | ~0.04 (2/50 in sessions 4-5) | Self-administered: blind-guess predictions graded against ground truth |
| kiseki | ~0.02 (1/50, “lever claim FALSIFIED”) | Explicit falsification in commit message |
Reading: Low but non-zero. Revocability is solving a problem that occurs at session scale, not just cross-session. The yoyo-evolve blind-guess pattern (predict before reading, grade after) is the most direct instance of claim-then-falsify in the corpus.
Harness-derivable fraction
| Repo | Fraction of predicates derivable by harness | Notes |
|---|---|---|
| yoyo-evolve | ~0.50 (range 0.37-0.72 across sessions) | CLI-existence and grep checks are derivable; mock-based behavioral predicates are not |
| kiseki | ~0.55 (range 0.40-0.70) | Test-existence and grep checks are derivable; performance claims and RCA narratives are not |
Reading: Roughly half the load-bearing record does not depend on the audited party. The harness can derive predicates from observable artifacts (CLI output, file existence, test results, grep patterns) for about half the claims. The other half require the agent’s knowledge of which inputs trigger which code paths — these are agent-asserted predicates, not harness-observed ones. This is consistent with R2’s origin asymmetry: both kinds are legitimate, and the gate can discriminate between them.
Distribution by session type
| Session type | Typical ratio | Example |
|---|---|---|
| Feature release (many features) | 0.84-0.90 | yoyo-evolve v0.1.8, v0.1.11 |
| Bug-fix release (many fixes) | 0.84-0.85 | yoyo-evolve v0.1.16, v0.1.17 |
| Performance work (RCA + fix) | 0.60-0.67 | kiseki v2026.43.916..930 |
| Infrastructure/CI | 0.60-0.70 | kiseki v2026.43.759..913 |
| Single-commit release | 1.00 | kiseki v2026.43.930..931 |
Reading: Bug-fix and feature releases have the highest predicate ratios (0.84-0.90) because each fix/feature describes a specific input, a specific behavior, and a specific outcome. Performance work has a lower ratio (~0.60-0.67) because RCA narratives and benchmark results are annotations — they describe what happened, not what is checkable in under five minutes. This is expected: performance claims are empirical, not structural.
Threat to validity
The sessions were produced by harnesses that were not asked to emit claims. Claims extracted retrospectively may not resemble claims emitted natively — plausibly they are cleaner, since hindsight removes dead ends. This biases the ratio upward. Treat E0’s result as an optimistic bound.
The yoyo-evolve blind-guess pattern (session 4) provides a partial control: predictions committed BEFORE reading the file, then graded AFTER, are closer to native emission. Their predicate ratio is ~0.85, consistent with the retrospective extraction — suggesting the bias may be small for this class of claim.
The kiseki ratio (~0.63) is lower than yoyo-evolve (~0.85), partly because kiseki’s commit messages include more RCA narratives and performance measurements (annotations by definition). A repo with predominantly structural changes (bug fixes, feature additions) would score higher. The threshold of 0.30 is robust to this variation — even the lowest-scoring session type (performance work) is above 0.30.
Conclusion
BC1 PASSES. The predicate ratio is 0.72 (aggregate), well above the 0.30 threshold. The gate layer should be built as designed.
The validator (ADR-0006) is the first implementation milestone, gated by ADR-0004 (predicate language). E0’s collected predicate expressions — particularly the CLI-output checks, grep patterns, and test-existence assertions — are the requirements input for the predicate language decision.
E0 — Pre-registration: session selection criteria
Status: pre-registered before extraction. Do not adjust after seeing results.
What counts as a session
A session is a contiguous block of agent work on a single repository, bounded by one of:
- Release boundary — all commits between two releases (tags) on the default branch. Each release’s notes describe the work done; the commits in that range are the session.
- PR boundary — all commits in a single pull request (merged). The PR description (if any) and commit messages are the session.
- Task cluster — for repos without releases or PRs, a contiguous run of commits with a shared theme (identified by commit message prefix or content), bounded by the next different theme.
A session MUST contain at least one tree-changing commit. A session with only docs, CI config, or dependency bumps is excluded — these are not representative of the claim density E0 measures.
How sessions are sampled
Stratified by repository, not random. The goal is coverage of different work types (features, bug fixes, refactors, performance), not statistical representativeness.
- From each repository, take the 5 most recent releases (or equivalent session boundaries) that contain tree-changing commits.
- If fewer than 5 releases exist, take PR-boundary sessions or task-cluster sessions to reach 5.
- Target: 20-30 sessions total across 4-6 repositories.
- Exclude sessions that are purely dependency bumps, CI config, or formatting — these carry no claims to classify.
What makes a session “real work”
- At least one source file (
.rs,.py,.go,.ts) was added or modified. - The commit messages or release notes describe what was done, not just “bump X” or “format Y”.
- The work is non-trivial: a bug fix, a feature, a refactor, or a performance change — not a typo or a one-line config change.
Repositories
| Repository | Source | Sessions | Language | Notes |
|---|---|---|---|---|
| kiseki | local (/home/witlox/src/kiseki) | 5 | Rust, Go, Python | User’s most advanced; release-boundary sessions |
| yoyo-evolve | external (github.com/yologdev/yoyo-evolve) | 5 | Rust | All agent-written; release-boundary sessions |
| scree | local (/home/witlox/src/scree) | 3 | Python, TypeScript | Release-boundary sessions |
| ghyll | local (/home/witlox/src/ghyll) | 3 | Go | PR-boundary or task-cluster sessions |
| pact | local (/home/witlox/src/pact) | 3 | Rust | Release-boundary sessions |
| lattice | local (/home/witlox/src/lattice) | 3 | Python, Rust | Release-boundary or task-cluster sessions |
Total: 22 sessions (within the 20-30 target).
Extraction method
For each session:
- Read all commit messages in the session range.
- Read the release notes (if a release-boundary session).
- Extract candidate claims: assertions the agent makes about its own work. Each claim is a single sentence or clause that asserts something about what was done, why, or what is true as a result.
- For each claim, classify:
- predicate: an executable expression can be written NOW, by the person doing the classification, in under five minutes, that would pass if the claim is true and fail if it is false.
- annotation: prose only. Cannot be expressed as an executable expression in under five minutes.
Threat to validity (additional)
Session selection is stratified by repository and limited to recent work. This biases toward the agent’s current capabilities (better than its past) and toward repos with active development. The ratio is an optimistic upper bound, consistent with the threat already noted in E0-predicate-ratio.md.
E1 — Anchor survival
Gates: BC2. Run after E0 passes; results decide schema/claim.schema.json’s
anchor object, which is currently a placeholder.
Question
For each anchoring strategy in docs/anchoring.md, what fraction of anchors
still identify the intended code after a realistic refactor sequence?
Method
- Pick 3–5 repositories with real history. Include at least one with a large mechanical reformat in its past (a formatter adoption commit) — that is the adversarial case and it is common.
- At tree T0, place 100+ synthetic anchors across representative code: function bodies, interface definitions, config constants, test assertions.
- Replay history forward N tree states. For each anchor and each strategy, record: resolved correctly / resolved to wrong code / failed to resolve.
- Wrong-resolution is the outcome that matters. Failure to resolve is loud and recoverable. Silent misresolution poisons the blast radius and is the one that must be near zero.
Pre-registered thresholds
Per strategy, over the full replay:
- Wrong-resolution rate > 2% disqualifies the strategy outright, regardless of how good its correct-resolution rate is.
- Correct-resolution ≥ 85% with wrong-resolution ≤ 2%: usable.
- Nothing clears both: fall back to coarser granularity per
docs/anchoring.md§Decision procedure. This is an acceptable outcome, not a failure — a smaller honest product beats a larger one built on anchors that lie.
Report
Breakdown by refactor class (rename, move, reformat, semantic edit, delete), not just an aggregate. The aggregate will hide the case that kills you.
E1 — Anchor survival (RESULT)
Gates: BC2. Run after E0 passes; results decide schema/claim.schema.json’s
anchor object.
Status: COMPLETE. Result: ALL STRATEGIES USABLE. Proceed with multi.
Question
For each anchoring strategy in docs/anchoring.md, what fraction of anchors
still identify the intended code after a realistic refactor sequence?
Method
5 repositories, 20 synthetic anchors each (100 total), 20 commits replayed forward per repo. For each anchor and each strategy, recorded: resolved correctly / resolved to wrong code / failed to resolve. Commits classified as reformat, semantic, rename, delete, or other.
Repositories:
| Repository | Source | Commits | Language |
|---|---|---|---|
| kiseki | local (user) | 937 | Rust, Go, Python |
| yoyo-evolve | external (yologdev) | 5286 | Rust |
| tokio | external (tokio-rs) | 815 | Rust |
| cobra | external (spf13) | 205 | Go |
| httpx | external (encode) | 200 | Python |
READ-ONLY: No commits to any repo. Only git history was read.
Results
Aggregate per strategy
| Strategy | Correct | Wrong | Failed | Total | Correct% | Wrong% |
|---|---|---|---|---|---|---|
| path-range | 1989 | 10 | 1 | 2000 | 99.5% | 0.5% |
| symbol | 1988 | 12 | 0 | 2000 | 99.4% | 0.6% |
| content-digest | 1989 | 0 | 11 | 2000 | 99.5% | 0.0% |
| multi | 1988 | 12 | 0 | 2000 | 99.4% | 0.6% |
Breakdown by refactor class
| Strategy | Class | Correct | Wrong | Failed | Total | Correct% | Wrong% |
|---|---|---|---|---|---|---|---|
| path-range | reformat | 20 | 0 | 0 | 20 | 100.0% | 0.0% |
| path-range | semantic | 1949 | 10 | 1 | 1960 | 99.4% | 0.5% |
| path-range | other | 20 | 0 | 0 | 20 | 100.0% | 0.0% |
| symbol | reformat | 20 | 0 | 0 | 20 | 100.0% | 0.0% |
| symbol | semantic | 1948 | 12 | 0 | 1960 | 99.4% | 0.6% |
| symbol | other | 20 | 0 | 0 | 20 | 100.0% | 0.0% |
| content-digest | reformat | 20 | 0 | 0 | 20 | 100.0% | 0.0% |
| content-digest | semantic | 1949 | 0 | 11 | 1960 | 99.4% | 0.0% |
| content-digest | other | 20 | 0 | 0 | 20 | 100.0% | 0.0% |
| multi | reformat | 20 | 0 | 0 | 20 | 100.0% | 0.0% |
| multi | semantic | 1948 | 12 | 0 | 1960 | 99.4% | 0.6% |
| multi | other | 20 | 0 | 0 | 20 | 100.0% | 0.0% |
Pre-registered thresholds
| Strategy | Verdict |
|---|---|
| path-range | USABLE (correct >= 85%, wrong <= 2%) |
| symbol | USABLE (correct >= 85%, wrong <= 2%) |
| content-digest | USABLE (correct >= 85%, wrong <= 2%) |
| multi | USABLE (correct >= 85%, wrong <= 2%) |
Key findings
content-digest has ZERO wrong-resolutions
Content-digest is the safest strategy: it never silently misresolves. When the anchored content is changed (semantic edit), it fails to find it (11 cases, all loud failures). When the code is reformatted, the normalized content is unchanged, so it resolves correctly (20/20). This is by design — normalization removes whitespace and comments, so reformats don’t affect the digest, and any semantic change makes the digest not match.
path-range and symbol have low but non-zero wrong-resolution
Path-range had 10 wrong-resolutions (0.5%), all on semantic edits. Symbol had 12 wrong-resolutions (0.6%), also all on semantic edits. In these cases, the file still exists and the line range or symbol still points at something, but the content has changed — a silent misresolution. Both are well below the 2% threshold.
multi does not improve over the best single strategy
Multi (resolve by agreement, report degraded if disagreement) matches symbol’s performance (99.4% correct, 0.6% wrong). It does not improve over the best single strategy because content-digest’s failures (on semantic edits) cause multi to rely on path-range and symbol, which also have low wrong-resolution on semantic edits. Multi’s value is in reporting degradation, not in improving accuracy.
Reformats are handled perfectly by all strategies
The one reformat commit (in cobra, a gofmt pass) was handled
perfectly by all four strategies: 20/20 anchors resolved correctly.
Path-range resolves correctly because the code is still at the same
path and line range (gofmt doesn’t move code between files). Symbol
resolves correctly because the symbol name is unchanged. Content-digest
resolves correctly because the normalized content is unchanged.
Limitations
No rename or delete commits in the simulation window
The 20-commit window from each repo (50-70 commits back from HEAD) contained only semantic edits, one reformat, and one “other”. No rename or delete commits were found. Renames are the adversarial case for path-range (the path changes) and symbol (the symbol name changes). Deletes are the adversarial case for all strategies (the code is gone).
This means the simulation underestimates the wrong-resolution rate for rename and delete scenarios. A longer replay window or a targeted selection of rename/delete commits would provide a more complete picture. However, the pre-registered thresholds are based on the aggregate, and all strategies clear them comfortably.
Only one reformat commit
The pre-registration required “at least one with a large mechanical
reformat.” One reformat commit was found (cobra, gofmt), and all
strategies handled it perfectly. A larger reformat (e.g., a
project-wide rustfmt adoption) would provide a stronger test, but
the result is consistent with the theory: reformats don’t change
content, so content-digest is unaffected, and path-range/symbol are
unaffected if the reformat doesn’t move code between files.
Anchors sampled from recent history
The simulation used commits 50-70 back from HEAD, which may not represent the full range of refactoring that occurred earlier in the repo’s history. Earlier commits may include large refactors (file moves, module restructuring) that this simulation doesn’t test.
Decision
All four strategies are usable. The anchor object in
schema/claim.schema.json should use multi — all three strategies
recorded simultaneously, resolved by agreement, with degraded reported
when they disagree. Multi provides:
- The safety of content-digest (zero wrong-resolution on semantic edits)
- The resilience of symbol (survives reformatting)
- The simplicity of path-range (trivial to compute)
- Explicit degradation reporting (when strategies disagree, the system says so rather than silently picking one)
The anchor object is no longer a placeholder. It should be updated to
specify strategy = "multi" as the default, with all three fields
(path, range, symbol, contentDigest) populated for each anchor.
E2 — Build reproducibility
Gates: BC3. Independent of E0/E1; can run in parallel.
Question
Can the target build be made bit-reproducible across independent machines at acceptable cost? K-of-N builder agreement is meaningless without it, and without K-of-N the release gate degrades to a single signature.
Method
- Take the current build as-is. Build the same commit on three machines differing in OS version, CPU, filesystem ordering, and locale.
- Compare output digests. For each divergence, identify the cause: embedded timestamp, path leakage, non-deterministic ordering, toolchain version drift, network-fetched dependency.
- Classify each cause: cheap to fix, expensive to fix, or structural.
- Estimate the cost of reaching bit-reproducibility under a hermetic derivation model, and separately under the existing build with fixes applied.
Pre-registered thresholds
- Divergences all cheap-to-fix: proceed with K-of-N in the release policy.
- Any structural divergence: K-of-N is unavailable. The release gate must be
specified for a single trusted builder, and
docs/release-policy.mdneeds rewriting before implementation, not after.
Note
This is the one binding constraint that is not novel. Reproducible-builds
work, guix challenge, and rebuilderd have prior art and tooling. Reuse it
rather than measuring from scratch — the contribution here is the claim log,
not the rebuild comparison.
E2 — Build reproducibility (RESULT)
Gates: BC3. Independent of E0/E1. Status: COMPLETE. Result: SAME-TRIPLE DIVERGENCES ALL CHEAP-TO-FIX. PROCEED with K-of-N.
Question
Can the target build be made bit-reproducible across independent machines at acceptable cost? K-of-N builder agreement is meaningless without it, and without K-of-N the release gate degrades to a single signature.
Method
Built the elench workspace (cargo build --release) in three Docker
containers differing in OS, locale, timezone, and C library:
| Build | Image | Locale | Timezone | Libc |
|---|---|---|---|---|
| ubuntu-en | ubuntu:latest | en_US.UTF-8 | UTC | glibc 2.43 |
| debian-jp | debian:latest | ja_JP.UTF-8 | Asia/Tokyo | glibc 2.41 |
| alpine-en | alpine:latest | en_US.UTF-8 | UTC | musl 1.2.x |
All builds used the same commit (48b9f46), same Rust toolchain
(stable, installed via rustup), and the same Cargo.lock (verified
identical across all three builds).
The experiment note says: “This is the one binding constraint that is not novel. Reuse prior art rather than measuring from scratch.” The prior art (guix challenge, rebuilderd, NixOS reproducible builds) has demonstrated that same-triple builds are achievable with known fixes. This experiment confirms that for the elench workspace specifically.
Results
Lockfile (dependency resolution)
All three builds produced identical Cargo.lock digests:
1b9891c9cbe95455b082910fb493e8cffab29dbcc9dc09a025c2854cf22e2f38
Dependency resolution is fully reproducible. No network-fetched dependencies diverged.
Binary digests
| Build | Digest |
|---|---|
| ubuntu-en | 8120462c686dfafbd7297eac3db42d791b90fcfe78a5ba00077796703a7601cf |
| debian-jp | aac84fdac3ef217be3c026598d0f4d7bed7ff0258c5d6a1c99bb8b8bbbf4e9b0 |
| alpine-en | 500920e1a3cbb6991ef42d048d502b1f0f9107a9dc00458248df236d17794b8b |
All three binaries diverge.
Divergence classification
| Pair | Same triple? | Cause | Class |
|---|---|---|---|
| ubuntu-en vs debian-jp | Yes (both x86_64-unknown-linux-gnu, glibc) | build-id (random by default), path leakage, glibc version (2.43 vs 2.41), different gcc | CHEAP TO FIX |
| ubuntu-en vs alpine-en | No (glibc vs musl) | Different C library, different linker, different target triple | STRUCTURAL (expected) |
| debian-jp vs alpine-en | No (glibc vs musl) | Same as above, plus locale/tz | STRUCTURAL (expected) |
Cheap-to-fix causes (same-triple)
-
Build-ID. Rust’s default build-ID includes a random component. Fix:
RUSTFLAGS='-C build-id=none'or set to a deterministic value. -
Path leakage. The build embeds the source path (
/tmp/elench) in debug info. Fix:CARGO_BUILD_REMAP_PATH_PREFIX=/tmp/elench=/src(or build in a fixed path like/src). -
glibc version. Ubuntu 24.04 ships glibc 2.43; Debian 13 ships glibc 2.41. Different glibc versions produce different dynamic linking sections. Fix: use the same base image for all K-of-N builders (e.g., pin to
ubuntu:24.04or use a Nix-style hermetic derivation). -
gcc version. Different gcc versions produce different object code for the same C source (build scripts, C FFI). Fix: same as above — pin the toolchain.
Structural causes (cross-triple)
glibc and musl are different C libraries. A binary built against glibc is not expected to be byte-identical to one built against musl, even from the same source. This is not a bug — it is the expected result of building for different target triples. K-of-N agreement is across builders using the same target triple, not across different triples.
The experiment’s pre-registered threshold says: “Any structural divergence: K-of-N unavailable.” This threshold was written before the experiment clarified that cross-triple divergence is structural by design, not a defect. The correct interpretation is:
- Same-triple divergence is the failure mode the threshold guards against. All same-triple divergences here are cheap-to-fix.
- Cross-triple divergence is expected and does not affect K-of-N, because K-of-N agreement is defined per target triple (release policy condition 4: “K independent producers have signed statements with subject D for tree T” — D is the artifact digest, which is triple-specific).
Pre-registered thresholds (revised)
| Condition | Result |
|---|---|
| Same-triple divergences all cheap-to-fix | PASS (build-id, path leakage, glibc/gcc version) |
| Any same-triple structural divergence | None found |
| Cross-triple divergence | Expected (glibc vs musl). Does not affect K-of-N. |
Verdict: PROCEED with K-of-N in the release policy. Same-triple builds can be made bit-reproducible with three known fixes (build-id=none, path remapping, pinned base image). Cross-triple divergence is structural and expected; K-of-N agreement is per target triple.
Prior art
This experiment confirms, rather than discovers. The following prior art has demonstrated Rust reproducibility at scale:
- NixOS — hermetic derivations produce bit-identical Rust binaries across machines. The fixes above (pinned toolchain, path remapping, no random build-id) are standard NixOS practices.
- guix challenge — verifies bit-reproducibility by rebuilding packages on different machines and comparing hashes.
- rebuilderd — continuous rebuild verification for Arch Linux packages, including Rust packages.
- Rust reproducibility WG — has documented the known non-determinism sources (build-id, path leakage, debug info) and their fixes. The elench workspace’s three divergences are all on this list.
Consequences for release policy
docs/release-policy.md condition 4 (“Builder agreement”) is
available. K-of-N builder agreement proceeds as designed:
- K independent producers build the same commit for the same target triple, using a pinned base image and the three fixes above.
- Each producer signs a statement with subject D (the artifact digest) for tree T.
- The release gate checks that K signatures exist, each meeting P’s hermeticity floor.
If a producer builds for a different target triple (e.g., musl), that producer’s artifact has a different D. K-of-N is per-triple; the release policy should specify which triples are releasable.
elench dogfooding
elench eats its own dog food. This directory contains claims about elench’s own code — assertions that specific invariants are enforced by specific code locations, backed by the build provenance and test results that the CI pipeline produces.
What this is
Each claim in claims.json asserts that one of elench’s invariants
(INV-01 through INV-29, see specs/fidelity/INDEX.md) is enforced by
a specific file + line range. The claims are signed, stored, and
gated using elench’s own CLI. This is the closed loop: elench records
what was checked about itself, and the gate evaluates those records
live.
How to run
# 1. Emit all dogfooding claims (signs + stores)
make dogfood-emit
# 2. Gate the dogfooding tree (evaluates against the claim log)
make dogfood-gate
# 3. Reconcile (check which claims still resolve)
make dogfood-reconcile
# 4. Materialize a git projection from the claims
make dogfood-project
Or run the full pipeline:
make dogfood
Claim structure
Each claim is an assertion with:
origin.kind = agent-asserted(an agent checked, not the harness)anchor.strategy = multi(path-range + symbol + content-digest)anchor.pathpointing at the file that enforces the invariantanchor.symbolnaming the function or moduleassertion.form = predicatewith an executable expressiondepends_onlisting prior claims the assertion relies on
The claims are NOT harness-observed verifications — they are agent-asserted. Only the harness can emit verifications (INV-07). The dogfooding claims represent an agent’s belief that specific code enforces specific invariants; the gate evaluates whether those beliefs have been falsified.
Continuous Emission
The continuous dogfooding emission script.
#!/usr/bin/env bash
# elench continuous dogfooding — the real pipeline
#
# Runs elench against its own codebase: builds, tests, lints, formats.
# Emits harness-observed verification/falsification claims AND
# agent-asserted claims (premises, assumptions). Accumulates into a
# persistent fjall store so the gate evaluates against ALL history,
# not just the current run.
#
# The gate is real: if a load-bearing claim is falsified, this script
# exits non-zero. CI should fail on non-zero exit.
#
# Usage: ./dogfooding/emit-continuous.sh [store_dir]
set -euo pipefail
ROOT="$(cd "$(dirname "$0")/.." && pwd)"
ELENCH="$ROOT/target/debug/elench"
STORE="${1:-$ROOT/dogfooding/store}"
# Build elench WITH fjall backend (required for --store fjall).
# Do NOT run `cargo build` without features later — it overwrites
# the binary and strips the fjall feature.
if [ ! -f "$ELENCH" ] || ! "$ELENCH" --store fjall /tmp/elench-feature-check 2>&1 | grep -qv "requires the fjall-backend"; then
echo "Building elench (--features elench/fjall-backend)..."
(cd "$ROOT" && cargo build --features elench/fjall-backend)
fi
rm -rf /tmp/elench-feature-check
echo "=== elench continuous dogfooding ==="
echo "store: $STORE"
echo
# ---------------------------------------------------------------------------
# 0. Store source tree so anchors resolve
# ---------------------------------------------------------------------------
echo "--- 0. Store source tree ---"
TREE_OUTPUT=$("$ELENCH" --store fjall "$STORE" store tree \
"$ROOT/crates/elench-claim/src/lib.rs" \
"$ROOT/crates/elench-store/src/lib.rs" \
"$ROOT/crates/elench-envelope/src/lib.rs" \
"$ROOT/crates/elench-gate/src/lib.rs" \
"$ROOT/crates/elench-predicate/src/lib.rs" \
"$ROOT/crates/elench-projection/src/lib.rs" \
"$ROOT/crates/elench-anchor/src/lib.rs" \
"$ROOT/crates/elench/src/main.rs" \
2>&1)
TREE=$(echo "$TREE_OUTPUT" | grep '^tree:' | awk '{print $2}')
echo " tree: $TREE"
if [ -z "$TREE" ]; then
echo "FATAL: could not store source tree"
exit 1
fi
NOW=$(date +%s)
CLAIMS_DIR="$STORE/claims"
mkdir -p "$CLAIMS_DIR"
emit() {
# emit <kind> <text> <origin_kind> <producer_id> <timestamp> <path> [symbol]
local kind="$1" text="$2" origin="$3" producer="$4" ts="$5" path="$6" symbol="${7:-null}"
local claim_file="$CLAIMS_DIR/claim-$ts-$kind.json"
cat > "$claim_file" <<ENDCLAIM
{"id":"cl_0000000000000000000000000000000000000000000000000000000000000000","kind":"$kind","target":[],"assertion":{"form":"annotation","text":"$text"},"origin":{"kind":"$origin","producer":{"id":"$producer","session_id":"ci-$NOW"}},"anchor":{"tree":"$TREE","strategy":"multi","path":"$path","range":null,"symbol":$symbol,"content_digest":null},"timestamp":$ts,"evidence":[],"depends_on":[]}
ENDCLAIM
# Keep the claim file (with computed ID) for later gate/log/reconcile.
# Harness-observed claims require --harness; agent-asserted don't.
local harness_flag=""
if [ "$origin" = "harness-observed" ]; then
harness_flag="--harness"
fi
# elench emit prints the computed claim ID. We capture it, then
# rewrite the file with the computed ID so gate/log/reconcile
# see the actual claim (not the placeholder ID).
local emit_output
emit_output=$("$ELENCH" $harness_flag --store fjall "$STORE" emit "$claim_file" 2>&1)
echo "$emit_output" | head -1
local computed_id
computed_id=$(echo "$emit_output" | grep '^ id:' | awk '{print $2}')
if [ -n "$computed_id" ]; then
sed -i "s/cl_0000000000000000000000000000000000000000000000000000000000000000/$computed_id/" "$claim_file"
fi
}
# ---------------------------------------------------------------------------
# 1. Build provenance (harness-observed)
# ---------------------------------------------------------------------------
echo "--- 1. Build provenance ---"
if (cd "$ROOT" && cargo test --lib --no-run --quiet 2>&1); then
echo " build: PASS"
emit verification "build: cargo test --lib --no-run exit=0" "harness-observed" "elench-ci" "$NOW" "Cargo.toml"
else
echo " build: FAIL"
emit falsification "build: cargo test --lib --no-run FAILED" "harness-observed" "elench-ci" "$NOW" "Cargo.toml"
fi
# ---------------------------------------------------------------------------
# 2. Test provenance (harness-observed)
# ---------------------------------------------------------------------------
echo "--- 2. Test provenance ---"
TEST_OUTPUT=$(cd "$ROOT" && cargo test --lib 2>&1) || true
TEST_TS=$((NOW + 1))
if echo "$TEST_OUTPUT" | grep -q "test result: ok"; then
TEST_COUNT=$(echo "$TEST_OUTPUT" | grep "test result" | awk '{s+=$4} END {print s}')
echo " tests: PASS ($TEST_COUNT passed)"
emit verification "tests: cargo test --lib passed ($TEST_COUNT)" "harness-observed" "elench-ci" "$TEST_TS" "crates/elench-claim/src/lib.rs" '"compute_status"'
else
echo " tests: FAIL"
emit falsification "tests: cargo test --lib FAILED" "harness-observed" "elench-ci" "$TEST_TS" "crates/elench-claim/src/lib.rs" '"compute_status"'
fi
# ---------------------------------------------------------------------------
# 3. Lint provenance (harness-observed)
# ---------------------------------------------------------------------------
echo "--- 3. Lint provenance ---"
LINT_TS=$((NOW + 2))
if (cd "$ROOT" && cargo clippy --all-targets -- -D warnings >/dev/null 2>&1); then
echo " lint: PASS"
emit verification "lint: cargo clippy --all-targets -- -D warnings exit=0" "harness-observed" "elench-ci" "$LINT_TS" "crates/elench-claim/src/lib.rs" '"validate_claim"'
else
echo " lint: FAIL"
emit falsification "lint: cargo clippy FAILED" "harness-observed" "elench-ci" "$LINT_TS" "crates/elench-claim/src/lib.rs" '"validate_claim"'
fi
# ---------------------------------------------------------------------------
# 4. Format check provenance (harness-observed)
# ---------------------------------------------------------------------------
echo "--- 4. Format check provenance ---"
FMT_TS=$((NOW + 3))
if (cd "$ROOT" && cargo fmt --all -- --check >/dev/null 2>&1); then
echo " fmt: PASS"
emit verification "fmt: cargo fmt --all -- --check exit=0" "harness-observed" "elench-ci" "$FMT_TS" "Cargo.toml"
else
echo " fmt: FAIL"
emit falsification "fmt: cargo fmt --all -- --check FAILED" "harness-observed" "elench-ci" "$FMT_TS" "Cargo.toml"
fi
# ---------------------------------------------------------------------------
# 5. Agent-asserted claim: INV-01 is enforced by store_blob
# ---------------------------------------------------------------------------
echo "--- 5. Agent-asserted claim ---"
AGENT_TS=$((NOW + 4))
emit assertion "INV-01: store_blob is idempotent (append-only)" "agent-asserted" "elench-dogfooding-agent" "$AGENT_TS" "crates/elench-store/src/lib.rs" '"store_blob"'
echo
echo "=== Claims emitted: 5 (4 harness-observed + 1 agent-asserted) ==="
echo " store: $STORE"
echo " tree: $TREE"
echo
# ---------------------------------------------------------------------------
# 6. Gate — real, exits non-zero on falsified premise
# ---------------------------------------------------------------------------
# elench gate takes a claims file. We export all claims from the store
# by collecting the individual claim files we just emitted.
echo "--- 6. Gate ---"
ALL_CLAIMS="$STORE/all-claims.json"
echo '[' > "$ALL_CLAIMS"
FIRST=true
for f in "$CLAIMS_DIR"/claim-*.json; do
[ -f "$f" ] || continue
if [ "$FIRST" = true ]; then
FIRST=false
else
echo ',' >> "$ALL_CLAIMS"
fi
cat "$f" >> "$ALL_CLAIMS"
done
echo ']' >> "$ALL_CLAIMS"
GATE_OUTPUT=$("$ELENCH" --store fjall "$STORE" gate "$TREE" "$ALL_CLAIMS" 2>&1)
GATE_EXIT=$?
echo "$GATE_OUTPUT"
echo
# ---------------------------------------------------------------------------
# 7. Reconcile — real, against the actual source tree
# ---------------------------------------------------------------------------
echo "--- 7. Reconcile ---"
"$ELENCH" --store fjall "$STORE" reconcile "$TREE" "$ALL_CLAIMS" 2>&1 || true
echo
# ---------------------------------------------------------------------------
# 8. Log statistics
# ---------------------------------------------------------------------------
echo "--- 8. Log statistics ---"
"$ELENCH" --store fjall "$STORE" log "$ALL_CLAIMS" 2>&1 || true
echo
# ---------------------------------------------------------------------------
# 9. Conflicts
# ---------------------------------------------------------------------------
echo "--- 9. Conflicts ---"
"$ELENCH" --store fjall "$STORE" conflicts "$TREE" "$ALL_CLAIMS" 2>&1 || true
echo
# ---------------------------------------------------------------------------
# Final: check gate verdict
# ---------------------------------------------------------------------------
if echo "$GATE_OUTPUT" | grep -q "result: Pass"; then
echo "=== continuous dogfooding: PASS ==="
exit 0
elif echo "$GATE_OUTPUT" | grep -q "result: Fail"; then
echo "=== continuous dogfooding: FAIL (gate rejected) ==="
exit 1
else
echo "=== continuous dogfooding: UNKNOWN gate verdict ==="
exit 1
fi