Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .ban-nondeterminism-allowlist
Original file line number Diff line number Diff line change
Expand Up @@ -18,3 +18,4 @@ std-env crates/warp-core/tests/wsc_store_tests.rs WSC filesystem fixture temp di
std-fs crates/warp-core/tests/wsc_store_tests.rs WSC filesystem fixture I/O only.
std-process crates/warp-core/tests/wsc_store_tests.rs WSC filesystem fixture temp directory disambiguation only.
std-fs crates/warp-math/tests/trig_golden_vectors.rs golden-vector fixture read/write only.
std-fs crates/echo-edict-provider-lowerer/tests/lowerer_contract.rs explicit ignored checked generated-helper fixture regeneration only.
18 changes: 18 additions & 0 deletions AGENTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -132,6 +132,24 @@ changed, update `CHANGELOG.md` when shipped behavior changed, run the narrow
witness and directly relevant checks, and commit the result as a focused new
commit. Record follow-on work in GitHub rather than in the repository.

## Pre-PR Documentation Accuracy Gate

Immediately before opening a pull request, and again after material review
changes, compare the branch's actual behavior and artifacts with the current
documentation. Revisit the relevant entrances and canonical owners:
`README.md`, `GUIDE.md`, `docs/README.md`, `docs/architecture/`, `docs/spec/`,
`docs/invariants/`, `docs/topics/`, and the evidence anchors of any applicable
accepted ADRs.

Search specifically for stale current-state claims such as “not implemented,”
“fixture-only,” old ownership or authority boundaries, obsolete version or
compatibility statements, and examples that still prescribe a superseded path.
Correct inaccuracies in their owning documents before opening the PR. Do not
create a status ledger or duplicate change-local implementation detail in
multiple documents; keep durable boundaries in their canonical owners and link
to them. If the review finds no documentation impact, say so explicitly in the
pull-request body.

---

**The goal is inevitability. Every feature is defined by its tests.**
70 changes: 64 additions & 6 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -36,13 +36,34 @@
field swaps, authority-source disagreement, malformed schemas/components,
and invalid requests all fail before guest execution. This proves package
readiness only, never Echo installation, execution, or runtime authority.
- `echo-wesley-gen` now carries a fixed 35-file package-local source and provider
- `echo-wesley-gen` now carries a fixed 38-file package-local source and provider
asset boundary, preserving original logical source labels while making its
`.crate` archive independent of workspace-parent files. An explicit sync tool
distinguishes authoritative generated/component owners from their checked
package corroboration, supports staged regeneration without circularity, and
checks exact Cargo archive selection. The extracted archive compiles when its
checks exact Cargo archive selection. Fixed owner leaves are opened without
following final symbolic links and read twice through one retained descriptor;
file-type, length, or byte disagreement refuses a moving owner. The generator
source identity now enumerates 20 files and includes the exact manifest and
implementation bytes of its canonicalization, operation-id-law, and
provider-registry dependencies. The extracted archive compiles when its
still-unpublished Echo dependencies are supplied through local patches.
- Echo now owns the versioned semantic operation-id law
`echo.semantic-operation-id.fnv1-32/v1`. It derives a persisted `u32` from the
exact semantic coordinate and generic query/mutation kind, remains
domain-separated from Wesley's GraphQL-field-name law, and reserves the top
two ids for Echo protocol envelopes: `u32::MAX` for scheduler control and
`u32::MAX - 1` for witnessed suffix import. The canonical generated-artifact
profile carries both the law coordinate and each derived id; generation
refuses either reserved value and package-local collisions without salting,
probing, or renaming. Its CDDL bounds `operationId` to the remaining numeric
application range, but schema admission alone does not prove derivation or
collision freedom: semantic generation recomputes the law and checks the
complete operation set. This packages an exact operation-identity proposition
but does not register, install, authorize, or execute the operation. Generated
source now carries public expected constants for the profile-owned law and id,
requires both as untrusted bundle claims, refuses disagreement, and exposes
the matched claim through the resulting private-state registration descriptor.
- Echo now provides the exact `edict:target-provider/lowerer@1.0.0`
Component Model implementation for the first checked provider closure. The
pure lowerer accepts only explicit digest-bound Core, target-profile,
Expand All @@ -51,7 +72,7 @@
wrapper; and returns typed refusals for unsupported ABI, profiles, semantics,
reads, rebound operations, unresolved authored optics, changed type bindings,
Core type definitions, evaluation budgets, out-of-scope locals, intrinsics,
and output roles. Local admission distinguishes pre-effect, obstruction-arm,
and undeclared or malformed output-role claims. Local admission distinguishes pre-effect, obstruction-arm,
and post-effect scope from the exact input, effect-result, and obstruction
declarations before cloning any expression into Target IR. The first closure
also requires an empty input-constraint set and the exact zero-argument
Expand All @@ -66,14 +87,51 @@
exact Rust and Cargo executables, binds Cargo to that compiler, owns the inner
Cargo home, removes ambient Cargo profile/build/target overrides, remaps its
dependency source paths to `/cargo`, and atomically promotes only distinct
candidates matching a reviewed repository digest.
candidates matching a reviewed repository digest. The promoted 189,668-byte
component has SHA-256
`9b5ecf1c87a4a98ad3d7381d85e3625649a4f9d62f80f74b2aca6ace26be14af`.
Other-host builds are structural and semantic witnesses
rather than cross-host compiler-identity claims. The publication-enabled,
archive-self-contained `echo-edict-provider-lowerer` source crate carries
package-local copies of its four exact admitted resources, with a workspace
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.
- The native Echo Edict lowerer model now accepts any exact, lexicographically
sorted subset of the declared `generated.echo-dpo` generated artifact,
`review.echo-dpo` review payload, and `target-ir.echo-dpo` Target IR roles.
It emits canonical-CBOR generated and review envelopes at
`generated/echo_dpo.rs` and `review/echo_dpo.json`, and refuses unknown,
mismatched, duplicate, or out-of-order role claims with typed
`UnsupportedOutputRole`. The generated Rust binds the semantic operation,
Target IR, Echo ABI and helper API, provider and operation schemas, target and
generated profiles, and abstract footprint
obligation/algebra. It then performs only an
explicit post-assembly equality and consistency comparison between an
independent expected pin and untrusted Edict semantic/release bundle claims,
with typed refusal for every identity class. Every domain-framed resource is
compared as a complete coordinate/domain/digest proposition.
The generated-artifact profile now owns `le-binary-v1`, and generated Rust
implements distinct bounded `Id`, `Input`, and `Output` types with fail-closed
decoding for malformed, over-bound, truncated, or trailing bytes. Descriptor
methods round-trip the exact input/output types and pack typed input into
canonical EINT v1; EINT `vars` remain codec-owned opaque bytes rather than a
universal canonical-CBOR value. The matched descriptor exposes a borrowed,
provider-generic registry and can bind its generated matcher to one explicitly
identified host mutation implementation. It returns only an opaque,
non-installing package proposal after checking the complete Target IR,
semantic/release bundle, target/generated/operation profile, provider/value
schema, codec, obstruction, operation-id, ABI, helper-API, rule-name, and
footprint identities. Echo adds the mandatory ingress matcher reads to the
host's effect footprint. Identity equality detects cross-binding but does not
prove arbitrary callback semantics. The mutation proposal fails closed for a
`Query`; authored reads remain a separate bounded observer/optic path. The
isolated actual-host fixture is green for binding, typed codec refusal and
round trips, EINT packing, the borrowed registry, and proposal preflight.
The permanently non-authoritative review is bound to the exact generated
artifact. Neither projection authenticates a pin, admits or installs a
package, or grants Echo runtime authority; checked-component promotion and
host-side CDDL admission remain separate crossings.
- 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
Expand All @@ -86,8 +144,8 @@
predicate, input-constraint, require-failure, and Core-value shapes before
separating malformed artifacts from well-formed unsupported semantics, and
one admitted diagnostic-ABI identity now binds both the target profile and
every emitted report. The 189,515-byte checked component has SHA-256
`11fcaf291ffacac62800ab3fc198e29a23a591bcd30ca98828fa10a8ad1f1952`
every emitted report. The 189,922-byte checked component has SHA-256
`4f99c07f1c6d682405945fbb3e36e5537b94c4a01bd1a4ec7f02ef8e9911249a`
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,
Expand Down
2 changes: 2 additions & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

102 changes: 68 additions & 34 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -103,16 +103,40 @@ model.

## How It Works

Echo currently implements two separate halves of the generated-contract path.
Wesley currently emits raw `RewriteRule` builders and generated helpers. Its
integration fixture enables the policy-gated `native_rule_bootstrap` feature
and registers those rules directly. It does not emit an `InstalledContractPackage`
or exercise package verification.

Echo separately verifies and registers `InstalledContractPackage` values,
dispatches registered handlers through the scheduler, and stamps rule-pack
identity into runtime evidence. No current Wesley or Edict generator connects
compiler output to that package path.
Echo currently implements three adjacent generated-contract boundaries. They
do not yet form one end-to-end application path.

The Wesley compatibility path emits raw `RewriteRule` builders and generated
helpers. Its integration fixture enables the policy-gated
`native_rule_bootstrap` feature and registers those rules directly. It does
not emit an `InstalledContractPackage` or exercise package verification.

The Edict provider path admits exact semantic-source, contract-pack, and
settings bytes; emits canonical semantic artifacts; runs a deterministic
lowerer and an independent verifier; and publishes a digest-locked provider
package plus a generated Rust helper projection.
The helper performs pure, fail-closed preflight across exact package, Target
IR, bundle, profile, schema,
codec, obstruction, ABI, helper API, operation, and footprint claims. It
exposes typed `Id`, `Input`, and `Output` codecs, packs typed input into
canonical EINT v1, and builds a provider-generic borrowed registry plus an
opaque, non-installing provider package proposal when explicitly bound to
matching host callbacks. Matching callback claims are cross-binding evidence,
not proof of callback semantics.
The helper does not construct an `InstalledContractPackage`, register or
install anything, invoke callbacks during proposal construction, schedule
execution, or mint runtime authority.

Echo separately verifies and registers host-constructed
`InstalledContractPackage` values, dispatches registered handlers through the
scheduler, and stamps rule-pack identity into runtime evidence.
No generated bridge yet carries either compiler path across Echo's trusted-host
installation boundary into native scheduler execution. The Edict mutation
helper can encode typed input and pack a canonical intent for submission through
a caller-owned Echo ingress; producing those bytes does not confer installation
or execution authority.

The following sequence is the existing Wesley bootstrap fixture:

```mermaid
sequenceDiagram
Expand All @@ -132,13 +156,15 @@ sequenceDiagram
Echo-->>Fixture: OpticReading or typed obstruction
```

The package-shaped flow below is the target corridor, not a current end-to-end application path:
The package-shaped flow below is partially implemented, but is not yet a
current end-to-end application path:

```text
authored Wesley or Edict source
-> verified compiler IR
-> generated handlers, observers, footprints, and package metadata
-> InstalledContractPackage verification
admitted Wesley or Edict source
-> verified mutation Target IR or lawful read semantics
-> generated handlers, observers, codecs, footprints, and package metadata
-> opaque provider proposal with explicit host binding
-> trusted-host InstalledContractPackage admission and registration
-> scheduler-owned execution
-> receipts and readings bound to package identity
```
Expand All @@ -148,19 +174,25 @@ authored Wesley or Edict source
Echo core is intentionally generic. Application nouns belong in authored
contracts and generated adapters, not in the runtime kernel.

- Wesley contract fixtures define nouns, operations, and queries in GraphQL and
use directives such as `@wes_op` and `@wes_footprint` for operation and
footprint claims.
- The current generator emits Rust rule builders and helper code, not a
verified installable package or a supported external application SDK.
- Wesley compatibility fixtures define nouns, operations, and queries in
GraphQL and use directives such as `@wes_op` and `@wes_footprint` for
operation and footprint claims.
- Edict semantic sources define admitted operations, capabilities, lawpacks,
target profiles, and schemas. The Echo provider path deterministically
lowers and verifies that meaning into a digest-locked publication package
and generated helper projection.
- The current Wesley compatibility generator emits Rust rule builders and
helper code, not a verified installable package or a supported external
application SDK.
- Echo's package registry and scheduler path is implemented independently of
that fixture generator.
- A package-qualified compiler must join those halves through the generic
package boundary; it must not create a second execution engine.
both compiler publication paths.
- A trusted Echo host must verify compiler-emitted material, bind the
host-supplied executor or observer, and install it through the generic
package boundary. A compiler must not create a second execution engine.

See [Generated Rule Authorship](docs/topics/GeneratedRules.md) for the exact
current/target boundary, including the fixture-only Edict bridge and the absent
release footprint-qualification lane.
current/target boundary, including the separate Wesley compatibility and Edict
provider paths and the absent release footprint-qualification lane.

```graphql
type Mutation {
Expand Down Expand Up @@ -191,8 +223,8 @@ Echo enforces determinism by narrowing every application action into explicit,
canonical evidence before the scheduler can act on it:

- application input enters as canonical EINT bytes, not ad hoc callbacks;
- Wesley-generated contract metadata names operation ids, codecs, and
footprint claims;
- admitted compiler-generated metadata names operation ids, exact codecs where
declared, and footprint or requirements claims;
- Echo-owned admission decides whether submitted work can become scheduler
work;
- the scheduler drains eligible work in deterministic order under explicit
Expand Down Expand Up @@ -224,7 +256,8 @@ You own:

- domain semantics;
- product policy and UI;
- authored GraphQL contracts;
- authored application contracts, including Edict semantic sources and
supported Wesley GraphQL contracts;
- generated contract helpers and host integrations.

## FAQ
Expand Down Expand Up @@ -400,19 +433,20 @@ for coincidental text.

### How Does Schema Evolution Work?

Contract identity, schema identity, operation ids, and generated helper
identity are explicit in Wesley output. A schema change produces new contract
artifact identity. Old readings name the schema and operation identity they
used, so multiple contract versions can coexist without silently invalidating
old receipts.
Contract identity, schema identity, operation ids, and generated helper or
package identity are explicit in admitted compiler output. A schema change
produces new contract artifact identity. Old readings name the schema and
operation identity they used, so multiple contract versions can coexist
without silently invalidating old receipts.

### Where Should Contributors Start?

Start with `warp-core` and read
[There Is No Graph](docs/architecture/there-is-no-graph.md) before changing
runtime boundaries. Echo core must not grow application nouns such as
`increment_counter`, `save_buffer`, or product-specific APIs. Those belong in
authored Wesley contracts and generated adapters above the runtime boundary.
authored application contracts and generated adapters above the runtime
boundary.

## Quick Start For Contributors

Expand Down
21 changes: 20 additions & 1 deletion crates/echo-edict-canonical/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -187,6 +187,25 @@ pub fn digest_canonical_value_v1(
domain: &str,
value: &CanonicalValueV1,
) -> Result<String, CanonicalValueError> {
Ok(format!(
"sha256:{}",
hex::encode(digest_canonical_value_bytes_v1(domain, value)?)
))
}

/// Computes the typed bytes of an Edict v1 domain-framed SHA-256 digest.
///
/// This is the wire-form counterpart of [`digest_canonical_value_v1`]. The
/// preimage and authority boundary are identical; only the returned rendering
/// differs.
///
/// # Errors
///
/// Returns a stable failure for an empty domain or an unencodable value.
pub fn digest_canonical_value_bytes_v1(
domain: &str,
value: &CanonicalValueV1,
) -> Result<[u8; 32], CanonicalValueError> {
if domain.is_empty() {
return Err(CanonicalValueError::new(
CanonicalValueErrorKind::UnsupportedValue,
Expand All @@ -203,7 +222,7 @@ pub fn digest_canonical_value_v1(
))?);
preimage.extend(encode_canonical_cbor_v1(value)?);

Ok(format!("sha256:{}", hex::encode(Sha256::digest(preimage))))
Ok(Sha256::digest(preimage).into())
}

fn encode_value(
Expand Down
Loading
Loading