Compile first-order source functions into authenticated Core #226

Jim's retained-buffer decoder needs ordinary, authored, first-order helper functions. Edict's language specification describes those functions, but the public compiler currently rejects even fn retainFact(value: text.FactBytes) -> text.FactBytes { return value; } at declaration parsing. This issue owns the compiler and authenticated contract prerequisite for real source functions. Jim remains responsible for its editing semantics; Echo stays generic.

Observable outcome and scope

A module can declare and call nongeneric, first-order, nonrecursive, effect-free functions with typed parameters, ordered immutable let bindings, and a terminal return. The compiler checks every definition, including unused ones, and preserves executable bodies and call coordinates in authenticated Core through Target validation. This is one coherent compiler change, not a parser-only milestone.

Use a distinct source-owned Core function map with typed parameters, local bindings, return type and result, based on the existing pure core-fn-body algebra. Omit the map when empty so existing function-free canonical artifacts remain identical. Source functions must not impersonate digest-locked imported lawpack facts. A Target duplicate is unnecessary when its semantic closure binds the exact Core module; any duplicate must be independently checked for equality.

• Collect signatures before checking bodies, allowing forward references. Keep lexical frames separate, disallow caller-local capture and invalid shadowing, and reject wrong arity/types, duplicate/forward locals, invalid returns, effects/requests/reads, and unsupported statements.
• Preserve argument order and evaluation exactly once, including unused arguments. Calls must stay inside their selected conditional/predicate/basis/failure context; textual substitution or eager hoisting is not an acceptable implementation.
• Reject direct and mutual recursion. Bound longest directed call paths using completed height summaries rather than an identity-only visited cache. Account for every call occurrence and transitive imported-helper cost with checked arithmetic. See the separate investigation Reproduce possible order-sensitive pure-helper call-depth validation #203; its suspected defect is not treated as confirmed without execution.
• Validate totality through function bodies. Unknown-call fallback must not hide a partial operation inside a function. Preserve source spans for useful diagnostics.
• Include signatures, bodies and callees in canonical semantic identity. Alpha-renaming parameters/locals must preserve identity; executable body changes must change it.
• Update the normative Core schema, canonical encoder, public Rust exports, and generated provider contract publication through cargo xtask provider-contract-pack --write. Explicit contract selection/admission must distinguish the new shape.

Acceptance

1. Deterministic RED on the existing public parser/compiler for a trivial function and a called helper factored from Jim's real range-assembly source.
2. Positive Core/Target witnesses for identity, a two-argument byte concatenation, nested forward calls, and ordered local bindings. Negative witnesses cover every refusal above, unused malformed definitions, direct/mutual recursion, 128/129 path boundaries, shared-suffix/diamond graphs, and checked transitive budget overflow.
3. Conditional and pre-body calls preserve placement and cost; transitive totality catches invalid operations in called bodies. Tests distinguish repeated parameter use from repeated evaluation and account for unused arguments where the compiler contract makes that observable.
4. Existing function-free canonical golden artifacts remain byte-identical. New function bodies are covered by schema/type/authority validation and identity tests.
5. A real public application build against an old provider explicitly refuses the unsupported contract without publishing package/report artifacts. This is the expected safe intermediate state until the companion generic Echo implementation lands.
6. Update owning syntax/compiler-spine/Core-IR/Target-IR topic requirements and test plans alongside tests; describe implemented branch behavior only after it exists. cargo xtask verify passes in the guarded shared Docker worker. Obtain Code Lawyer and independent adversarial review before merge.

Evidence and dependencies

The recovered Jim experiment used compiler 17397e2aad18a83ffc617d1afd628764501f49cd, CLI SHA-256 e2700698829b03f437c66425ed9878b002ef7a34ac183a39bac4eaf6a758cc6d. Its read control built package/report; trivial fn refused with InvalidApplicationSource / ExpectedToken at bytes 151–153. The full Decimal draft independently refused earlier in lexing, so it does not establish the fn boundary. The original harness expected the wrong diagnostic and exited 1; raw evidence is being retained in Jim PR302, supporting Jim296.

Current declaration dispatch remains limited to type/enum/intent at crates/edict-syntax/src/parser.rs on merged base 80ae9edc2c4ed127e18ea2434c20dd20ed39cadc. Existing Core function bodies are lawpack-owned; CoreModule has no source-function table. Source-function execution through Echo is a separate dependent issue, not a claim of this compiler merge.

Excluded: generics/higher-order functions, recursion, source variants/match, byte-escape repair, checked arithmetic/Option expansion, result-producing folds, a complete Buffer decoder, rope mutation, or Jim admission/recovery. Pure-block assertions remain explicitly unsupported unless given an actual proof-node lowering in this change; do not silently discard them.