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

Current acceptance reconciliation (2026-10-04)

The original df80f92a diagnosis below is historical; it does not describe the current compiler. PRs #193, #194, #196 and #201 supplied the source/Core/helper foundations. The remaining mutation evidence is in PR #207, now refreshed by an ordinary merge of main cd3e52eb89d4f6686a1915eb44f12662df81b408 at signed head 17397e2aad18a83ffc617d1afd628764501f49cd.

The refreshed diff remains evidence-only: two test files and five owning documentation files, no production Rust or runtime change. The public API witnesses author a helper result changing from 7 to 8, reject mismatched exports/manifest and stale source pins with typed failures, and verify repinned Core/Target identity changes. Independent conditional, loop-bound and loop-body changes retain their controlled inputs. The public CLI witness verifies repeated artifacts, InvalidApplicationClosure, preservation of old output, absence of fresh output on failure, and changed artifacts after exact repinning.

The loop boundary is unchanged: bounded source loops reach Core, and body/bound mutations change Core identity; Target returns UnsupportedCoreNode and no artifact. These checks do not establish loop packaging, evaluator execution, rope behavior or a runtime receipt.

Fresh validation at the exact signed head:

• Three focused API mutation tests and one public CLI test passed in Docker.
• Four isolated temporary compiler faults caused five expected assertion failures. Each production source was restored and hash-checked before the next fault; this calibrates the tests rather than claiming a baseline bug was repaired.
• cargo +1.95.0 xtask verify passed: 967 passed, 0 failed, 1 ignored across 57 summaries, strict Clippy, formatting, fixture/golden checks, 27 topic shelves and 11 release tags.
• Current main's test-plan IDs remain intact. Mutation rows are now CSPINE-TP-046 / TIR-TP-078, and their calibration reference is consistent.

The original 902-test run and old review results remain historical, not current-head validation. Both old documentation threads are resolved. Fresh hosted checks and Code Lawyer/independent review remain required before merge; this issue remains open until #207 merges. All nine acceptance criteria below retain executable evidence at their stated compiler/artifact boundaries, with the final mutation criterion awaiting integration.

Current evidence: crates/edict-syntax/tests/lawpack_authoring.rs#291@17397e2aad18a83ffc617d1afd628764501f49cd; crates/edict-cli/tests/lawpack_authoring_cli.rs#84@17397e2aad18a83ffc617d1afd628764501f49cd; calibration recipe docs/topics/lawpack-authoring/test-plan.md#53@17397e2aad18a83ffc617d1afd628764501f49cd. The earlier whole-issue reconciliation remains in this issue's edit history; frozen Jim and provider pins are unchanged by this refresh.

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.