Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

elench

An evidence layer for repositories — reimagining git for agentic flow.

License: MIT Rust: stable CI

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

MIT

Getting Started

Prerequisites

  • Rust 1.85+ (edition 2024). rust-toolchain.toml pins stable with rustfmt and clippy.
  • make (for the Makefile targets)
  • git (for elench git init materialization)
  • 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.

TierCommandWhatWhen
1 (fast)make testcargo test --libBetween every edit; pre-commit
2 (slow)make test-slowTier 1 + cargo test --all-targetsPre-PR
3 (full)make test-fullTier 2 + dogfooding e2ePre-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/
  1. 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).

  2. 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.

  3. 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, not passed (R5).

  4. 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).

  5. 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, and git checkout work — humans use git without knowing elench exists.

  6. Retroactive invalidation. A finding late in a session can falsify a claim that a shipped artifact depended on. The blast radius is the transitive dependsOn closure — 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:

  1. 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.

  2. 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).

  3. 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 carries origin.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 emit from 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:

CrateRole
elenchBinary. CLI + git projection. Synthesizes git objects from the claim log (ADR-0002, ADR-0007). Materializes real .git/ directories.
elench-claimClaim data model, log-folding status computation, emission-rule validation, conflict detection.
elench-predicateParser and evaluator for elench-predicate-v1 DSL (ADR-0004). Four primitives: grep, test, run, exists.
elench-envelopeDSSE envelopes carrying in-toto statements. Ed25519 signing/verification (A1).
elench-storeContent-addressed store: blobs, trees, claims. The substrate (ADR-0001). In-memory (default), fjall (optional, ADR-0008).
elench-gateRelease gate evaluation — a predicate over claims, not a build. Artifact format (INV-15).
elench-projectionDeterministic git synthesis + .git/ materialization from the claim log (ADR-0002, ADR-0007).
elench-anchorMulti-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

  1. Agents produce code faster than review capacity absorbs it.
  2. VCS records tree state and authorship. The author field no longer identifies a responsible party — it names whichever key the agent held.
  3. Verification depth is not recorded anywhere. A passing test suite and an absent test suite are indistinguishable in the repository.
  4. Failures carry information that is discarded entirely. Nineteen rejected approaches vanish; the twentieth is merged with no record of what constrained it.
  5. 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) and 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).

  • 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 before elench accept issues 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 by elench 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;
  • unevaluated residue 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. Returns Correct (all agree), Degraded (disagreement), Failed (all fail), or WrongResolution.
  • 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:

  1. No falsified premise. No claim in the transitive dependsOn closure rooted at T’s claim set has status falsified.
  2. Bounded residue. Claims with status unevaluated are within P’s allowance, and each excess is covered by a residue-acceptance record signed by a key P names.
  3. Origin floor. Claims that P designates load-bearing have origin.kind = harness-observed. Agent-asserted claims may inform, but P should not let them alone carry a release.
  4. Builder agreement. K independent producers have signed statements with subject D for tree T, each meeting P’s hermeticity floor.

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 P reaching 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)

OperationDurability
elench emitClaim stored in memory; lost on process exit
elench gateLive evaluation; no persistence needed
elench git initWrites real git objects to disk (zlib-compressed)

Fjall backend

OperationDurability
elench --store fjall <path> emitClaim persisted to disk (SyncAll)
elench --store fjall <path> store blobBlob persisted to disk (Buffer)
elench --store fjall <path> store treeTree 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

CratePathBounded contextRole
elenchcrates/elenchCLI, Git ProjectionBinary. Reads/writes store, verifies envelopes, evaluates predicates, computes closures, synthesizes git projection.
elench-claimcrates/elench-claimClaim Emission, Claim EvaluationData model matching schema/claim.schema.json, log-folding status computation, emission-rule validation.
elench-predicatecrates/elench-predicatePredicate EvaluationParser and evaluator for elench-predicate-v1 DSL (ADR-0004). Four primitives: grep, test, run, exists.
elench-envelopecrates/elench-envelopeEnvelope VerificationDSSE envelope signing/verification, in-toto statement handling, signer/producer distinction.
elench-storecrates/elench-storeelench StoreContent-addressed store: blobs, trees, claims. The substrate (ADR-0001). In-memory (default), fjall (optional, ADR-0008).
elench-gatecrates/elench-gateRelease GatingRelease policy evaluation: four conditions from docs/release-policy.md.
elench-projectioncrates/elench-projectionGit ProjectionDeterministic synthesis of git-compatible objects from the claim log (ADR-0002, ADR-0007).

Dependencies

FromToWhy
elenchelench-claimClaim data model
elenchelench-envelopeEnvelope signing/verification
elenchelench-storeContent-addressed storage
elenchelench-gateRelease gate evaluation
elenchelench-predicatePredicate validation
elenchelench-projectionGit projection
elench-envelopeelench-claimClaim type (sign/verify)
elench-storeelench-claimClaim type (store/read)
elench-gateelench-claimStatus computation (log fold)
elench-projectionelench-claimClaim types
elench-projectionelench-storeStore (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

CrateWhy deferred
elench-anchorE1 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 store
  • elench verify — verify an envelope and validate the claim
  • elench status — compute a claim’s status by folding the log
  • elench gate — evaluate the release gate for a tree
  • elench blast — compute the blast radius from a claim
  • elench 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)

INVEnforcement pointStatus
INV-01: Append, not modifyelench-store::store_blob/tree/claim — idempotent, no update (MemoryStore + FjallStore)ENFORCED
INV-02: Prior status visibleelench-claim::compute_status — fold reads all recordsENFORCED
INV-03: Claim identity stableelench-claim::ClaimId — content address, immutableENFORCED
INV-04: Status computed, not storedelench-claim::compute_status — pure functionENFORCED
INV-28: Claim OID is content hashelench-claim::ClaimId::from_content — SHA-256 of canonical JSONENFORCED
INV-29: dependsOn acyclicelench-claim::validate_claim — DFS cycle detection over logENFORCED

Origin typing (R2, AGENTS.md)

INVEnforcement pointStatus
INV-05: origin.kind requiredelench-claim — type system, OriginKind non-optionalENFORCED
INV-06: No harness-observed from agentselench-claim::validate_claim — cross-checks signer.entity against origin.kindENFORCED
INV-07: Only harness emits verificationelench-claim::validate_claim — cross-checks signer.entity against kindENFORCED
INV-08: Predicate requires expressionelench-claim::validate_claim — calls elench-predicate::parseENFORCED
INV-09: Annotations never read by policyelench-gate::evaluate — filters on form=predicate, skips annotationsENFORCED
INV-11: Failure recorded only when status changedelench-claim::validate_claim — checks target status in logENFORCED
INV-12: No residue-acceptance from agentselench-claim::validate_claim — cross-checks signer.entity against kindENFORCED

Gate and release (R3, R4)

INVEnforcement pointStatus
INV-13: Gate without buildelench-gate::evaluate — takes &[Claim], no build callsENFORCED
INV-14: Artifact acceptability is live evaluationelench-gate::evaluate — called on demand, no cached verdictENFORCED
INV-15: Artifact carries (tree, policy), not verdictelench-gate::Artifact — version, tree, policy, digest, released_at; schema/artifact.schema.json; no verdict fieldENFORCED (MOCK)

Unevaluated (R5)

INVEnforcement pointStatus
INV-16: unevaluated first-classelench-claim::ClaimStatus::UnevaluatedENFORCED
INV-17: Bounded residue with acceptanceelench-gate::evaluate — condition 2, residue-acceptance recordsENFORCED

Substrate and projection (R6, ADR-0001, ADR-0002, ADR-0007)

INVEnforcement pointStatus
INV-18: elench owns content-addressed storeelench-store — no git dependency, owns storage; MemoryStore (default) + FjallStore (optional, ADR-0008)ENFORCED
INV-19: Git projection is read-onlyelench-projection::synthesize — takes &dyn StoreBackend, no writes; elench-projection::materialize — writes to filesystem, not to storeENFORCED
INV-20: Git synthesis deterministicelench-projection — proptest_inv_20_synthesis_deterministic + proptest_inv_20_synthesis_order_independentENFORCED
INV-21: Git projection no side effectselench-projection — scenario_inv19_projection_does_not_write_to_storeENFORCED
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 truthelench-store — all views derive from store; `–store memoryfjall ` selects backend at runtime
INV-27: Git projection is lossy, not authoritativeelench-projection — scenario_inv27_projection_is_lossyENFORCED

Supply-chain composability (R7, ADR-0003)

INVEnforcement pointStatus
INV-22: DSSE/in-toto shared formatelench-envelope::sign / verify; PREDICATE_TYPE_AGENT; Ed25519 signatures (A1)ENFORCED

Predicate language (ADR-0004)

INVEnforcement pointStatus
INV-23: Expressions executable/deterministic/sandboxableelench-predicate — 4 primitives (grep, test, run, exists), not Turing-completeENFORCED

Validator (ADR-0006)

INVEnforcement pointStatus
INV-24: AGENTS.md rules enforcedelench-claim::validate_claim — implemented, all rules enforcedENFORCED

Conflict detection

FunctionEnforcement pointStatus
elench_claim::detect_conflictsSame-anchor, different expression — crates/elench-claim/src/lib.rs; 8 unit tests + 4 CLI testsENFORCED

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

CategoryMeaningCaller action
PermanentCannot succeed; data loss, corruption, or configuration errorReport to user/admin; do not retry
RetriableTransient failure (I/O, network); may succeed on retryRetry with backoff
SecurityAuthentication or authorization failureDeny and audit
ValidationClaim or envelope rejected by emission rulesAgent 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

  1. Fail closed. If the gate cannot evaluate, the verdict is fail, not pass. An unevaluated claim is NOT a passing claim.

  2. No silent corruption. A corrupt store yields StoreError::CorruptStore and marks all unreadable claims as unevaluated. It does not guess.

  3. Append-only is a store invariant, not a recovery mechanism. StoreError::ContentAddressingViolation prevents overwriting; it does not provide conflict resolution.

  4. Agent emission errors are rejection, not retry. The validator rejects; the agent reformulates and re-emits. There is no partial acceptance.

  5. Builder agreement unavailability is explicit. The gate reports it as a named condition failure, not a silent degradation to single signature.

  6. 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.

  7. 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:
    1. No falsified premise (uses blast radius from Phase 1)
    2. Bounded residue with acceptance (INV-17)
    3. Origin floor (uses origin from Phase 1)
    4. 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 log shows commits derived from tree-changing claims
  • git blame maps 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 claim
  • elench verify — verify envelope and validate claim
  • elench status — compute a claim’s status
  • elench gate — evaluate the release gate for a tree
  • elench blast — compute the blast radius from a claim
  • elench git — materialize the git projection
  • elench store — store a blob or tree

Depends on: All prior phases.

Deferred phases

PhaseCrateGated byStatus
Anchor resolutionelench-anchorE1 (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:

ShapeCount%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:

  1. 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.”

  2. 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.

  3. 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".

  4. exists(path) → bool — a file exists. Covers ~1% of predicates. A special case of grep(.+, path) >= 1 or run("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 grep and string matching (e.g., IBM Storage Scale|WEKA|DAOS|BeeGFS, \d+.*tokens?/s, error\[E0308\]).
  • File I/O (read-only) — grep and exists read files; neither writes.
  • Process execution — test runs cargo test <name>; run runs 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 E0DSL expression
grep -cE "IBM Storage Scale|WEKA|DAOS|BeeGFS" docs/performance/competitive-targets.md >= 4grep(/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 == 255run("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 0run("cargo clippy -- -D warnings").exit == 0
scripts/perf-gate.sh existsexists("scripts/perf-gate.sh")
rg("fn set_model", "src/").len() >= 1grep(/fn set_model/, "src/") >= 1
rg("auto_downgrade|editor_model_map", "src/").len() == 0grep(/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> where EvalContext carries the workspace root, sandbox configuration, and allowed-command list.
  • Validator integration: elench-claim::validate_claim calls elench-predicate::parse to 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 > &&

||. The run primitive is the most dangerous: the validator must sandbox process execution (whitelist allowed commands, restrict working directory, capture stdout/stderr). The grep and exists primitives are read-only and need only filesystem path restrictions (workspace root). The test primitive runs cargo 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").passed has the same shallowness risk as the “existing test frameworks” candidate: the test might assert almost nothing. The DSL makes this visible — the predicate expression is test("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 run commands (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 restrict run to deterministic, local commands (cargo, git, file utilities) and flag network-dependent predicates as unevaluated (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 in elench-predicate-v2, with a new ADR. Existing v1 claims are evaluated by the v1 evaluator 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:

  1. 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.
  2. 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).
  3. Sandboxing. Rust’s unsafe discipline and absence of a runtime make the audit surface small — important for a tool that must be trusted as evidence infrastructure.
  4. 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 git plumbing. 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:

  1. 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.
  2. Commit OID. Computed from (tree OID, parent commit OIDs, author, committer, message, timestamps) — all derived from the claim log, not the machine.
  3. Author/committer. Derived from the claim’s producer.id. The signer (DSSE envelope) is not the author; the producer is. No user-configurable user.name / user.email.
  4. Timestamps. Derived from the claim’s timestamp, not the wall clock. Two parties synthesizing the same claim at different times get the same commit.
  5. 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.
  6. 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 blame maps 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 blame maps 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):

KeyspaceKeyValueDurability
blobsSHA-256 OID (64 hex)blob dataBuffer (content-addressed, can be recomputed)
treesSHA-256 OID (64 hex)serialized tree entriesBuffer
claimscl_ + SHA-256 OID (67 chars)serialized claim JSONSyncAll (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: current HashMap implementation (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

Criterionfjallredbsledrocksdbcustom
Pure RustYesYesYesNo (C++)Yes
Build depsNoneNoneNonecmake, clangNone
Binary size~100KB~50KB~200KB~5MB0
LSM-treeYesNo (B-tree)YesYesManual
Append-onlyNaturalNoYesYesManual
Crash recoveryAutomaticAutomaticYesAutomaticManual
CompactionYesNoneYesYesNone
CompressionLZ4NoYesYesNo
Cross-keyspace atomicYesNoNoNoManual
Key-value separationYesNoNoNoManual
Stable disk formatYesYesNoYesN/A
MaintainedYes (2.3k stars)YesNo (since 2022)YesN/A
Proven in productionkiseki 3.1kiseki (rev-1)NoYesNo

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

ContextResponsibilityKey entity
Claim EmissionCreate, sign, and store claims in the storeClaim
Claim EvaluationCompute status by folding the logClaimStatus
Anchor ResolutionResolve anchors to code spans within a treeAnchor
Release GatingEvaluate release policy against claimsVerdict
Predicate EvaluationExecute predicate expressions (GATED by E0)Expression
Git ProjectionSynthesize git objects from the claim logGitCommit
elench StoreContent-addressed storage: blobs, trees, claimsStore
Envelope VerificationDSSE envelope signing and verificationEnvelope

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.

FieldTypeRequiredNotes
idstring ^cl_[0-9a-f]{64}$yesContent address, never reassigned
kindenum: assertion, falsification, verification, supersession, residue-acceptanceyesfalsification/verification/supersession require target
targetarray of claim idsnoClaims this record acts upon
assertionobjectyesContains form (predicate/annotation), optional expression, optional text
originobjectyesContains kind and producer
anchorobjectyesContains tree (elench OID) and strategy
timestampinteger (Unix epoch)yesSet by producer at emission. Used by ADR-0007 for deterministic commit synthesis.
evidencearraynoEmpty for agent-asserted claims by default
dependsOnarray of claim idsnoPremises. 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

FieldTypeRequiredNotes
formenum: predicate, annotationyespredicate can gate; annotation cannot
expressionobject: { language, source, digest? }required when form=predicateexecutable, deterministic, sandboxable
textstring, max 2000 charsnoHuman-readable. Never load-bearing.

Origin

FieldTypeRequiredNotes
kindenum: harness-observed, agent-asserted, human-assertedyesR2. Agents cannot emit harness-observed.
producerobject: { id, sessionId?, hermeticity? }yesDistinct from signer (envelope).

Anchor

FieldTypeRequiredNotes
treestring (elench tree OID)yesContent address of the tree state in the store. NOT a git commit OID.
strategyenum: path-range, symbol, content-digest, multiyesUNRESOLVED — E1 decides.
pathstringnoFor path-range strategy.
range[int, int]noFor path-range strategy.
symbolstringnoFor symbol strategy.
contentDigeststringnoFor content-digest strategy.

Evidence

FieldTypeRequiredNotes
kindenum: process-exit, test-report, artifact-digest, external-attestationyes
digeststringno
exitCodeintegernoFor process-exit.
uristringno

ClaimStatus (computed, not stored)

ValueMeaning
unevaluatedNo verification or falsification record targets this claim. Default.
passedA verification record exists and no falsification has invalidated it.
falsifiedA 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.

FieldTypeNotes
resultenum: pass, fail
reasonsarray of stringsWhich conditions failed and why.
treestringThe elench tree OID evaluated.
policystringThe 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.

FieldTypeNotes
oidstringDeterministic function of (tree, parents, author, committer, message, timestamps).
treestringelench tree OID, mapped to a git tree OID.
parentsarray of git commit OIDsDerived from the claim log.
authorstringDerived from the claim’s producer.id.
committerstringSame as author (no separate committer).
messagestringDerived from an annotation claim, if present.

Store entities

Blob

FieldTypeRequiredNotes
oidstring [0-9a-f]{64}yesSHA-256 content hash. Identical to git SHA-256 blob OID.
databytesyesContent.

TreeEntry

FieldTypeRequiredNotes
namestringyesEntry name within the parent tree (e.g., “lib.rs”, “src”). NOT a full path — git-compatible.
modeintegeryesFile mode (0o100644 regular file, 0o100755 executable, 0o120000 symlink, 0o040000 directory).
oidstring [0-9a-f]{64}yesSHA-256 content hash. For files: blob OID. For directories: tree OID.
kindenum: blob, treeyesWhether this entry is a blob (file) or a tree (directory).

Tree

FieldTypeRequiredNotes
oidstring [0-9a-f]{64}yesSHA-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.
entriesarray of TreeEntryyesSorted 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

ContextOwnsConsumes
Claim EmissionClaim creation, signing, storageEnvelope Verification (before accepting)
Claim EvaluationStatus computation (log folding)elench Store (reads log)
Anchor ResolutionAnchor → code span resolutionClaim Evaluation (for blast radius)
Release GatingVerdict computationClaim Evaluation (uses status), Predicate Evaluation
Predicate EvaluationExpression execution— (gated by E0/ADR-0004)
Git ProjectionGit object synthesis from claim logelench Store (reads), Claim Log (reads)
elench StoreContent-addressed storage: blobs, trees, claims— (leaf in workspace)
Envelope VerificationDSSE envelope signing/verificationClaim 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:

  1. No falsified premise in transitive dependsOn closure
  2. Bounded residue (unevaluated within P’s allowance, excess covered by residue-acceptance)
  3. Origin floor (load-bearing claims are harness-observed)
  4. 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

  1. 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).

  2. 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).

  3. 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).

  4. 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

INVDescriptionDepthNotes
INV-01Status changed by appending, not modifyingMOCKelench-store: store_blob/tree/claim idempotent (memory + fjall)
INV-02Prior status remains visibleMOCKelench-claim: compute_status reads entire log
INV-03Claim identity stable across status changesMOCKelench-claim: ClaimId immutable
INV-04Status computed by folding, not storedMOCKelench-claim: compute_status pure fn
INV-05origin.kind required and structurally distinctMOCKelench-claim: type system enforces
INV-06Agents cannot emit harness-observedMOCKelench-claim: validate_claim cross-checks signer
INV-07Only harness emits verificationMOCKelench-claim: validate_claim cross-checks signer
INV-08Predicate requires executable expressionMOCKelench-claim: validate_claim calls elench-predicate::parse
INV-09Annotations never read by policyMOCKelench-gate: evaluate filters on form=predicate
INV-10dependsOn populated with premisesREMOVEDDowngraded to guideline; empty dependsOn is a warning, not a rejection
INV-11Failure recorded only when status changedMOCKelench-claim: validate_claim checks target status in log
INV-12Agents cannot emit residue-acceptanceMOCKelench-claim: validate_claim cross-checks signer
INV-13Gate evaluable without build capabilityMOCKelench-gate: evaluate takes &[Claim], no build
INV-14Artifact acceptability is live evaluationMOCKelench-gate: evaluate called on demand, no cache
INV-15Artifact carries (tree, policy), not verdictMOCKelench-gate: Artifact struct with version field; schema/artifact.schema.json; 6 tests
INV-16unevaluated is first-class statusMOCKelench-claim: ClaimStatus::Unevaluated
INV-17Policies permit bounded unevaluated residueMOCKelench-gate: condition 2, residue-acceptance
INV-18elench owns content-addressed storeMOCKelench-store: no git dependency, owns storage; both backends pure-Rust
INV-19Git projection is read-onlyMOCKelench-projection: synthesize takes &dyn StoreBackend, no writes
INV-20Git synthesis is deterministic (BC4)PROPERTYelench-projection: proptest_inv_20_synthesis_deterministic + order_independent
INV-21Git projection produces no side effectsMOCKelench-projection: scenario_inv19_projection_does_not_write_to_store
INV-22Agent claims and provenance share DSSE/in-totoMOCKelench-envelope: sign/verify, PREDICATE_TYPE_AGENT, Ed25519 (A1)
INV-23Predicate expressions executable/deterministic/sandboxableMOCKelench-predicate: 4 primitives, not Turing-complete
INV-24AGENTS.md rules enforced by validatorMOCKelench-claim: validate_claim (Phase 0)
INV-25Content addressing (SHA-256)PROPERTYelench-claim: ClaimId::from_content; elench-store: Oid::from_blob_data/from_tree_entries + deserialize_tree_bytes round-trip + FjallStore::read_tree (feature tier)
INV-26Store is sole source of truthMOCKelench-store: all views derive from store; selectable at runtime via `–store memory
INV-27Git projection is lossy, not authoritativeMOCKelench-projection: scenario_inv27_projection_is_lossy
INV-28Claim OID is content hashPROPERTYelench-claim: ClaimId::from_content (SHA-256 of canonical JSON); proptest_inv_28
INV-29dependsOn acyclicPROPERTYelench-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

FeatureScenariosDepthNotes
claim-emission7MOCKelench-claim: validate_claim + types. 1 scenario untested (empty dependsOn warning — dead code)
claim-revocation7MOCKelench-claim: compute_status + blast_radius + dependsOn propagation. All 7 covered.
origin-typing6MOCKelench-claim: validate_claim cross-checks. 2 scenarios untested (query-by-origin.kind not implemented)
release-gate9MOCKelench-gate: evaluate, 4 conditions. 1 scenario untested (contradictory predicates — FM-P2-02 known limitation)
anchor-resolution11MOCKelench-anchor: resolve_path_range/symbol/content_digest, reconcile CLI. 1 scenario untested (wrong-resolution — dead code)
unevaluated-residue6MOCKelench-claim: ClaimStatus::Unevaluated. 1 scenario untested (corrupt cascade — no corrupt status)
git-projection4MOCKelench-projection: synthesize, git_log_oneline/full, materialize, git blame, write-through rejected. All 4 covered.
store-backend5MOCKelench-store: –store flag, FjallStore::read_tree round-trip. All 5 covered.
build-provenance4SHALLOWelench: –artifact flag, SHA-256 of build output. CLI output checks, not in-process claim verification.
proptest-property5PROPERTYproptest: INV-25/20/13/29/28 (256 cases each). All 5 covered.
dogfooding7NONEShell 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)

FeatureScenarioReason
anchor-resolutionWrong-resolution is reported distinctly from failureStrategyOutcome::Wrong is dead code (#[allow(dead_code)])
claim-emissionA claim with empty dependsOn is accepted with a warningValidationError::EmptyDependsOn is defined but never returned
dogfooding (×6)Dogfooding claims emitted/stored, gate, log stats, git projection, continuous emission, CI nightlyShell scripts with || true, no assertions
origin-typing (×2)Harness-observed and agent-asserted claims are distinct; human-asserted distinct from agentNo query-by-origin.kind function exists
release-gateTwo contradictory predicates: gate passes (known limitation)FM-P2-02 not tested
unevaluated-residueA corrupt claim cascades to unevaluated dependentsNo “corrupt” status distinction; compute_status returns Err(ClaimNotFound)

Experiments

ExperimentGatesStatusResult
E0 — Predicate ratioBC1PASSED0.72 (threshold >= 0.30). PROCEED AS DESIGNED.
E1 — Anchor survivalBC2PASSEDAll strategies USABLE (correct >= 85%, wrong <= 2%). Proceed with multi.
E2 — Build reproducibilityBC3PASSEDSame-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

  1. No timestamp field in claim schema — ADR-0007 requires timestamps for deterministic git commit synthesis, but schema/claim.schema.json has 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.

  2. 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’s origin.kind is self-reported; without the DSSE envelope’s signer, the validator cannot distinguish an agent forging harness-observed from a genuine harness claim. R2 is unenforceable as designed.

  3. 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

  1. Supersession status semantics self-contradictory — UL says “not falsified but replaced” and also “status becomes falsified.” Contradictory.
  2. No invariant for claim ID content addressing — INV-25 covers blobs and trees but not claims. What goes into the hash is unspecified.
  3. dependsOn cycles unaddressed — blast_radius and compute_status can loop infinitely. No cycle detection, no invariant, no error type.
  4. INV-11 cannot be enforced by validate_claim(&Claim) — Needs the full log to check whether a falsification “changed some claim’s status.”
  5. Schema does not enforce conditional requirements — target is “required unless kind=assertion” but no JSON Schema if/then. residue-acceptance needs non-empty target but no minItems.
  6. 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

  1. Two contradictory predicates invisible to the gate (worse than “undefined status”)
  2. origin.producer.id is a free string — impersonation possible
  3. Corrupt log cascading — claims depending on corrupt claims have undefined status
  4. origin.producer.hermeticity is self-reported — release gate condition 4 checks self-attested value
  5. E0 session selection criteria not pre-registered — gate is gameable
  6. predicateType for agent claims vs build provenance not specified
  7. Empty store / zero claims / minimal case behavior undefined
  8. No “residue-acceptance from human” or “harness emits verification” feature scenarios
  9. Schema $id is example.invalid placeholder
  10. additionalProperties: false inconsistency (anchor, evidence, producer)

Low

  1. AGENTS.md says “no source code” but scaffold stubs exist
  2. “tree-changing claim” used but not in UL
  3. TreeEntry.blob field name misleading for directory entries
  4. No maxItems on dependsOn, target, evidence arrays
  5. compute_status and blast_radius are 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

  1. Take 20–30 completed agent sessions on a real repository. Brownfield, not greenfield: the unevaluated fraction is the point.
  2. 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.
  3. Classify each: predicate (an executable expression can be written now, by the person doing the classification, in under five minutes) or annotation.
  4. 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.

RatioReading
≥ 0.30Proceed as designed.
0.15 – 0.30Proceed with reduced scope: gating over a small predicate core, annotations demoted to a search index only. Re-derive requirements before continuing.
< 0.15Stop. 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.

  • dependsOn density. 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

RepositorySourceSessionsCommitsLanguage
kisekilocal (user)5~400 sampledRust, Go, Python
yoyo-evolveexternal (yologdev)5~4250Rust
screelocal (user)3—Python, TypeScript
ghylllocal (user)3—Go
pactlocal (user)3—Rust
latticelocal (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

SessionRepoClaimsPredicatesAnnotationsRatio
v0.1.8yoyo-evolve201820.90
v0.1.11yoyo-evolve252140.84
v0.1.15yoyo-evolve272340.85
v0.1.16yoyo-evolve322750.84
v0.1.17yoyo-evolve332850.85
v2026.43.930..931kiseki1101.00
v2026.43.916..930kiseki7646300.61
v2026.43.913..916kiseki6420.67
v2026.43.759..913kiseki6744230.66
v2026.40.534..759kiseki~50~30~20~0.60

Aggregate

MetricValue
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

RatioReading
≥ 0.30Proceed as designed.
0.15 – 0.30Proceed with reduced scope.
< 0.15Stop.

Result: 0.72 — well above 0.30. PROCEED AS DESIGNED.

Secondary measurements

dependsOn density

RepoMean 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

RepoFalsification rateNotes
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

RepoFraction of predicates derivable by harnessNotes
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 typeTypical ratioExample
Feature release (many features)0.84-0.90yoyo-evolve v0.1.8, v0.1.11
Bug-fix release (many fixes)0.84-0.85yoyo-evolve v0.1.16, v0.1.17
Performance work (RCA + fix)0.60-0.67kiseki v2026.43.916..930
Infrastructure/CI0.60-0.70kiseki v2026.43.759..913
Single-commit release1.00kiseki 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:

  1. 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.
  2. PR boundary — all commits in a single pull request (merged). The PR description (if any) and commit messages are the session.
  3. 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.

  1. From each repository, take the 5 most recent releases (or equivalent session boundaries) that contain tree-changing commits.
  2. If fewer than 5 releases exist, take PR-boundary sessions or task-cluster sessions to reach 5.
  3. Target: 20-30 sessions total across 4-6 repositories.
  4. 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

RepositorySourceSessionsLanguageNotes
kisekilocal (/home/witlox/src/kiseki)5Rust, Go, PythonUser’s most advanced; release-boundary sessions
yoyo-evolveexternal (github.com/yologdev/yoyo-evolve)5RustAll agent-written; release-boundary sessions
screelocal (/home/witlox/src/scree)3Python, TypeScriptRelease-boundary sessions
ghylllocal (/home/witlox/src/ghyll)3GoPR-boundary or task-cluster sessions
pactlocal (/home/witlox/src/pact)3RustRelease-boundary sessions
latticelocal (/home/witlox/src/lattice)3Python, RustRelease-boundary or task-cluster sessions

Total: 22 sessions (within the 20-30 target).

Extraction method

For each session:

  1. Read all commit messages in the session range.
  2. Read the release notes (if a release-boundary session).
  3. 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.
  4. 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

  1. 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.
  2. At tree T0, place 100+ synthetic anchors across representative code: function bodies, interface definitions, config constants, test assertions.
  3. Replay history forward N tree states. For each anchor and each strategy, record: resolved correctly / resolved to wrong code / failed to resolve.
  4. 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:

RepositorySourceCommitsLanguage
kisekilocal (user)937Rust, Go, Python
yoyo-evolveexternal (yologdev)5286Rust
tokioexternal (tokio-rs)815Rust
cobraexternal (spf13)205Go
httpxexternal (encode)200Python

READ-ONLY: No commits to any repo. Only git history was read.

Results

Aggregate per strategy

StrategyCorrectWrongFailedTotalCorrect%Wrong%
path-range1989101200099.5%0.5%
symbol1988120200099.4%0.6%
content-digest1989011200099.5%0.0%
multi1988120200099.4%0.6%

Breakdown by refactor class

StrategyClassCorrectWrongFailedTotalCorrect%Wrong%
path-rangereformat200020100.0%0.0%
path-rangesemantic1949101196099.4%0.5%
path-rangeother200020100.0%0.0%
symbolreformat200020100.0%0.0%
symbolsemantic1948120196099.4%0.6%
symbolother200020100.0%0.0%
content-digestreformat200020100.0%0.0%
content-digestsemantic1949011196099.4%0.0%
content-digestother200020100.0%0.0%
multireformat200020100.0%0.0%
multisemantic1948120196099.4%0.6%
multiother200020100.0%0.0%

Pre-registered thresholds

StrategyVerdict
path-rangeUSABLE (correct >= 85%, wrong <= 2%)
symbolUSABLE (correct >= 85%, wrong <= 2%)
content-digestUSABLE (correct >= 85%, wrong <= 2%)
multiUSABLE (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:

  1. The safety of content-digest (zero wrong-resolution on semantic edits)
  2. The resilience of symbol (survives reformatting)
  3. The simplicity of path-range (trivial to compute)
  4. 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

  1. Take the current build as-is. Build the same commit on three machines differing in OS version, CPU, filesystem ordering, and locale.
  2. Compare output digests. For each divergence, identify the cause: embedded timestamp, path leakage, non-deterministic ordering, toolchain version drift, network-fetched dependency.
  3. Classify each cause: cheap to fix, expensive to fix, or structural.
  4. 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.md needs 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:

BuildImageLocaleTimezoneLibc
ubuntu-enubuntu:latesten_US.UTF-8UTCglibc 2.43
debian-jpdebian:latestja_JP.UTF-8Asia/Tokyoglibc 2.41
alpine-enalpine:latesten_US.UTF-8UTCmusl 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

BuildDigest
ubuntu-en8120462c686dfafbd7297eac3db42d791b90fcfe78a5ba00077796703a7601cf
debian-jpaac84fdac3ef217be3c026598d0f4d7bed7ff0258c5d6a1c99bb8b8bbbf4e9b0
alpine-en500920e1a3cbb6991ef42d048d502b1f0f9107a9dc00458248df236d17794b8b

All three binaries diverge.

Divergence classification

PairSame triple?CauseClass
ubuntu-en vs debian-jpYes (both x86_64-unknown-linux-gnu, glibc)build-id (random by default), path leakage, glibc version (2.43 vs 2.41), different gccCHEAP TO FIX
ubuntu-en vs alpine-enNo (glibc vs musl)Different C library, different linker, different target tripleSTRUCTURAL (expected)
debian-jp vs alpine-enNo (glibc vs musl)Same as above, plus locale/tzSTRUCTURAL (expected)

Cheap-to-fix causes (same-triple)

  1. Build-ID. Rust’s default build-ID includes a random component. Fix: RUSTFLAGS='-C build-id=none' or set to a deterministic value.

  2. 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).

  3. 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.04 or use a Nix-style hermetic derivation).

  4. 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)

ConditionResult
Same-triple divergences all cheap-to-fixPASS (build-id, path leakage, glibc/gcc version)
Any same-triple structural divergenceNone found
Cross-triple divergenceExpected (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:

  1. K independent producers build the same commit for the same target triple, using a pinned base image and the three fixes above.
  2. Each producer signs a statement with subject D (the artifact digest) for tree T.
  3. 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.path pointing at the file that enforces the invariant
  • anchor.symbol naming the function or module
  • assertion.form = predicate with an executable expression
  • depends_on listing 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