Compile bounded control flow and digest-bound pure lawpack helpers into Core

[flyingrobots]

Current acceptance reconciliation (2026-09-07)

The diagnosis below is retained as historical evidence at df80f92a; it no longer describes the landed compiler. PRs #193, #194, #196, and #201 delivered the relevant compiler, branch-result, public lawpack-authoring, and type/Target integrity foundations.

Reverified Edict main 3f81f759e921a69b04fe8cf8e62e62f8f3dc7b7e with cargo test -p edict-syntax --test compiler_spine --test lawpack: 80 compiler-spine tests and 58 lawpack tests passed.

Acceptance	Current evidence
Exact imported Edict helper	exact_lawpack_pure_helper_signature_enters_source_compilation, lawpack_compilation_requires_the_exact_digest_locked_source_import in crates/edict-syntax/tests/lawpack.rs
Conditional values	pure_conditional_expression_lowers_to_core, pure_conditional_expression_rejects_incompatible_branches in crates/edict-syntax/tests/compiler_spine.rs
Explicit branch joins	effectful_branch_yield_lowers_to_bound_core_branch, branch_yield_records_join_compatible_fields_independently, branch_yield_does_not_leak_locals in compiler_spine.rs
Bounds and budgets	digest_bound_coordinate_loop_cap_lowers_to_core, bounded_list_loops_reject_cumulative_and_nested_over_budget_work, pure_helper_costs_are_charged_at_call_sites_and_inside_loops in compiler_spine.rs
Fail before provider invocation	edict_pure_helper_call_graph_must_be_acyclic, edict_pure_helpers_reject_effectful_and_unresolved_callees, export_digest_substitution_rejects in lawpack.rs; invalid-bound compiler tests; public compilation precedes invocation at crates/edict-cli/src/application_build.rs#287@3f81f759e921a69b04fe8cf8e62e62f8f3dc7b7e
Deterministic public artifacts	repeated_public_builds_preserve_core_and_package_bytes in Jedit edict/replace-range/tests/proof-harness.spec.mjs at a894c7c4c6d150c0fb210d2e0ca4c27bf518b4c7; real Jedit source and authored lawpack, Edict main above, exact Echo 49e9efb68001dfd78563d18bac9359a87671e431; two independent builds compare embedded Core, Target and projection plus emitted package/report bytes
Closed pure-helper representation	edict_pure_helper_body_must_match_the_closed_pure_core_schema and purity/callee rejection tests in lawpack.rs; this does not claim the host CLI has no explicit filesystem or process boundary
Artifact distinctions	Edict compiler-spine, lawpacks, Target IR and result-projections topic shelves; Jedit edict/replace-range/README.md at a894c7c4c6d150c0fb210d2e0ca4c27bf518b4c7 explicitly distinguishes package verification from evaluator/rope/Tick evidence

The final mutation-evidence criterion is now implemented and reviewed in PR #207, exact signed head 19ccbccf5bbe391a055a5ac04b2fd9912c9a8971. All 9 acceptance criteria have executable evidence; #207 remains open and this issue awaits its merge.

The new Rust witnesses in crates/edict-syntax/tests/lawpack_authoring.rs publicly author a helper result changing from 7 to 8, reject stale manifest/exports and source-pin combinations with stable kinds, prove repinned Core/Target identity changes, and isolate conditional, loop-bound, and loop-body mutations. The public CLI witness public_build_requires_repinning_an_authored_helper_body_change in crates/edict-cli/tests/lawpack_authoring_cli.rs proves deterministic builds, stale-pin rejection, preservation of old output, absence of fresh output on failure, and artifact changes after repinning.

The loop witness deliberately preserves the current boundary: loops compile into Core and body/bound changes move Core identity, while Target lowering returns UnsupportedCoreNode and emits no artifact. This is compiler evidence, not loop packaging, evaluation, rope semantics, or a runtime receipt.

Exact committed-head cargo xtask verify passed 902 tests, strict Clippy, fixture checks, and all 27 topic shelves. The dependency audit passed. Hosted exact-head CI 34180126556 passed all five jobs. The final Codex review found no major issues at 19ccbccf5b. CodeRabbit independently marked its two documentation findings addressed and resolved; its superseded review submission was dismissed with evidence. No production Rust change was required.

Exact-head Jedit CI 34168569421 passed at a894c7c4c6d150c0fb210d2e0ca4c27bf518b4c7, including the package-chain job.

Jedit #302 is still an open draft and Echo #724 is still an open provider candidate. The verified first source constructs a typed boundary result; no rope mutation, generic runtime evaluation, or Tick is claimed. #203 remains a separate NEEDS_REPRODUCTION follow-up and does not reopen #201.

---

Problem

The public Edict application-build boundary cannot yet compile the first real Jim-owned bounded data-structure operation.

This is an Edict source-to-Core gap. It is not a request for Echo to learn any Jim, Jedit, rope, buffer, or ReplaceRange vocabulary.

At current origin/main (df80f92ad6242c6da31a64224666fd37aa43b0d0):

• the AST already represents statement if and statically bounded for (ast.rs lines 247-262);
• the compiler rejects both as UnsupportedSourceShape (compiler.rs lines 888-891);
• value expressions still reject calls, conditional expressions, variants, and matches (compiler.rs lines 1931-1944);
• the lawpack ABI already parses and validates hash-bound exported pure functions (lawpack.rs lines 742-775);
• but CompilerContext contains only operation-profile, effect, and budget facts (compiler.rs lines 59-70), and prepare_lawpack_compilation imports only those categories (lawpack_adapter.rs lines 203-268).

The ABI already defines the intended authority-free representation: Edict-authored helpers carry hash-bound pure Core bodies, and those bodies cannot contain effects, guards, branches, loops, proof nodes, or runtime callbacks (edict-core.cddl lines 118-142).

First consumer

Jedit #296 owns the real ReplaceRange.edict source and Jim lawpack closure.

The language specification already sketches the required source shape: digest-locked helper calls, a conditional value, and bounded loops (SPEC lines 3115-3181).

Local diagnostic probes ran through the same public edict application build path used successfully by Hello Echo. The known-good Hello Echo producer closure built successfully. Replacing only the source with a bounded-loop probe and a conditional probe produced the stable structured failure:

{
  "kind": "ApplicationCompilationFailed",
  "message": "Edict application did not compile to Core: [CompilerError { stage: TypeCheck, kind: UnsupportedSourceShape, message: \"statement is outside the initial lowerable subset\", ... }]"
}

Those probes are diagnostic scaffolding only. They are not ReplaceRange.edict, and the causal-cell profile used to isolate compiler behavior is not Jim semantics.

Required capability

Compile the already-specified bounded, target-neutral source constructs into canonical Core:

1. Lower conditional expressions and statement conditionals with deterministic type/state joins.
2. Lower for ... bounded ... only when its maximum cardinality is digest-bound and provable.
3. Resolve calls to pure functions from the exact imported lawpack closure.
4. Carry each helper implementation and call identity into Core/package identity so substitution changes the digest.
5. Account helper cost templates and loop bounds in the operation budget and declared footprint obligations.
6. Preserve typed diagnostics and obstruction flow without host exceptions.
7. Produce stable structured failures for missing helpers, type disagreement, invalid bounds, recursion/cycles, or non-pure helper bodies.

Acceptance criteria

• A source module can call a hash-bound source: edict pure helper from its exact imported lawpack closure.
• A conditional value whose branches agree in type lowers to canonical Core.
• A statement conditional lowers with explicit branch-join rules.
• A bounded loop lowers with a statically admitted maximum and deterministic budget accounting.
• Recursive helper call graphs, missing callees, effectful helper bodies, unprovable bounds, and digest substitution reject before provider invocation.
• Public application build emits byte-identical Core/package artifacts for byte-identical source plus closure.
• Mutation tests prove helper-body, bound, branch, and loop semantics affect emitted Core or fail the gate.
• No filesystem, network, process, native callback, opaque host function, or application-specific intrinsic is introduced.
• Documentation distinguishes application source, lawpack helper semantics, target IR, provider package, and runtime receipt.

Explicit non-scope

This issue does not:

• define Jim or Jedit operations;
• add rope, buffer, leaf, branch, TextWindow, or ReplaceRange intrinsics;
• implement a generic graph runtime in Echo;
• allow caller-authored mutation plans or patches;
• construct executable semantics from an oracle;
• prove the final Jim active-observer loop.

Once real source compiles to generic Core, target-profile gaps belong to Echo #684. The compiler-produced package, not the Jedit oracle, must drive that work.