Skip to content

Build an Echo-backed Edict behavioral test runner with TAP 14 reporting #208

Description

@flyingrobots

Edict-authored behavioral tests, executed by Echo, reported as TAP 14

Goal and status

PROPOSED specification and implementation plan. No behavioral runner is implemented by this issue.

An application author should be able to write a bounded test intent in Edict, build it through the public compiler and independent provider verifier, execute that exact program through Echo, and receive a TAP result backed by the execution evidence. Jim is the first substantial consumer; the framework must also work for an application with no editor or Rope concepts.

Edict owns test authoring conventions, result interpretation, orchestration, and reporting. Echo owns generic execution and its evidence. Jim owns its application semantics and independent expected behavior, implemented in Jedit. Echo must not acquire test, assert, TAP, Rope, or editor-specific execution primitives.

This is one umbrella issue. Existing compiler, provider, runtime, and Jim issues remain the owners of their prerequisites. This issue does not reopen PR #201 or expand PR #207. The speculative helper call-depth concern in #203 remains a separate reproduction task.

Verified starting point

These are inspected revision-specific facts, not claims that open branches have landed:

Boundary Observed behavior Evidence
Edict public CLI JSONL compiler interface with build, check, and project; no behavioral-test operation. [claim:compiler-surface, confidence:0.99] crates/edict-cli/src/main.rs#63@3f81f759e921a69b04fe8cf8e62e62f8f3dc7b7e; CLI shelf in appendix.
Compiler result projection Describes how a result is assembled; does not execute it. Public application builds require exactly one admitted result projection. [claim:projection-boundary, confidence:0.99] docs/topics/result-projections/README.md#5@3f81f759e921a69b04fe8cf8e62e62f8f3dc7b7e and line 42.
Current compiler evidence work #192 / PR #207 adds source-mutation and pin-binding evidence; its stated oracle is compiler identity, with no helper, loop, or provider execution. PR #207 was open at inspection. [claim:compiler-evidence-scope, confidence:0.99] docs/topics/lawpack-authoring/test-plan.md#75@19ccbccf5bbe391a055a5ac04b2fd9912c9a8971; PR #207.
Jedit application proof The current ReplaceRange source proves a pure compilation/package boundary. No evaluator runs, no Rope changes, and no Tick settles. [claim:jim-current-proof, confidence:0.99] Jedit edict/replace-range/README.md#18@a894c7c4c6d150c0fb210d2e0ca4c27bf518b4c7 and line 43; draft PR #302.
Echo runtime gap The inspected runtime's program enum contains the earned anchored attachment profiles; generic compiler-produced bounded program interpretation is the separate #684 work. Provider acceptance is insufficient execution evidence. [claim:echo-execution-gap, confidence:0.99] Echo crates/warp-core/src/echo_operation.rs#575@49e9efb68001dfd78563d18bac9359a87671e431; #684, draft PR #724.

Edict main was 3f81f759e921a69b04fe8cf8e62e62f8f3dc7b7e at issue preparation. The other cited heads are explicit candidate evidence. Refresh exact pins before implementation; do not silently turn these candidates into release dependencies.

Scope and ownership

Repository / owner Required work Boundary to preserve
Edict Versioned suite and case-result contracts; strict decoder; runner library; separate edict-test binary; Echo adapter; TAP reporter; evidence report; compiler/runtime integration fixtures; optional pure assertion lawpack. The compiler remains deterministic and free of hidden runtime I/O. Preserve the existing edict JSONL contract.
Echo Finish the generic evaluator/profile earned by #684; expose the ordinary bounded install/admit/execute/outcome boundary to a host; provide independently checkable result/obstruction evidence and normal effect settlement/recovery. No test-aware execution mode, assertion intrinsic, application callback, Rope operation, or special authority bypass.
Jim, in Jedit Author application tests and fixtures; retain the independent ReplaceRange oracle; drive real Edict programs; compare typed outcomes and observable state; maintain exact producer/artifact pins and application CI. Tests and the Rust oracle may compute expectations. They must not supply the operation's production mutation plan or execute in place of Edict.
Local Jim workspace Coordinate compatible checkout/lock selections and a reproducible cross-repo invocation once demonstrated. A workspace pin records coordinates; it does not prove execution compatibility. No separate hosted Jim repository is assumed.
Wesley Regenerate existing schema/codec/identity artifacts if a consumer contract changes; add generation evidence only for changed contracts. It does not generate test outcomes, execute assertions, or become an alternate application interpreter. No unconditional Wesley feature is required.
Bijou / CI consumers Consume TAP or the machine report later; initially invoke the runner and preserve its exit status/artifacts. A UI, plugin, or new test dashboard is not a prerequisite.

Existing dependencies

  • Edict #192 / #207: compiler expressivity and evidence baseline. Additional language/lowering features require an actual failing authored specimen; this issue does not demand an unrestricted VM or all loop forms.
  • Echo #684: generic execution. Its required first RED still comes from the genuine Jedit-authored, public-compiler-produced package specified there. A convenient test fixture does not replace that provenance requirement.
  • Echo #724: candidate provider/package work; landing it alone does not satisfy the execution prerequisite.
  • Edict #171 and Echo #693: complete ordered lawpack closures through lowering and verification. Required before a suite imports separate application and assertion lawpacks that need this crossing. Start with an inline ordinary result record when possible; never flatten imports or drop pins to evade this dependency.
  • Jedit #296: real ReplaceRange source and oracle conformance; #302 is its current package-proof slice. Jedit #295 remains the larger Jim active-observer goal.

Compiler packaging can proceed before this runner. Reporter/decoder unit work can proceed before Echo execution. Neither may be presented as an end-to-end behavioral test. The runner is an evidence consumer of #684, not a new prerequisite for implementing #684.

Proposed architecture

The program supplies an assertion result; the host earns permission to report that result by checking the ordinary artifact and execution chain.

flowchart LR
    S[Suite and authored Edict cases] --> C[Public Edict build]
    C --> V[Independent provider verification]
    V --> H[Edict runner and Echo adapter]
    H --> E[Generic Echo admission and execution]
    E --> O[Bound result or typed obstruction evidence]
    O --> J[Edict verdict checks]
    J --> T[TAP 14 and machine report]
    R[Jim oracle and expected fixtures] --> J
Loading
Caption: Program execution and test reporting have different owners
  1. Suite entries select real authored programs and explicit fixture inputs.
  2. The public build and independent verifier establish the executable subject.
  3. The Edict-side adapter submits that subject through Echo's ordinary authority path.
  4. Echo returns generic execution evidence. The runner checks its binding before interpreting application data as a test result.
  5. Jim's oracle supplies expectations at the comparison boundary; it supplies no executable program or mutation plan to Echo.

The TAP report is a derived test verdict. It does not become a new source of runtime authority, and a valid receipt proves only its stated execution proposition, not universal correctness of the application or its tests.

Normative proposed v1 contract

The following requirements specify the intended implementation. The proposed command, schemas, and fixture names below do not exist yet.

R1 — Public surface and discovery

Provide an Edict-owned runner library and a separate binary:

edict-test --suite tests/edict.test-suite.json --report-json artifacts/edict-test-run.json

The existing edict executable retains JSONL on its public streams. The new runner emits only TAP on stdout and bounded structured diagnostics on stderr. It invokes the public application-build boundary; it must not introduce a second compiler or construct Core/Target by hand.

Discovery is an explicit ordered manifest, not filesystem/glob order. Case IDs are unique ASCII identifiers matching [A-Za-z0-9][A-Za-z0-9._-]{0,127}. Paths resolve against the suite file, independent of the caller's working directory. Resolve and snapshot input bytes before use; reject undeclared path escapes and symlink escapes. Compiler outputs belong in a runner-owned temporary directory. Never rewrite source, vendored lawpacks, producer locks, or expected fixtures during a run.

A proposed minimal manifest:

{
  "schema": "edict.test-suite/v1",
  "id": "example.pure-contract",
  "toolchainLock": "edict.test-toolchain-lock.json",
  "cases": [
    {
      "id": "choose-left",
      "application": "cases/choose-left/edict.application.json",
      "input": "fixtures/choose-left.input.bin",
      "expect": {
        "kind": "caseResult",
        "schema": "edict.test.case-result/v1"
      }
    }
  ]
}

The input file contains bytes in the operation's declared, pinned input codec; .bin does not imply CBOR or a universal Echo value codec. Validate its schema/codec before invocation. The application document selects one independently buildable test entry point. Do not assume today's application builder can package arbitrary test intents from one module into one application; content-identical builds may be reused, but case executions may not.

The manifest and lock schemas reject unknown fields, duplicate JSON keys, duplicate case IDs, unsupported versions, and missing references. Canonical suite identity covers the ordered manifest plus exact transitive input content; filesystem paths and timestamps are locator/telemetry data, not substitutes for content identity. Define and freeze the digest framing with canonical positive and negative vectors in slice 1.

The complete v1 manifest field set is the minimal example above plus these optional fields; fields not listed are rejected:

Location / field Contract
Suite limits Object with optional maxManifestBytes, maxCases, maxSetupOperationsPerCase, maxFixtureBytes, maxCaseResultBytes, maxFrameBytes, maxReportBytes, maxArtifactBytes, and wallTimeoutMs. Positive integers may lower the R4 ceilings; omission uses those ceilings/defaults. No environment overrides.
Case description Display-only UTF-8 label, at most 1,024 bytes; defaults to case ID. Rendering is escaped independently from identity/correlation.
Case setup Ordered list of {application, input} entries; defaults to empty. Both paths follow the same resolution/snapshot rules as the case.
Case skip {reason, trackingReference} with two nonempty UTF-8 strings of at most 1,024 bytes each. The case must remain structurally valid; no build/setup/execution is performed for it.
Case expect alternative {kind: "obstruction", stage: "execution", coordinate, payload}. Coordinate is a nonempty versioned identity, at most 1,024 UTF-8 bytes; payload is the expected fixture path. It is mutually exclusive with the caseResult shape.

Suite id uses the case-ID grammar. Required case fields remain id, application, input, and expect. No filtering or recursive suite imports in v1. The edict.test-toolchain-lock/v1 document has a closed role map for the runner, compiler, lowerer, verifier, host/runtime, target/interpreter profile, and codec/report ABIs. Each entry carries the owning typed identity plus an explicit local artifact locator; source-built entries also carry the expected Git revision. Existing application locks remain authoritative for their source/lawpack closure; the runner lock must agree with them, not replace them. All lock bytes are included in the input snapshot. Slice 1 must publish the exact JSON Schema/CDDL and digest vectors before calling the public ABI frozen.

Construct the suite's semantic identity from a canonical subject in which locator paths are replaced by verified typed content references; retain the original manifest separately for reproduction. This avoids treating a change of temporary directory as a semantic change while still binding case order, expectations, setup, limits, skip declarations, and producer identities.

R2 — Ordinary Edict case result

edict.test.case-result/v1 is an Edict-side interpretation contract for an ordinary closed output record, not an Echo runtime type. Initial cases may declare that record locally; the compiler still binds each case's actual declared output type through its result projection.

Field Required meaning
status U32, exactly 0 for passed assertions or 1 for an assertion failure. Other values reject as malformed results.
assertions U32, between 1 and 65,535 inclusive. Zero cannot produce a passing or valid assertion-result case.
message UTF-8 string, at most 1,024 bytes. Empty is allowed. Human diagnostics never determine the verdict.

These integer tags make the first contract expressible as a bounded record without requiring new surface-language enum/generic features. Unknown/missing fields, wrong types, invalid UTF-8, trailing bytes, and bound violations are InvalidCaseResult, not assertion failures. The runner uses the declared output codec/projection and validates the logical record; it must not cast unrelated same-sized bytes into this result.

The authored case performs the comparison and returns this record. The host counts one case as one TAP point; assertions is diagnostic coverage information, not a substitute for receipt verification or proof that an assertion implementation is sound. The case cannot supply its own trusted package ID, run ID, receipt ID, or execution status.

R3 — Exact execution binding

For every executed case, retain and verify the relationship among:

  1. exact source/input/fixture closure and producer lock;
  2. Core, Target, lawpack closure, and compiler-owned result projection;
  3. executable package/subject and independent verifier identity and report;
  4. admitted installation/invocation, selected basis, and declared semantic budgets;
  5. terminal runtime result or obstruction and the evidence that binds it to that invocation;
  6. decoded application value and host verdict.

Recompute identities using their owning schemas and digest domains. Do not compare a digest while ignoring its coordinate/domain or trust a report paired with a substituted artifact. Bind the case to a fresh runner-owned execution context using the runtime's normal invocation/history identity, and reject foreign or prior-context evidence. Repeated equivalent executions may legitimately have equal semantic digests; do not require artificial randomness merely to make digests differ. A cached build is allowed; a cached verdict or substituted historical receipt is not a new execution.

The producer lock pins the compiler, provider/lowerer, independent verifier, Echo runtime/host artifact, target/interpreter profile, codec, and report ABI by exact identity. Local Git builds additionally require the expected revision and clean relevant source. A missing host, unsupported profile, stale pin, or unavailable evaluator is a structured infrastructure failure. There is no native/mock fallback in behavioral mode.

Echo must provide evidence appropriate to the operation. Effectful cases need normal admitted settlement evidence, actual footprints, and the authoritative Tick/WAL relationship. A pure case must use the generic pure-execution evidence contract earned by Echo; do not fabricate a Tick to describe computation that committed no effect. If that result-to-execution binding is unavailable, slice 3 remains blocked.

R4 — Isolation, setup, budgets, and adapter

Use a small Edict-owned execution port and an adapter to Echo's public generic host boundary. Keep Echo implementation dependencies out of compiler/type-kernel crates. Prefer a pinned host process and its versioned generic transport; reuse an existing adequate transport before inventing another. If no public transport can expose the required operations/evidence, add that narrow application-neutral capability under Echo #684. No runTest command is required inside Echo.

The adapter must preflight supported profiles and evidence versions before running cases, impose frame/response limits before allocation, and correlate every terminal outcome with its submitted invocation. Unknown, duplicate, missing, reordered-for-the-wrong-invocation, or truncated outcomes fail closed. There is exactly one terminal outcome per submitted operation. Tests may use a fake port for runner unit tests; those results are never labeled Echo execution evidence.

V1 runs cases sequentially. Every case starts from the same declared empty fixture basis in a separate runtime context. Later stateful cases may declare a bounded ordered setup list of {application, input} pairs executed through the same public build/verification/admission path, within that case only. Setup failure is infrastructure/setup failure and cannot satisfy the case's expected obstruction. Setup operations have separate retained receipts, are not TAP cases, and cannot smuggle a native application planner into the host. Teardown destroys only runner-owned resources; a case may not inherit another case's mutations, installed authority, result, or caches that carry contextual validity.

Semantic work bounds come from the authored, verified operation and Echo's declared cost model. The runner never increases or reinterprets them. A wall timeout is a host safety limit, distinct from deterministic semantic exhaustion; it cannot satisfy an expected application obstruction. Kill and reap a timed-out owned host, retain a bounded partial report, and do not continue with an uncertain shared runtime state.

Proposed v1 hard ceilings, measured before allocation: 1 MiB manifest; 1,024 cases; 128 setup operations per case; 8 MiB aggregate input-fixture bytes; 2,048 decoded case-result bytes; 16 MiB per transport frame; 64 MiB total retained report/evidence metadata. Artifact bodies may be stored separately by verified reference, subject to explicit streaming/disk limits. Add a 256 MiB total runner-owned artifact/log disk cap and a 30-second default wall timeout per operation, configurable only downward in v1. Existing compiler/runtime limits apply too; the stricter limit wins. A limit failure never becomes a skip. Exercise exact-limit and one-over-limit behavior for every new bound.

R5 — Outcomes and expected obstructions

The host verdict is one of passed, assertion_failed, unexpected_obstruction, build_failed, setup_failed, runtime_failed, invalid_evidence, invalid_result, or skipped, with a stable stage and failure kind.

For expect.kind = caseResult, only verified execution plus a valid record with status = 0 passes. Status 1 fails the case. A successful build, admitted package, process exit, or generic receipt by itself cannot pass it.

An alternative expect.kind = obstruction declares the execution stage, exact versioned obstruction coordinate, and an expected payload fixture in the declared codec. Equality is typed canonical payload equality, not prose matching or a loose error substring. Passing requires verified terminal evidence for that invocation and the exact declared obstruction. An unexpected success fails. Compiler errors, setup failures, malformed evidence, transport errors, and wall timeouts cannot match this expectation. Admission-negative and compiler-negative fixtures remain separate host/compiler tests. Generic deterministic budget exhaustion may be tested as an obstruction only when Echo's profile explicitly exposes it as such and its evidence is verified.

R6 — TAP and process behavior

Use the official TAP 14 specification as the normative external format. Emit UTF-8, the version line first, one leading plan, and explicit sequential point numbers. Flat points suffice for v1; subtests, TODO, pragmas, and YAML diagnostics are deferred. Escape description/reason backslashes and hashes. Remove line breaks/control characters from rendered labels so data cannot inject protocol lines or directives. Only explicit suite skip declarations may produce SKIP points. Infrastructure loss emits a bailout and a nonzero exit; it must never look like a completed successful stream. Rich diagnostics belong in the bounded machine report/stderr. Test output must be accepted by an independent TAP parser.

Illustrative output for two executed cases, the second failing its assertion:

TAP version 14
1..2
ok 1 - choose-left
not ok 2 - reject-wrong-result

Runner-specific exit policy: 0 means all selected, executed cases passed; 1 means one or more assertion/expected-outcome comparisons failed; 2 means the suite could not be faithfully completed because of configuration, build, setup, runtime, evidence, protocol, output, or resource failure. Infrastructure failure takes precedence over assertion failure. Continue after ordinary case failures; bail out when execution integrity is unavailable. Failure to write stdout or the requested machine report is not success.

Empty suites and suites with zero executable cases fail with NoExecutableCases and exit 2; intentional per-case skips require a nonempty reason and a tracking reference, and do not count as executed coverage. Invalid manifests discovered before a plan is knowable produce a failed bailout stream, not a fabricated passing zero-case run. CI acceptance below requires its designated witness cases to execute, regardless of any permitted skips elsewhere. Do not infer skip permission from a platform or missing dependency.

R7 — Machine report and reproducibility

Always construct edict.test.run/v1; optionally persist it through --report-json. It contains suite/producer identities, selected ordered case IDs, per-case verdict/stage/kind, expected-outcome identity, bounded application diagnostics, exact artifact/evidence references, assertion count when valid, and aggregate executed/passed/failed/skipped counts. Never silently truncate authoritative IDs or evidence. Diagnostic excerpts may truncate with an explicit marker; raw fixture data need not be echoed by default.

When a persisted report references retained bodies, keep them in a report-adjacent content-addressed artifact directory within the declared storage budget, or reference an explicitly supplied durable artifact store whose identities are verified. Do not leave successful report references pointing into deleted temporary directories. Finalize the report atomically after its referenced artifacts are durable; on interruption retain a clearly incomplete report when possible. Existing caller-owned report/artifact paths must not be overwritten without an explicit output policy. CI supplies a fresh output directory.

Separate semantic results and their evidence references from incidental telemetry such as absolute paths, wall duration, host PID, and ephemeral context locators. Identical pinned inputs must reproduce the same semantic verdicts, artifact identities, and TAP bytes. Compare runtime evidence according to its declared equivalence/basis law, not by stripping meaningful fields until bytes match. Changed case order must change only declared scheduling/report order, not each case's behavior. V1 has no implicit environment-driven discovery, retries, random seeds, or parallel execution.

R8 — Optional assertions library

After the inline result witness works, author a small pure edict.test lawpack with the result contract and the concrete equality/inequality/boolean-condition helpers the first real cases need. Helpers return ordinary bounded values; they cannot print, panic to signal a test verdict, install authority, or call a native testing callback. Use monomorphic helpers supported by actual authored source first; generic assertions, reflection, macros, arbitrary host closures, property testing, and shrinking are follow-up work.

Expected terminal obstructions remain a runner concern when evaluation cannot return a normal value. Where a program can handle a declared obstruction and return a normal assertion result, that remains ordinary Edict semantics. Do not add exception-catching power solely for the library. Require #171/#693 closure evidence before the separate helper lawpack is used across provider boundaries.

R9 — Jim adoption

Jedit owns the Edict test sources, typed input/expected fixtures, and the independent application oracle under its existing edict/replace-range/ and contract-corpus surfaces. Start with the real authored subset, then expand only when the corresponding operation semantics exist.

ReplaceRange conformance must cover the corpus's insertion/deletion/replacement cases, empty and boundary ranges, Unicode/UTF-8 contracts, application-defined invalid coordinates, stale basis/preconditions, and obstruction behavior. For effectful cases, compare bounded observed text/state plus authoritative settlement evidence; a returned “pass” record or package hash alone is insufficient. Structural sharing, node identity, and balance laws are tested only where the Jim contract actually promises them.

A test-only Jedit host adapter may decode observed values and compare them with independent expected fixtures/oracle outputs. It may not choose or submit the application's structural edits. If an Edict-authored driver cannot yet invoke/observe the needed operation through earned generic capabilities, record that concrete limitation; do not hide it behind native control flow and call the whole case Edict-authored.

Keep the existing package/verifier proof and native oracle tests. Add runtime behavior as a new evidence layer. Passing this suite does not by itself complete Jim's production active-observer loop in #295, replace the UI's event routing, or authorize deleting the native path before #296's cutover requirements hold.

Implementation sequence and gates

Each slice starts with owning requirement/case rows and a deterministic RED, then the smallest GREEN change. Proposed paths are placement suggestions, not present artifacts. Keep changes in the owning repository; record exact cross-repo dependencies in implementation PRs.

Slice Owner / dependencies Deliverable and stopping gate
1. Freeze contracts and reporting Edict; no evaluator needed Create docs/topics/behavioral-tests/test-plan.md; define suite/result/report schemas, digest framing, stable failures, discovery, bounds, exit rules, and TAP producer. Proposed edict-test library/CLI crates. RED on malformed result/manifest and a deliberately failing point; GREEN checked by an independent TAP consumer. Unit-only status is explicit.
2. Build and adapter boundary Edict plus Echo's existing public surface Public application build, full artifact verification, pins/snapshotting, execution port, frame limits, fresh-context correlation. Prove substituted report/package and replayed outcome reject using host-contract fixtures. Specify the exact generic host/evidence ABI with Echo; never invent successful runtime evidence to unblock development.
3. Small real runtime witness Echo #684 capabilities, then Edict integration Preserve #684's mandated real-Jedit compiler witness. Once the required generic evaluator is available, run a tiny genuine Edict case with a nonconstant comparison through public build → independent verification → real Echo execution → checked result → TAP. Prove a passing case and an intentional failing case. An authored behavior change must alter the actual executed result and flip the expected verdict. No package-only GREEN.
4. Failure, isolation, and CI hardening Edict runner; Echo generic tests where runtime behavior changes Expected obstructions, setup, state isolation, budgets, malformed/foreign/missing evidence, crash/timeout/output failure, bounded reports, deterministic repetition and independent-parser acceptance. Add a pinned Linux end-to-end CI job with no required-case skips. Add other platforms only with execution evidence; existing Windows lawpack-publication limitations (#198) are not waived.
5. Pure assertion lawpack Edict; #171/#693 when multi-lawpack use requires them Author supported bounded helpers, test their truth tables and failure propagation, and repeat the real witness through the public multi-lawpack build and independent verifier. Mutating an assertion helper must be detected. No new compiler feature without a minimal source RED.
6. Jim conformance adoption Jedit #296; generic Echo graph capabilities as earned Add real Edict application tests and independent oracle comparison; preserve source/package/receipt chain; exercise accepted state changes and obstructions, normal settlement, and recovery. Update exact producer locks only after compatibility is demonstrated. Keep #295's production-observer acceptance separate.
7. Documentation and release evidence Each owner Document runnable examples and expected output, migration/compatibility, supported profiles/platforms, failure taxonomy, limitations, exact validation commands, and CI artifacts. Add an Edict testing tutorial after execution exists. Coordinate Jim workspace pins only from accepted exact revisions.

Before slice 3 can claim GREEN, resolve three concrete runtime questions with executable answers: the generic host entry point, the pure-result-to-invocation evidence contract, and the interpreter's exact budget units/obstruction law. These are Echo integration requirements, not permission to add application or testing semantics to Echo.

Test plan

All cases below are planned. IDs are stable requirements/evidence links; replace proposed fixture names with actual paths and test symbols as each slice lands. Unit tests, compiler/provider tests, actual Echo integration, and Jim application conformance must remain separately labeled.

Case Requirement / layer Fixture and action Required oracle
BT-001 R1 / runner unit Valid ordered suite; invoke from two different working directories. Same resolved input bytes, case order, suite identity; no input changes.
BT-002 R1 / runner unit Duplicate keys/IDs, unknown version/field, missing input, path/symlink escape. Exact structured rejection kind; zero host execution.
BT-003 R1/R4 / host integration Input changes between inspection and use; dirty/wrong producer; substituted lock target. Snapshot bytes used consistently or explicit mismatch; no execution of unverified bytes.
BT-004 R2 / decoder Both valid statuses, every missing/extra/wrong field, status 2, zero assertions, trailing bytes. Exact record accepted or InvalidCaseResult; malformed input cannot pass.
BT-005 R2/R4 / bounds Each new limit at minimum, exact maximum, one over; overflow/truncated length claims. Maximum accepted when otherwise valid; one-over rejects before unsafe allocation.
BT-006 R3 / compiler-provider integration Real source → public build → independent verification; swap Core, closure, projection, package, verifier, or report one at a time. Exact owning failure kind; zero runtime invocation on rejected artifacts.
BT-007 R3 / actual Echo Tiny authored comparison whose result depends on an input/helper/branch. Verified runtime application value, valid case result, one passing TAP point.
BT-008 R3/R5 / actual Echo Same legitimate program with a deliberately false assertion. assertion_failed, failing TAP point, exit 1; accepted execution remains distinguishable from passed assertion.
BT-009 R3 / mutation calibration Change authored helper/branch behavior, rebuild and repin legitimate inputs, retain the independent expected value. Runtime value changes and formerly passing comparison fails; artifact-identity change alone is insufficient.
BT-010 R3/R4 / adapter adversarial Foreign invocation, stale basis/context, wrong result binding, duplicate/missing/late terminal outcome. Structured evidence/protocol failure; no passing verdict; legitimate equal semantic digests still work.
BT-011 R5 / actual Echo Exact expected execution obstruction; wrong coordinate, wrong payload, unexpected success. Only exact verified expectation passes; other outcomes fail comparisons.
BT-012 R5 / negative boundary Compile/setup/admission/transport failure or timeout while expecting an execution obstruction. Infrastructure/appropriate host failure, exit 2; never a passing obstruction case.
BT-013 R4 / actual Echo Two stateful cases in A/B and B/A order, each using its declared setup. Same per-case observations/verdicts; no cross-case authority/state/result leakage.
BT-014 R4 / actual Echo Exact semantic work limit and one beyond, plus a separate wall timeout. Echo's declared deterministic budget behavior; timeout classified separately; no partial published effect.
BT-015 R4 / host integration Host crash, broken pipe, malformed/oversized frame, report/stdout write failure. Bounded cleanup and partial diagnostics; failed run, never synthetic successful remainder.
BT-016 R6 / reporter Passing/failing cases and an explicit skip with reason/reference. Independent TAP parser sees exact plan/count/order/status/skip; exit agrees with host verdict.
BT-017 R6 / reporter adversarial Labels/diagnostics with hashes, backslashes, CR/LF, ANSI/control characters and Unicode. No injected point, directive, bailout, or log on TAP stdout; labels remain bounded.
BT-018 R6 / reporter negative Empty suite, all skipped, interrupted stream, omitted point, wrong plan count, malformed framing. NoExecutableCases where applicable; independent consumer rejects unsuccessful/truncated runs; no exit-0 green.
BT-019 R7 / repeatability Same pinned suite twice, different temp roots; then reordered independent cases. Stable semantic results/artifacts/TAP for same order; per-case semantics unchanged by reordering.
BT-020 R7 / report Bounded diagnostic truncation; wrong evidence reference; missing requested report. Explicit excerpt marker only; authoritative references never truncated; requested-output failure fails run.
BT-021 R8 / lawpack Assertion truth tables, disagreement, exact string/byte bounds, helper-body mutation, stale and refreshed pins. Expected typed result and assertion failure; full closure independently verified.
BT-022 R9 / Jim Real ReplaceRange corpus through authored source and actual generic runtime. Independent expected text/state/outcomes, correct footprint/settlement evidence; no native planner on execution path.
BT-023 R9 / Jim + Echo Obstruct/crash around private evaluation and settlement; restart and observe. Echo's atomicity/recovery contract and Jim's expected state agree; no duplicated or half-published edit.
BT-024 R3/R6 / fault calibration Temporarily force host verdict to pass, drop a failed point, bypass evidence check, or replace runtime with a canned result. The corresponding independent assertion/parser/evidence/runtime witness fails. Restore faults before commit.
BT-025 R1/R7 / compatibility Existing Edict CLI and package proof suites; exact runtime/codec/profile version mismatch. Existing JSONL behavior unchanged; incompatible versions reject explicitly, no fallback/auto-repin.

For every implemented case, record the exact RED command/result, GREEN command/result, test symbol, fixture path, and committed revision in its owning test plan. Expected intentional failing specimens must be verified by a parent test that checks the precise failure and exit code; they must not be permanently skipped to make CI green.

Validation gates

  • Edict: focused tests first, affected compiler/CLI/provider/result-projection suites when those boundaries change, then cargo xtask verify; strict all-target/all-feature Clippy with warnings denied and cargo deny check advisories bans licenses sources for the resulting dependency closure.
  • Echo: owning evaluator/host/evidence tests, existing operation pipeline and recovery tests, and its required repository gate. Extend generic tests only where the new runtime behavior requires them.
  • Jedit: retain the exact package-chain proof and independent native corpus; add the real-runtime suite and the owning repository checks. Name exact Edict/Echo/Jedit revisions and hosted check runs separately.
  • Reporter: pin an independent TAP 14-capable consumer as a development/test dependency, document the choice, and check both accepted and intentionally failed streams. Do not validate the emitter only with its own parser or string snapshots.
  • CI: archive TAP, machine report, exact producer/subject identities, and bounded execution evidence. Verify the real witness's executed count and backend identity. A green job that merely builds packages or skips the evaluator does not close this issue.

Completion criteria

  • The versioned contracts, strict failure taxonomy, bounds, and runnable edict-test interface exist with RED/GREEN evidence.
  • A real bounded Edict assertion case passes through public compilation, independent verification, and actual generic Echo execution.
  • A legitimate authored behavior mutation makes the corresponding test fail at runtime; canned output/package-only substitutes are caught.
  • Expected obstructions, malformed evidence, timeouts, limits, empty/skip behavior, and exit codes obey the specified distinctions.
  • Independent TAP consumption agrees with the machine report and process status, including adversarial output cases.
  • Fresh-context execution, isolation, setup, and order independence have executable witnesses.
  • The assertion library, when introduced, uses complete pinned lawpack closures and adds no runtime intrinsic.
  • Jim has at least one real authored application conformance slice using its independent oracle and normal Echo settlement; remaining corpus coverage is explicitly enumerated.
  • Documentation and exact-head CI distinguish compiler evidence, provider evidence, runtime evidence, and application conformance; designated runtime witnesses are not skipped.
  • Echo remains application-neutral; no Rope/test/TAP primitive, handwritten application package, or native application planner was added as an execution shortcut.

Deferred work

Parallel cases, TAP subtests/TODO/YAML reporting, watch mode, IDE/Bijou dashboards, property testing/shrinking, coverage instrumentation, broad language reflection/generics, alternative runtimes, universal platform support, and the complete Jim observer/UI cutover are separate work. They must not block the first honest runtime-backed test result.

Appendix: Citations
Claim Evidence Confidence Notes
claim:compiler-surface Edict crates/edict-cli/src/main.rs#63@3f81f759e921a69b04fe8cf8e62e62f8f3dc7b7e; docs/topics/cli/README.md#11@3f81f759e921a69b04fe8cf8e62e62f8f3dc7b7e 0.99 Current source/shelf inspection; no new runner tests executed during issue preparation.
claim:projection-boundary Edict docs/topics/result-projections/README.md#5@3f81f759e921a69b04fe8cf8e62e62f8f3dc7b7e, same file line 42 0.99 Projection description and single-projection application boundary.
claim:compiler-evidence-scope Edict docs/topics/lawpack-authoring/test-plan.md#75@19ccbccf5bbe391a055a5ac04b2fd9912c9a8971; #207 0.99 Candidate evidence inspected; not represented as merged/runtime evidence.
claim:jim-current-proof Jedit edict/replace-range/README.md#18@a894c7c4c6d150c0fb210d2e0ca4c27bf518b4c7, same file lines 43 and 93 0.99 Exact authored/package slice explicitly disclaims evaluator and Tick evidence.
claim:echo-execution-gap Echo crates/warp-core/src/echo_operation.rs#575@49e9efb68001dfd78563d18bac9359a87671e431; #684; #724 0.99 Earned runtime profiles inspected separately from candidate pure-program packaging.
Planned verification workflow Edict docs/topics/tests/README.md#19@3f81f759e921a69b04fe8cf8e62e62f8f3dc7b7e 0.99 RED/GREEN and evidence discipline; all BT cases in this issue are planned.
TAP external contract Official TAP 14 specification 0.99 Normative external reference. The proposed producer still needs implementation and independent conformance tests.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions