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