Implement the Echo Target IR semantic verifier

.github/workflows/ci.yml

@@ -206,6 +206,32 @@ jobs:
             - name: clippy (wasm32 Edict provider adapter)
               run: cargo +1.90.0 clippy -p echo-edict-provider-lowerer --target wasm32-unknown-unknown --lib -- -D warnings -D missing_docs
 
+    build-edict-provider-verifier:
+        name: Build and check Edict provider verifier
+        runs-on: ubuntu-24.04
+        container:
+            image: docker.io/library/rust@sha256:3914072ca0c3b8aad871db9169a651ccfce30cf58303e5d6f2db16d1d8a7e58f
+            options: --platform linux/amd64
+        steps:
+            - uses: actions/checkout@v4
+              with:
+                  submodules: false
+            - uses: dtolnay/rust-toolchain@1.90.0
+              with:
+                  components: clippy
+                  targets: wasm32-unknown-unknown
+            - name: build, audit, and check exact verifier component bytes
+              env:
+                  GIT_CONFIG_COUNT: 1
+                  GIT_CONFIG_KEY_0: safe.directory
+                  GIT_CONFIG_VALUE_0: ${{ github.workspace }}
+              run: |
+                  cargo xtask provider-verifier-component check \
+                    --target-dir target/provider-verifier-component \
+                    --output schemas/edict-provider/components/v1/verifier.echo-dpo.component.wasm
+            - name: clippy (wasm32 Edict provider verifier)
+              run: cargo +1.90.0 clippy -p echo-edict-provider-verifier --target wasm32-unknown-unknown --lib -- -D warnings -D missing_docs
+
     edict-provider-host-v1:
         name: Edict provider host contract (Rust 1.94)
         runs-on: ubuntu-24.04

.github/workflows/det-gates.yml

@@ -257,6 +257,11 @@ jobs:
             --output target/lowerer.echo-dpo.component.wasm
           sha256sum target/lowerer.echo-dpo.component.wasm > "lowerer-hash${CANDIDATE}.txt"
           cp target/lowerer.echo-dpo.component.wasm "build${CANDIDATE}.lowerer.component.wasm"
+          cargo xtask provider-verifier-component designated-build \
+            --target-dir target/provider-verifier-repro \
+            --output target/verifier.echo-dpo.component.wasm
+          sha256sum target/verifier.echo-dpo.component.wasm > "verifier-hash${CANDIDATE}.txt"
+          cp target/verifier.echo-dpo.component.wasm "build${CANDIDATE}.verifier.component.wasm"
       - name: Upload isolated candidate
         uses: actions/upload-artifact@v4
         with:
@@ -267,6 +272,8 @@ jobs:
             build${{ matrix.candidate }}.wasm
             lowerer-hash${{ matrix.candidate }}.txt
             build${{ matrix.candidate }}.lowerer.component.wasm
+            verifier-hash${{ matrix.candidate }}.txt
+            build${{ matrix.candidate }}.verifier.component.wasm
 
   build-repro:
     name: G4 independent build comparison
@@ -303,6 +310,10 @@ jobs:
           cp candidate2/lowerer-hash2.txt lowerer-hash2.txt
           cp candidate1/build1.lowerer.component.wasm build1.lowerer.component.wasm
           cp candidate2/build2.lowerer.component.wasm build2.lowerer.component.wasm
+          cp candidate1/verifier-hash1.txt verifier-hash1.txt
+          cp candidate2/verifier-hash2.txt verifier-hash2.txt
+          cp candidate1/build1.verifier.component.wasm build1.verifier.component.wasm
+          cp candidate2/build2.verifier.component.wasm build2.verifier.component.wasm
       - name: Compare, promote, and check exact bytes
         run: |
           diff hash1.txt hash2.txt || (echo "Reproducibility failure: Hashes differ!" && exit 1)
@@ -317,8 +328,19 @@ jobs:
           cmp build1.lowerer.component.wasm target/lowerer.echo-dpo.promoted.component.wasm
           cmp build1.lowerer.component.wasm schemas/edict-provider/components/v1/lowerer.echo-dpo.component.wasm
           cmp build2.lowerer.component.wasm schemas/edict-provider/components/v1/lowerer.echo-dpo.component.wasm
+          diff verifier-hash1.txt verifier-hash2.txt || (echo "Verifier reproducibility failure: Hashes differ!" && exit 1)
+          cmp build1.verifier.component.wasm build2.verifier.component.wasm
+          cargo xtask provider-verifier-component promote \
+            --candidate-a build1.verifier.component.wasm \
+            --candidate-b build2.verifier.component.wasm \
+            --output target/verifier.echo-dpo.promoted.component.wasm \
+            --write
+          cmp build1.verifier.component.wasm target/verifier.echo-dpo.promoted.component.wasm
+          cmp build1.verifier.component.wasm schemas/edict-provider/components/v1/verifier.echo-dpo.component.wasm
+          cmp build2.verifier.component.wasm schemas/edict-provider/components/v1/verifier.echo-dpo.component.wasm
           echo "Hashes match: $(cat hash1.txt)"
           echo "Lowerer hashes match: $(cat lowerer-hash1.txt)"
+          echo "Verifier hashes match: $(cat verifier-hash1.txt)"
       - name: Upload build artifacts
         if: always()
         uses: actions/upload-artifact@v4
@@ -334,6 +356,10 @@ jobs:
             lowerer-hash2.txt
             build1.lowerer.component.wasm
             build2.lowerer.component.wasm
+            verifier-hash1.txt
+            verifier-hash2.txt
+            build1.verifier.component.wasm
+            build2.verifier.component.wasm
 
   validate-evidence:
     name: Evidence artifact presence
@@ -416,6 +442,10 @@ jobs:
               gathered-artifacts/build-repro-artifacts/lowerer-hash2.txt
               gathered-artifacts/build-repro-artifacts/build1.lowerer.component.wasm
               gathered-artifacts/build-repro-artifacts/build2.lowerer.component.wasm
+              gathered-artifacts/build-repro-artifacts/verifier-hash1.txt
+              gathered-artifacts/build-repro-artifacts/verifier-hash2.txt
+              gathered-artifacts/build-repro-artifacts/build1.verifier.component.wasm
+              gathered-artifacts/build-repro-artifacts/build2.verifier.component.wasm
             )
           fi
 

CHANGELOG.md

@@ -38,6 +38,24 @@
   witness binding them to the checked generated corpus. Its full package gate
   follows publication of `echo-edict-canonical 0.1.0`. These artifacts describe
   and translate provider semantics; they confer no Echo runtime authority.
+- Echo now provides the exact `edict:target-provider/verifier@1.0.0`
+  Component Model implementation for the checked provider closure. The pure
+  verifier independently compares explicit digest-bound Core and Target IR
+  artifacts under the exact target profile and ordered semantic inputs. It
+  emits a canonical accepted report for the reviewed relation, admits a
+  well-formed intrinsic disagreement as a rejected report with an error
+  diagnostic and host-authored output manifest, and preserves an unsupported
+  output-role overclaim as a typed provider refusal with neither response nor
+  manifest. The 183,513-byte checked component has SHA-256
+  `61c833dddb1919a4b92b55b984baf01116b82f6b7d6dc23760b7ecba01dc52c9`
+  and reproduces byte-for-byte across independently provisioned designated
+  `linux/amd64` builders. The isolated pinned Edict host preflights the exact
+  request artifacts and declared output schema, invokes that checked component,
+  then schema-admits each returned accepted or rejected report and authors its
+  output manifest. It replays accepted, rejected, and refused completed outcomes
+  identically in independent fresh stores and separate host processes. These
+  witnesses prove provider verification and host replay only; they do not
+  install, authorize, execute, or observe an operation in Echo.
 - `echo-edict-canonical` now owns the shared pure implementation of Edict's
   canonical CBOR and domain-framed digest contracts as a publishable `0.1.0`
   leaf. `echo-wesley-gen` retains its existing compatibility surface through a

Cargo.toml

@@ -18,6 +18,7 @@ members = [
     "crates/echo-registry-api",
     "crates/echo-edict-canonical",
     "crates/echo-edict-provider-lowerer",
+    "crates/echo-edict-provider-verifier",
     "crates/echo-wesley-gen",
     "crates/echo-dry-tests",
     "crates/echo-cas",

crates/echo-edict-provider-verifier/Cargo.toml

@@ -0,0 +1,29 @@
+# SPDX-License-Identifier: Apache-2.0
+# © James Ross Ω FLYING•ROBOTS <https://github.com/flyingrobots>
+[package]
+name = "echo-edict-provider-verifier"
+version = "0.1.0"
+edition = "2021"
+rust-version = "1.90.0"
+description = "Pure Echo semantic verifier for Edict's frozen Component Model boundary."
+license = "Apache-2.0"
+repository = "https://github.com/flyingrobots/echo"
+readme = "README.md"
+keywords = ["echo", "edict", "wasm", "verification", "compiler"]
+categories = ["compilers", "wasm", "development-tools"]
+
+[lib]
+crate-type = ["cdylib", "rlib"]
+
+[dependencies]
+echo-edict-canonical = { workspace = true }
+
+[target.'cfg(target_arch = "wasm32")'.dependencies]
+wit-bindgen = { version = "=0.58.0", default-features = false, features = ["macros", "realloc"] }
+
+[dev-dependencies]
+hex = "0.4"
+sha2 = "0.10"
+
+[lints]
+workspace = true

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

@@ -0,0 +1,47 @@
+<!-- SPDX-License-Identifier: Apache-2.0 OR LicenseRef-MIND-UCAL-1.0 -->
+<!-- © James Ross Ω FLYING•ROBOTS <https://github.com/flyingrobots> -->
+
+# Echo Edict Provider Verifier
+
+This crate owns Echo's pure semantic decision for Edict's frozen verifier
+boundary. It compares explicit, digest-bound Edict Core and Target IR artifacts
+under the checked Echo provider closure. It performs no discovery or I/O and
+grants no Echo runtime authority.
+
+The first native slice is intentionally independent from the provider lowerer.
+A supported but semantically false Target IR produces a rejected verifier
+report; malformed input in the selected native closure and unsupported source
+semantics produce typed provider refusals. Complete structural admission for
+every CDDL alternative remains the Edict host's owning-schema check before the
+component runs; decoding this native model's result is never admission.
+The `wasm32` guest adapter vendors Edict's exact frozen
+`edict:target-provider/verifier@1.0.0` WIT world and performs only exhaustive
+transport-to-model conversion. Its reproducibly built 183,513-byte checked
+component has SHA-256
+`61c833dddb1919a4b92b55b984baf01116b82f6b7d6dc23760b7ecba01dc52c9`.
+Component identity and admitted host replay remain separate propositions: the
+pinned Edict host preflights the request artifacts and declared output schema,
+invokes the checked component, then admits and manifests each returned accepted
+or rejected report. It preserves an unsupported output-role overclaim as a typed
+refusal without a response or manifest and replays all three completed outcome
+classes identically in independent fresh stores and separate host processes.
+
+For this first one-operation closure, the exact checked target profile, exact
+lowerability facts, and exact `echo.dpo@1.replace` intrinsic jointly bind the
+`precommit-atomic` guard posture and `echo.dpo.footprint/v1` algebra identity. The
+current Target IR has no independent footprint field and its requirements list
+is empty, so this crate does not claim a general guard-order or footprint-
+expression proof. The crate embeds the exact generated type, intrinsic,
+footprint, cost, operation-profile, obstruction, lawpack-adapter, and verifier
+resources. Before comparing Core with Target IR, it reproduces their
+domain-framed identities, resolves the profile and lawpack references, and
+checks the complete reviewed semantic crossing. Raw byte identities remain a
+separate pinned proposition, and workspace validation must still prove these
+package-local copies equal the CDDL-admitted checked corpus.
+
+A verifier report's proposition is deliberately narrow: the fixed verifier
+accepted or rejected the exact Target IR reference named by that report. The
+report alone does not identify the Core, target profile, or semantic closure;
+the digest-locked package assembled by the next campaign goalpost binds those
+inputs and the verifier component together. Neither artifact grants Echo
+runtime installation, execution, or consequence authority.

crates/echo-edict-provider-verifier/resources/authority-facts.echo-dpo.cbor

@@ -0,0 +1 @@
+¥fsource£dkindmtargetProfilefdigest‚fsha256X ôóVbZÁî‹Îe/ýßçTþ~ê¹ÒUÐØ2-°jcoordinatejecho.dpo@1gbudgets japiVersionxedict.authority-facts/v1qoperationProfiles¡kp.effectful¢dcorexcontinuum.profile.write/v1sallowedWriteClasses¡greplaceöreffectWriteClasses¡ntarget.replacegreplace

crates/echo-edict-provider-verifier/resources/generated-artifact-profile.echo-dpo-registration.cbor

@@ -0,0 +1 @@
+¤etypes¦ha.b@1.Id£dkindocoreStringAliasicanonicalhraw-utf8omaxScalarValueska.b@1.Input¢dkindfrecordffields¢dnamebiddtypeha.b@1.Idla.b@1.Output¢dkindfrecordffields¢dnamebiddtypeha.b@1.Idma.b@1.Receipt¢dkindfrecordffields¢dnamebiddtypeha.b@1.Idwtarget.replace.rejected¢dkindfrecordffields€xdomain.WriteRejected.Payload¢dkindfrecordffields€japiVersionx"echo.generated-artifact-profile/v1joperations¡ga.b@1.t©fbudgetfp.tinyfeffectntarget.replaceiinputTypeka.b@1.InputjoutputTypela.b@1.OutputmopticContractmreplace-pointnimplementation¢dkindfnativejcoordinaterecho.dpo@1.replaceninvocationKindhmutationpoperationProfilexcontinuum.profile.write/v1sobstructionMappings¡hrejectedtdomain.WriteRejectedmtargetProfilejecho.dpo@1

crates/echo-edict-provider-verifier/resources/resource.lawpack-exports.cbor

@@ -0,0 +1 @@
+¦etypes¢jcoordinateha.b@1.Idjdefinitionx!String<max=16,canonical=raw-utf8>geffectsªiinputTypeha.b@1.Idjcoordinatentarget.replacejoutputTypema.b@1.ReceiptlguardSupportõncostObligationstarget.replace.costneffectFailures¡hrejected¢kpayloadTypewtarget.replace.rejectednauthorityClassndomainMappableneffectKindHintgreplacenexecutionClassgruntimentypeParameters€sfootprintObligationxtarget.replace.footprinticonstants€lobstructions£jcoordinatetdomain.WriteRejectedmpayloadSchemaxdomain.WriteRejected.PayloadnauthorityClassndomainMappablempureFunctions€qoperationProfiles 

crates/echo-edict-provider-verifier/resources/resource.lawpack-target-adapter.cbor

@@ -0,0 +1 @@
+¥eclasskdeclarativejapiVersionx-echo.edict-provider.lawpack-target-adapter/v1mtargetProfilejecho.dpo@1ntargetIrDomainoecho.span-ir/v1ueffectImplementations¡ntarget.replace£dkindfnativejcapabilityrecho.dpo@1.replacejwriteClassgreplace

crates/echo-edict-provider-verifier/resources/resource.lawpack-verifier.cbor

@@ -0,0 +1 @@
+£eclasskdeclarativejapiVersionx'echo.edict-provider.lawpack-verifier/v1uoperationObstructions¡ga.b@1.t¢feffectntarget.replaceofailureMappings¡hrejectedtdomain.WriteRejected

crates/echo-edict-provider-verifier/resources/resource.target-cost-algebra.cbor

@@ -0,0 +1 @@
+£eclasskdeclarativejapiVersionpecho.dpo.cost/v1lcapabilities¡recho.dpo@1.replace£feffectntarget.replacelcostTemplatestarget.replace.costrsemanticObligationstarget.replace.cost

crates/echo-edict-provider-verifier/resources/resource.target-footprint-algebra.cbor

@@ -0,0 +1 @@
+£eclasskdeclarativejapiVersionuecho.dpo.footprint/v1lcapabilities¡recho.dpo@1.replace¤feffectntarget.replacejwriteClassgreplaceqfootprintTemplatextarget.replace.footprintrsemanticObligationxtarget.replace.footprint

crates/echo-edict-provider-verifier/resources/resource.target-intrinsics.cbor

@@ -0,0 +1 @@
+¢japiVersionx"edict.target-profile.intrinsics/v1jintrinsics¡recho.dpo@1.replace«jeffectKindgreplacejreturnTypema.b@1.ReceiptjwriteClassgreplacelcostTemplatestarget.replace.costlguardSupportõmargumentTypesha.b@1.IdneffectFailures¡hrejected¢kpayloadTypewtarget.replace.rejectednauthorityClassndomainMappablenintrinsicClassfeffectntypeParameters€qfootprintTemplatextarget.replace.footprintxcanParticipateInAtomicGuardõ

crates/echo-edict-provider-verifier/resources/resource.target-ir.cbor

@@ -0,0 +1 @@
+¥eclasskdeclarativefdomainoecho.span-ir/v1japiVersionoecho.span-ir/v1lcapabilities¡recho.dpo@1.replaceömtargetProfilejecho.dpo@1

crates/echo-edict-provider-verifier/resources/resource.target-obstruction-taxonomy.cbor

@@ -0,0 +1 @@
+¤eclasskdeclarativejapiVersionxecho.dpo.obstructions/v1neffectFailures¡wtarget.replace.rejected¢kpayloadTypewtarget.replace.rejectednauthorityClassndomainMappablerdomainObstructions¡tdomain.WriteRejected¢mpayloadSchemaxdomain.WriteRejected.PayloadnauthorityClassndomainMappable

crates/echo-edict-provider-verifier/resources/resource.target-operation-profiles.cbor

@@ -0,0 +1 @@
+¢hprofiles¡xcontinuum.profile.write/v1¢mopticTemplate¥iopticKindsaffectReintegrationlboundaryKindfaffectmsupportPolicyx&continuum.support.carry-or-obstruct/v1olossDispositionx#continuum.support.reject-on-loss/v1sapertureRequirement¢crefxtarget.replace.footprintdkindxabstractFootprintObligationoeffectPredicatex'echo.dpo.operation-mode.replace-only/v1japiVersionx*edict.target-profile.operation-profiles/v1

crates/echo-edict-provider-verifier/resources/resource.target-verifier-contract.cbor

@@ -0,0 +1 @@
+§eclasskdeclarativejapiVersiontecho.dpo.verifier/v1lcapabilities¡recho.dpo@1.replaceömtargetProfilejecho.dpo@1nopticContracts¡xcontinuum.profile.write/v1mreplace-pointntargetIrDomainoecho.span-ir/v1qoperationProfiles¡xcontinuum.profile.write/v1ö