Admit generic Edict pure-program contracts

CHANGELOG.md

@@ -5,8 +5,53 @@
 
 ## Unreleased
 
+### Fixed
+
+- Native pure executable-package providers now enforce the compiler-owned
+  projection artifact, node, path, text, and exact-field bounds. The pure output
+  budget remains Core-declared; the anchored route's fixed output ceiling is
+  not applied to pure programs. Both independently reproduced checked components
+  include these bounds.
+- Native pure executable-package providers now require an adapter profile with
+  empty `semanticEffects` and a nonempty `budgetObligation` before constructing
+  or accepting a no-effects package. Effectful profiles remain unsupported on
+  this route. Both checked components include this validation.
+- The native pure executable-package lowerer and verifier now validate source
+  artifacts before dispatch: the source reference must match Core's coordinate,
+  and its canonical value must be a UTF-8 byte string. Rebinding an invalid
+  source's digest no longer bypasses these checks. Both checked components
+  include this validation.
+- The pure executable-package verifier now compares the application
+  result projection with the authored Core result and its output contract.
+  A digest-bound projection could previously select another field or binding,
+  omit a field, or change its output type or budget and still be accepted.
+  The independently reproduced checked component includes this check.
+- The Edict executable-package verifier now refuses pure-v1 Target IR
+  that changes Core let bindings, results, input constraints, or basis, or
+  introduces extra intents or requirements. Exact package reconstruction alone
+  could accept an independently rebound but semantically inconsistent pair.
+  The native verifier and checked WASM package carry the same relation check.
+
 ### Added
 
+- The checked Edict provider contract now admits generic nominal Core types as
+  exact contract coordinates over bounded storage representations. The
+  regenerated provider package remains application-neutral and adds no Jim,
+  buffer, head, rope, or range vocabulary to Echo.
+- The checked Edict provider package now admits the exact contract pack from
+  Edict #201, including source-ordered generic pure Target IR bindings and
+  compiler-owned pure-binding result projections. Echo pins the new source and
+  manifest identities, preserves the bounded contract-pack admission boundary,
+  and regenerates every affected provider schema, provenance record, package
+  manifest, and package-local carrier without adding application vocabulary.
+- The provider schema now admits the exact two-field
+  `compiler-produced-bounded-pure/v1` target configuration. The configuration
+  contains no operation coordinate, application vocabulary, budget override,
+  or runtime authority. The checked lowerer now emits a distinct generic pure
+  package containing the exact compiler Core, lawpack exports, Target IR, and
+  result projection; the structurally separate verifier independently
+  reconstructs and accepts that relation. This is executable package
+  construction evidence, not Echo runtime evaluation or settlement evidence.
 - Strict filesystem WAL stores now persist a checksummed writer-epoch ledger
   containing the active epoch, its exact latest closed predecessor, and final
   LSN and commit-digest evidence. Bounded retention keeps ledger writes and
@@ -159,12 +204,12 @@
   coordinate-framed exports and adapter references independently from their
   provider-envelope domains. Its lowerer and verifier components were
   independently reproduced in copy-only, mount-free designated `linux/amd64`
-  containers and promoted at 258,787 bytes /
-  `dfd14015705ff555a7efdb3787ddb0f8b4f304168a9a0ebf324fd25d430bf5cd`
-  and 277,836 bytes /
-  `279738ffeea40027eb493c15e873b87cf3aa0677a57f9f03fb824698e532322f`,
+  containers and promoted at 277,694 bytes /
+  `a4758f060122fba8c073841ccaa22bf0b8a742b495b76eb33c914eff3250dcf5`
+  and 308,859 bytes /
+  `174cf8758815bf2b9f2ef575517aa6d144ed3f2d1995fc65d25a211b9dea82d9`,
   respectively. The resulting 25-file package has provider identity
-  `sha256:6685b7c629ae6955515d69158feb1d7db06af2193de7e5d13e1095101670b977`.
+  `sha256:a4e0d9e31ada5c8c14adfce05fdecb228e5b79545f3574a5e21e7db71ab3f307`.
   This package build proves generic compiler/provider lowering and independent
   verification. The separate `run-edict-operation` witness now consumes that
   crossing through Echo-owned runtime execution.

crates/echo-edict-provider-lowerer/README.md

@@ -117,8 +117,8 @@ proposal constructor supports mutations and refuses a `Query`; authored reads
 remain a separate bounded observer/optic path and must never be represented as
 synthetic mutations.
 
-The refreshed 258,787-byte checked lowerer component has SHA-256
-`dfd14015705ff555a7efdb3787ddb0f8b4f304168a9a0ebf324fd25d430bf5cd` and has
+The refreshed 279,564-byte checked lowerer component has SHA-256
+`11244b22dcf7128489953f7a2d09df1eeb69e7b25bddb54e0e255b51ca23e016` and has
 crossed the reproducible promotion boundary. The pinned Edict host admits its
 generated envelope under the owning `generated-artifact` CDDL root, and the
 isolated host fixture exercises the exact helper binding, typed codecs, EINT
@@ -132,6 +132,15 @@ lawpack import in the supplied source. Lawpack-owned export and adapter
 references retain their coordinate-framed digests independently from the
 provider envelope's schema-domain digests.
 
+The provider schema also admits the exact zero-choice
+`compiler-produced-bounded-pure/v1` target configuration. That admission only
+allows a compiler-produced pure-program request to reach this component. The
+lowerer validates the effect-free compiler relation and emits a separate
+generic package variant that retains the exact Core, lawpack exports, Target
+IR, and result-projection bytes under bounded budget, empty-footprint, and
+no-effect authority identities. It does not evaluate those bytes, install the
+package, mutate a graph, or settle an Echo Tick.
+
 The native Rust model is also the narrow unit-test boundary. A `wasm32` adapter
 generated from [`wit/edict-target-provider.wit`](wit/edict-target-provider.wit)
 exports the exact Component Model function and performs total conversions to