diff --git a/CHANGELOG.md b/CHANGELOG.md index 4792d9baf..1a7b59a0f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,54 +5,6 @@ ## Unreleased -### Added - -- Bounded pure evaluation executes compiler-produced U32/U64 addition with - checked width bounds and ordinary work/value-storage charging. Independent - native provider judgments require same-width operands and a dominating - no-overflow proof, including legacy Core without a function table. - -- Experimental feature `application_root_shadow` (M1, off by default): an - incremental application root over every node, edge and attachment record of - a worldline state, kept beside the legacy state root, which it neither - replaces nor changes. It uses the `echo.application-root.radix.v0` - compressed radix trie, advances from each commit's complete write set, and - survives rollback, replay and forks. `WorldlineState::application_root`, - `application_opening` and `verify_application_opening` expose the root and - membership and absence openings. - -### Fixed - -- Completed shadow application-root benchmark rounds are invalid when their - recorded incremental/rebuild or live/replay parity is missing or failed, including - builds without `delta_validate`. - -- F5 benchmark validation rejects observations from a different executed - workload, including runs without a pinned script golden. - -- Stale-basis Action corroboration (#837) reads every slot a retained tick - wrote, not only its declared `out_slots`. Runtime-ingress materialization - writes the event node, its intent attachment and its kind edge outside any - rule footprint; those writes were invisible to the interval check. A tick - that upserts or deletes a warp instance now makes the interval's writes - unknown, so a stale Action across it keeps the whole-frontier rule. - -- Outgoing-edge bucket iterators expose their exact remaining length without - inspecting edges, so bounded readers can precharge the entire source bucket - before filtering by type. - -- The native pure interpreter evaluates bounded UTF-8 byte predicates with - complete aperture charging and typed Boolean values. Native provider judgments - independently validate matching helper/read guards and their bounded scan work. - -- Pure evaluation executes compiler-produced negated input guards, including - authored no-op refusal after checked byte-range predicates, with bounded - decoding, combined traversal and deterministic step accounting. - -- Pure evaluation accepts compiler-produced conjunctive input guards instead of - rejecting their `all` predicate shape as an invalid artifact. Conjunctions - retain deterministic short-circuit metering and combined traversal limits. - ### Removed - The `echo-trace` and `echo-graph` crates. Nothing in the workspace used @@ -81,6 +33,66 @@ combined booleans its caller supplied and checked nothing; the gate list is tracked in #858. +- Removed the provisional caller-authoritative causal-anchor API: + `CausalAnchorRequest`, `CausalAnchorFact::from_request`, public admitted-fact + fields, and raw admitted-identity constructors. Applications now submit a + `CausalAnchorAdmissionRequest` and treat the returned Echo fact, receipt, and + identities as opaque. This is an intentional breaking Rust API correction; + preserving the old surface would let callers manufacture Echo authority. +- Removed the abandoned Method system: its workspace crate and `xtask` + commands, checked-in backlog, cycles, retrospectives, status ledgers, process + manuals, and generated task graphs. Current architecture now lives in + canonical topics/specs/invariants, durable decisions live in ADRs, and live + work/status lives in GitHub. +- Removed the superseded `docs/design/` packet corpus and the retired TTD + counterfactual-creation invariant after promoting current doctrine into + canonical topics, ADRs, architecture documents, specifications, and tests. +- Removed the remaining architecture drift/future packets and dated benchmark + reports after preserving the retained-reading storage and proof boundary in + ADR 0020. Benchmark instructions now keep methodology in source docs and + measurements in generated artifacts and pull requests. +- Deleted zombie crates with no consumers (recoverable from git history): + `echo-wasm-bindings` (browser demo kernel), `echo-ttd`, `ttd-protocol-rs`, + and `echo-session-proto` (the TTD stack now lives with `warp-ttd`), plus + `echo-config-fs` (desktop app-shell fossil) and the + `packages/ttd-protocol-ts` generated consumer. +- Deleted `echo-app-core` (desktop app-shell fossil: toasts, prefs, config + ports) and the `echo-dry-tests` in-memory config fake that existed only to + test its trait; no other crate consumed either. +- Removed the unused `echo-wasm-abi::ttd` module and its public `PrivacyMask`, + `SessionToken`, and `TtdError` exports after the owning TTD/session stack was + retired. This is a breaking Rust API removal for unknown external consumers. +- Deleted `cargo xtask wesley` (existed only to sync the removed TTD + protocol consumer artifacts). +- Deleted stale point-in-time audit reports under `docs/audit/` and + `docs/audits/`. +- Removed the deleted crates from workspace members, CI clippy lanes, + `det-policy.yaml`, `scripts/verify-local.sh`, and the unordered-ABI + allowlist. +- Removed the VitePress docs-site toolchain from active repo tooling: npm + scripts, Make targets, tracked docs-site config, the dead browser-open helper, + and VitePress/Mermaid dependencies are gone. +- Removed the broken `warp-core/serde` feature and the gated `Serializable*` + wrapper exports. `warp-core` no longer declares direct `serde`, `serde-value`, + or `ciborium` dependencies; authoritative core serialization must stay in + explicit canonical boundary encoders rather than general serde derives. +- Removed the legacy `ttd-browser` crate from Echo's active workspace. The + release browser/runtime boundary now stays centered on `warp-wasm` and + `echo-wasm-abi`; debugger session semantics and browser delivery adapters + belong in `warp-ttd`. +- `docs/METHODOLOGY.md` — 5x Duty Model (never practiced; see graveyard). +- 17 unimplemented future spec files (see graveyard). +- `docs/march-16.plan.md` — stale planning scratchpad. +- `docs/plans/parallel-merge-and-footprint-optimizations.md` — superseded + by design review. +- Old plans, book (LaTeX), and research artifacts. All remain recoverable from + Git history. +- **`warp-ffi` crate deleted:** The C ABI integration path (`crates/warp-ffi`) + has been removed. The C ABI approach was abandoned in favor of Rust plugin + extension via `RewriteRule` trait registration and Rhai scripting. See + TASKS-DAG.md #26 (Graveyard). This is a **BREAKING CHANGE** for any + downstream code that depended on the C FFI surface. + ### Changed - Provider semantic declarations now support explicitly bounded Core byte @@ -175,380 +187,354 @@ than cumulative counts for the thread. `recover_filesystem_store` counts nothing. -### Added - -- Outgoing-edge range claims retain source WARP, source node and edge type in - footprint union and scheduler reservation, including observed empty ranges. - Range-bearing operation footprint identities bind both range axes separately; - footprints without ranges keep their V1 identities. Range slots survive patch - identity, retained provenance and native Tick input/output metadata. Historical - host range readings replay a selected prefix and preserve edge relabeling, - movement and deletion. This does not implement the authored operation effect - bridge. - -- Native Edict provider judgments accept the distinct bounded source-closure - artifact, preserve its identity and refuse mixed or relabelled source forms. - An explicit generation variant carries its owning schema binding; generic - bounded-read decoding rechecks the source domain and every retained unit. - -- Explicit Edict source-module contract publication admission pins the exact - upstream CDDL/manifest pair and validates its source-closure envelope without - changing existing publication selections or enabling executable module support. +- `ExecItem` constructors require an explicit canonical evidence sequence. + Manually assembled work units no longer silently reuse a per-rule match + index as the execution sequence. Engine callers pass the existing batch-wide + enumeration directly, preserving scheduler order. -- Bounded pure Edict evaluation accepts compiler-produced byte constants with - raw octets and ordinary deterministic value-copy charges. Closed shape checks - reject text payloads and extra fields. A retained public compiler package and - separate accepted report exercise literal output and evaluation budgets. -- Causal intents get an identity recipe that a plain intent cannot alias - (#885). Under the original recipe a plain intent could reproduce a causal - intent's hash input exactly and take its ingress and submission IDs. New - causal intents are identified by `"echo.ingress.causal.v3\0" || ...`, record - `IngressIdentityVersion::SeparatedCausal`, and are retained as `EINGR004`. - `EINGR001` to `EINGR003` decode exactly as before, as `Original`. A resend of - a causal request accepted before this change resolves to its original - submission when its retained envelope states the same request, and is staged - with that envelope; an alias is not a match. Missing legacy material is - `OriginalIngressIdentityUnverifiable`, a request with both identities is - `IngressIdentityAmbiguous`, and new admission in the original causal recipe - is `OriginalCausalIdentityNotAdmissible`. -- A strand inherits the Continuum occurrences decided in its causal past - (#886). Redelivering such an occurrence to the strand returns - `AlreadyPresentInInheritedHistory` (from `submit_intent` and `ingest`) - naming the original submission, its head, the fork basis and its receipt - when ticketed; nothing is admitted and no acceptance is written. - `IntentSubmissionHandle` reports it as a duplicate with `inherited_through` - set. Reusing an inherited occurrence key for other material is an - occurrence conflict. Occurrences undecided at the fork basis, or decided - after it, are not inherited. Nested forks and restart preserve this. -- Restoring committed history without the witnessed submissions it accounts - for no longer reopens admission (#887). `restore_causal_runtime_history` - keeps the restored worldline readable, but `submit_intent`, `ingest` and - ticketed staging fail with `RuntimeError::AdmissionCoverageUnestablished` - until the trusted host attests, after WAL recovery, that the witnessed - submissions and receipt correlations it restored are its complete acceptance - and decision logs. The attestation releases a worldline only when every - submission its ticks attribute has retained material, and it covers only the - restores made before it; final graph state is never treated as evidence of - a decision. Before this, a runtime rebuilt from history alone accepted a resent - request as a new one, and `ingest` could re-queue a request an unticketed - tick had already decided. Normal host recovery is unaffected. -- Echo preserves Continuum occurrence identity at admission (#880). - `IngressEnvelope::continuum_occurred_intent` binds an intent to a - `ContinuumOccurrence` (Continuum's occurrence key and applied digests), and - the occurrence key is hashed into the ingress ID. Two occurrences of - identical content are two submissions with their own decisions and - attribution; redelivering an occurrence returns its existing submission; and - reusing an occurrence key for other content, applied intent or writer head on - the same worldline is refused with - `RuntimeError::ContinuumOccurrenceConflict`. All three hold after restart: - such envelopes are retained as `EINGR003` and the mapping is rebuilt from - them. Local submission identity is unchanged, and envelopes without an - occurrence are still retained as `EINGR002`. - Restoring retained material that changes a submission's occurrence is - refused and changes nothing. After record-only replay, which restores - submissions without envelopes, occurrence admission on that worldline fails - with `RuntimeError::ContinuumOccurrenceCoverageUnavailable` until the - envelopes are restored. `ContinuumOccurrence::from_occurred_digests` checks - that an `occurredDigest` binds its occurrence key and applied digest; it - does not authenticate the issuer or check the applied digest against the - intent bytes. -- Every new scheduler tick commits an attribution section in its tick - receipt: one record per accepted submission the tick decided, naming the - receipt entries that carry its decision, or recording that no rule matched - it. Plain ticks and Action ticks seal it from their own batch, and refuse to - commit when a decision and the receipt disagree; a direct host commit, which - decides no submission, records an empty section. Every new tick's receipt is - also commit-bound: receipt format 4, retained as `EPRV0003` (see the commit - hash v3 entry). Receipts attributed before commit binding (format 3, - `EPRV0002`) and receipts without a section (format 2, `EPRV0001`) are read - byte for byte, so existing history replays unchanged and a legacy history can - be extended by attributed ticks (#873). -- `warp-core` trusted applications can now traverse bounded causal receipt - history at an explicit worldline frontier in either canonical direction - (#660). Echo-issued continuation cursors bind worldline, basis, direction, the - next tick and the last submission returned within it; each entry includes witnessed submission identity, - contract evidence, canonical parent receipts, and any typed inverse - derivation. Filesystem recovery returns identical pages without a - process-local history authority, while missing, duplicate, or inconsistent - retained evidence produces typed obstructions instead of truncated history. -- `submit_bound_echo_operation_request_v1` submits the Action bound to a - logical request and durably links the request to that submission; - `echo_operation_request_outcome_v1` returns the linked submission and its - recorded outcome, live and after reopening (#854, R1). The link is retained - after durable acceptance; a retry after a failure between the two completes - it, and a second submission of one request to another head is refused. +- Echo and Edict share exact `bunny-num` 0.6.0 for the canonical signed Q32.32 + foundation. `warp-math` exposes Bunny's checked type and delegates existing + `DFix64` arithmetic and motion conversions while preserving saturation, + ties-to-even, raw payload bytes, and the separate legacy ABI truncation policy. + This does not add fixed-point language syntax or runtime operation profiles. +- The general Rust toolchain and numerical consumer MSRVs are 1.96.0. Independent + leaves and authenticated provider component producers retain their explicit + 1.90.0 policy; the outer component driver uses 1.96.0. The MSRV guard also + validates a final policy row without a newline and reads package MSRVs only + from `[package]`, excluding metadata. The standalone host witness selects + Rust 1.96.0 locally, and the guard rejects a missing or stale nested pin. -- `ActualFootprint` records the graph resources an execution actually touched - and compares them against a declared `Footprint`, returning the existing - `ViolationKind` vocabulary in a deterministic axis order. Footprint - enforcement previously answered "was this access declared?" and forgot, so - the soundness relation `Actual ⊆ Declared` could only be observed as a panic - and never evaluated as a value. `ActualFootprint::from_ops` derives the write - axis from an emitted op sequence using the same extraction as enforcement, so - a recorded write set and an enforced write check cannot disagree. Cross-warp - and instance-level concerns are deliberately excluded: they are scope and - authority questions the guard already reports, not footprint-subset - questions. The read axis is recorded as accesses happen through - `ExecutionGraphView`; it cannot be reconstructed from emitted ops. -- `ExecutionGraphView` is the executor-only capability that records what an - execution actually read. `GraphView` could not grow a recorder: its accessors - take `&self`, so mutating a borrowed accumulator would need interior - mutability, which its contract forbids and which would cost it `Sync` — and - `WorkUnit: Sync` is required for workers to borrow the shared unit slice. - Moving the mutable execution frame rather than the declared guard into - exclusive worker ownership makes `&mut self` sufficient, so no lock, no - `UnsafeCell`, and no manual `Sync` are involved, and `GraphView` and - `WorkUnit` are untouched. Accessors record before consulting the guard, so - the access that trips enforcement is already in the transcript when the panic - unwinds; recording afterwards would retain an actual footprint missing its own - counterexample. The recorded axis mirrors enforcement exactly — `edges_from` - records a node read, because declaring a node grants its outbound adjacency — - and an absent resource is still a recorded coordinate, so a rule cannot probe - undeclared coordinates for free by picking empty ones. -- `ActualFootprintPosture` states what a footprint record is entitled to claim. - An empty violation set means "the declaration covered the execution" only when - the lane both recorded and enforced; from an unobserved lane it means only - that nothing was compared. `read_axis_is_complete` keeps that difference - legible, so an empty read axis from an unobserved lane reads as _unknown_ - rather than as _this execution read nothing_, and only `RecordedAndEnforced` - may ground an admitted falsification witness. `build_footprint_posture` caps - every lane by the enforcement the binary actually compiled. -- `ObservedExecuteFn` and `RuleExecutor` route native scheduler execution through - one worker-local evidence core. Native and generated contract-host executors - receive `ExecutionGraphView`; the frozen provider-v1 callback remains an - explicit legacy `GraphView` ABI and can never manufacture a complete read - axis. `ExecutionFootprintEvidence` retains one canonical record per executed - Action on `Engine` and `WorldlineState`, including the emitted write set when - the executor or read guard unwinds. Records are keyed before worker dispatch - and sorted independently of worker claim or completion order. Successful, - panicking, legacy, generated-consumer, provider-v1, and worker-count-invariant - witnesses complete stage 2 of the falsification roadmap without exporting - `FootprintGuard` or weakening its ordinary panic path. -- Differential tests run the recorded write set and the enforced write check - against the same ops and the same declaration, closing an assumption the - design had only asserted. They also pin the two deliberate disagreements: - cross-warp emission and unauthorized instance ops are scope and authority - failures that the recorder declines to report as footprint-subset failures, - so a reducer cannot hop between bug classes by conflating them. - -- `submit_intents_with_runtime_wal_ack` accepts several intents and returns after one storage sync has made all of their acceptance transactions durable. Each intent writes the same acceptance transaction as a single submission, so recovery is unchanged. No acceptance of a batch counts as durable, or can be scheduled, before that sync succeeds. A failed batch acknowledges nothing. If the runtime refuses an intent before anything is written for it, the intents before it stay accepted and are synced. If an append or the sync fails, the call's intake is rolled back and the WAL refuses further work with `StorageFailed` until it is reopened. - -- `SlotWriteIndex` resolves the value of one node, edge or attachment slot at a tick cursor from tick patches and the initial boundary, without materializing a graph or replaying unrelated ticks. It indexes the operations that wrote each slot, including values cleared by node, edge and instance deletion, and truncates in proportion to the ticks removed. A reader is bound to the exact patches the index was built from by patch digest, and truncation refuses patches that are not the indexed suffix. It is a derived reading aid; the runtime does not use it yet. - -- Native projected compare-and-set invocation encoding retains canonical application input and statically binds the expected attachment-value digest. The native lowerer and the structurally separate verifier reconstruct CAS-specific profiles and reject rebound digest paths or under-budget configurations. Generated schema, reproducible components and a retained public Edict compiler build establish package production. The retained compiler package now has scheduler execution, pending/committed Action recovery, stale-digest noncommit recovery and typed refusal witnesses. `EchoOperationInvocationV1::anchored_node_attachment_compare_and_set_with_application_input` and `ExecutableOperationPackageV1::with_compare_and_set_application_result_projection` construct the projected forms without byte editing. - -- The trusted executable-operation host can retain two native alternative strands, - continue a losing strand under new observations, and recover its fork ancestry - and operation outcomes from the WAL. Application selection records do not - imply merge or promotion. - -- Bounded executable-operation host sessions retain immutable observations and - logical-request bindings in the native WAL. Echo evaluates supplied node/atom - preconditions inside operation preparation, includes their reads in scheduler - footprints, and retains typed refusal or commitment outcomes across reopening. - The generic `run-edict-operation --serve` driver supports repeated operations, - historical outcome lookup, and derived observation-change discovery. - -- An opt-in create-operation configuration v2 derives Unicode scalar key bounds in both provider components and binds them into packages. Runtime admission enforces nonempty keys and separate scalar/UTF-8 byte ceilings; legacy configuration v1 is unchanged. - -- A disabled-by-default experimental Keep ReferenceStore adapter implements the complete-object CAS port with explicit limits, private bindings, sanitized backend errors and atomic output promotion. It preserves existing CAS defaults and claims no restart durability. - -- An isolated experimental Echo–Keep identity bridge checks both independent hash laws and exact byte length from one bounded stream. It leaves the default CAS dependency graph unchanged. - -- A fallible complete-object CAS port stages and verifies exact bytes before atomic destination promotion. Memory and disk adapters share conformance checks; existing APIs remain compatible and no durability or authenticated absence is claimed. - -### Fixed - -- `dispatch_intent` no longer stages a witnessed suffix import against the - kernel's default worldline (#892). It ignored the request's receiving - worldline and recorded `Staged` without the bundle and basis checks the - library performs. Until comparable-basis transport exists, import intents - are refused with `NOT_SUPPORTED` and nothing is admitted, staged or - attributed. - -- A tick that decides a submission no rule matched now commits and recovers - under the WAL (#873). The WAL tick decision gains `NoMatchingRule` (code 4), - recovery maps it to `RecoveredSubmissionPosture::DecidedNoMatchingRule`, and - a retry reports `SubmissionRetryPosture::AlreadyDecidedNoMatchingRule`. - Before, such a tick failed with `TickOutcomeUnavailable` and could not be - recorded at all. Older WALs never contain the code. -- `Footprint::independent` no longer treats an unpopulated `factor_mask` as - partition evidence. The mask fast path now applies only when both masks are - non-zero; a zero placeholder on either side falls through to the node, edge, - attachment, and port set checks. Previously two zero-mask footprints with - conflicting writes compared as independent. Nothing in the engine calls it - today (the scheduler never consults the mask), but it is public API. A - union of footprints (`union_assign`) also stays unpopulated when either side - with claims is unpopulated, so a composite cannot look fully masked. -- A tick with the in-memory WAL no longer costs time in proportion to the - whole log. The host copied the in-memory log, its catalog and its indexes - before every tick so it could undo a failed one; at 8,000 updates a tick - took 13.5 ms. It now marks the log's end and, only if a tick fails, - truncates back to the mark and rebuilds what is derived from the log. In - `wal_record_cost` the in-memory update now costs about 0.22 ms at 500 and at - 8,000 updates of history. - -- A commit record whose storage sync failed is no longer acknowledged. The - record can be readable without being durable; a trusted host used to - re-read the log after the error and treat what it found as committed, for - submissions, scheduler ticks, causal anchors, operation installations and - operation ticks. The filesystem store now refuses further writes after any - failure while a commit record is written or synced, and the host takes the - work back and refuses further WAL work with `StorageFailed` until the WAL - is reopened, as batched submission already did. An error that arrives after - a successful sync is still reconciled from the log. - -- A trusted host takes the filesystem WAL writer lease before it runs - writable recovery. It used to recover first and take the lease afterwards, - so a second host that opened a log with a live writer could drop that - writer's in-progress tail by rewriting its segment files, and only then be - refused. The second host is now refused at the lease and modifies nothing. - -- The canonical CBOR decoder in `echo-wasm-abi` no longer reserves memory in - proportion to a length its input claims, and no longer recurses without - bound. A header that claims more array elements, map entries or string - bytes than the input has left is refused with `Incomplete`, and the - comparison is made before the length is narrowed, so 32-bit and 64-bit - targets refuse the same inputs. A container reserves at most a few slots - before its elements are decoded, so nested headers cannot multiply the - memory a request asks for. Nesting deeper than - `MAX_CANONICAL_NESTING_DEPTH` (128) is refused, by the encoder as well, so - bytes it returns always decode. Before, a nine-byte request could abort the - process. - -- Writable WAL recovery no longer removes committed records in order to drop - an uncommitted tail. It rebuilt the whole log by deleting every segment - file and re-appending what it kept, so a crash in between lost all - committed history; it also synced the WAL root instead of the directory - that holds the segments, and collapsed rotated segments into the first. - Each segment that loses records is now rebuilt in a scratch file and - swapped in by one rename, a segment with nothing to drop is not touched, - an emptied trailing segment is removed, and the containing directory is - synced. A crash at any step leaves the same committed history. - -- A worldline frontier retains the state root computed by its last executable-operation Action commit and returns it without hashing until the graph is next accessed mutably. An Action tick after the first now hashes the whole reachable state once instead of twice. Debug builds hash again to check each retained root, so they do not get the saving. The graph field of `WorldlineState` is private to its module so that every mutation goes through the accessor that drops the retained root. - -- A filesystem WAL writer that takes over an existing log syncs its segment files before reading them as recovered history. A record that an earlier writer wrote and never synced was readable after reopen and was reported as a durable acceptance; a later power loss could still lose it. - -- A scheduler pass that commits executable-operation Actions hashes the worldline's whole reachable state twice instead of three times. The root before the commit is the root the pass already computed for the frontier basis; the commit no longer computes it again. - -- A scheduler pass resolves a writer head's frontier basis once instead of once per admitted executable-operation Action. Resolving it hashes the whole reachable state, so a tick's cost grew with Actions times graph size. The bases produced are unchanged. - -- A scheduler pass builds and digests its retained WAL state delta once per commit instead of once per admitted Action. The WAL bytes are unchanged. - -- A scheduler pass that commits executable-operation Actions no longer copies the worldline's graph. The commit wrote its patch to a copy of the graph and then replaced the original, and the pass's rollback marker held a second copy. The patch is now written in place and each replaced value is journaled before its write; rollback restores from the journal. This applies to patches of node upserts and non-portal attachment writes. A patch that changes graph structure, and a pass that runs native rules through the engine, still retains one copy. Debug builds keep a copy to check the journal. - -- A worldline's initial boundary is shared instead of copied. It never changes after construction, but every scheduler rollback marker, replay checkpoint and replay base cloned the whole graph it holds. Tick cost on a large graph drops by roughly a fifth; the remaining graph-proportional copies are the live state itself. - -- Scheduler rollback checkpoints no longer copy a worldline's committed tick history or committed-ingress ledger on every SuperTick. A checkpoint records the history length and the attempt journals the ingress ids it adds; rollback truncates and removes them. The trusted host no longer clones the runtime, provenance and retained Action outcomes before every tick, or the runtime before every WAL-acknowledged submission: a completed scheduler pass returns an undo handle, and Action staging and submissions are journaled. Rollback results are unchanged; tick and submission cost no longer grow with committed history. - -- A strict filesystem WAL commit no longer rewrites and syncs the writer-epoch ledger and its directory after syncing the commit record. The commit record remains the durability boundary; reopening already derives each epoch's final commit from the segment. Each transaction now forces one sync instead of three. The on-disk formats are unchanged. - -- Package admission rejects result projections whose expected-digest binding conflicts with the selected mutation program, before they can occupy an installed operation coordinate. Recovery applies the same rule to retained installations: a WAL that holds such a hand-built package is refused rather than reinstalled. Echo's providers never emitted that shape, and no invocation of it could be admitted. Admission likewise refuses an expected-digest path that is empty or overlaps the key or replacement path. - -- Both executable mutation providers refuse transformed effect arguments instead of silently projecting the caller input into a different mutation. Direct application-input arguments remain supported; the structurally separate verifier enforces the same boundary. - -- Retained local fork retries reconcile durable topology after uncertain appends, preserving the original basis and preventing duplicate fork records. - -- Observation slots preflight their canonical byte bound and charge execution reads before copying Atom payloads. - -- Private Edict runtime decoding resolves named integer types through their declared width, matching source-function provider acceptance. - -- Filesystem writer takeover preserves unused LSNs after empty epochs and refuses unreconciled tails before changing the epoch ledger. - -- Incremental snapshot state roots now include the existing v1 domain separator and agree with canonical snapshot hashing. Previously emitted incorrect accumulator roots are not migrated. - -- The SPDX checker preserves Markdown frontmatter when it checks or repairs license headers. - -- Action WAL recovery reuses ordered verified replay cursors instead of retaining a full state for each basis tick. It preserves basis, Tick, result, obstruction and conflict checks, including delayed stale bases. - -- The generic operation runner names typed obstruction kinds, footprint conflicts, and missing outcomes in bounded summaries. It omits raw outcome records and invocation data on both Action error paths. - -- `xtask run-edict-operation` runs outside Git and resolves relative artifact and WAL paths from the caller directory. Repository maintenance commands retain their Git-root behavior. - -- `WorldlineState::state_root` documentation now states its reachable-state boundary. Detached create-if-absent writes remain bound by patch and commit identities. Hash bytes are unchanged. +- Public installed-contract evidence fields on runtime ingress, receipt + correlation, outcome, and WAL state-delta carriers now use + `Option` instead of + `Option`. This is an intentional pre-1.0 source + compatibility change: legacy callers wrap with `LegacyContract` or `.into()` + and inspect with `legacy_contract()`, while provider callers inspect + `provider_v1()`. The enum is non-exhaustive to match the extensible wire-tag + family, so direct downstream matches require a wildcard arm. The legacy tag-1 + WAL encoding remains byte-identical. +- The public `RuntimeError` enum now includes + `InstalledContractIntentKindMismatch` and + `UnsupportedInstalledProviderContractMutation`, and the public + `ContractInverseObstruction` enum now includes `ProviderTargetUnsupported`. + These are intentional pre-1.0 source-compatibility additions: downstream + exhaustive matches must handle the new variants (or use an appropriate + wildcard arm). +- `echo-wesley-gen` now follows Wesley's operation-neutral adapter names: + `import_runtime_optic_artifact(...)` accepts `OperationArtifact`, and + `import_registration_descriptor(...)` accepts + `OperationRegistrationDescriptor`. Source consumers using Wesley's former + `OpticArtifact` or `OpticRegistrationDescriptor` names must update when they + adopt the corresponding Wesley 0.3 prerelease; Echo's runtime-local optic + artifact types and handles are unchanged. +- Provider semantic-source, generation-input, and contract-pack `Display` + diagnostics now render explicit kebab-case failure labels instead of Rust + `Debug` variant spellings. Typed error enums remain the programmatic + contract, while human/CLI diagnostics no longer move when Rust variants are + refactored. +- Restored the durable ADR 0001–0011 namespace and moved the post-Method + decisions to ADR 0012–0019, preserving the meaning of existing source + citations. CI now rejects missing, duplicate, non-contiguous, unindexed, or + collided ADR identifiers. +- Recorded the WSC, CAS, semantic reading identity, and optional proof boundary + as ADR 0020 without carrying forward the source packet's implementation + roadmap or application-specific checkpoint design. +- Replaced the opaque numeric determinism claim-pack generator with an honest + gate over upstream job results and exact artifact payload presence. The + executable suites remain the authority for what passed. +- Replaced the frozen root architecture and advanced guides with explicit + supersession signposts to the living no-graph architecture, topics, + specifications, invariants, and ADRs. +- Echo 1.0 release eligibility now depends only on Continuum participant + conformance, networked causal suffix exchange, and release integrity. Edict, + `jedit`, and any particular generated package remain downstream compatibility + work and no longer gate the Echo release. +- Echo 1.0 planning references now point at the cross-repository Continuum + Stack Convergence Project instead of the retired Echo-only Project. +- Local `scripts/verify-local.sh full` now treats broad Cargo test lanes as + GitHub Actions-owned by default, while keeping a maintainer opt-in through + `VERIFY_LOCAL_FULL_TESTS=1` for intentional local full-suite runs. +- `warp-core` renamed the generated contract package host API from + `install_contract_package(...)` to `register_contract_package(...)` so the + trusted-runtime boundary reads as explicit runtime-owned registration instead + of process-global installation. +- `warp-core` sealed braid member lookup now requires authority-bound sealed + query material, redacts non-public blinding material from debug output, and + keeps hidden-member commitments stable across parent frontier movement. +- `warp-core` settlement planning now rejects non-`Shared` strands before + producing import candidates. Author-only/debugger strand suffixes can remain + real causal work, but they cannot enter base shared history without an + explicit shared admission posture. Settlement compare remains local + revelation/inspection only: it can inspect a locally held strand suffix + without promoting, planning, admitting, or settling it. +- `warp-core` settlement plural artifacts and retained braid shells now carry + the source strand posture instead of hard-coding author-only posture for + shared settlement records. +- Local determinism tooling now fails closed around + `scripts/check-warp-core-serialization-boundaries.sh`. The serialization + boundary guard is mandatory, runs through `bash` rather than executable mode, + works without `rg`, rejects table-form serde/ciborium dependencies, and + blocks direct, grouped, multiline, or aliased canonical ABI serialization + imports outside explicit `warp-core` boundary modules. +- The nondeterminism guard now shares the same `rg`/Perl fallback scanner, + supports `DETERMINISM_FORCE_NO_RG=1` regression coverage, catches namespace + imports and alias calls for `std::env`, `std::fs`, and `std::process`, bans + `std::thread::available_parallelism`, and replaces file-wide allowlists with + rule-scoped waivers for build/native filesystem boundaries and test fixtures. +- `warp-core` engine and scheduler state now use ordered `BTreeMap`/`BTreeSet` + storage instead of `HashMap`, `HashSet`, or `FxHashMap` in deterministic core + paths. WAL filesystem tests also recreate stale deterministic fixture roots + before use so previous local residue cannot change the test outcome. +- `warp-core` engine construction now defaults to deterministic serial + execution instead of reading `ECHO_WORKERS` or host CPU availability. Callers + can still opt into parallel execution explicitly with + `EngineBuilder::workers(...)` or worker-count constructors. +- `echo-cli wal submission-posture` now exposes generic read-only recovery JSON + for one submission id and canonical envelope digest. The output reports retry + posture, recovered submission posture, receipt digest, and ticket digest + without importing any application nouns into Echo. +- Runtime WAL-backed scheduler ticks now roll back all tick WAL evidence from a + failed multi-head scheduler pass, treat missing or mismatched receipt + correlation evidence as an invariant error instead of a normal obstruction, + and bind runtime recovery certificates to rebuilt submission and receipt + indexes. +- `warp-wasm` no longer contains the legacy Stack Witness 0001 + `createBuffer`/`replaceRange`/`textWindow` shortcut. QueryView requests now + route through the generic installed contract observer boundary only; without + an installed observer, WASM `observe(...)` returns `UNSUPPORTED_QUERY` + instead of materializing hardcoded text bytes. +- `warp-core` structured binding tests no longer use rope/text-shaped fixture + names. The executable examples now exercise generic authored scopes, heads, + segments, and markers so core test fixtures do not imply built-in editor + semantics. +- The canonical pre-push hook now runs the narrowest changed-file Rust witness + instead of reusing the broader local PR gate. Rust module edits map to exact + `cargo test -p --lib ::tests` slices, integration-test edits + map to exact `--test ` invocations, and tooling edits stay on local + shell smoke checks. Broader clippy, rustdoc, package, and workspace coverage + remains available through `make verify-pr`, `make verify-full`, and CI. The + selector now avoids fake zero-test module filters for source files without + inline tests, maps `src/bin/*.rs` edits to exact binary targets, and preserves + required features for gated integration tests. +- Deterministic math now lives in a slim `warp-math` workspace crate. + `warp-core` keeps the existing `warp_core::math::*` compatibility surface as + a re-export, while `warp-geom` depends directly on `warp-math` instead of + pulling in all of `warp-core`. Math-only integration tests, deterministic + trig golden vectors, PRNG golden regression, and the LUT generator moved with + the math crate. +- CI and local verification now split broad clippy coverage into explicit + library, binary, and selected integration-test lanes instead of invoking one + monolithic cargo pass. The `warp-core` runtime inbox test target is now an + explicit lint lane with the same `native_rule_bootstrap,host_test` features + used by the ticketed-ingress regression suite. +- Local verification now treats rustdoc warnings as CI-owned by default. + `scripts/verify-local.sh` skips local rustdoc lanes unless + `VERIFY_LOCAL_RUSTDOC=1` is set, keeping pre-push and full local gates focused + on faster edit-loop witnesses while preserving CI rustdoc coverage. +- Tooling-only full verification now selects focused hook regression scripts by + changed file family, so a `scripts/verify-local.sh` edit runs the verify-local + hook regression without also running unrelated runtime-schema, PR-status, or + timing hook tests. +- Local hook regression tests are now CI-owned by default. The local full gate + skips hook tests unless `VERIFY_LOCAL_HOOK_TESTS=1` is set, and the opt-in + hook-test lane clears verifier override variables before launching nested + hook regressions. -- `ReadView::at` validates the aperture and derives the selected current frontier - basis with one state hash. `ReadView::new` still checks an independently - selected expected basis. Both retain the same aperture and trust boundaries. +### Added -- Public bounded-read compiler timeouts retain partial stdout/stderr and the - original timeout as the failure cause. +- Bounded pure evaluation executes compiler-produced U32/U64 addition with + checked width bounds and ordinary work/value-storage charging. Independent + native provider judgments require same-width operands and a dominating + no-overflow proof, including legacy Core without a function table. -- Bounded-read lowering recognizes only the exact unsigned primitive coordinates. - Named structural types starting with `U` now reach ordinary type lookup, as - they already do in independent verification and runtime parsing. +- Experimental feature `application_root_shadow` (M1, off by default): an + incremental application root over every node, edge and attachment record of + a worldline state, kept beside the legacy state root, which it neither + replaces nor changes. It uses the `echo.application-root.radix.v0` + compressed radix trie, advances from each commit's complete write set, and + survives rollback, replay and forks. `WorldlineState::application_root`, + `application_opening` and `verify_application_opening` expose the root and + membership and absence openings. -- Private read evaluation identifies the input by its verified `arg.0` identity. - Reordering a package's local declarations no longer changes input selection. +- Outgoing-edge range claims retain source WARP, source node and edge type in + footprint union and scheduler reservation, including observed empty ranges. + Range-bearing operation footprint identities bind both range axes separately; + footprints without ranges keep their V1 identities. Range slots survive patch + identity, retained provenance and native Tick input/output metadata. Historical + host range readings replay a selected prefix and preserve edge relabeling, + movement and deletion. This does not implement the authored operation effect + bridge. -- Read-provider lawpack validation remains separate from the pure profile's - empty-effect requirement, preserving read acceptance and pure-effect refusal - after integration of the strengthened pure-provider checks. +- Native Edict provider judgments accept the distinct bounded source-closure + artifact, preserve its identity and refuse mixed or relabelled source forms. + An explicit generation variant carries its owning schema binding; generic + bounded-read decoding rechecks the source domain and every retained unit. -- The bounded-read public compiler witness preserves return status and raw - streams when malformed or non-object JSONL prevents structured validation. +- Explicit Edict source-module contract publication admission pins the exact + upstream CDDL/manifest pair and validates its source-closure envelope without + changing existing publication selections or enabling executable module support. -- Bounded-read evaluator tests now require `trusted_runtime` in Cargo and run - in feature-enabled CI and opt-in local routes, including shared parser edits. +- Bounded pure Edict evaluation accepts compiler-produced byte constants with + raw octets and ordinary deterministic value-copy charges. Closed shape checks + reject text payloads and extra fields. A retained public compiler package and + separate accepted report exercise literal output and evaluation budgets. +- Causal intents get an identity recipe that a plain intent cannot alias + (#885). Under the original recipe a plain intent could reproduce a causal + intent's hash input exactly and take its ingress and submission IDs. New + causal intents are identified by `"echo.ingress.causal.v3\0" || ...`, record + `IngressIdentityVersion::SeparatedCausal`, and are retained as `EINGR004`. + `EINGR001` to `EINGR003` decode exactly as before, as `Original`. A resend of + a causal request accepted before this change resolves to its original + submission when its retained envelope states the same request, and is staged + with that envelope; an alias is not a match. Missing legacy material is + `OriginalIngressIdentityUnverifiable`, a request with both identities is + `IngressIdentityAmbiguous`, and new admission in the original causal recipe + is `OriginalCausalIdentityNotAdmissible`. +- A strand inherits the Continuum occurrences decided in its causal past + (#886). Redelivering such an occurrence to the strand returns + `AlreadyPresentInInheritedHistory` (from `submit_intent` and `ingest`) + naming the original submission, its head, the fork basis and its receipt + when ticketed; nothing is admitted and no acceptance is written. + `IntentSubmissionHandle` reports it as a duplicate with `inherited_through` + set. Reusing an inherited occurrence key for other material is an + occurrence conflict. Occurrences undecided at the fork basis, or decided + after it, are not inherited. Nested forks and restart preserve this. +- Restoring committed history without the witnessed submissions it accounts + for no longer reopens admission (#887). `restore_causal_runtime_history` + keeps the restored worldline readable, but `submit_intent`, `ingest` and + ticketed staging fail with `RuntimeError::AdmissionCoverageUnestablished` + until the trusted host attests, after WAL recovery, that the witnessed + submissions and receipt correlations it restored are its complete acceptance + and decision logs. The attestation releases a worldline only when every + submission its ticks attribute has retained material, and it covers only the + restores made before it; final graph state is never treated as evidence of + a decision. Before this, a runtime rebuilt from history alone accepted a resent + request as a new one, and `ingest` could re-queue a request an unticketed + tick had already decided. Normal host recovery is unaffected. +- Echo preserves Continuum occurrence identity at admission (#880). + `IngressEnvelope::continuum_occurred_intent` binds an intent to a + `ContinuumOccurrence` (Continuum's occurrence key and applied digests), and + the occurrence key is hashed into the ingress ID. Two occurrences of + identical content are two submissions with their own decisions and + attribution; redelivering an occurrence returns its existing submission; and + reusing an occurrence key for other content, applied intent or writer head on + the same worldline is refused with + `RuntimeError::ContinuumOccurrenceConflict`. All three hold after restart: + such envelopes are retained as `EINGR003` and the mapping is rebuilt from + them. Local submission identity is unchanged, and envelopes without an + occurrence are still retained as `EINGR002`. + Restoring retained material that changes a submission's occurrence is + refused and changes nothing. After record-only replay, which restores + submissions without envelopes, occurrence admission on that worldline fails + with `RuntimeError::ContinuumOccurrenceCoverageUnavailable` until the + envelopes are restored. `ContinuumOccurrence::from_occurred_digests` checks + that an `occurredDigest` binds its occurrence key and applied digest; it + does not authenticate the issuer or check the applied digest against the + intent bytes. +- Every new scheduler tick commits an attribution section in its tick + receipt: one record per accepted submission the tick decided, naming the + receipt entries that carry its decision, or recording that no rule matched + it. Plain ticks and Action ticks seal it from their own batch, and refuse to + commit when a decision and the receipt disagree; a direct host commit, which + decides no submission, records an empty section. Every new tick's receipt is + also commit-bound: receipt format 4, retained as `EPRV0003` (see the commit + hash v3 entry). Receipts attributed before commit binding (format 3, + `EPRV0002`) and receipts without a section (format 2, `EPRV0001`) are read + byte for byte, so existing history replays unchanged and a legacy history can + be extended by attributed ticks (#873). +- `warp-core` trusted applications can now traverse bounded causal receipt + history at an explicit worldline frontier in either canonical direction + (#660). Echo-issued continuation cursors bind worldline, basis, direction, the + next tick and the last submission returned within it; each entry includes witnessed submission identity, + contract evidence, canonical parent receipts, and any typed inverse + derivation. Filesystem recovery returns identical pages without a + process-local history authority, while missing, duplicate, or inconsistent + retained evidence produces typed obstructions instead of truncated history. +- `submit_bound_echo_operation_request_v1` submits the Action bound to a + logical request and durably links the request to that submission; + `echo_operation_request_outcome_v1` returns the linked submission and its + recorded outcome, live and after reopening (#854, R1). The link is retained + after durable acceptance; a retry after a failure between the two completes + it, and a second submission of one request to another head is refused. -- Removed the bounded-read witness's unguarded image/entrypoint recipe. Public - compiler and fresh-output runtime witnesses require a continuously guarded - reusable worker; pre/post measurements alone are not budget enforcement. +- `ActualFootprint` records the graph resources an execution actually touched + and compares them against a declared `Footprint`, returning the existing + `ViolationKind` vocabulary in a deterministic axis order. Footprint + enforcement previously answered "was this access declared?" and forgot, so + the soundness relation `Actual ⊆ Declared` could only be observed as a panic + and never evaluated as a value. `ActualFootprint::from_ops` derives the write + axis from an emitted op sequence using the same extraction as enforcement, so + a recorded write set and an enforced write check cannot disagree. Cross-warp + and instance-level concerns are deliberately excluded: they are scope and + authority questions the guard already reports, not footprint-subset + questions. The read axis is recorded as accesses happen through + `ExecutionGraphView`; it cannot be reconstructed from emitted ops. +- `ExecutionGraphView` is the executor-only capability that records what an + execution actually read. `GraphView` could not grow a recorder: its accessors + take `&self`, so mutating a borrowed accumulator would need interior + mutability, which its contract forbids and which would cost it `Sync` — and + `WorkUnit: Sync` is required for workers to borrow the shared unit slice. + Moving the mutable execution frame rather than the declared guard into + exclusive worker ownership makes `&mut self` sufficient, so no lock, no + `UnsafeCell`, and no manual `Sync` are involved, and `GraphView` and + `WorkUnit` are untouched. Accessors record before consulting the guard, so + the access that trips enforcement is already in the transcript when the panic + unwinds; recording afterwards would retain an actual footprint missing its own + counterexample. The recorded axis mirrors enforcement exactly — `edges_from` + records a node read, because declaring a node grants its outbound adjacency — + and an absent resource is still a recorded coordinate, so a rule cannot probe + undeclared coordinates for free by picking empty ones. +- `ActualFootprintPosture` states what a footprint record is entitled to claim. + An empty violation set means "the declaration covered the execution" only when + the lane both recorded and enforced; from an unobserved lane it means only + that nothing was compared. `read_axis_is_complete` keeps that difference + legible, so an empty read axis from an unobserved lane reads as _unknown_ + rather than as _this execution read nothing_, and only `RecordedAndEnforced` + may ground an admitted falsification witness. `build_footprint_posture` caps + every lane by the enforcement the binary actually compiled. +- `ObservedExecuteFn` and `RuleExecutor` route native scheduler execution through + one worker-local evidence core. Native and generated contract-host executors + receive `ExecutionGraphView`; the frozen provider-v1 callback remains an + explicit legacy `GraphView` ABI and can never manufacture a complete read + axis. `ExecutionFootprintEvidence` retains one canonical record per executed + Action on `Engine` and `WorldlineState`, including the emitted write set when + the executor or read guard unwinds. Records are keyed before worker dispatch + and sorted independently of worker claim or completion order. Successful, + panicking, legacy, generated-consumer, provider-v1, and worker-count-invariant + witnesses complete stage 2 of the falsification roadmap without exporting + `FootprintGuard` or weakening its ordinary panic path. +- Differential tests run the recorded write set and the enforced write check + against the same ops and the same declaration, closing an assumption the + design had only asserted. They also pin the two deliberate disagreements: + cross-warp emission and unauthorized instance ops are scope and authority + failures that the recorder declines to report as footprint-subset failures, + so a reducer cannot hop between bug classes by conflating them. -- Generated provider helpers bind the bounded-read schema publication, including - its exact schema identity in the helper contract and derivation materials. +- `submit_intents_with_runtime_wal_ack` accepts several intents and returns after one storage sync has made all of their acceptance transactions durable. Each intent writes the same acceptance transaction as a single submission, so recovery is unchanged. No acceptance of a batch counts as durable, or can be scheduled, before that sync succeeds. A failed batch acknowledges nothing. If the runtime refuses an intent before anything is written for it, the intents before it stay accepted and are synced. If an append or the sync fails, the call's intake is rolled back and the WAL refuses further work with `StorageFailed` until it is reopened. -- Byte-equality fixture reproduction guidance now requires guarded reusable - compiler storage and preserves the limits of its frozen provider evidence. +- `SlotWriteIndex` resolves the value of one node, edge or attachment slot at a tick cursor from tick patches and the initial boundary, without materializing a graph or replaying unrelated ticks. It indexes the operations that wrote each slot, including values cleared by node, edge and instance deletion, and truncates in proportion to the ticks removed. A reader is bound to the exact patches the index was built from by patch digest, and truncation refuses patches that are not the indexed suffix. It is a derived reading aid; the runtime does not use it yet. -- Byte-equality evaluator tests now require `trusted_runtime` in Cargo and run - in the feature-enabled CI and opt-in local test routes. Selecting the target - without the feature can no longer produce a zero-test success. +- Native projected compare-and-set invocation encoding retains canonical application input and statically binds the expected attachment-value digest. The native lowerer and the structurally separate verifier reconstruct CAS-specific profiles and reject rebound digest paths or under-budget configurations. Generated schema, reproducible components and a retained public Edict compiler build establish package production. The retained compiler package now has scheduler execution, pending/committed Action recovery, stale-digest noncommit recovery and typed refusal witnesses. `EchoOperationInvocationV1::anchored_node_attachment_compare_and_set_with_application_input` and `ExecutableOperationPackageV1::with_compare_and_set_application_result_projection` construct the projected forms without byte editing. -- The ordered-publication compiler witness retains the return code and raw - streams when unexpected output violates JSONL, instead of hiding the compiler - result behind a JSON decoding or non-object error. +- The trusted executable-operation host can retain two native alternative strands, + continue a losing strand under new observations, and recover its fork ancestry + and operation outcomes from the WAL. Application selection records do not + imply merge or promotion. -- Removed the unguarded ordered-publication image-build recipe. Its test-only - witness requires a guarded reusable worker with copied sources and accounted - compiler output; the supported runner remains separate follow-up work. +- Bounded executable-operation host sessions retain immutable observations and + logical-request bindings in the native WAL. Echo evaluates supplied node/atom + preconditions inside operation preparation, includes their reads in scheduler + footprints, and retains typed refusal or commitment outcomes across reopening. + The generic `run-edict-operation --serve` driver supports repeated operations, + historical outcome lookup, and derived observation-change discovery. -- Provider artifact generation rejects a contract publication whose exact - schema or manifest differs from the generation input. Cross-publication calls - can no longer emit artifacts with misleading input provenance. +- An opt-in create-operation configuration v2 derives Unicode scalar key bounds in both provider components and binds them into packages. Runtime admission enforces nonempty keys and separate scalar/UTF-8 byte ceilings; legacy configuration v1 is unchanged. -- The filesystem WAL writer lease now attempts an explicit unlock when its - owning guard drops. A retained duplicate descriptor no longer extends a - successfully released lease and blocks immediate writer takeover. Live-writer - exclusion and the successor's independent lease remain enforced. +- A disabled-by-default experimental Keep ReferenceStore adapter implements the complete-object CAS port with explicit limits, private bindings, sanitized backend errors and atomic output promotion. It preserves existing CAS defaults and claims no restart durability. -- 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. +- An isolated experimental Echo–Keep identity bridge checks both independent hash laws and exact byte length from one bounded stream. It leaves the default CAS dependency graph unchanged. -### Added +- A fallible complete-object CAS port stages and verifies exact bytes before atomic destination promotion. Memory and disk adapters share conformance checks; existing APIs remain compatible and no durability or authenticated absence is claimed. - Generic source-owned Edict functions execute through both private pure and bounded-read evaluation with fresh lexical frames, ordered argument evaluation, @@ -2058,224 +2044,226 @@ Applied, Rejected, Obstructed}` with receipt evidence and typed contract - Three graveyard entries (BOAW naming, 5x Duty Model, unimplemented future specs). -### Removed +### Fixed + +- Completed shadow application-root benchmark rounds are invalid when their + recorded incremental/rebuild or live/replay parity is missing or failed, including + builds without `delta_validate`. + +- F5 benchmark validation rejects observations from a different executed + workload, including runs without a pinned script golden. + +- Stale-basis Action corroboration (#837) reads every slot a retained tick + wrote, not only its declared `out_slots`. Runtime-ingress materialization + writes the event node, its intent attachment and its kind edge outside any + rule footprint; those writes were invisible to the interval check. A tick + that upserts or deletes a warp instance now makes the interval's writes + unknown, so a stale Action across it keeps the whole-frontier rule. + +- Outgoing-edge bucket iterators expose their exact remaining length without + inspecting edges, so bounded readers can precharge the entire source bucket + before filtering by type. + +- The native pure interpreter evaluates bounded UTF-8 byte predicates with + complete aperture charging and typed Boolean values. Native provider judgments + independently validate matching helper/read guards and their bounded scan work. + +- Pure evaluation executes compiler-produced negated input guards, including + authored no-op refusal after checked byte-range predicates, with bounded + decoding, combined traversal and deterministic step accounting. + +- Pure evaluation accepts compiler-produced conjunctive input guards instead of + rejecting their `all` predicate shape as an invalid artifact. Conjunctions + retain deterministic short-circuit metering and combined traversal limits. + +- `dispatch_intent` no longer stages a witnessed suffix import against the + kernel's default worldline (#892). It ignored the request's receiving + worldline and recorded `Staged` without the bundle and basis checks the + library performs. Until comparable-basis transport exists, import intents + are refused with `NOT_SUPPORTED` and nothing is admitted, staged or + attributed. + +- A tick that decides a submission no rule matched now commits and recovers + under the WAL (#873). The WAL tick decision gains `NoMatchingRule` (code 4), + recovery maps it to `RecoveredSubmissionPosture::DecidedNoMatchingRule`, and + a retry reports `SubmissionRetryPosture::AlreadyDecidedNoMatchingRule`. + Before, such a tick failed with `TickOutcomeUnavailable` and could not be + recorded at all. Older WALs never contain the code. +- `Footprint::independent` no longer treats an unpopulated `factor_mask` as + partition evidence. The mask fast path now applies only when both masks are + non-zero; a zero placeholder on either side falls through to the node, edge, + attachment, and port set checks. Previously two zero-mask footprints with + conflicting writes compared as independent. Nothing in the engine calls it + today (the scheduler never consults the mask), but it is public API. A + union of footprints (`union_assign`) also stays unpopulated when either side + with claims is unpopulated, so a composite cannot look fully masked. +- A tick with the in-memory WAL no longer costs time in proportion to the + whole log. The host copied the in-memory log, its catalog and its indexes + before every tick so it could undo a failed one; at 8,000 updates a tick + took 13.5 ms. It now marks the log's end and, only if a tick fails, + truncates back to the mark and rebuilds what is derived from the log. In + `wal_record_cost` the in-memory update now costs about 0.22 ms at 500 and at + 8,000 updates of history. + +- A commit record whose storage sync failed is no longer acknowledged. The + record can be readable without being durable; a trusted host used to + re-read the log after the error and treat what it found as committed, for + submissions, scheduler ticks, causal anchors, operation installations and + operation ticks. The filesystem store now refuses further writes after any + failure while a commit record is written or synced, and the host takes the + work back and refuses further WAL work with `StorageFailed` until the WAL + is reopened, as batched submission already did. An error that arrives after + a successful sync is still reconciled from the log. + +- A trusted host takes the filesystem WAL writer lease before it runs + writable recovery. It used to recover first and take the lease afterwards, + so a second host that opened a log with a live writer could drop that + writer's in-progress tail by rewriting its segment files, and only then be + refused. The second host is now refused at the lease and modifies nothing. + +- The canonical CBOR decoder in `echo-wasm-abi` no longer reserves memory in + proportion to a length its input claims, and no longer recurses without + bound. A header that claims more array elements, map entries or string + bytes than the input has left is refused with `Incomplete`, and the + comparison is made before the length is narrowed, so 32-bit and 64-bit + targets refuse the same inputs. A container reserves at most a few slots + before its elements are decoded, so nested headers cannot multiply the + memory a request asks for. Nesting deeper than + `MAX_CANONICAL_NESTING_DEPTH` (128) is refused, by the encoder as well, so + bytes it returns always decode. Before, a nine-byte request could abort the + process. + +- Writable WAL recovery no longer removes committed records in order to drop + an uncommitted tail. It rebuilt the whole log by deleting every segment + file and re-appending what it kept, so a crash in between lost all + committed history; it also synced the WAL root instead of the directory + that holds the segments, and collapsed rotated segments into the first. + Each segment that loses records is now rebuilt in a scratch file and + swapped in by one rename, a segment with nothing to drop is not touched, + an emptied trailing segment is removed, and the containing directory is + synced. A crash at any step leaves the same committed history. + +- A worldline frontier retains the state root computed by its last executable-operation Action commit and returns it without hashing until the graph is next accessed mutably. An Action tick after the first now hashes the whole reachable state once instead of twice. Debug builds hash again to check each retained root, so they do not get the saving. The graph field of `WorldlineState` is private to its module so that every mutation goes through the accessor that drops the retained root. + +- A filesystem WAL writer that takes over an existing log syncs its segment files before reading them as recovered history. A record that an earlier writer wrote and never synced was readable after reopen and was reported as a durable acceptance; a later power loss could still lose it. + +- A scheduler pass that commits executable-operation Actions hashes the worldline's whole reachable state twice instead of three times. The root before the commit is the root the pass already computed for the frontier basis; the commit no longer computes it again. + +- A scheduler pass resolves a writer head's frontier basis once instead of once per admitted executable-operation Action. Resolving it hashes the whole reachable state, so a tick's cost grew with Actions times graph size. The bases produced are unchanged. + +- A scheduler pass builds and digests its retained WAL state delta once per commit instead of once per admitted Action. The WAL bytes are unchanged. + +- A scheduler pass that commits executable-operation Actions no longer copies the worldline's graph. The commit wrote its patch to a copy of the graph and then replaced the original, and the pass's rollback marker held a second copy. The patch is now written in place and each replaced value is journaled before its write; rollback restores from the journal. This applies to patches of node upserts and non-portal attachment writes. A patch that changes graph structure, and a pass that runs native rules through the engine, still retains one copy. Debug builds keep a copy to check the journal. + +- A worldline's initial boundary is shared instead of copied. It never changes after construction, but every scheduler rollback marker, replay checkpoint and replay base cloned the whole graph it holds. Tick cost on a large graph drops by roughly a fifth; the remaining graph-proportional copies are the live state itself. + +- Scheduler rollback checkpoints no longer copy a worldline's committed tick history or committed-ingress ledger on every SuperTick. A checkpoint records the history length and the attempt journals the ingress ids it adds; rollback truncates and removes them. The trusted host no longer clones the runtime, provenance and retained Action outcomes before every tick, or the runtime before every WAL-acknowledged submission: a completed scheduler pass returns an undo handle, and Action staging and submissions are journaled. Rollback results are unchanged; tick and submission cost no longer grow with committed history. + +- A strict filesystem WAL commit no longer rewrites and syncs the writer-epoch ledger and its directory after syncing the commit record. The commit record remains the durability boundary; reopening already derives each epoch's final commit from the segment. Each transaction now forces one sync instead of three. The on-disk formats are unchanged. + +- Package admission rejects result projections whose expected-digest binding conflicts with the selected mutation program, before they can occupy an installed operation coordinate. Recovery applies the same rule to retained installations: a WAL that holds such a hand-built package is refused rather than reinstalled. Echo's providers never emitted that shape, and no invocation of it could be admitted. Admission likewise refuses an expected-digest path that is empty or overlaps the key or replacement path. + +- Both executable mutation providers refuse transformed effect arguments instead of silently projecting the caller input into a different mutation. Direct application-input arguments remain supported; the structurally separate verifier enforces the same boundary. + +- Retained local fork retries reconcile durable topology after uncertain appends, preserving the original basis and preventing duplicate fork records. + +- Observation slots preflight their canonical byte bound and charge execution reads before copying Atom payloads. + +- Private Edict runtime decoding resolves named integer types through their declared width, matching source-function provider acceptance. + +- Filesystem writer takeover preserves unused LSNs after empty epochs and refuses unreconciled tails before changing the epoch ledger. + +- Incremental snapshot state roots now include the existing v1 domain separator and agree with canonical snapshot hashing. Previously emitted incorrect accumulator roots are not migrated. + +- The SPDX checker preserves Markdown frontmatter when it checks or repairs license headers. + +- Action WAL recovery reuses ordered verified replay cursors instead of retaining a full state for each basis tick. It preserves basis, Tick, result, obstruction and conflict checks, including delayed stale bases. + +- The generic operation runner names typed obstruction kinds, footprint conflicts, and missing outcomes in bounded summaries. It omits raw outcome records and invocation data on both Action error paths. + +- `xtask run-edict-operation` runs outside Git and resolves relative artifact and WAL paths from the caller directory. Repository maintenance commands retain their Git-root behavior. + +- `WorldlineState::state_root` documentation now states its reachable-state boundary. Detached create-if-absent writes remain bound by patch and commit identities. Hash bytes are unchanged. + +- `ReadView::at` validates the aperture and derives the selected current frontier + basis with one state hash. `ReadView::new` still checks an independently + selected expected basis. Both retain the same aperture and trust boundaries. + +- Public bounded-read compiler timeouts retain partial stdout/stderr and the + original timeout as the failure cause. + +- Bounded-read lowering recognizes only the exact unsigned primitive coordinates. + Named structural types starting with `U` now reach ordinary type lookup, as + they already do in independent verification and runtime parsing. + +- Private read evaluation identifies the input by its verified `arg.0` identity. + Reordering a package's local declarations no longer changes input selection. + +- Read-provider lawpack validation remains separate from the pure profile's + empty-effect requirement, preserving read acceptance and pure-effect refusal + after integration of the strengthened pure-provider checks. + +- The bounded-read public compiler witness preserves return status and raw + streams when malformed or non-object JSONL prevents structured validation. + +- Bounded-read evaluator tests now require `trusted_runtime` in Cargo and run + in feature-enabled CI and opt-in local routes, including shared parser edits. + +- Removed the bounded-read witness's unguarded image/entrypoint recipe. Public + compiler and fresh-output runtime witnesses require a continuously guarded + reusable worker; pre/post measurements alone are not budget enforcement. + +- Generated provider helpers bind the bounded-read schema publication, including + its exact schema identity in the helper contract and derivation materials. + +- Byte-equality fixture reproduction guidance now requires guarded reusable + compiler storage and preserves the limits of its frozen provider evidence. -- Removed the provisional caller-authoritative causal-anchor API: - `CausalAnchorRequest`, `CausalAnchorFact::from_request`, public admitted-fact - fields, and raw admitted-identity constructors. Applications now submit a - `CausalAnchorAdmissionRequest` and treat the returned Echo fact, receipt, and - identities as opaque. This is an intentional breaking Rust API correction; - preserving the old surface would let callers manufacture Echo authority. -- Removed the abandoned Method system: its workspace crate and `xtask` - commands, checked-in backlog, cycles, retrospectives, status ledgers, process - manuals, and generated task graphs. Current architecture now lives in - canonical topics/specs/invariants, durable decisions live in ADRs, and live - work/status lives in GitHub. -- Removed the superseded `docs/design/` packet corpus and the retired TTD - counterfactual-creation invariant after promoting current doctrine into - canonical topics, ADRs, architecture documents, specifications, and tests. -- Removed the remaining architecture drift/future packets and dated benchmark - reports after preserving the retained-reading storage and proof boundary in - ADR 0020. Benchmark instructions now keep methodology in source docs and - measurements in generated artifacts and pull requests. -- Deleted zombie crates with no consumers (recoverable from git history): - `echo-wasm-bindings` (browser demo kernel), `echo-ttd`, `ttd-protocol-rs`, - and `echo-session-proto` (the TTD stack now lives with `warp-ttd`), plus - `echo-config-fs` (desktop app-shell fossil) and the - `packages/ttd-protocol-ts` generated consumer. -- Deleted `echo-app-core` (desktop app-shell fossil: toasts, prefs, config - ports) and the `echo-dry-tests` in-memory config fake that existed only to - test its trait; no other crate consumed either. -- Removed the unused `echo-wasm-abi::ttd` module and its public `PrivacyMask`, - `SessionToken`, and `TtdError` exports after the owning TTD/session stack was - retired. This is a breaking Rust API removal for unknown external consumers. -- Deleted `cargo xtask wesley` (existed only to sync the removed TTD - protocol consumer artifacts). -- Deleted stale point-in-time audit reports under `docs/audit/` and - `docs/audits/`. -- Removed the deleted crates from workspace members, CI clippy lanes, - `det-policy.yaml`, `scripts/verify-local.sh`, and the unordered-ABI - allowlist. -- Removed the VitePress docs-site toolchain from active repo tooling: npm - scripts, Make targets, tracked docs-site config, the dead browser-open helper, - and VitePress/Mermaid dependencies are gone. -- Removed the broken `warp-core/serde` feature and the gated `Serializable*` - wrapper exports. `warp-core` no longer declares direct `serde`, `serde-value`, - or `ciborium` dependencies; authoritative core serialization must stay in - explicit canonical boundary encoders rather than general serde derives. -- Removed the legacy `ttd-browser` crate from Echo's active workspace. The - release browser/runtime boundary now stays centered on `warp-wasm` and - `echo-wasm-abi`; debugger session semantics and browser delivery adapters - belong in `warp-ttd`. -- `docs/METHODOLOGY.md` — 5x Duty Model (never practiced; see graveyard). -- 17 unimplemented future spec files (see graveyard). -- `docs/march-16.plan.md` — stale planning scratchpad. -- `docs/plans/parallel-merge-and-footprint-optimizations.md` — superseded - by design review. -- Old plans, book (LaTeX), and research artifacts. All remain recoverable from - Git history. -- **`warp-ffi` crate deleted:** The C ABI integration path (`crates/warp-ffi`) - has been removed. The C ABI approach was abandoned in favor of Rust plugin - extension via `RewriteRule` trait registration and Rhai scripting. See - TASKS-DAG.md #26 (Graveyard). This is a **BREAKING CHANGE** for any - downstream code that depended on the C FFI surface. +- Byte-equality evaluator tests now require `trusted_runtime` in Cargo and run + in the feature-enabled CI and opt-in local test routes. Selecting the target + without the feature can no longer produce a zero-test success. -### Changed +- The ordered-publication compiler witness retains the return code and raw + streams when unexpected output violates JSONL, instead of hiding the compiler + result behind a JSON decoding or non-object error. -- `ExecItem` constructors require an explicit canonical evidence sequence. - Manually assembled work units no longer silently reuse a per-rule match - index as the execution sequence. Engine callers pass the existing batch-wide - enumeration directly, preserving scheduler order. +- Removed the unguarded ordered-publication image-build recipe. Its test-only + witness requires a guarded reusable worker with copied sources and accounted + compiler output; the supported runner remains separate follow-up work. -- Echo and Edict share exact `bunny-num` 0.6.0 for the canonical signed Q32.32 - foundation. `warp-math` exposes Bunny's checked type and delegates existing - `DFix64` arithmetic and motion conversions while preserving saturation, - ties-to-even, raw payload bytes, and the separate legacy ABI truncation policy. - This does not add fixed-point language syntax or runtime operation profiles. -- The general Rust toolchain and numerical consumer MSRVs are 1.96.0. Independent - leaves and authenticated provider component producers retain their explicit - 1.90.0 policy; the outer component driver uses 1.96.0. The MSRV guard also - validates a final policy row without a newline and reads package MSRVs only - from `[package]`, excluding metadata. The standalone host witness selects - Rust 1.96.0 locally, and the guard rejects a missing or stale nested pin. +- Provider artifact generation rejects a contract publication whose exact + schema or manifest differs from the generation input. Cross-publication calls + can no longer emit artifacts with misleading input provenance. -- Public installed-contract evidence fields on runtime ingress, receipt - correlation, outcome, and WAL state-delta carriers now use - `Option` instead of - `Option`. This is an intentional pre-1.0 source - compatibility change: legacy callers wrap with `LegacyContract` or `.into()` - and inspect with `legacy_contract()`, while provider callers inspect - `provider_v1()`. The enum is non-exhaustive to match the extensible wire-tag - family, so direct downstream matches require a wildcard arm. The legacy tag-1 - WAL encoding remains byte-identical. -- The public `RuntimeError` enum now includes - `InstalledContractIntentKindMismatch` and - `UnsupportedInstalledProviderContractMutation`, and the public - `ContractInverseObstruction` enum now includes `ProviderTargetUnsupported`. - These are intentional pre-1.0 source-compatibility additions: downstream - exhaustive matches must handle the new variants (or use an appropriate - wildcard arm). -- `echo-wesley-gen` now follows Wesley's operation-neutral adapter names: - `import_runtime_optic_artifact(...)` accepts `OperationArtifact`, and - `import_registration_descriptor(...)` accepts - `OperationRegistrationDescriptor`. Source consumers using Wesley's former - `OpticArtifact` or `OpticRegistrationDescriptor` names must update when they - adopt the corresponding Wesley 0.3 prerelease; Echo's runtime-local optic - artifact types and handles are unchanged. -- Provider semantic-source, generation-input, and contract-pack `Display` - diagnostics now render explicit kebab-case failure labels instead of Rust - `Debug` variant spellings. Typed error enums remain the programmatic - contract, while human/CLI diagnostics no longer move when Rust variants are - refactored. -- Restored the durable ADR 0001–0011 namespace and moved the post-Method - decisions to ADR 0012–0019, preserving the meaning of existing source - citations. CI now rejects missing, duplicate, non-contiguous, unindexed, or - collided ADR identifiers. -- Recorded the WSC, CAS, semantic reading identity, and optional proof boundary - as ADR 0020 without carrying forward the source packet's implementation - roadmap or application-specific checkpoint design. -- Replaced the opaque numeric determinism claim-pack generator with an honest - gate over upstream job results and exact artifact payload presence. The - executable suites remain the authority for what passed. -- Replaced the frozen root architecture and advanced guides with explicit - supersession signposts to the living no-graph architecture, topics, - specifications, invariants, and ADRs. -- Echo 1.0 release eligibility now depends only on Continuum participant - conformance, networked causal suffix exchange, and release integrity. Edict, - `jedit`, and any particular generated package remain downstream compatibility - work and no longer gate the Echo release. -- Echo 1.0 planning references now point at the cross-repository Continuum - Stack Convergence Project instead of the retired Echo-only Project. -- Local `scripts/verify-local.sh full` now treats broad Cargo test lanes as - GitHub Actions-owned by default, while keeping a maintainer opt-in through - `VERIFY_LOCAL_FULL_TESTS=1` for intentional local full-suite runs. -- `warp-core` renamed the generated contract package host API from - `install_contract_package(...)` to `register_contract_package(...)` so the - trusted-runtime boundary reads as explicit runtime-owned registration instead - of process-global installation. -- `warp-core` sealed braid member lookup now requires authority-bound sealed - query material, redacts non-public blinding material from debug output, and - keeps hidden-member commitments stable across parent frontier movement. -- `warp-core` settlement planning now rejects non-`Shared` strands before - producing import candidates. Author-only/debugger strand suffixes can remain - real causal work, but they cannot enter base shared history without an - explicit shared admission posture. Settlement compare remains local - revelation/inspection only: it can inspect a locally held strand suffix - without promoting, planning, admitting, or settling it. -- `warp-core` settlement plural artifacts and retained braid shells now carry - the source strand posture instead of hard-coding author-only posture for - shared settlement records. -- Local determinism tooling now fails closed around - `scripts/check-warp-core-serialization-boundaries.sh`. The serialization - boundary guard is mandatory, runs through `bash` rather than executable mode, - works without `rg`, rejects table-form serde/ciborium dependencies, and - blocks direct, grouped, multiline, or aliased canonical ABI serialization - imports outside explicit `warp-core` boundary modules. -- The nondeterminism guard now shares the same `rg`/Perl fallback scanner, - supports `DETERMINISM_FORCE_NO_RG=1` regression coverage, catches namespace - imports and alias calls for `std::env`, `std::fs`, and `std::process`, bans - `std::thread::available_parallelism`, and replaces file-wide allowlists with - rule-scoped waivers for build/native filesystem boundaries and test fixtures. -- `warp-core` engine and scheduler state now use ordered `BTreeMap`/`BTreeSet` - storage instead of `HashMap`, `HashSet`, or `FxHashMap` in deterministic core - paths. WAL filesystem tests also recreate stale deterministic fixture roots - before use so previous local residue cannot change the test outcome. -- `warp-core` engine construction now defaults to deterministic serial - execution instead of reading `ECHO_WORKERS` or host CPU availability. Callers - can still opt into parallel execution explicitly with - `EngineBuilder::workers(...)` or worker-count constructors. -- `echo-cli wal submission-posture` now exposes generic read-only recovery JSON - for one submission id and canonical envelope digest. The output reports retry - posture, recovered submission posture, receipt digest, and ticket digest - without importing any application nouns into Echo. -- Runtime WAL-backed scheduler ticks now roll back all tick WAL evidence from a - failed multi-head scheduler pass, treat missing or mismatched receipt - correlation evidence as an invariant error instead of a normal obstruction, - and bind runtime recovery certificates to rebuilt submission and receipt - indexes. -- `warp-wasm` no longer contains the legacy Stack Witness 0001 - `createBuffer`/`replaceRange`/`textWindow` shortcut. QueryView requests now - route through the generic installed contract observer boundary only; without - an installed observer, WASM `observe(...)` returns `UNSUPPORTED_QUERY` - instead of materializing hardcoded text bytes. -- `warp-core` structured binding tests no longer use rope/text-shaped fixture - names. The executable examples now exercise generic authored scopes, heads, - segments, and markers so core test fixtures do not imply built-in editor - semantics. -- The canonical pre-push hook now runs the narrowest changed-file Rust witness - instead of reusing the broader local PR gate. Rust module edits map to exact - `cargo test -p --lib ::tests` slices, integration-test edits - map to exact `--test ` invocations, and tooling edits stay on local - shell smoke checks. Broader clippy, rustdoc, package, and workspace coverage - remains available through `make verify-pr`, `make verify-full`, and CI. The - selector now avoids fake zero-test module filters for source files without - inline tests, maps `src/bin/*.rs` edits to exact binary targets, and preserves - required features for gated integration tests. -- Deterministic math now lives in a slim `warp-math` workspace crate. - `warp-core` keeps the existing `warp_core::math::*` compatibility surface as - a re-export, while `warp-geom` depends directly on `warp-math` instead of - pulling in all of `warp-core`. Math-only integration tests, deterministic - trig golden vectors, PRNG golden regression, and the LUT generator moved with - the math crate. -- CI and local verification now split broad clippy coverage into explicit - library, binary, and selected integration-test lanes instead of invoking one - monolithic cargo pass. The `warp-core` runtime inbox test target is now an - explicit lint lane with the same `native_rule_bootstrap,host_test` features - used by the ticketed-ingress regression suite. -- Local verification now treats rustdoc warnings as CI-owned by default. - `scripts/verify-local.sh` skips local rustdoc lanes unless - `VERIFY_LOCAL_RUSTDOC=1` is set, keeping pre-push and full local gates focused - on faster edit-loop witnesses while preserving CI rustdoc coverage. -- Tooling-only full verification now selects focused hook regression scripts by - changed file family, so a `scripts/verify-local.sh` edit runs the verify-local - hook regression without also running unrelated runtime-schema, PR-status, or - timing hook tests. -- Local hook regression tests are now CI-owned by default. The local full gate - skips hook tests unless `VERIFY_LOCAL_HOOK_TESTS=1` is set, and the opt-in - hook-test lane clears verifier override variables before launching nested - hook regressions. +- The filesystem WAL writer lease now attempts an explicit unlock when its + owning guard drops. A retained duplicate descriptor no longer extends a + successfully released lease and blocks immediate writer takeover. Live-writer + exclusion and the successor's independent lease remain enforced. -### 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. - Filesystem writer leases explicitly unlock when their owner leaves scope, so a descriptor briefly inherited by a concurrent child process cannot keep diff --git a/README.md b/README.md index d4355ad49..ce885a9a7 100644 --- a/README.md +++ b/README.md @@ -186,15 +186,21 @@ result, composition, and terminal outcome. Runtime-control installation and scheduler Tick records permit callback-free fresh-host recovery. Program bytes explicitly bind the interpreter and intrinsic profiles, while Tick evidence binds each admitted installation. A program digest cannot confer operation -identity, invocability, or authority. Each package also retains the canonical -lawpack obstruction coordinate resolved from the authored source-local import; -the scheduler reports that exact typed coordinate without interpreting -application vocabulary. +identity, invocability, or authority. Each package whose program is imported +from a lawpack also retains the canonical lawpack obstruction coordinate +resolved from the authored source-local import; the scheduler reports that +exact typed coordinate without interpreting application vocabulary. A package +compiled from Edict source binds no lawpack: under the accepted +[Authored Operation Effects](docs/architecture/authored-operation-effects.md) +design, which is not yet implemented, its obstructions are qualified by the +admitted package and installed operation. That generic runtime witness is not yet the Jim/Jedit vertical. A standalone application-owned Edict operation now crosses it through a compiler-produced package and structurally separate accepted verification report, but no Jedit -rope lawpack or `ReplaceRange` operation uses it. It does not yet claim +`ReplaceRange` operation uses it. Under the accepted Edict-source decision, the +rope law will be compiled from Jedit-owned Edict source rather than imported as +a lawpack. It does not yet claim cross-category scheduler composition or independently implemented semantic conformance. It also temporarily reuses `TrustedRuntimeHost`'s joint `native_rule_bootstrap` and `trusted_runtime` feature gate. The program itself diff --git a/crates/warp-core/tests/fixtures/edict-byte-literals/README.md b/crates/warp-core/tests/fixtures/edict-byte-literals/README.md index 8556e3efc..7cdd0d5af 100644 --- a/crates/warp-core/tests/fixtures/edict-byte-literals/README.md +++ b/crates/warp-core/tests/fixtures/edict-byte-literals/README.md @@ -22,7 +22,12 @@ pinned Echo `schemas/edict-provider/package/v1` into `.build/echo-provider`. Build the pinned Edict CLI, then send this request to it from the copied root: ```json -{"schema":"edict.compiler.settings/v1","type":"compilerSettings","operation":"build","application":"edict.application.json"} +{ + "schema": "edict.compiler.settings/v1", + "type": "compilerSettings", + "operation": "build", + "application": "edict.application.json" +} ``` Compare `.build/application` package/report bytes with the decoded carriers. diff --git a/crates/warp-core/tests/fixtures/edict-unsigned-addition-control/README.md b/crates/warp-core/tests/fixtures/edict-unsigned-addition-control/README.md index 6e6bd7d54..62d4a7d37 100644 --- a/crates/warp-core/tests/fixtures/edict-unsigned-addition-control/README.md +++ b/crates/warp-core/tests/fixtures/edict-unsigned-addition-control/README.md @@ -1,5 +1,6 @@ + # Public unsigned-addition control The source and unmodified hex carriers come from Edict's public JSONL application diff --git a/crates/warp-core/tests/fixtures/legacy_causal_wal/README.md b/crates/warp-core/tests/fixtures/legacy_causal_wal/README.md index 51da1d552..14244eeaa 100644 --- a/crates/warp-core/tests/fixtures/legacy_causal_wal/README.md +++ b/crates/warp-core/tests/fixtures/legacy_causal_wal/README.md @@ -14,10 +14,10 @@ separated form must resolve to its original submission. a reader accepts what an earlier writer actually wrote; bytes produced by the current encoder cannot show that. -| File | Bytes | SHA-256 | -| --- | --- | --- | -| `segments/segment-00000000000000000001.ecwal` | 7594 | `95a762b44e674e7612ea74aff516034cdab192c8700c6c75d0a76b6386894457` | -| `writer-epochs.ecwal` | 231 | `bdef26980af969e059f52c3a212ade94cc26329083020b8bd1119313877efc61` | +| File | Bytes | SHA-256 | +| --------------------------------------------- | ----- | ------------------------------------------------------------------ | +| `segments/segment-00000000000000000001.ecwal` | 7594 | `95a762b44e674e7612ea74aff516034cdab192c8700c6c75d0a76b6386894457` | +| `writer-epochs.ecwal` | 231 | `bdef26980af969e059f52c3a212ade94cc26329083020b8bd1119313877efc61` | ## Provenance @@ -28,13 +28,13 @@ guarded container, by a throwaway test added to - the reference host (`runtime()`, `empty_engine()`) with a filesystem WAL and the reference contract package; - one WAL-acknowledged causal EINT intent, `causal_eint_envelope(lane, - [causal_receipt_ref(lane, "legacy-parent", 41)])`, staged with +[causal_receipt_ref(lane, "legacy-parent", 41)])`, staged with `admission_ticket(61)` and decided by `run_until_idle(4)`: submission `2348e63b4cd2b630e659d9bcac2e5456d56c35c7a5f04f717d07820a113888f7`, ingress `811015cf74795d042fc637d41d506024f538206586707d533fede984a2dddcbf`; - one WAL-acknowledged causal Continuum occurrence, `pack_intent_v1(MUTATION_OP_ID, - b"amount=9")` with the same parent and `ContinuumOccurrence::new([7; 32], - [0xa7; 32])`, left pending: submission +b"amount=9")` with the same parent and `ContinuumOccurrence::new([7; 32], +[0xa7; 32])`, left pending: submission `8879b31036123e5b70962a068958f51e379750627e13abecf5b585d43fdd3f63`, ingress `4af4cf66ff6f479386420b7d1df87e762ee5964323d402b3f378d007381acf8e`. diff --git a/docs/README.md b/docs/README.md index ee915981b..f66cc8eb9 100644 --- a/docs/README.md +++ b/docs/README.md @@ -20,6 +20,7 @@ causal history. Git history is the archive; GitHub owns live work and status. - [There Is No Graph](architecture/there-is-no-graph.md) - [Sliced readings and copy-on-write strands](architecture/sliced-readings-and-copy-on-write-strands.md) (accepted design, not implemented) +- [Authored operation effects](architecture/authored-operation-effects.md) (architecture accepted on merge of #889, detailed specification provisional, not implemented) - [Batched strict submission](architecture/batched-strict-submission.md) - [Participant history as a braid](architecture/participant-history-as-a-braid.md) (accepted design, not implemented) - [Continuum transport](architecture/continuum-transport.md) diff --git a/docs/adr/0023-admitted-executable-operation-packages.md b/docs/adr/0023-admitted-executable-operation-packages.md index cc41e986e..004a04957 100644 --- a/docs/adr/0023-admitted-executable-operation-packages.md +++ b/docs/adr/0023-admitted-executable-operation-packages.md @@ -10,6 +10,24 @@ - **Superseded in part by:** the [Action validity across ticks](../topics/GeneratedRules.md#action-validity-across-ticks) decision of 2026-10-14 (#837), for every exact-basis requirement below as it applies to Actions that meet that decision's conditions +- **Superseded in part by:** the + [Application operation semantics authored in Edict source](../topics/GeneratedRules.md#application-operation-semantics-authored-in-edict-source) + decision, accepted 2026-10-15 and effective when + [flyingrobots/echo#889](https://github.com/flyingrobots/echo/pull/889) merges + to `main`, for the declarative-resource and lawpack requirements that + assume the rope law is an imported resource, in this ADR's rope-law + closure, package binding, package obligations, evidence grades, + Jurisdiction, and Consequences (enumerated in the "Jedit rope-law closure" + banner), and the selection under "Alternatives for Expressing the Rope Law" +- **Superseded in part by:** + [Authored Operation Effects](../architecture/authored-operation-effects.md), + effective when [flyingrobots/echo#889](https://github.com/flyingrobots/echo/pull/889) + merges to `main`, for bridge Actions only: the prepared-evaluation outcome + (a successful evaluation exposes one patch; the closed + `PreparedEchoOperationOutcomeV1`; no patch digest on `Obstructed`), marked + where it appears. The merge accepts this as architecture; the detailed + bridge contract stays provisional until executable evidence, per + [What merging accepts](../architecture/authored-operation-effects.md#what-merging-accepts) > **Scheduler lifecycle amendment:** This ADR established exact package, > invocation, private-evaluation, and recovery semantics. ADR 0025 supersedes @@ -101,6 +119,13 @@ Edict intent / admitted executable-operation package → binds the exact EchoOperationProgramV1 bytes and digest ``` +> **Superseded in part,** effective when flyingrobots/echo#889 merges: the +> lawpack step applies only to a program whose executable meaning is imported +> from a lawpack resource. A program compiled from Edict source, such as +> Jedit's `ReplaceRange`, goes from the canonical semantic closure directly to +> the exact program bytes and digest, and binds no lawpack resource. See the +> [Jedit rope-law closure](#jedit-rope-law-closure) banner. + The admitted Edict operation supplies the public operation coordinate, invocation and result schemas, basis contract, budget and footprint contract, authority requirements, result and obstruction interpretation, and the @@ -136,6 +161,13 @@ Every `ExecutableOperationPackageV1` must canonically bind: - result and obstruction interpretation; - one evaluator ABI and intrinsic-profile identity. +> **Superseded in part,** effective when flyingrobots/echo#889 merges: the +> lawpack resource coordinate and digest are bound only by a package whose +> program is imported from a lawpack resource. A package whose program is +> compiled from Edict source binds no lawpack resource; every other +> obligation above still applies to it. See the +> [Jedit rope-law closure](#jedit-rope-law-closure) banner. + Every bound `EchoOperationProgramV1` must canonically bind its executable meaning: @@ -159,6 +191,22 @@ exposes one normal Echo patch; an obstructed evaluation exposes no parent mutation. Version 1 retains an execution or trace identity sufficient to bind later evidence without claiming that a durable child worldline already exists. +> **Superseded in part,** effective when flyingrobots/echo#889 merges: for +> bridge Actions, whose compiled Edict program proposes effects, the +> evaluation and outcome contract here is replaced by +> [Authored Operation Effects](../architecture/authored-operation-effects.md). +> A bridge evaluation yields an `EffectProposal` or a typed obstruction rather +> than a patch, Echo derives the patch afterwards in the same Tick +> construction, and the receipt posture defined there replaces +> `PreparedEchoOperationOutcomeV1`; some obstructed postures record a derived +> patch digest that was never committed. Atomic visibility, one parent patch +> or one obstruction, still governs. The original text is preserved and still +> governs every other Action. The merge accepts this replacement as +> architecture. The posture, record, and digest details stay provisional +> until executable evidence fixes them, as +> [What merging accepts](../architecture/authored-operation-effects.md#what-merging-accepts) +> states, and no bridge Action exists until the first bridge profile ships. + The program may use generic primitives for typed graph access, canonical scalar operations, checked `u64` arithmetic, bounded byte manipulation, UTF-8 validation, canonical hashing, content-address derivation, and graph-delta @@ -220,6 +268,22 @@ An `Obstructed` outcome never enters parent commit or scheduler composition and never carries a patch digest. It may produce retained typed execution evidence, but it does not claim a committed consequence. +> **Superseded in part,** effective when flyingrobots/echo#889 merges: for +> bridge Actions, whose compiled Edict program proposes effects, the +> evaluation and outcome contract here is replaced by +> [Authored Operation Effects](../architecture/authored-operation-effects.md). +> A bridge evaluation yields an `EffectProposal` or a typed obstruction rather +> than a patch, Echo derives the patch afterwards in the same Tick +> construction, and the receipt posture defined there replaces +> `PreparedEchoOperationOutcomeV1`; some obstructed postures record a derived +> patch digest that was never committed. Atomic visibility, one parent patch +> or one obstruction, still governs. The original text is preserved and still +> governs every other Action. The merge accepts this replacement as +> architecture. The posture, record, and digest details stay provisional +> until executable evidence fixes them, as +> [What merging accepts](../architecture/authored-operation-effects.md#what-merging-accepts) +> states, and no bridge Action exists until the first bridge profile ships. +> > **Superseded in part (2026-10-14, #837):** for Actions that meet the > conditions of [Action validity across ticks](../topics/GeneratedRules.md#action-validity-across-ticks), > the exact-basis requirement here is replaced by dependency-scoped validity. @@ -291,6 +355,32 @@ admission posture without adding broad authorization policy to this decision. ### Jedit rope-law closure +> **Superseded in part,** effective when +> [flyingrobots/echo#889](https://github.com/flyingrobots/echo/pull/889) merges +> to `main`. The rope law is authored in Jedit-owned Edict source rather than +> imported as a declarative executable resource. See +> [Application operation semantics authored in Edict source](../topics/GeneratedRules.md#application-operation-semantics-authored-in-edict-source). +> The text below is kept as written, for its reasoning. +> +> **No longer required:** the declarative resource and lawpack named in the +> first paragraph; the fifth required binding (the rope-law resource +> coordinate and digest); the lawpack and `EchoOperationProgramV1` steps of the +> binding chain and the paragraph after it; the paragraphs on what makes +> the resource acceptable and who owns it; and, outside this section, the +> lawpack step of the package binding direction and the lawpack obligation in +> "First-version execution obligations" (both now apply only to a program +> imported from a lawpack resource), the +> lawpack-resource binding in the evidence-grade table, the rope-law resource +> and generic resource binding in Jurisdiction, and the executable-resource +> binding in Consequences, each marked where it appears. +> +> **Still governing:** the versioned canonical text-schema declaration and its +> first four required bindings; the package's binding of that declaration's +> coordinate and digest, with the typed schema-closure refusal, applied to the +> package's compiled Edict program in place of the lawpack and subordinate +> program; the prohibited forms, which the compiled Edict program may not +> contain or resolve to; and the handwritten planner's test-only role. + For the first `ReplaceRange` vertical, Jedit will use a digest-locked canonical declarative executable semantic resource imported through a Jedit-owned Edict lawpack. This decision does not require Edict source to express the complete @@ -375,6 +465,10 @@ smaller. Implementing the entire language surface before any hook-free operation runs would turn the first witness into a broad language and runtime design effort and would make `ReplaceRange` define unproven universal syntax. +> **Superseded in part,** effective when flyingrobots/echo#889 merges: the +> superseding decision linked in this record's header selects this route, +> Edict source, for the rope law. The rejection above is kept as written. + ### Bind a canonical declarative executable resource from a Jedit lawpack This route adds only the Edict prerequisites needed to type the real operation, @@ -388,6 +482,11 @@ proof chain without broad Edict expansion. It does not establish a permanent rule that complex Edict operations must be authored as external resources. Later Edict syntax may compile to the same target program boundary. +> **Superseded in part,** effective when flyingrobots/echo#889 merges: this +> selection was never implemented and is superseded by +> [Application operation semantics authored in Edict source](../topics/GeneratedRules.md#application-operation-semantics-authored-in-edict-source). +> The selection and its rationale above are kept as written. + ## Verification Evidence Grades The word "independent" is reserved for an implementation that does not merely @@ -409,6 +508,12 @@ the following grades. | Repeated evaluation by the same Echo evaluator | Deterministic self-validation | The implementation is repeatable for the tested basis and inputs; it is not an independent implementation. | | Receipt/WAL round-trip and fresh-host reconstruction | Deterministic self-validation | Retained bytes reconstruct the same installed and execution identities without callbacks. | +> **Superseded in part,** effective when flyingrobots/echo#889 merges: the +> "lawpack resource" in the target-verifier row above. The row's check now +> covers the admitted package and Target IR to the program compiled from +> Jedit's Edict source, with the same evidence grade. See the +> [Jedit rope-law closure](#jedit-rope-law-closure) banner. + A separate verifier crate is not, by itself, independently implemented conformance evidence. This decision does not claim formal refinement, complete semantic equivalence, a clean-room Echo interpreter, or a proof that all @@ -422,6 +527,11 @@ by comparing two wrappers around the same algorithm. ## Jurisdiction +> **Superseded in part,** effective when flyingrobots/echo#889 merges: Jedit +> owns the `ReplaceRange` law as Edict source rather than a rope-law resource, +> and Edict's generic resource binding is no longer part of this operation's +> route. See the [Jedit rope-law closure](#jedit-rope-law-closure) banner. + - **Jedit** owns `ReplaceRange.edict`, the rope-law resource, fact schemas, codec/identity law, operation semantics, and the differential oracle corpus. - **Edict** owns source parsing, typing, canonical meaning, Core, generic @@ -485,6 +595,11 @@ by comparing two wrappers around the same algorithm. - The existing Jedit planner becomes migration evidence rather than production execution authority. +> **Superseded in part,** effective when flyingrobots/echo#889 merges: the +> rope law no longer needs executable-resource binding, and Edict gains +> language features only when the authored source demonstrates the need. See +> the [Jedit rope-law closure](#jedit-rope-law-closure) banner. + ## Non-Goals - Cyber Kitten syntax or runtime; diff --git a/docs/adr/0025-scheduler-owned-executable-operation-actions.md b/docs/adr/0025-scheduler-owned-executable-operation-actions.md index 62307203d..6b89177cd 100644 --- a/docs/adr/0025-scheduler-owned-executable-operation-actions.md +++ b/docs/adr/0025-scheduler-owned-executable-operation-actions.md @@ -9,6 +9,14 @@ - **Superseded in part by:** the [Action validity across ticks](../topics/GeneratedRules.md#action-validity-across-ticks) decision of 2026-10-14 (#837), for the shared parent basis of Actions in one Tick +- **Superseded in part by:** + [Authored Operation Effects](../architecture/authored-operation-effects.md), + effective when [flyingrobots/echo#889](https://github.com/flyingrobots/echo/pull/889) + merges to `main`, for bridge Actions only: the prepared candidate returned + on success and the lawpack qualification of an evaluation obstruction, + marked where it appears. The merge accepts this as architecture; the detailed + bridge contract stays provisional until executable evidence, per + [What merging accepts](../architecture/authored-operation-effects.md#what-merging-accepts) ## Context @@ -74,6 +82,18 @@ worldline: and no parent-visible operations; - neither result mutates the parent state. +> **Superseded in part,** effective when flyingrobots/echo#889 merges: for +> bridge Actions, whose program is compiled from Edict source and binds no +> lawpack resource, an obstruction is qualified by the admitted package and +> installed-operation identities instead of a lawpack, and success returns an +> `EffectProposal` rather than a prepared candidate, as +> [Authored Operation Effects](../architecture/authored-operation-effects.md) +> defines. The original text is preserved and still governs every other +> Action. The merge accepts this replacement as architecture. The detailed +> bridge contract stays provisional until executable evidence fixes it, as +> [What merging accepts](../architecture/authored-operation-effects.md#what-merging-accepts) +> states, and no bridge Action exists until the first bridge profile ships. + The direct `prepare_echo_operation_v1` and `commit_prepared_echo_operation_v1` methods remain publicly reachable on `TrustedRuntimeHost` as explicitly transitional, documentation-hidden diff --git a/docs/architecture/authored-operation-effects.md b/docs/architecture/authored-operation-effects.md new file mode 100644 index 000000000..1d838ac86 --- /dev/null +++ b/docs/architecture/authored-operation-effects.md @@ -0,0 +1,2017 @@ + + + +# Authored Operation Effects + +- **Status:** Architecture accepted, and a bounded first implementation + authorized, effective when + [flyingrobots/echo#889](https://github.com/flyingrobots/echo/pull/889) merges + to `main`. The detailed specification stays provisional until executable + evidence demonstrates it. [What merging accepts](#what-merging-accepts) + draws the line. Before that merge the whole document is a proposal and + governs nothing. **Not implemented.** Acceptance establishes the + architecture; it does not claim the bridge exists. The section + [Current implementation](#current-implementation) states what the runtime + does today. +- **Proposed:** 2026-10-15 in + [flyingrobots/echo#889](https://github.com/flyingrobots/echo/pull/889); + application context in + [flyingrobots/jedit#302](https://github.com/flyingrobots/jedit/pull/302) +- **Depends on:** [Application operation semantics authored in Edict source](../topics/GeneratedRules.md#application-operation-semantics-authored-in-edict-source) +- **Refines:** [ADR 0023](../adr/0023-admitted-executable-operation-packages.md) + and [ADR 0025](../adr/0025-scheduler-owned-executable-operation-actions.md) + for Actions whose program is evaluated Edict rather than a fixed + single-node profile +- **Supersedes in part:** for bridge Actions only, ADR 0023's + prepared-evaluation outcome: that a successful evaluation exposes one + normal Echo patch, that every evaluation yields a closed + `PreparedEchoOperationOutcomeV1` (`Committable` or `Obstructed`), and that + an `Obstructed` outcome never carries a patch digest. A bridge evaluation + yields an `EffectProposal` or a typed obstruction; Echo derives the patch + afterwards in the same Tick construction, and the receipt posture in + [Evidence](#evidence) replaces the closed outcome. Some obstructed postures + record the digest of a derived patch that was never committed. ADR 0023's + atomic visibility (one parent patch or one obstruction) still governs, and + every other Action keeps ADR 0023 unchanged. Each superseded passage is + marked in ADR 0023. +- **Supersedes in part:** for bridge Actions only, ADR 0025's requirements + that a successful evaluation return one complete prepared candidate and + that an evaluation obstruction return a lawpack-qualified coordinate. A + bridge evaluation returns an `EffectProposal`. Its program is compiled + from Edict source and binds no lawpack resource, so its typed obstruction + is qualified by the admitted package and installed-operation identities + instead. ADR 0025's other requirements, + including that neither result mutates the parent, still govern. The + superseded clause is marked in ADR 0025. +- **Related:** [Sliced Readings and Copy-on-Write Strands](sliced-readings-and-copy-on-write-strands.md), + [Generated Rule Authorship](../topics/GeneratedRules.md), + [WAL](../topics/WAL.md) + +## What merging accepts + +The maintainer decision of 2026-10-17 +([flyingrobots/echo#889](https://github.com/flyingrobots/echo/pull/889#issuecomment-6241449977)) +accepts this document at three strengths. Merging accepts the first two. It +does not ratify the third: those details become compatibility obligations +only alongside executable evidence. + +**1. Accepted architecture.** These govern from the merge: + +- Application operation semantics are authored in application-owned Edict + source; for Jedit's rope law, see + [Application operation semantics authored in Edict source](../topics/GeneratedRules.md#application-operation-semantics-authored-in-edict-source). +- The ownership boundary. The application owns behavior. Echo owns admission, + generic execution, witnessed reads, validation, derivation of the + authoritative patch, atomic publication, history, and recovery. Echo learns + no application vocabulary. No application callback, caller-supplied patch, + `MutationPlan`, or editor-specific intrinsic enters Echo. +- The five invariants under [Decision](#decision). Evaluation proposes typed + node, edge, and atom effects; it never performs them. +- Recovery verifies the original decision and never makes a new admission + decision. +- Deterministic resource behavior is correctness, not tuning. Evaluation is + charged deterministically against declared budgets. Every working structure + has a bounded capacity fixed before evaluation. A host allocation failure is + a host fault and never becomes an Action obstruction or any other recorded + outcome. Scratch history never becomes a semantic input: cold and warm + scratch produce identical evidence. +- **Unreachable records remain readable by key.** This is accepted + deliberately, with its cost: it constrains storage and reclamation. A + record that no root reaches any longer, such as a superseded rope chunk, + cannot be discarded for that reason alone. Reclamation must preserve what a + keyed read observes, or change it through an explicit, versioned semantic + mechanism. See [Basis, budget, retries](#basis-budget-retries). + +**2. Authorized first implementation.** The first bridge profile is bounded +as follows. Existing executable-operation profiles keep their current +behavior. + +- The five typed effects of [EffectProposal](#effectproposal). +- **Exact-basis validity.** A bridge Action is evaluated against the exact + commit parent. An Action whose evaluation basis is not the commit parent + obstructs with whole-frontier `BasisChanged` before evaluation. + **Dependency-scoped validity is deferred for this profile.** The text below + that specifies it (scoped eligibility, origin evaluation, the written-slot + history check, `HistoryChanged`, `OriginOnly`, and the scoped rows of + [Required tests](#required-tests)) is retained design for a later profile. + It is not an obligation of the first one. Jedit's structural edits already + need whole-frontier validity under this design, so deferring scoped + validity does not block the motivating rope operation. +- Witnessed reads, including observed absence and outgoing-edge ranges. +- Canonical validation with one specified obstruction precedence. +- Echo-derived patches, atomic publication, and receipt-bound evidence. +- Recovery that verifies the original decision. + +Exact-basis validity does not remove same-Tick conflicts. Two Actions +evaluated against the same parent can still invalidate each other's +observations, for example when one observes an empty outgoing-edge range and +the other inserts into it. Wherever the first profile allows concurrent +composition, range dependencies and complete conflict footprints remain +required. + +The first end-to-end witness is an authored edit that creates content, links +it, and moves a head atomically, and that a fresh engine then recovers. A +flat-text representation is acceptable for this milestone. It meets the first +acceptance target in the +[authorship decision](../topics/GeneratedRules.md#application-operation-semantics-authored-in-edict-source) +and does not complete the persistent rope. + +These witnesses decide whether the first profile is accepted. Each takes its +expected result from an independent source or an adversarial case, never from +a second implementation that shares the first one's assumptions: + +- several simultaneous violations produce the specified first obstruction + (Validation order); +- duplicate targets cannot disappear through patch deduplication (One effect + per slot); +- a forbidden read never reaches authored computation (Reads authorized + before use); +- a same-Tick edge insertion conflicts with a relevant range observation + (Negative reads); +- a failure on the last effect leaves no partial mutation (Atomicity); +- a stale exact parent produces no application mutation (Exact parent); +- cold and warm scratch produce identical evidence (Scratch independence); +- crash recovery reproduces committed, obstructed, and conflicting outcomes + without a new admission decision (Recovered outcomes). + +**3. Provisional specification.** Everything else here is a reviewed proposal, +not a compatibility obligation. That covers exact record layouts and byte +encodings, digest constructions, numeric codes, the specific order of the +validation steps, metering constants and charges, recovery variants, the +dependency-scoped and delayed-validity rules, and the physical zero-copy and +arena layouts. Each detail becomes an obligation when an executable check that +exercises it lands with independent expected results. Until then it may change +without a new decision. Bytes that enter an identity, a digest, or retained +evidence must be fixed and witnessed before the profile that writes them +ships. Physical layouts that no identity depends on can stay provisional +after that. + +## Decision + +An admitted executable operation whose program is compiled Edict may produce a +bounded set of graph effects. Evaluation proposes those effects. Echo witnesses +what the evaluation actually read and what it proposes to write, validates both +against the admitted contract and the basis, and commits all of the effects in +one Tick or none of them. + +Five invariants govern the design: + +1. **Evaluation is not commitment.** A successful evaluation yields a + proposal. Nothing it computes is authoritative until the scheduler commits + the Tick that contains it. +2. **The footprint is witnessed, not claimed.** The evaluator records every + slot it actually reads. The proposal states every slot it writes. Echo + checks both against the footprint law the package declares. A declaration + bounds the footprint; it never substitutes for it. +3. **Multi-node mutation is atomic.** A proposal commits whole within one Tick + and its decided-Tick WAL record, or it obstructs with no parent-visible + patch. A failed operation never leaves part of its effect in history. +4. **A proposal introduces no dangling reference.** Every edge a proposal + adds or retargets has endpoints that exist in the basis or are created in + the same proposal. In particular, a head that a proposal retargets is never + observable before every node and edge the proposal makes it reach has been + validated and committed in the same Tick. This invariant covers only the + edges a proposal introduces or retargets. It does not claim that the basis + is free of dangling edges: other writers do not check endpoints today (see + [Current implementation](#current-implementation)), and this design does not + validate the rest of the graph. +5. **A proposal identity names exactly one evaluated proposal.** Every outcome + that carries a proposal identity binds it to the exact effects the + evaluation produced, whether those effects committed or were rejected. A + rejected proposal is never ambiguous on replay or audit: re-deriving it over + the recorded basis must reproduce effects that hash to the recorded + identity and the recorded target-set digest, and, where a patch was + derived, the recorded write-set and patch digests. Each slot is the target + of at most one effect, so the derived patch applies every effect the + identity names. + +Echo learns no application vocabulary. A proposal is nodes, edges, and atoms. + +## Current implementation + +- Echo main admits two executable programs: anchored single-node alpha-atom + compare-and-set and create-if-absent. Both write bytes supplied by the + invocation (`crates/warp-core/src/echo_operation.rs`). +- `edict_pure` and `edict_read` evaluate compiled Edict values, but no admitted + path turns their results into writes. `edict_read` reads alpha atoms by + explicit node key; it cannot follow edges. It counts reads against a limit + but does not record which slots it read + (`crates/warp-core/src/edict_read/evaluate.rs`). +- Create-if-absent obstructs when the node already exists, even with identical + content. +- `GraphStore::upsert_edge_record` does not check that an edge's endpoints + exist (`crates/warp-core/src/graph.rs`). +- Footprint independence is a set test: any write overlapping another Action's + read or write conflicts, including two identical writes + (`crates/warp-core/src/footprint.rs`, `Footprint::independent`). Its key + sets are nodes, edges, attachments, ports, and, since + [flyingrobots/echo#917](https://github.com/flyingrobots/echo/pull/917), + outgoing-edge ranges: an `OutgoingEdgeRange` names one source node + (including its WARP) and one edge type, and a footprint claims ranges read + (`r_read`, including an observed empty range) and ranges written + (`r_write`). A write to a range conflicts with another Action's read or + write of it, so a declared empty range conflicts with an insertion into it + under a fresh edge id. Range keys take part in footprint and patch + identities (`SlotId::OutgoingEdges` in `crates/warp-core/src/tick_patch.rs`) + and survive scheduling, retained patches, provenance, and admission. Range + conflicts participate in blocker computation: a rejected Action records the + indices of the earlier Actions that blocked it, not the exact conflicting + range. The limits: range claims + are declared, not witnessed. No graph accessor or edge writer records them + automatically. A range claim does not cover the source node's presence, + which needs its own node dependency. No Edict program gains graph mutation + authority from it. The automatic witnessed reads, complete effect write + claims, exact-parent effect validation, and fresh-engine recovery that this + design requires remain to be built. +- `WarpTickPatchV1::new` keeps one operation per canonical sort key, the last + one supplied, and silently drops earlier operations with the same key + (`crates/warp-core/src/tick_patch.rs`). +- The retained provenance record `EPRV0003` writes each receipt entry as rule, + scope hash, scope, disposition, and blockers, with no per-entry length or + version (`crates/warp-core/src/provenance_codec.rs`). +- An executable-operation Action batch selects at most 64 candidates + (`ACTION_BATCH_CANDIDATE_LIMIT_V1`) and accepts at most 128 patch operations + summed over its accepted Actions (`ACTION_BATCH_OPERATION_LIMIT_V1`); a + candidate that would exceed the operation limit is obstructed rather than + accepted (`crates/warp-core/src/echo_operation.rs`). These are Action-batch + composition limits, not Tick limits: `WarpTickPatchV1::new` accepts an + operation vector of any length. +- Recovery verifies each decided Action by outcome class + (`crates/warp-core/src/trusted_runtime_host.rs`, ADR 0025). First, for + every class, it recomputes the Action's basis posture against the scheduler + Tick's parent and refuses history where the recorded posture disagrees. + Then: + - **Committed and `RejectedFootprintConflict`:** it reconstructs the + preparation from the recovered parent state and refuses history whose + package, installed-operation, invocation, basis, private-evaluation, + patch, result, footprint, or preparation identity differs from the + recorded evidence. + - **Obstructed `BasisChanged`:** it verifies the invocation-admission + evidence and the recomputed basis posture. It does not re-evaluate the + Action. + - **Other obstructions:** it re-evaluates the Action and requires the same + pre-decision evidence, except that a scheduler-assigned `BudgetExceeded` + (an Action-batch limit, decided after a successful evaluation) is accepted + as a reconstructed preparation and verified through the batch + reconstruction below. Finally, for every Action Tick and every outcome + class, it reconstructs the whole Action batch's composition over the + recovered parent state and refuses history where any reconstructed outcome + differs from the recorded one; for each `RejectedFootprintConflict` it + also recomputes the blocking earlier Actions and requires them to equal + the recorded blockers. +- `echo_operation_written_slots_v1` collects the slots written between an + origin and a commit parent by unioning each retained replay patch's + `out_slots`. `WarpTickPatchV1::new` accepts `out_slots` independently of + its operations, and only debug builds or `footprint_enforce_release` check + that a rewrite stays inside its declared footprint. +- The state root is a full walk of the reachable graph on every commit. See the + open state-root decision in + [Sliced Readings and Copy-on-Write Strands](sliced-readings-and-copy-on-write-strands.md#open-decisions-that-bound-these-laws). + +## Lifecycle + +```text +admitted package + invocation at an exact basis +-> scheduler selects the Action while constructing a Tick +-> bounded evaluation over a sliced reading of that basis + records: every slot read, steps, allocation + yields: a canonical EffectProposal, or a typed obstruction +-> validation against the package's footprint law, budget, authority, + identity law, and the basis +-> composition with other Actions under the existing independence rule +-> one decided Tick: patch, receipt, decided-Tick WAL record +``` + +Evaluation runs inside Tick construction, as ADR 0025 already requires for +Actions. Proposals are not persisted on their own. Recovery replays decided +Ticks and verifies each decided Action by its outcome class: it re-derives the +evaluation for the classes whose check does so, and verifies a `BasisChanged` +decided before evaluation without re-evaluating it (see [Recovery](#recovery)). +A pending Action is evaluated after recovery when the scheduler selects it. +Re-derivation is sound because evaluation is deterministic over a fixed +basis. + +## EffectProposal + +A proposal is a canonical value with a domain-separated identity: + +```text +EffectProposal { + basis exact parent coordinate evaluated against + readSet slots read: node, alpha atom, outgoing edges by type + effects [ in canonical order + EnsureNode { node, type, atom } create, or require identical + CreateNode { node, type, atom } require absent + ReplaceAtom { node, expectedAtomDigest, atom } + EnsureEdge { edge, from, to, type } create, or require identical + ReplaceEdge { edge, expectedTo, to } retarget an existing edge + ] + result compiler-declared application result bytes + cost steps, read bytes, write bytes; allocated bytes +} +``` + +Every `node` is an instance-scoped `NodeKey { warp_id, local_id }` and every +`edge` an `EdgeKey`. An edge's `from`, `to`, and `expectedTo` are local node +ids in the edge's own warp, because a `GraphStore` holds one warp and an +`EdgeRecord`'s endpoints are local `NodeId`s within it. For `EnsureNode` and +`CreateNode`, `type` is the node record's type; for `EnsureEdge` it is the edge +record's type (`EdgeRecord.ty`), validated against the edge types the schema +admits, never against node types. `atom` is an +`AtomPayload { type_id, bytes }`: its `type_id` is a separate proposition from +the node type, and the +[two-plane law](../invariants/warp-two-plane-law.md) (L3) requires it in every +encoding and digest that includes the bytes. `ReplaceAtom` replaces both the +payload type and the bytes, and its `expectedAtomDigest` covers both. + +Rules: + +- **Effects are the only writes.** The proposal contains no prepared patch. + Echo derives the patch from the effects. +- **Patch constructor.** The derived patch is built by + `WarpTickPatchV1::new`, as the fixed-profile path builds its patch, with + these arguments: + - `policy_id`: the scheduler's policy id for the Tick; + - `rule_pack_id`: the installed-operation identity; + - `commit_status`: `Committed`; + - `in_slots`: every node, edge, and attachment slot in the read set, the + precondition and resolution slots, and the portal chains. A range key + has no `SlotId` form, so it is not listed here; the write-set and + read-set digests cover it; + - `out_slots`: the write set's node, edge, and attachment slots; + - `ops`, in canonical effect order: `UpsertNode` then `SetAttachment` for + a creating `EnsureNode` or `CreateNode`, and nothing for an identical + `EnsureNode`; `SetAttachment` for `ReplaceAtom`; `UpsertEdge` for a + creating `EnsureEdge`, and nothing for an identical one; and + `UpsertEdge` with the same id and the new target for `ReplaceEdge`. + + The constructor sorts and deduplicates slots and operations itself. The + patch digest is `WarpTickPatchV1::digest` of that value, which hashes every + argument above. + +- **Canonical order.** Echo sorts the effects the evaluator emits; the order in + which evaluation produced them never reaches the identity. Each effect has a + primary slot: the node record for `EnsureNode` and `CreateNode`, the atom for + `ReplaceAtom`, and the edge for `EnsureEdge` and `ReplaceEdge`. Effects sort + by the primary slot's class (node record, then attachment, then edge), then by + its warp id bytes, then its local id bytes, compared lexicographically. A tie + can occur only in a proposal that obstructs with `DuplicateEffectTarget`; it + breaks by effect kind (`EnsureNode`, `CreateNode`, `ReplaceAtom`, + `EnsureEdge`, `ReplaceEdge`), then by the effect's `EffectRow` bytes with its + `atom` range zeroed, then by its atom bytes (see [Encoding and + memory](#encoding-and-memory)); every semantic field of the effect, expected + values included, is in those bytes. Blob ranges are assigned only after + sorting, so emission order never reaches them. Sorting never removes an + effect, so duplicates stay visible to the one-effect-per-slot rule. +- **One effect per slot.** No two effects in one proposal may target the same + slot: one node record, one node's atom, or one edge. Targets are compared + by canonical slot identity (the node id, the node id's atom, or the edge + id), never by the effect's kind or form, so differently expressed effects + cannot reach one slot undetected. `EnsureNode` and `CreateNode` target the + node record and its atom, so an `EnsureNode` plus a `ReplaceAtom` of the + same node collide, and an `EnsureEdge` plus a `ReplaceEdge` of the same + edge id collide. A collision is a typed `DuplicateEffectTarget` obstruction + before any patch is derived. Without this rule `WarpTickPatchV1::new` would + keep only the last operation per key and silently drop effects the proposal + identity names. +- **Slots.** One canonical slot model serves the target set, the write set, + the read set, and the footprint. A slot is a node record, an attachment, an + edge, or an outgoing-edge range key `(source node, edge type)` (see + [Witnessed reads](#witnessed-reads-over-a-bounded-slice)). An attachment + slot is an `AttachmentKey`: an owner node or edge and a plane. A node's + atom is its alpha attachment. The same slot can instead hold a portal + (`AttachmentValue::Descend`), so a write of an atom and a read of a portal + on one node meet in one slot and conflict. Every slot is instance-scoped: + node records and node attachments by `NodeKey`, edges and edge attachments + by `EdgeKey`, and a range key by its source `NodeKey`, so equal local ids + in different warps are different slots. +- **Portal chain.** When an effect or a read names a key in a descended + warp, the footprint and a scoped Action's dependency set (kind `5`) + include every portal attachment on the validated root-to-target + reachability chain. Portals an effect's chain crosses are not part of the + read set, which holds exactly what the program's view resolved, as + [Generated Rule Authorship](../topics/GeneratedRules.md) requires for + descended targets and as Echo's existing descent check already reads + them. Each is a `ValueDigest` dependency on its `Descend` target. A + co-scheduled write to a portal therefore conflicts, and a portal that + changed between origin and commit parent, even if restored, obstructs with + `BasisChanged`. Effects never write a portal. Every key an effect names + must lie in the root warp or in a warp reached by a valid root-to-target + chain at the basis; a key in a missing or unreachable warp is a typed + `UnreachableWarp` obstruction, posture `Proposed`, `NotDerived`, decided + before any patch is derived. +- **Target set.** The proposal's target set is the canonical set of slots its + effects target: for `EnsureNode` and `CreateNode` the node record and its + atom, for `ReplaceAtom` the atom, and for `EnsureEdge` and `ReplaceEdge` the + edge. It is a function of the effects alone, defined for every proposal + before validation, and its digest is part of the evidence. +- **Write set.** The proposal's write set is the target set less the slots of + each `Ensure` whose target already exists identically in the basis (those + are reads), plus the outgoing-edge range key of every edge the proposal + creates or retargets: the `(from, type)` of a creating `EnsureEdge`, and the + source and type of the basis edge a `ReplaceEdge` retargets. Range keys + depend on the basis, so the write set is known only once validation has + resolved each effect against it. +- **Effect preconditions.** Each effect states what must hold for it to + apply, whether or not the program read it: + - `CreateNode`: the node record and its atom are both absent. If either + exists, including an atom without a node record, the effect obstructs + with `PreconditionMismatch`, as today's create-if-absent does; + - `EnsureNode`: the node record and its atom are both absent, or both + present with identical node type, atom `type_id`, and atom bytes. Any + other state, including a record without an atom or an atom without a + record, is `ContentIdentityConflict`; + - `EnsureEdge`: the edge is absent, or present with identical endpoints + and type; + - `ReplaceAtom`: the node record exists, else `NodeMissing` (as today's + compare-and-set reports), and its alpha slot holds an atom + (`AttachmentValue::Atom`) with the expected digest, else + `PreconditionMismatch`. A slot holding a portal is therefore + `PreconditionMismatch`, decided before any patch is derived, never a + portal removed by the patch. An orphan atom without its record never + satisfies a `ReplaceAtom` either; + - `ReplaceEdge`: the edge exists with the expected target; + - a creating `EnsureEdge` and every `ReplaceEdge`: each endpoint the + edge will name (`from` and `to`, or the retargeted edge's source and + the new `to`) exists, unless the same proposal creates it. An + `EnsureEdge` that finds an identical edge is a read; it adds and + retargets nothing, so its target is not checked, as invariant 4 and + [Visibility and referential integrity](#visibility-and-referential-integrity) + limit endpoint checks to edges the proposal introduces or retargets. + Its source must still exist, because the identity law reads the + source's type to check the edge's id; a missing source is + `DanglingReference` at step 8, for an identical `EnsureEdge` as for a + creating one; + + Every precondition slot is a read in the Action's footprint, is checked by + validation, and belongs to the dependency set of a dependency-scoped Action + (see [Basis, budget, retries](#basis-budget-retries)). + +- **Ensure is idempotent only on identity.** An `EnsureNode` whose node exists + with identical type and atom adds nothing to the patch and counts as a read. + An existing node with different content is a typed + `ContentIdentityConflict` obstruction. The same holds for `EnsureEdge`. This + is the idempotent create profile that Edict's I-022 requires before + duplicate content-addressed creation can be lawful. +- **Compare-before-replace.** `ReplaceAtom` and `ReplaceEdge` carry the value + they expect. A mismatch is a typed `PreconditionMismatch` obstruction, the + kind today's compare-and-set uses, with posture `Proposed`, `NotDerived`. + It is never a merge. It is distinct from `BasisChanged`, which reports a + dependency that changed after the origin (see + [Basis, budget, retries](#basis-budget-retries)). +- **No deletes in this profile.** Persistent structures do not need them. + Deletion needs its own design. +- **Identity derivation is the program's.** Echo checks that each node and edge + id matches the identity law the package declares, so ids cannot be chosen to + collide with unrelated nodes. A node or edge id that does not match is a + typed `IdentityLawViolation` obstruction before any patch is derived. Echo + does not invent ids. + +### Identity laws + +A package names its identity law by number, and Echo recomputes ids under it; +a digest alone could not be executed. One law is defined: + +- **`1`, `ContentAddressV1`.** It applies by node type: the package's + schema marks each node type `content` or `mutable`, and a record's type, + which every record carries, decides, so no creation history is needed. An + edge follows its source node's type. + - A **content** node is created only by an `EnsureNode` whose id is its + content address, together with every outgoing edge it will ever have, + each by an `EnsureEdge` in the same proposal. It is immutable + afterwards: a `ReplaceAtom` of it, a `ReplaceEdge` of an edge from it, + a creating `EnsureEdge` from it in a later proposal, or a `CreateNode` + of a content type is `IdentityLawViolation`. + - A **mutable** node, such as an application's anchor (the buffer `B` + in the trace), has a program-chosen id. It is created only by a + `CreateNode`, which requires the id to be absent, and it may be + replaced. An `EnsureNode` of a mutable type is `IdentityLawViolation`. + - A content node's id is BLAKE3 over `echo.bridge.node-id.v1\0`, the + warp id, the node type id, the attachment value digest of its atom (see + [Evidence](#evidence)), the number of its outgoing edges as a + little-endian `u64`, and, for each edge sorted by edge type id and then + `to` local id, the edge type id and the `to` local id. Those are exactly + the edges its creating proposal's `EnsureEdge` effects give it. + - An edge from a content node has the content id BLAKE3 over + `echo.bridge.edge-id.v1\0`, the warp id, the `from` local id, the edge + type id, and the `to` local id. It is immutable, like its source. + - An edge from a mutable node has the slot id BLAKE3 over + `echo.bridge.slot-edge-id.v1\0`, the warp id, the `from` local id, and the + edge type id: one edge per source and type, whose id stays the same when a + `ReplaceEdge` retargets it. A creating `EnsureEdge` of it must carry that + id. Because a non-bridge writer can store an edge under any id, step 2 + scans the source's whole outgoing bucket (see [Validation + reads](#basis-budget-retries)) for every `EnsureEdge` and `ReplaceEdge` + from a mutable source. Any other edge of the same type from that source is + an alias, and the effect obstructs with `IdentityLawViolation`. + + An `EnsureNode` whose content-typed target already exists adopts it only + if the existing node's record, atom, and complete outgoing edge set equal + what the proposal gives it. Echo then recomputes the id from those, so a + node written under some other id is never adopted; a mismatch is + `IdentityLawViolation`. + + Echo recomputes every id a proposal creates, and the id of every edge a + `ReplaceEdge` or an identical `EnsureEdge` resolves from the basis (its + slot or content id from the resolved record's source, type, and, for a + content edge, target), and refuses a mismatch with `IdentityLawViolation`. + A basis edge written by a non-bridge writer under some other id is + therefore never adopted. `ReplaceAtom` names an existing mutable node, + whose id is program-chosen. + All ids are 32 bytes. A content node's id therefore commits to its content + and its children, as Jim's rope requires, and no later effect can make it + stale. A program computes the same BLAKE3 inputs; Edict must expose them + before an effect package can be produced. + +## Witnessed reads over a bounded slice + +The program never declares what it read. Evaluation reaches state only through +a recording view over the basis, and the read set is exactly the set of slots +that view resolved: node records, alpha atoms, and outgoing edges by type. A +program has no other path to state, so the record is complete by construction. +This needs new instrumentation; today's `edict_read` only counts reads. + +Absence is a dependency too. Every resolution is recorded with its outcome, +against the basis it was resolved at: + +| Resolution | Recorded dependency | +| -------------------------------------- | ---------------------------------------------------------------------- | +| node or atom present | the slot and a digest of its value | +| node or atom absent | the slot, observed absent | +| outgoing edges of one type from a node | the source node and type, with the target set observed, empty included | + +An `Ensure` that finds no existing node depends on that absence, so a +co-scheduled Action that creates the slot invalidates it like any other +changed read. + +A read of the outgoing edges of one type from a node is a range, not a set of +known edge ids, so it needs its own footprint key. With edge ids alone, if +Action A observes no `canonicalHead` edge from `B` and co-scheduled Action B +creates a fresh one, their edge-id sets are disjoint and the test calls them +independent, although A's observed absence no longer holds. Echo's +`Footprint` has carried that key since +[flyingrobots/echo#917](https://github.com/flyingrobots/echo/pull/917): an +`OutgoingEdgeRange` `(source node, edge type)`, claimed in `r_read` and +`r_write`. Independence treats range keys like every other key: a write +against a read or write conflicts. What #917 does not do, and the bridge +must, is make the claims witnessed rather than declared. A range read claims +its range as a read. Every effect that creates or retargets an edge with that +source and type claims it as a write, in addition to the edge id. + +A range read is checked and metered before it materializes anything. A +range read of an edge type outside the footprint law's `range_edge_types` +obstructs evaluation at once (`FootprintLawViolation`, posture `NoProposal`), +before it reads anything, so a package whose law admits no range read can +never produce a proposal that depends on one, and its static scoped +eligibility holds. For an admitted type, the view takes the length of the +source node's whole outgoing bucket, without copying an edge. `GraphStore` +keeps one bucket per source, not per type, so finding the matching edges +inspects every edge in it; the view therefore charges one step and 64 +`read_bytes` for every edge in the bucket, matching or not, and compares the +bucket length, not the match count, with `max_range_edges`. If the length +exceeds `max_range_edges`, or the charge exceeds the remaining budget, +evaluation obstructs with `BudgetExceeded`, posture `NoProposal`, before any +edge is inspected. Otherwise the view writes the matching edges' +`EdgePairRow`s directly into the arena. Consumed cost and the read set +therefore depend only on the basis, and a high-degree node cannot force work +or allocation the budget did not cover. + +These dependency kinds follow the +[Action validity across ticks](../topics/GeneratedRules.md#action-validity-across-ticks) +decision (#837). Value and single-key absence dependencies are the kinds that +decision +supports. A read of outgoing edges by type is a topology dependency, which that +decision does not yet support. Eligibility is decided statically at admission, +never by the branch an evaluation takes. An Action keeps the whole-frontier +rule, whatever this invocation does, and commits only onto the exact basis it +was evaluated against, when its package's footprint law admits any of: + +- an outgoing-edge range read (a non-empty `range_edge_types`); +- an edge write (a non-empty `write_edge_types`). Creating or retargeting an + edge from a mutable source requires that no other edge of its type leave + that source, and that depends on the source's whole bucket; +- a write of a content-addressed node type. Adopting an existing content node + requires its whole outgoing edge set to match; +- node creation (a non-empty `write_node_types`). Creating a node requires its + outgoing bucket to be empty, which depends on the whole bucket. + +Each of these is a topology dependency: a write from outside the bridge (the +unrestricted `UpsertEdge` path) can add an edge to a bucket without changing any +single slot a scoped Action recorded. Every other bridge Action is eligible for +dependency-scoped validity; its writes are atoms of existing mutable nodes. +Widening that requires sound edge-set tracking under #837, not a looser rule +here. + +The view resolves each slot on demand from the basis, as +[Sliced Readings and Copy-on-Write Strands](sliced-readings-and-copy-on-write-strands.md) +law 1 requires. The contract never depends on a complete materialized graph: +the read limit and the footprint law bound the slice. A range read beyond +`max_range_edges` or the budget obstructs evaluation itself (`BudgetExceeded`, +`NoProposal`), since it would materialize data. Every other read is authorized +by the view before its value reaches the program: a node, atom, or portal read +whose type (as `read_type` records it) is outside the law's read permissions, +or that would take the read set past `max_reads`, obstructs evaluation at once +with `FootprintLawViolation`, posture `NoProposal`, and the program never sees +the value. A read of a key in a descended warp first resolves its +root-to-target chain, as validation step 1 does for effect keys: each portal +crossed is charged, its owner authorized against `portal_owner_types`, and an +unreachable warp obstructs evaluation with `UnreachableWarp`, posture +`NoProposal`, before anything in it is read. So a forbidden or unreachable +value can never shape an evaluation obstruction, whatever exit the program takes +after the read. + +A read that may find nothing names the type it expects: a node read names a node +type, and an atom read names an atom `type_id`. The view records the authorizing +type in every node and atom `ReadRow`'s `read_type` field: the record's actual +type when the read finds one, and the type the read named when it finds nothing. +The footprint law's `read_node_types` or `atom_types` decides from that field +whether each read is permitted, live and on recovery alike. An atom read of an +alpha slot that holds a portal (`Descend`) has the outcome `portal`: the program +sees the portal, never an atom. The view also reads the slot owner's node +record, charged as a node-record read, and records the owner's node type as the +row's `read_type`, with the portal's attachment value digest as `subject`. The +read is authorized when that type is in `portal_owner_types`, decided from the +row alone, live and on recovery. The portal is a `ValueDigest` dependency, and +the owner record is a resolved-record dependency, like any present value. A first +implementation may still sit on today's fully materialized worldline state, but +nothing in this contract may rely on that. + +## Footprint law + +### Set encoding + +Every set-valued field in a footprint law or a schema is a CBOR array of +distinct elements in strictly ascending order. An id is a 32-byte byte string, +ordered bytewise. A pair is a two-element array ordered by its first element, +then its second. Admission refuses a law or schema with an unsorted or +duplicated set, rather than normalizing it. Record maps (`footprint-law`, +`graph-schema`, `node-type`) have the fixed text keys shown. The id-keyed maps +`node_types` and `edge_types` have 32-byte byte-string keys, each id at most +once. `edict.canonical-cbor/v1` orders map keys by their encoded bytes, which +for these equal-length keys is bytewise order of the ids. The complete shapes, +in CDDL, are: + +```text +footprint-law = { + "read_node_types": [* id], "write_node_types": [* id], + "atom_types": [* id], "range_edge_types": [* id], + "write_edge_types": [* id], "portal_owner_types": [* id], + "max_reads": uint, "max_writes": uint, "max_range_edges": uint, +} +graph-schema = { + "node_types": { * id => node-type }, + "edge_types": { * id => [* endpoint-pair] }, +} +node-type = { "addressing": 0 / 1, "atom_types": [* id] } ; 0 content, 1 mutable +endpoint-pair = [source: id, target: id] +id = bstr .size 32 +``` + +No other key may appear, and every key shown is required, so each law and +schema has exactly one encoding and one identity. + +The package declares a footprint law, fixed per package with no invocation +parameters. It is an `edict.canonical-cbor/v1` map, in the exact shape that [Set +encoding](#set-encoding) gives, with these entries: `read_node_types` and +`write_node_types` (sets of node type ids), `atom_types` (the atom `type_id`s it +may read or write), `range_edge_types` (edge types it may read as outgoing +ranges; empty makes it eligible for scoped validity), `write_edge_types`, the +unsigned counts `max_reads` (at most 4,096), `max_writes` (at most 256), and +`max_range_edges` (per range read, at most 65,536), which admission checks +against these effect-profile ceilings so no law can overflow the arena's sizing +arithmetic, and `portal_owner_types` (node types whose alpha portals an effect or +read in a descended warp may cross; empty confines the package to its root +warp). Each portal on a validated chain must be owned by a node of one of these +types, or validation obstructs with `FootprintLawViolation`. The bridge does not +traverse edge-owned (beta) portals: an edge has no node type for this law to +admit, so a chain crossing one is `FootprintLawViolation` at step 1, before any +owner record is read. The counts are taken after deduplication: +`max_reads` bounds the rows of the witnessed read set (one per slot, or one per +named type for an absent slot read under several types; see the sort orders in +[Encoding and memory](#encoding-and-memory)), where one range read is one row (its +range key) and its edges are bounded by `max_range_edges`; `max_writes` bounds +the resolved write set after Ensure resolution, range keys included, so an +identical Ensure adds nothing. Validation reads are bounded by the budget, not +by `max_reads`. The law's canonical bytes are part of the program's identity. At +validation Echo checks: + +- every node type, atom `type_id`, and edge type an effect writes is admitted + by the package's typed graph and attachment schema, which ADR 0023 requires + the package to bind, including which atom types a node type may carry. A + violation is a typed `SchemaViolation` obstruction, posture `Proposed`, + `NotDerived`; + +- the witnessed read set, the precondition slots, and the proposal's target + set lie inside the law; +- counts do not exceed the declared maxima; +- once validation has resolved each effect against the basis, the complete + write set, range keys included, and its counts lie inside the law. A range + key is known only after resolution: a `ReplaceEdge` whose basis edge has a + source or type outside the law fails here, before any patch exists; +- the derived patch's actual footprint equals the proposal's write set (see + [EffectProposal](#effectproposal)). The actual footprint is computed in the + same slot model: each node upsert writes the node record, each attachment + set writes the node's atom, and each edge upsert writes the edge and the + range key of its source and type. + +The schema check yields a typed `SchemaViolation` obstruction and the law +checks a typed `FootprintLawViolation`; both run before any patch is derived, +with patch tag `NotDerived`, at the steps [Validation order](#validation-order) +gives them, after the facts an effect does not carry have been resolved. The +patch equality can only run after derivation; a mismatch is a typed +`FootprintMismatch` obstruction with patch tag `Derived`, recording the patch +digest it compared. Neither commits a patch. +Independence between Actions in one Tick uses the witnessed footprints, +including outgoing-edge range keys, under the existing rule: write against read +or write conflicts, read against read does not. + +Reading a large shared subtree costs footprint entries but never conflicts. + +An `Ensure` of a node or edge that already exists identically in the basis is +a read, not a write, so Actions that share existing structure do not conflict. +Two Actions in one Tick that both create the same new content-addressed node +do write the same slot, and the existing rule makes the later one obstruct. +This design adds no merge rule for identical writes. Every Action's write +set, and so whether its `Ensure` is a read, is resolved against the Tick's +commit parent, never against the writes of Actions accepted earlier in the +same Tick. A later Action therefore cannot turn an earlier Action's new node +into a read of its own, even under dependency-scoped validity, whose value +comparison runs at the validation position. The rejected Action's +outcome is final (see Retries); a new submission evaluated later finds the +node in its basis, so its `Ensure` is a read and does not conflict. + +## Validation order + +Validation of a proposal runs in one fixed order, and the first failing step +decides the outcome, so a proposal that breaks several rules has exactly one +recorded obstruction: + +1. warp reachability, at the evaluation basis, of every effect key and every + key in the witnessed read set that lies in a descended warp: root first, + effect keys in canonical effect order and then read keys in slot order, + each chain crossed once. Each portal crossed costs one step + and 64 `read_bytes`, charged before it is read; a crossing the remaining + budget cannot cover is `BudgetExceeded`. A portal owned by a node whose + type is not in the footprint law's `portal_owner_types` is + `FootprintLawViolation`; reading the owner's node record to check that + costs one more step and 64 `read_bytes`. A key in a missing or unreachable + warp is `UnreachableWarp`, decided before any record is looked up. A warp + unreachable at a scoped Action's origin obstructs even if a later Tick + made it reachable. Each portal attachment and each portal owner's node + record are dependencies (kind `5`), so step 3 catches a change to either, + including an owner whose type changed; +2. resolution at the evaluation basis (for a scoped Action, its origin): in + canonical effect order, read every record validation needs. That is the + target of each `EnsureNode` and `CreateNode`, both its node record and its + alpha atom slot, and the target edge record of each `EnsureEdge`, present or + absent, which decides whether the effect writes or only confirms; for an + `EnsureNode` whose content-typed target exists, a scan of that node's whole + outgoing bucket and a hash of its atom. Those are compared with the proposal + here: an existing node whose type, atom, or outgoing edges differ from what + the proposal gives it is `ContentIdentityConflict` at this step, so the + identity law at step 6 sees only content that matches. For every node the + proposal creates, its outgoing bucket's length, which must be zero, since a + node cannot be created over edges a non-bridge writer left under its id + (`PreconditionMismatch` otherwise); each `ReplaceAtom`'s node record and + current alpha value, hashed so its type and digest are known before the + footprint law; each `ReplaceEdge`'s edge record; the source node record of + every `EnsureEdge` and `ReplaceEdge`, whose type selects the edge-id rule, + and, when that source is mutable, its whole outgoing bucket for the alias + check; and the target node record of a creating `EnsureEdge` or a + `ReplaceEdge`, each unless the proposal creates that node. Charges follow + [Validation reads](#basis-budget-retries). Failures are `NodeMissing` for a + `ReplaceAtom`'s missing node, `PreconditionMismatch` for a missing edge, + `ContentIdentityConflict` for an existing content node that differs from the + proposal, or `BudgetExceeded`; whether a present target matches is decided at + step 8, and a missing endpoint is reported as `DanglingReference` there. + Every record read here is a dependency (kind `4`): `ValueDigest` when present + and `Absence` when absent, so step 3 catches a target or endpoint that an + intervening Tick created, changed, or removed. After this step the complete + write set is known; +3. the dependency-scoped history check, for a scoped Action + (`BasisChanged`); +4. one effect per slot (`DuplicateEffectTarget`); +5. the schema (`SchemaViolation`), before the identity law, which reads the + schema's node-type addressing. Every node type, edge type, and atom + `type_id` an effect carries or step 2 resolved must be admitted; a node + type must admit its atom type (for `EnsureNode`, `CreateNode`, and a + `ReplaceAtom`'s resolved owner); a `ReplaceEdge`'s preserved edge type + must be admitted; and for every creating `EnsureEdge` and every + `ReplaceEdge`, the schema must admit the edge between its source and + target node types, taken from the resolved records or from the + proposal's own node effects. An endpoint step 2 found absent has no type + and is skipped here; +6. the identity law (`IdentityLawViolation`). An edge whose source step 2 + found absent, and the proposal does not create, has no source type to + select its id rule, so this step skips it; it is `DanglingReference` at + step 8, as an absent endpoint is at step 5; +7. the footprint law, now that every slot is known (`FootprintLawViolation`). + The witnessed read set was authorized read by read during evaluation; this + step rechecks it from the recorded rows, as recovery does. The target set + and the resolved write set, with + its range keys, must lie inside its write permissions. The counts must not + exceed its maxima. Each effect is permitted, and the slots it implies are + authorized, exactly as this table gives; an implied slot found absent needs + no type and passes here (an absent endpoint is `DanglingReference` at step + 8): + + | Effect | Its write requires | Each present implied record requires | + | -------------------------- | ---------------------------------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------- | + | `EnsureNode`, `CreateNode` | node type in `write_node_types`; atom type in `atom_types` | the existing target's node type in `read_node_types`; its atom type in `atom_types`; each scanned bucket edge's type in `write_edge_types` or `range_edge_types` | + | `ReplaceAtom` | new atom type in `atom_types` | owner node type in `read_node_types`; current atom type in `atom_types` | + | `EnsureEdge` | edge type in `write_edge_types` | source and target node types in `read_node_types`; bucket edges' types in `write_edge_types` or `range_edge_types` | + | `ReplaceEdge` | edge type in `write_edge_types` | source and new target node types in `read_node_types` (the old target is never read); bucket edges as for `EnsureEdge` | + + So an Action that only replaces atoms of existing nodes needs no + `write_node_types`, as dependency-scoped validity requires; + +8. the remaining effect preconditions, effect by effect in canonical order, + and within an effect in the order its precondition list gives + (`PreconditionMismatch`, `ContentIdentityConflict`, `DanglingReference`, + or `BudgetExceeded` when a validation read exceeds the remaining budget); +9. patch derivation and the actual-footprint equality + (`FootprintMismatch`); +10. composition (`RejectedFootprintConflict`); +11. the Action-batch operation limit (`BudgetExceeded`), tested only for a + candidate with no blockers, as today's scheduler does. + +Steps 1 through 8 yield `NotDerived`, and steps 9 through 11 yield +`Derived`. Within a step that examines several effects, the first failing +effect in canonical order decides. Steps 1, 2, and 8 can yield more than one +kind; within step 1 a crossing is charged, then its owner checked, then the +next portal read. + +## Visibility and referential integrity + +Validation enforces invariant 4 before a proposal can join a Tick, through +the endpoint preconditions defined in [EffectProposal](#effectproposal): + +- every creating `EnsureEdge` and every `ReplaceEdge` endpoint exists in the + basis or is + created by an `EnsureNode` or `CreateNode` in the same proposal; +- every edge a `ReplaceEdge` retargets exists in the basis with the expected + target. + +A missing endpoint is a typed `DanglingReference` obstruction with no patch. +Because endpoints are precondition reads, a co-scheduled Action that writes +one conflicts, and a delayed Action whose endpoint changed in the intervening +history obstructs with `BasisChanged`, even if the endpoint was restored. + +Validation examines only the edges the proposal adds or retargets, and the +endpoints those edges name. An existing dangling edge elsewhere in the basis +neither obstructs an unrelated proposal nor is repaired by it. Whether Echo +should reject dangling edges from every writer is a separate decision. + +Commit then makes partial visibility impossible by construction. All of an +Action's effects belong to one Tick. Observers, readings, and later Actions bind +to committed Tick coordinates, and a Tick is published only after its decided +WAL record. The order of operations inside the Tick's patch is therefore never +observable: the coordinate before the Tick shows the old head, and the +coordinate after shows the new head with every node and edge the proposal +introduced. Pre-existing structure the head now reaches is whatever the basis +held; this design validates only what the proposal adds or retargets. + +## Basis, budget, retries + +- **Basis.** Reads, including observed absences, are taken from the exact + basis: the materialized state at that coordinate, which replaying the + worldline's patches determines exactly. That state includes records no + longer reachable from a root, and a keyed read resolves them. This is + observable bridge semantics, not a storage detail: a record leaves the + state only through a patch that deletes it, and no host may drop one + outside a Tick. Retention governs only the history before a coordinate. + The state root does not commit to unreachable records, so a keyed read of + one is bound by the coordinate and replay. Any future reclamation of + unreachable records must either preserve what a keyed read observes, for + example by deleting them in a Tick's patch, or ship as a new version of + these semantics; it can never silently change what an Action reads. At commit, + every `expected…` value and every recorded dependency that a co-scheduled + Action wrote must still hold; an overlap with an earlier accepted Action in + the same Tick is `RejectedFootprintConflict` (see **Within one Tick** below). + Action validity across ticks keeps its existing rules, and an Action is never + re-stamped as if it had been evaluated against a later basis. +- **Two kinds of basis change.** The first bridge profile implements only the + whole-frontier kind; dependency-scoped validity is deferred for it (see + [What merging accepts](#what-merging-accepts)), and the scoped text here is + retained design for a later profile. Today's executable programs have fixed, + statically known reads, so Echo decides dependency-scoped validity before + evaluation. A bridge Action's reads are known only by evaluating it, so the + bridge splits basis change in two: + - **Whole-frontier `BasisChanged`,** decided before evaluation: the Action + is not eligible for dependency-scoped validity (its footprint law admits + a range read, an edge write, or a content-node write; see + [Witnessed reads](#witnessed-reads-over-a-bounded-slice)) and its evaluation basis is + no longer the commit parent. Posture `NoProposal`, empty read set, no + evaluation. + - **Dependency-scoped,** decided after evaluation: the Action is eligible, + so Echo evaluates it at its recorded origin basis, then checks its + dependency set against the history between that origin and the commit + parent. The dependency set is every witnessed read, presence and + absence, plus every effect precondition defined in + [EffectProposal](#effectproposal), whether or not the program read it, + including each edge endpoint. Consistent with the Action validity across + ticks decision, a dependency that changed in that history counts as + changed even if it was later restored. + - **How a restored value is detected.** Comparing current values cannot + see a change from A to B and back to A. The history check therefore + compares slots, not values: it uses the set of slots written by the + retained replay patches from the origin to the commit parent. A + dependency whose slot is in that set has changed, whatever its value + now. The set is derived from each patch's replay operations, in the + slot model of the actual footprint, never from its declared + `out_slots`, which a release build does not check against the + operations (see [Current implementation](#current-implementation)). + `echo_operation_written_slots_v1` must therefore project operations, or + verify that `out_slots` covers them exactly and treat any mismatch as + unknown. Value comparison runs only at validation, against the commit + parent, as the **Order** bullet below places it. No new versioning system + is added. + - **Unknown history is decided before evaluation.** The written set + depends only on the origin and the commit parent, so Echo computes it + before evaluating the Action. If any Tick in the interval has no + retained replay patch, or its writes cannot be derived, the set is + unknown and the Action takes the whole-frontier rule at once: since the + origin is not the commit parent, it obstructs with whole-frontier + `BasisChanged`, posture `NoProposal`, validity `WholeFrontier`, empty + read set, zero consumed budget, no evaluation. + - **Evaluation obstructions stand.** An evaluation that obstructs before + producing a proposal (`BudgetExceeded`, or an authored guard) keeps + that obstruction with posture `NoProposal`. Its later reads never ran + and it has no effects, so its dependency set is incomplete, and it is + never reclassified as `BasisChanged`. It commits nothing either way. + - **Order.** For a proposal, the history check runs immediately after + evaluation and the reachability and origin resolution of steps 1 and 2 of + the [Validation order](#validation-order), and before any other + validation. If a dependency changed, the Action obstructs with + `BasisChanged`, posture `Proposed` with patch tag `NotDerived`, and keeps + its witnessed read set and the dependency it names as changed. No patch is + derived from a proposal whose dependencies changed, so a proposal that + would also have failed validation (for example `DuplicateEffectTarget`) + still has one encodable outcome. Only when every dependency holds does + validation run. Echo never validates a delayed Action without its actual + dependencies. + - **Within one Tick, footprints before earlier writes.** Every check before + composition, preconditions and expected values included, runs against the + Tick's commit parent, never against writes accepted earlier in the same + Tick. The exceptions are resolution and warp reachability, which run + at the evaluation basis (see [Validation order](#validation-order)). Composition then reserves each candidate's complete footprint + (witnessed reads, precondition reads, and write set) in canonical order, + and any overlap with an earlier accepted Action in which either of the two + writes the slot is `RejectedFootprintConflict` with its blockers, as the + [within-one-tick rule](../topics/GeneratedRules.md#action-validity-across-ticks) + requires. + Read against read never conflicts, so Actions that share existing + structure both proceed. A candidate with no such overlap depends on no + slot an earlier Action wrote, so its values at the validation position + (the commit parent plus earlier accepted writes) equal its values at the + commit parent. A later Action that expects a value an earlier Action + replaced is therefore a footprint conflict, never a + `PreconditionMismatch`. +- **Budget.** The delegated budget stays `EchoOperationBudgetV1`, with its three + axes: steps, read bytes, and write bytes. For an effect program, admission + refuses a package ceiling or delegated budget above the effect profile's + fixed `EFFECT_BUDGET_CEILING_V1`: 1,048,576 steps, 64 MiB of `read_bytes`, and + 16 MiB of `write_bytes`. A proposal also holds at most 1,024 effects + (`EFFECT_COUNT_CEILING_V1`), counted at emission, whether or not they write; + the 1,025th obstructs evaluation with `BudgetExceeded`, posture `NoProposal`. + Every region the arena sizes from a budget or a count is therefore bounded, + and sizing arithmetic cannot overflow. Evaluation is metered as + `edict_pure` already meters it. Each effect is charged when emitted, whatever + validation later resolves: one step, plus `write_bytes` of 64 and the atom's + byte length for `EnsureNode`, `CreateNode`, and `ReplaceAtom` (the charge + today's compare-and-set makes for its replacement), or 128 for `EnsureEdge` + and `ReplaceEdge`. A large payload therefore cannot fit a budget that would + not cover its bytes. Exhausting any evaluation limit obstructs with + `BudgetExceeded`, posture `NoProposal`, and no patch. Allocation is not a + delegated axis: evaluation is bounded by the `max_allocated_bytes` the program + map declares, and exceeding it is likewise `BudgetExceeded` with `NoProposal`. + Admission refuses a program that declares more than the effect profile's fixed + ceiling, `EFFECT_ALLOCATION_CEILING_V1` (16 MiB), which every host + implementing the profile must provide. So no host's own limit enters an + outcome: a host that cannot provide the declared bytes fails as a host fault + and decides nothing, as **No host-dependent decisions** below requires. The + allocated bytes are recorded as evidence, never compared against the delegated + budget. +- **Evaluation reads are charged.** The recording view charges each read + before it resolves it, in the order the program makes them. A node-record + read costs one step and 64 `read_bytes`, present or absent. An atom read + costs one step and 64 `read_bytes`, plus the atom's byte length when it is + present, so a large atom cannot be read beyond the budget. Range reads are + charged as [Witnessed reads](#witnessed-reads-over-a-bounded-slice) states. + A read the remaining budget cannot cover obstructs with `BudgetExceeded`, + posture `NoProposal`, before anything is read; its charge is not added to + the consumed budget, which records every charge made before it. +- **Validation reads are charged.** Every slot validation reads is charged once + per Action, before it is read, at the first step that reads it, and never + again: a node record or an atom's presence costs one step and 64 `read_bytes`, + an edge record one step and 128 `read_bytes`, and hashing an atom's value adds + its byte length. A slot the program's view already read is not charged again, + since its value is known. A bucket scan reads every edge in the bucket as a + full edge record, one step and 128 `read_bytes` each, and is charged for the + whole bucket before any edge is inspected; a bucket length read alone costs + one step and 64 `read_bytes`. A scan the remaining budget cannot cover + obstructs before inspecting anything, and its charge is not added. So step 1 + charges the portals and owners' records of effect-key chains the view did + not already walk; a chain the view resolved for a read was charged then and is + reused without another charge, + step 2 charges each resolved record, including every Ensure and Create target + with its alpha slot, every edge source, and the outgoing bucket of an existing + content node, per edge, with that node's atom, hashed at step 2 because the + identity law at step 6 recomputes the node's id from it, and each + `ReplaceAtom`'s current alpha value, whose digest step 8 then compares + without charging again; step 8 charges nothing of its own. Charges come from + the budget left after evaluation. A read the remaining budget cannot cover + obstructs with `BudgetExceeded`, posture `Proposed`, `NotDerived`, at that + step. The receipt's consumed budget is evaluation and validation together; + `allocated_bytes` is evaluation alone. +- **Batch limit.** A proposal whose derived + patch alone exceeds the Action-batch operation limit + (`ACTION_BATCH_OPERATION_LIMIT_V1`) also obstructs with `BudgetExceeded` and + no committed patch, rather than splitting across Ticks, but its posture is + `Proposed` with a derived patch: the proposal exists, so its identity, + target-set, write-set, and patch digests are recorded, not discarded. A + proposal that fits alone but not beside the Actions already accepted into the + batch is handled by the existing batch rule, which obstructs that candidate in + this batch, likewise with posture `Proposed`. +- **Retries.** A decided outcome is final. An Action is identified by its + submission (see Identity and existing contracts); once it is decided + (committed, obstructed, or `RejectedFootprintConflict`), its outcome, + receipt, and attribution never change, and a later success is never written + over an earlier conflict. Echo's intake already enforces this: resubmitting + identical content on the same head returns the existing submission as a + `Duplicate`, with its original outcome and no new Tick. A real new attempt + must differ, for example an invocation rebased onto the new head, or a + causal parent citing the earlier outcome; that difference makes it a new + submission with its own identity, attribution, and recorded evaluation + basis. Like any Action, it is evaluated at that recorded basis, never + re-stamped onto whatever state is current when the scheduler selects it, + and then committed under the whole-frontier or dependency-scoped rule. + Echo does not retry on its own; whether to submit again is the + application's decision. +- **Pending is not retried.** An Action that was never decided, for example + one whose Tick was lost in a crash before its WAL record, remains the same + submission. It is evaluated again when the scheduler selects it; that is not + a retry, because no outcome was ever recorded for it. +- **Verification is not re-admission.** Recovery re-evaluates decided Actions + only to verify their recorded evidence (see [Recovery](#recovery)). It never + re-decides them, never stamps a new outcome, and never applies a re-derived + proposal. + +## Identity and existing contracts + +The bridge adds evidence, not a new identity root or a new authority path. Each +step below already exists except the proposal, which is evidence inside one +decision: + +| Object | Identity | Owner | Status | +| ---------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------- | ------------------ | +| Submission | `submission_id = H("echo.intent-submission.v0", worldline, head, ingress_id)`; a Continuum occurrence key is hashed into `ingress_id` | [Submission Attribution](../topics/SubmissionAttribution.md), [canonical inbox sequencing](../spec/canonical-inbox-sequencing.md) | existing | +| Action | admitted package and projected invocation | ADR 0023, ADR 0025 | existing | +| Proposal | `H(Action, evaluation basis, canonical EffectProposal)` when evaluation produced a proposal; otherwise none (see Evidence); deterministic, so re-evaluation over the same basis reproduces it | this design | new, evidence only | +| Decision | committed, obstructed, or `RejectedFootprintConflict`, recorded once in the Tick's attribution section by `submission_id` | Submission Attribution | existing | + +Consequences: + +- **Admission** is unchanged: the bridge runs inside scheduler-owned Tick + construction after ordinary admission, and adds checks; it removes none. V1 + admission refuses a package ceiling or delegated budget below the program's + `minimum_budget()`. An effect program's minimum budget is fixed: one step and + zero bytes on each byte axis, the least that can evaluate anything. Admission + applies it exactly as V1 does, and everything above it is decided by + evaluation (`BudgetExceeded`), never by admission. +- **Attribution** is unchanged: an Action batch already attributes each + candidate to its own receipt entry. The proposal identity and digests below + ride in that entry; the attribution section still names only submissions. +- **Tick scope.** Every `TickReceiptEntry` needs a `scope` and its + `scope_hash`, which `action_batch_plan_digest` hashes. A fixed-profile + Action's scope is its anchored node. A bridge Action has none, so its scope + is synthetic and canonical: the worldline's root warp id, with the + invocation identity's 32 bytes as the local id. Its `scope_hash` is + `scope_hash(installed_operation_id, scope)`, as for fixed profiles. It names + no graph node, is never read, and recovery recomputes it from the retained + invocation. +- **Batch digests.** The batch rewrites and composition digests hash one + identity tuple per applied member. A Tick of fixed-profile Actions alone + keeps today's recipes and `v1` domains byte for byte. A Tick that contains + a bridge Action uses `echo:operation-action-batch-rewrites:v2\0` and + `echo:operation-action-batch-composition:v2\0`, with a one-byte member kind + before each member (fixed `1`, bridge `2`), so the two kinds of tuple can + never alias. A fixed member contributes exactly its V1 tuple. A bridge + member contributes its proposal identity where a fixed member has its + `preparation_id`, then its candidate patch digest, its `result_identity`, + its invocation's evaluation-basis identity, and its write-set digest as + its actual footprint. The rewrites digest takes the first element of each + tuple, as V1 takes `preparation_id`. +- **Durability** is unchanged in kind: the decided-Tick WAL record is the only + persistence. Proposals are never retained apart from their Tick. The record + gains a new layout version for the new evidence (see Evidence). +- **Package version.** `ExecutableOperationPackageV1` embeds + `EchoOperationSemanticClosureV1`, which requires `lawpack_coordinate` and + `lawpack_identity`, and `EchoOperationProgramV1`, which has only the two + fixed profiles. A source-compiled bridge package therefore uses + `ExecutableOperationPackageV2`. Fixed-profile programs and invocations are + not re-encoded: they keep their V1 maps, schema strings, and identities + byte for byte. V2 adds exactly this: + - **Package.** The V1 package map with `schema` set to + `echo.operation-package/v2`, `semantic_closure` set to a + `closure-v2`, and `program` set to an effect program. Every other key, + and its value shape, is as in V1, except that the optional + `application_result_projection` must be absent: an effect program's + application result is its own output, which `result_identity` binds, + so no projection can compete with it. Where V1 derives a package identity + field from its program, V2 fixes it for the effect program, using V1's + `profile_digest` (BLAKE3 over `echo:operation-profile:v1\0` and the + length-prefixed label), and admission requires each equality: + - `target_profile_identity` is the profile digest of + `echo.operation-target.edict-effect/v1`; + - `application_basis_schema_identity` is the profile digest of + `echo.operation.basis.edict-effect/v1`; + - `input_schema_identity`, `result_schema_identity`, and + `obstruction_schema_identity` are the profile digests of + `echo.operation.input.edict-effect/v1`, + `echo.operation.result.edict-effect/v1`, and + `echo.operation.obstruction.edict-effect/v1`; + - `result_interpretation_identity` and + `obstruction_interpretation_identity` are the profile digests of + `echo.operation.result-interpretation.edict-effect/v1` and + `echo.operation.obstruction-interpretation.edict-effect/v1`; + - `evaluation_basis_schema_identity` is the profile digest of + `echo.operation.evaluation-basis/v1`, as in V1; + - `footprint_contract_identity` is the `v2` footprint-law digest + below. + + Together with the profile identities the program carries, this fixes + every identity field of the package. `obstruction_coordinate` and + `operation_coordinate` remain the application's text, as in V1. + + - **Semantic closure.** The V1 closure map, with `lawpack_coordinate` and + `lawpack_identity` both omitted. A V2 package carries only an effect + program, which requires their absence, so no sentinel lawpack is + fabricated. A fixed-profile program stays in a V1 package with its + lawpack, as ADR 0023 requires today. The closure has no identity of its + own; its bytes are part of the package's. + - **Effect program.** A new map, `program-v2-effect` below. Like a V1 + program, it carries `interpreter_profile_identity` and + `intrinsic_profile_identity`. Admission requires each to equal the + package's value of the same name and the profile Echo implements for + effect programs: the profile digests of + `echo.operation-interpreter.edict-effect/v1` and + `echo.operation-intrinsics.edict-effect/v1`. Any other value is + refused as an unsupported profile, as in V1. Its other entries are: + - `compiled_program`, the compiled bytes; + - `target_ir_identity`, which must equal the closure's; + - `identity_law`, an unsigned integer naming an + [identity law](#identity-laws); unknown values are refused; + - `graph_schema`, the canonical bytes of a `graph-schema`; + - `footprint_law`, the canonical bytes of a `footprint-law`; + - `max_input_bytes` and `max_result_bytes`, each at most 65,536, the + application input and result ceilings ADR 0025 sets. A result + longer than `max_result_bytes` obstructs evaluation with + `BudgetExceeded`, posture `NoProposal`; + - `max_allocated_bytes`, the program's declared allocation ceiling, + at most `EFFECT_ALLOCATION_CEILING_V1`, which bounds evaluation and + sizes the scheduler's evaluation arena; + - `output_type`, the compiler-declared output type coordinate of the + program's application result, which `result_identity` hashes. + Admission requires it to be nonempty UTF-8 of at most 1,024 bytes, + the bound V1 applies to result coordinates. + + The graph schema is the executable graph contract, a different + artifact from the application's own schema declaration. The closure's + `application_schema_identity` keeps naming that declaration, with its + codecs and migration posture, as ADR 0023 requires. The graph schema + is bound by the program identity, whose bytes contain it, so no + equality between the two is required. The package's inherited + `footprint_contract_identity` must equal BLAKE3 over + `echo:operation-footprint-law:v2\0` and the `footprint_law` bytes, so + the attested footprint contract is exactly the law validation + executes. The `graph_schema` is a map that Echo executes, not only a + digest. `node_types` maps each + admitted node type to its addressing, which the + [identity law](#identity-laws) reads, and its atom types. `edge_types` + maps each admitted edge type to its (source node type, target node + type) pairs. Validation step 5 reads these relations directly. No + artifact is attested under one identity and executed under another. + + - **Effect invocation.** A new map, `invocation-v2-effect` below. It + carries the V1 invocation's common entries other than the anchored + node and replacement (`authority_grant_identity`, `delegated_budget`, + `evaluation_basis`, `operation_coordinate`, `package_id`), plus the + required `application_input_bytes`, the program's input in + `edict.canonical-cbor/v1`. Its `evaluation_basis` names + the frontier exactly as V1 does, and V1's basis check resolves it + there. Its application basis is the input itself: + `application_basis_schema_identity` is the package's value above, and + `application_basis_value_identity` is BLAKE3 over + `echo:operation-edict-effect-basis:v1\0`, the input's length as a + little-endian `u64`, and the input bytes. Admission recomputes both and + refuses a mismatch, so the basis evidence is bound to the input the + program evaluates. Admission checks only what it can check + without a schema language: that the bytes are canonical and no longer + than the program's `max_input_bytes`. The input's shape is the compiled + program's to check, as its first act; a malformed input obstructs + evaluation with the authored `InputRejected`, posture `NoProposal`. An + effect program admits only effect invocations, and a fixed profile only + its own V1 invocations, so no invocation crosses between them. + + ```text + closure-v2 = { + "application_schema_coordinate": tstr, "application_schema_identity": id, + "canonical_meaning_identity": id, "core_identity": id, + "edict_source_identity": id, "target_ir_identity": id, + } + program-v2-effect = { + "schema": "echo.operation-program/v2", "kind": "edict-effect-program/v1", + "interpreter_profile_identity": id, "intrinsic_profile_identity": id, + "compiled_program": bstr, "target_ir_identity": id, + "identity_law": uint, "graph_schema": bstr, "footprint_law": bstr, + "max_input_bytes": uint, "max_result_bytes": uint, + "max_allocated_bytes": uint, "output_type": tstr, + } + invocation-v2-effect = { + "schema": "echo.operation-invocation/v2", + "authority_grant_identity": id, "delegated_budget": budget-v1, + "evaluation_basis": evaluation-basis-v1, "operation_coordinate": tstr, + "package_id": id, "application_input_bytes": bstr, + } + ; budget-v1 and evaluation-basis-v1 are the V1 values, unchanged. + ``` + + No other key may appear in any of these maps. A V2 package, effect program, + and effect invocation hash their identities under + `echo:operation-package:v2\0`, `echo:operation-program:v2\0`, and + `echo:operation-invocation:v2\0`. Their invocation-bytes digest, package + admission, invocation admission, and installation identities use + `echo:operation-invocation-bytes:v2\0`, + `echo:operation-package-admission:v2\0`, + `echo:operation-invocation-admission:v2\0`, and + `echo:operation-installation:v2\0`. Every other domain is unchanged. The + retained installation record of a V2 package is the V1 installation map + (`admission_policy`, `admission_policy_id`, `installed_operation_id`, + `package_admission_id`, `package_bytes`, `package_id`, `schema`) with + `schema` set to `echo.operation-installation/v2`. Recovery dispatches on + `schema`: `v1` decodes `package_bytes` with the V1 package decoder and + identity recipes, and `v2` with the V2 ones; any other value is refused. So + V2 identities never coincide with V1 identities, and V1 encoding, + validation, and identities are unchanged. + +## Evidence + +Each Action's receipt entry binds, in addition to its current fields: + +- the proposal posture, a tagged value with exactly three variants: + - `NotBridge`: the entry is not a bridge Action. Fixed-profile Actions and + every other existing receipt entry take this variant. Its existing + fields are encoded and hashed exactly as under receipt digest version + 4, and its row in the bridge table is all zero (posture `0`). No bridge + evidence is manufactured for it; + - `NoProposal`: no proposal exists, because evaluation obstructed before + producing one (for example `BudgetExceeded` or an authored guard such + as `BasisNotCanonical`) or never ran (whole-frontier `BasisChanged`). + No proposal identity, target-set, write-set, or patch digest exists, + and none is manufactured; + - `Proposed { proposal identity, target-set digest, patch }`: evaluation + produced a proposal. The target-set digest is always defined, because + the target set depends only on the effects. `patch` is itself tagged: + - `Derived { write-set digest, patch digest }` when Echo derived a + patch: the proposal committed, was rejected at composition, or was + obstructed by `FootprintMismatch` or an Action-batch limit. The + write set is known only once validation has resolved each effect + against the basis, so it is recorded only here; + - `NotDerived` when no patch was derived: validation refused the + proposal (`DanglingReference`, `ContentIdentityConflict`, + `DuplicateEffectTarget`, `FootprintLawViolation`, + `IdentityLawViolation`, `SchemaViolation`, `UnreachableWarp`, + `NodeMissing`, `PreconditionMismatch`, or a `BudgetExceeded` + charged by a validation read), or a + dependency-scoped `BasisChanged` was decided before validation. No + write-set or patch digest is manufactured; an overwrite patch that + `Ensure` forbids is never hashed; +- for `NoProposal` and `Proposed`, the witnessed read-set digest, including + observed absences, for every outcome that evaluated, because a refusal is + still evidence of what the program saw; it is the empty set's digest when + evaluation never ran; +- for `NoProposal` and `Proposed`, the validity rule, a tagged value: + - `WholeFrontier`: the Action commits only onto its exact evaluation + basis; the recorded basis posture is its evidence; + - `Scoped`: the evidence the + [Action validity across ticks](../topics/GeneratedRules.md#action-validity-across-ticks) + decision requires: the origin basis, the validation position, and one + of three evidence forms, each recording only a comparison that actually + ran: + - `OriginOnly`, for every outcome decided before the history check: an + evaluation obstruction, or a failure of reachability or resolution + (steps 1 and 2 of the [Validation order](#validation-order)). No + dependency comparison ran; + - `HistoryChanged`, for a dependency-scoped `BasisChanged`: the + dependency-set digest over each dependency's descriptor and + comparison mode, and the first changed dependency in canonical + order. Validation never ran, so no values were compared; + - `Compared`, for every Action that passed the history check, + whatever its later outcome: the dependency-set digest and a + compared-values digest. The pre-composition checks compare, at the + commit parent, the value of every effect-precondition and + resolved-record dependency. Witnessed reads are verified by the + history check's written-slot test, not by value, and are recorded + as not compared. A precondition or resolved-record dependency + those checks never reached, because validation stopped at an + earlier step or a validation read exhausted the budget before + hashing its value, is recorded as not compared, with no value. For + an accepted + Action these equal its values at the validation position (the + commit parent plus the writes of every earlier accepted Action), + because composition admits no overlap; a + `RejectedFootprintConflict` is never compared at its validation + position; + +- for `NoProposal` and `Proposed`, consumed budget: evaluation and validation + charges together, with `allocated_bytes` from evaluation alone. When + evaluation never ran (whole-frontier `BasisChanged`, including unknown + history), it is zero on every axis, and recovery verifies that. + +**Dependency kinds and modes.** A dependency is its slot, its kind, and its +comparison mode: + +- kind: value present `0`, observed absent `1`, expected value `2`, endpoint + existence `3`, resolved record `4` (a record step 2 resolved, including an + Ensure or Create target and an endpoint), and portal `5` (a portal + attachment on an effect's chain, or its owner's node record); +- comparison mode: `ValueDigest` `0`, a payload-value dependency that + compares the slot's value digest, and `Absence` `1`, a single-key absence + dependency. These are exactly the two kinds the Action validity decision + admits. Value present, expected value, endpoint existence, and portal use + `ValueDigest`: an endpoint's dependency is on its node record's value, so it + holds only while the node exists with that value. Observed absent uses + `Absence`. A resolved record uses `ValueDigest` when step 2 found it and + `Absence` when it did not. Positive presence alone is not a mode. + Revision-sensitive and identity-sensitive dependencies are refused at + admission and have no tag. + +A scoped Action reads no edge ranges (an edge read keeps the whole-frontier +rule), so its dependency slots are node records, attachments (atoms and +portals), and edges. + +**Value digests.** A present slot's value digest is BLAKE3 over a +class-specific domain tag and its canonical fields: + +- node record: `echo.bridge.node-value.v1\0`, then the node type id; +- attachment: `echo.bridge.attachment-value.v1\0`, then for an atom tag `0`, + its `type_id`, its byte length as a little-endian `u64`, and its bytes, or + for a portal tag `1` and its target warp id. `expectedAtomDigest` is this + digest of the expected atom; +- edge: `echo.bridge.edge-value.v1\0`, then the edge type id and the local + `from` and `to` node ids. + +The read-set, target-set, write-set, dependency-set, and compared-values +digests, and the byte images they hash, are defined in +[Encoding and memory](#encoding-and-memory). + +The submission identity is present in every variant. An identified submission +whose evaluation produced no proposal is a different evidence state from an +evaluated proposal, and the receipt keeps them distinct. + +**Proposal identity.** The proposal identity is BLAKE3 over +`echo.bridge.effect-proposal.v1\0` followed by the proposal's canonical +image, defined in [Encoding and memory](#encoding-and-memory). + +The proposal identity is `H(Action, evaluation basis, canonical +EffectProposal)` in this encoding, and the canonical `EffectProposal` contains +every effect in canonical order, so the identity binds the exact evaluated +effects (invariant 5). The target-set digest and, when a patch was derived, the +write-set and patch digests are derived from those same effects. Proposals are +not retained apart from their Tick; the binding is checked by re-deriving the +proposal, as the recovery matrix below requires for every class that carries +one. + +Today every `BasisChanged` is decided before evaluation runs +(`echo_operation.rs`). For bridge Actions that remains true only of the +whole-frontier case; a dependency-scoped `BasisChanged` is decided after +evaluation and keeps its evidence (see Basis, budget, retries). + +These fields change the receipt entry's encoding, which commit hash v3 binds, +and its retained layout. `EPRV0003` has no per-entry length or version, so a +legacy decoder would read the new fields as blocker data. The new evidence is +therefore written only under a new retained provenance record version, +`EPRV0004`, and a new receipt digest version, 5. The retained magic alone is +not enough, because it sits outside the receipt digest that commit hash v3 +binds: receipt digest version 5 puts every entry's proposal posture and, for +bridge entries, the target-set digest, patch tag with its digests, read-set +digest, validity rule with its scoped evidence, and consumed budget into the +digest's preimage. Two validations that compared different values therefore +have different receipt identities, and a version-4 receipt identity never +changes meaning. Ticks that mix bridge and `NotBridge` entries encode in +`EPRV0004` without fabricated evidence. + +**Receipt and outcome records.** The `EPRV0004` bridge table, the receipt +digest version 5 preimage, and the `EOACT004` retained Action outcome are +defined in [Encoding and memory](#encoding-and-memory). Fixed-profile +Actions keep `EOACT003`, its decoder is unchanged, and each record decodes by +its own magic. Recovery requires the `EOACT004` outcome coordinate to equal +the receipt's bridge-row coordinate. +The implementation adds this row to +[Submission Attribution's format table](../topics/SubmissionAttribution.md#format-binding-and-legacy) +when it lands: + +| Receipt | Receipt digest | Retained record | Commit hash | +| ----------------------------------------- | -------------- | --------------- | ----------- | +| Commit-bound section with bridge evidence | version 5 | `EPRV0004` | v3 | + +Only a Tick that contains a bridge Action uses receipt digest version 5 and +`EPRV0004`; a Tick of fixed-profile Actions alone keeps version 4 and +`EPRV0003`, byte for byte. + +The `EPRV0003` decoder and receipt digest version 4 stay unchanged, retained +legacy Ticks recover through them byte for byte, a mixed history decodes each +record by its own magic, and an `EPRV0003` record never carries the new +fields. + +### Recovery + +The bridge keeps Echo's existing recovery verification and extends it to the +new evidence. Verification is not re-admission. + +- A decided Tick is recovered from its WAL record by replaying its patch. + Echo then checks the patch digest and the commit hash, which binds the + receipt and its attribution section, so the recovered evidence is exactly + the evidence that was committed. Recovered state comes from the committed + patch, never from a re-derived proposal. +- Recovery keeps the per-class verification described in + [Current implementation](#current-implementation) and adds the new evidence + to whatever each class already compares, as the matrix below states. Any + disagreement refuses the history. +- The comparison never changes a decision. The recorded outcome, receipt, and + attribution stand as written; a re-derived proposal is checked against them + and then discarded. +- An Action recorded as `Scoped` follows + [Action validity across ticks](../topics/GeneratedRules.md#action-validity-across-ticks): + for a `Proposed` outcome recorded as `OriginOnly`, recovery replays only + the pre-history failure (reachability or resolution) and requires the same + obstruction, without reconstructing a dependency set that live execution + never built. For one recorded as `HistoryChanged` or `Compared`, it + recomputes the complete dependency set (every witnessed read and every + effect precondition) and the + written-slot set from the replay operations. It then repeats what live + execution did, in the same order: the history check, the pre-composition + checks against the commit parent, and the batch composition, and it + rebuilds the recorded evidence form from the comparisons those steps + actually make. A `RejectedFootprintConflict` is verified through its + preparation against the commit parent and its recomputed blockers, never + by validating it at its validation position. Recovery refuses a history + whose evidence form, dependency-set digest, compared-values digest, + changed dependency, or result differs. For an evaluation obstruction it + re-evaluates at the origin. +- An undecided Action stays the same pending submission and is evaluated when + the scheduler next selects it. + +Recovery matrix. "Existing check" is what recovery verifies today for that +class; "Added" is what the bridge adds. "Effects bound" means the re-derived +effects must hash to the recorded proposal identity and reproduce the +recorded target-set digest and patch tag, with the write-set and patch +digests when it is `Derived` (invariant 5). + +Two checks apply to every row and are not repeated in it, because recovery +already performs them for every Action Tick: the basis posture is recomputed +against the scheduler Tick's parent, and the whole Action batch's composition +is reconstructed and every reconstructed outcome must equal the recorded one. +The bridge keeps both. The reconstruction already compares declared +outgoing-edge range keys and recomputes blockers, as earlier-Action indices +(#917); the bridge +supplies the range keys that its witnessed reads and effects claim, and its +precondition reads, to that reconstructed composition. The scoped-validity recomputation +above likewise applies to every row recorded as `Scoped`. + +| Outcome | Posture | Existing check | Added | +| ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | ------------------------ | ------------------------------------------------------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Committed | `Proposed`, `Derived` | replay patch; reconstruct preparation; compare identities | effects bound; read-set digest; the row's `patch_digest` equals this Action's re-derived candidate patch; the Tick's replay patch equals the batch composition of every accepted candidate | +| `RejectedFootprintConflict` | `Proposed`, `Derived` | reconstruct preparation; compare identities; recompute recorded blockers | effects bound; read-set digest; blockers include range-key conflicts | +| Obstructed at validation (`DanglingReference`, `ContentIdentityConflict`, `DuplicateEffectTarget`, `FootprintLawViolation`, `IdentityLawViolation`, `SchemaViolation`, `UnreachableWarp`, `NodeMissing`, `PreconditionMismatch`, validation-read `BudgetExceeded`) | `Proposed`, `NotDerived` | re-evaluate; compare pre-decision evidence | effects bound; read-set digest; obstruction kind; no write-set or patch digest present | +| Obstructed by `FootprintMismatch` (after derivation) | `Proposed`, `Derived` | re-evaluate; compare pre-decision evidence | effects bound; read-set digest; re-derived patch reproduces the mismatch | +| `BudgetExceeded`, scheduler-assigned (Action-batch limit) | `Proposed`, `Derived` | accept reconstructed preparation; verify through the batch reconstruction | effects bound; read-set digest | +| `BudgetExceeded` during evaluation, an evaluation-time `FootprintLawViolation` (an out-of-law read, an undeclared range type, or `max_reads` exceeded), an evaluation-time `UnreachableWarp` (a read through an unreachable warp), or an authored guard | `NoProposal` | re-evaluate; compare pre-decision evidence | re-evaluation, at the origin for a `Scoped` Action, again yields no proposal and the same obstruction; read-set digest | +| `BasisChanged`, whole-frontier (before evaluation, including unknown history) | `NoProposal` | admission evidence; recomputed basis posture; no re-evaluation | none; posture must be `NoProposal` with an empty read set and zero consumed budget | +| `BasisChanged`, dependency-scoped (after evaluation, before validation) | `Proposed`, `NotDerived` | none today: current programs decide this before evaluation | re-evaluate at the origin; effects bound; read-set digest; recompute the written-slot set from replay operations, the complete dependency set (witnessed reads and effect preconditions), and the changed dependency | +| Any outcome of a `NotBridge` entry | `NotBridge` | unchanged | none; its bridge row is all zero | + +## Encoding and memory + +The layouts in this section are provisional (see +[What merging accepts](#what-merging-accepts)). Deterministic charging, +bounded capacity, and the rule that host allocation failure never becomes an +Action outcome are accepted. Any bytes that enter an identity, a digest, or +retained evidence must be fixed before the profile that writes them ships. + +Every bridge record is a zero-copy image in the style of Echo's WSC snapshot +format (`crates/warp-core/src/wsc/`). It is read in place through a view that +a validator has checked, and it is never hydrated into owned structures. The +rules: + +- **Rows.** Every fixed-size row is `#[repr(C)]` and `bytemuck` `Pod` and + `Zeroable`, with explicit padding fields. Integers are little-endian, ids + and digests are 32 bytes, and every row size is a multiple of 8 bytes. +- **Images.** An image is an 8-byte magic, a fixed header, and sections of + rows, each section starting 8-byte aligned. Variable-length bytes live in + a trailing blob section and are addressed by a 16-byte `Range` + (`start_le`, `len_le`), WSC's range row. +- **One canonical image per value.** Rows appear in the sort order given + below. Padding, and every field a row's tags make unused, are zero. Blob + bytes are packed in row order, each run starting 8-byte aligned, with zero + bytes between runs and none after the last. Two images of one value are + therefore byte-identical, and every digest below is BLAKE3 over a domain + tag and exact image bytes. +- **Validation before trust.** A reader checks the magic, the sizes, + alignment, tags, zero padding and zero unused fields, sort order, range + bounds, and blob packing before using a view. Any failure refuses the + history. Validation runs in place and allocates nothing. + +**Rows.** + +| Row | Bytes | Fields, in order | +| ---------------- | ----- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `SlotRow` | 104 | `class` u8 (node record `0`, attachment `1`, edge `2`, range key `3`); `owner` u8 (attachment: node `0`, edge `1`); `plane` u8 (attachment: alpha `0`, beta `1`); 5 padding bytes; `warp_id`; `local_id` (the node, edge, attachment owner, or range source); `edge_type` (range key only) | +| `ReadRow` | 192 | `slot` (`SlotRow`); `outcome` u8 (present `0`, absent `1`, range `2`, portal `3`); 7 padding bytes; `read_type`, 32 bytes: the type that authorizes the read, the record's node type or atom `type_id` when present and the type the read named when absent, the owner's node type for a portal, and zero for a range; `subject`, 32 bytes: the value digest when present or a portal, zero otherwise; `pairs` (`Range` into the pair section; range only) | +| `EdgePairRow` | 64 | `edge_local_id`; `target_local_id` | +| `EffectRow` | 280 | `kind` u8 (`EnsureNode` `0`, `CreateNode` `1`, `ReplaceAtom` `2`, `EnsureEdge` `3`, `ReplaceEdge` `4`); 7 padding bytes; `key_warp_id`; `key_local_id`; `type_id` (node type, or `EnsureEdge`'s edge type); `atom_type_id`; `atom` (`Range` into the blob); `expected_digest` (`ReplaceAtom`); `from_local_id` (`EnsureEdge`); `to_local_id` (`EnsureEdge`, and `ReplaceEdge`'s new target); `expected_to_local_id` (`ReplaceEdge`) | +| `DependencyRow` | 152 | `slot` (`SlotRow`); `kind` u8; `mode` u8; 6 padding bytes, which together with `slot` form the 112-byte descriptor; `compared` u8 (present `0`, absent `1`, not compared `2`); 7 padding bytes; `compared_digest` (present only) | +| `OutcomeRow` | 40 | `outcome` u8 (none `0`, bridge kind `1`, authored `2`); `code` u8 (the bridge kind code); 6 padding bytes; `authored_id` (authored only; see below) | +| `BridgeEntryRow` | 496 | `posture`, `patch`, `validity`, and `evidence` tags, u8 each; `outcome` and `code` as in `OutcomeRow`; 2 padding bytes; `proposal_id`; `target_set`; `write_set`; `patch_digest`; `read_set`; `origin_basis`; `dependency_set`; `compared_values`; `changed_dependency` (a 112-byte descriptor); `authored_id`; `validation_position` u64; `steps`, `read_bytes`, `write_bytes`, and `allocated_bytes`, u64 each; `result_identity`; `result` (`Range` into the result blob) | + +Tags not defined above use the values given in [Evidence](#evidence): +posture `NotBridge` `0`, `NoProposal` `1`, `Proposed` `2`; patch `NotDerived` +`0`, `Derived` `1`; validity `WholeFrontier` `0`, `Scoped` `1`; evidence +`OriginOnly` `0`, `HistoryChanged` `1`, `Compared` `2`. Bridge kind codes are +`BasisChanged` `0`, `BudgetExceeded` `1`, `DuplicateEffectTarget` `2`, +`IdentityLawViolation` `3`, `UnreachableWarp` `4`, `SchemaViolation` `5`, +`FootprintLawViolation` `6`, `NodeMissing` `7`, `PreconditionMismatch` `8`, +`ContentIdentityConflict` `9`, `DanglingReference` `10`, and +`FootprintMismatch` `11`. A `NotBridge` row is all zero after its posture. + +`validation_position` is the Action's zero-based index among the Tick's +selected candidates in canonical order, counting every candidate whatever its +outcome; it is `0` when the validity tag is `WholeFrontier`. Each tag sets +exactly these `BridgeEntryRow` fields; every other field is zero: + +| Tag value | Fields it sets | +| ------------------------- | ----------------------------------------------------------------------------- | +| posture `NotBridge` | none | +| posture `NoProposal` | `read_set`, the budget fields, `validity`, `outcome`, `code` or `authored_id` | +| posture `Proposed` | as `NoProposal`, plus `proposal_id`, `target_set`, `patch` | +| patch `Derived` | `write_set`, `patch_digest` | +| validity `Scoped` | `origin_basis`, `validation_position`, `evidence` | +| evidence `HistoryChanged` | `dependency_set`, `changed_dependency` | +| evidence `Compared` | `dependency_set`, `compared_values` | +| outcome committed | `result_identity`, `result` | + +`authored_id` identifies an authored obstruction. The program reports one as +a code, a UTF-8 string of at most 1,024 bytes such as `InputRejected` or +`BasisNotCanonical`, and detail bytes in `edict.canonical-cbor/v1`, bounded +by the program's `max_allocated_bytes`. `authored_id` is BLAKE3 over +`echo.bridge.authored-obstruction.v1\0`, the program identity, the code's +length as a little-endian `u64` and its bytes, and the detail's length and +bytes. Recovery re-evaluates the Action at its origin and requires the same +identity. + +`result_identity` is BLAKE3 over `echo.bridge.result.v1\0`, the program +identity, the length of the program's `output_type` as a +little-endian `u64` and its UTF-8 bytes, and the length of the result bytes as +a little-endian `u64` and the bytes: the propositions ADR 0025 binds for an +applied Action. An obstruction or conflict carries no result, and both fields +are zero. Recovery re-evaluates the Action and requires its result bytes to +equal the retained ones before it publishes the outcome. + +A `Range` addresses its section in that section's units, from the section's +start: the blob in bytes, and the `EdgePairRow` section in rows. + +**Sort orders.** `SlotRow`s sort by `class`, `warp_id`, `local_id`, +`edge_type`, `owner`, then `plane`, so a set's rows are in slot order. +`ReadRow`s sort by their slot, then by `read_type`. A slot the program reads +more than once under different named types while it is absent has one row per +named type, each authorized on its own, so a permitted type cannot mask a +forbidden probe; repeated reads with the same type are one row. A present slot +has one row, under its actual type. `max_reads` counts rows. `DependencyRow`s +sort by their slot, and `DependencyRow`s with +one slot by `kind`, then `mode`. A range's `EdgePairRow`s are contiguous, +sorted by `edge_local_id`, and the ranges follow `ReadRow` order. `EffectRow`s +follow the canonical effect order in [EffectProposal](#effectproposal). + +**Images and digests.** + +- **Proposal** (magic `EBPRP001`): after the magic, a 192-byte header holding + the installed-operation identity, the canonical invocation digest, the + `EchoOperationEvaluationBasisV1` identity, the read-set digest, the + evaluation cost alone (`steps`, `read_bytes`, `write_bytes`, + `allocated_bytes` as evaluation consumed them, never validation charges, so + the proposal identity does not depend on how far validation ran), the + result as a + `Range` into the blob, the effect count, and the blob length; then the + `EffectRow`s; then the blob, holding the atoms in effect order and then the + result. The proposal identity is BLAKE3 over + `echo.bridge.effect-proposal.v1\0` and the image. +- **Sets.** The read-set digest is BLAKE3 over `echo.bridge.read-set.v1\0`, + the `ReadRow` count as a little-endian `u64`, the `ReadRow`s, the + `EdgePairRow` count, and the `EdgePairRow`s. The target-set and write-set + digests hash their domain tags (`echo.bridge.target-set.v1\0`, + `echo.bridge.write-set.v1\0`), the count, and the `SlotRow`s. The + dependency-set digest hashes `echo.bridge.dependency-set.v1\0`, the count, + and each `DependencyRow`'s 112-byte descriptor. The compared-values digest + hashes `echo.bridge.compared-values.v1\0`, the count, and the whole + `DependencyRow`s. +- **`EPRV0004`**: the eight ASCII bytes `EPRV0004` as the record magic, then + the `EPRV0003` payload that follows that record's own magic, byte for byte, + then zero padding to an 8-byte boundary, then a bridge table of one + `BridgeEntryRow` per receipt entry, in entry order, then the result blob: + its length as a little-endian `u64`, then the blob. The blob follows the + image rule above: each committed bridge Action's exact result bytes, in + entry order, each run starting 8-byte aligned from the blob's start, with + zero bytes between runs and none after the last. The length counts the + padding between runs. The record ends with the blob. Each row's `result` + range addresses the blob, which carries the + result bytes ADR 0025 requires in the Receipt. Only the magic differs from + `EPRV0003` before the table, so the unchanged `EPRV0003` decoder never sees + an `EPRV0004` record. The table is indexable in place. +- **Receipt digest version 5**: the version-4 preimage with its leading + little-endian `u16` version tag set to `5`, in the same position as + versions 2 through 4, followed by the bridge table and result blob bytes + exactly as `EPRV0004` retains them. +- **`EOACT004`**: a bridge Action's retained outcome. It is a sequential + record like `EOACT003`, not one of the zero-copy images above, because it + is read once at recovery: + - the eight ASCII bytes `EOACT004`, the submission id and ingress id (32 + bytes each), and a one-byte variant tag (committed `1`, obstructed `2`, + conflict `3`); + - the 40-byte `OutcomeRow` and the Action's 496-byte `BridgeEntryRow`; + - the 152-byte decision coordinate, exactly as `EOACT003` retains it + (`retain_action_decision_coordinate_v1`): writer-head worldline id and + head id, `worldline_tick_after` and `commit_global_tick` as + little-endian `u64`s, commit id, Tick receipt digest, and member index + as a little-endian `u64`. Every variant carries it, because a bridge + Action is decided by a sealed Tick whether it commits, obstructs, or + conflicts; + - for a committed Action, its exact result bytes, as a little-endian + `u64` length and the bytes; + - for a conflict, the blocker count as a little-endian `u64` and each + blocker's candidate index as a little-endian `u32`, as `EOACT003` does. + + A bridge Action has no `EchoOperationReceiptV1` and no prepared candidate: + its evidence is the `BridgeEntryRow`, which the receipt digest already + binds. Committed and conflict variants carry the all-zero `OutcomeRow`. + The `OutcomeRow` is not separately bound by the receipt: it must equal the + projection of the receipt-bound `BridgeEntryRow` (its `outcome`, `code`, and + `authored_id`, with zero padding). Recovery derives that projection and + refuses a record whose `OutcomeRow` differs before it publishes the outcome. + Recovery also requires the `BridgeEntryRow` to equal the receipt's byte for + byte, and the decision coordinate to name the sealed Tick that holds that + receipt entry at that member index. Fixed-profile Actions keep `EOACT003`. + +**Memory.** The bridge allocates nothing on its hot path: + +- **One reused arena per scheduler.** The scheduler owns a bridge arena that + is reset, never freed, at each Tick boundary, as it already reuses its + radix `scratch` buffer. Every working structure is a typed region in it: + the recording view's `ReadRow`s and `EdgePairRow`s, the emitted + `EffectRow`s and blob, the `DependencyRow`s and `SlotRow`s, the proposal + images, and the bridge table. +- **Built in final form.** Records are written in place as their final + images. Hashing, the WAL append, and receipt construction read those bytes + directly; nothing is copied into intermediate structures. +- **Capacity fixed before evaluation.** Each region's size is a pure function of + the selected candidates' footprint-law maxima, each clamped to what its + delegated budget can pay for (a read costs at least 64 `read_bytes`, a range + edge 64, a write 64 `write_bytes`), delegated budgets, the + program's `max_allocated_bytes`, and its `max_result_bytes`, which bounds the + result bytes the blob must also hold independently of allocation (a result + can carry bytes the program never allocated, such as its input). Each is + sized per candidate from its own declared maxima, never from + the 128-operation batch limit, so a candidate whose patch exceeds that limit + is still derived in place and then rejected with `BudgetExceeded`. The + 64-candidate limit bounds how many such candidates a Tick selects. The arena + grows, if at all, after selection and before evaluation. Evaluation, + validation, derivation, and composition never allocate. +- **No host-dependent decisions.** Arena capacity never changes which + Actions a Tick contains or how they are decided. If the host cannot grow + the arena, the Tick fails as a host fault and nothing is decided, as on a + crash before the WAL record, rather than obstructing an Action. +- **Recovery reads views.** Recovery validates retained images in place and + reads them through views; it rebuilds proposals in the same arena to + compare them, and allocates nothing per Action. + +`allocated_bytes` remains `edict_pure`'s metered evaluator allocation, which +is evidence about the program, not about host memory. + +## Execution traces + +These traces follow Jim's flat-text reference `ReplaceRange` (the first +acceptance target in flyingrobots/jedit#302). The application vocabulary below +belongs to Jim's package; Echo sees only nodes, edges, and atoms. + +Basis coordinate `c` (Tick `t`): + +```text +Buffer B atom {bufferKey "a.txt", version 7} + -canonicalHead-> H1 atom {byteLength 11, lineCount 1, sequence 4} +H1 -root-> T1 atom {bytes "hello world", lineBreaks 0} +H1 -anchor-> I atom {fileCoordinate "a.txt", hostDigest d0} +``` + +Invocation: `{bufferId B, basisHeadId H1, startByte 6, endByte 11, +replacement "there"}` at basis `c`. + +### Committed + +1. **Admission.** The invocation is admitted at `c` under the package's + authority and delegated budget, retained before acknowledgement. +2. **Selection.** The scheduler selects the Action while constructing Tick + `t+1` and opens a recording view over `c`. +3. **Evaluation reads**, recorded by the view: `B` atom; `B` `canonicalHead` + edge (to `H1`); `H1` atom; `H1` `root` edge (to `T1`); `H1` `anchor` edge + (to `I`); `T1` atom. Six slots. +4. **Pure computation.** The guard `canonicalHead == H1` holds; range and + boundaries check; the new bytes are `"hello there"`; the program derives ids + `T2` and `H2` under its identity law. +5. **Proposal**, in canonical order: node records, then atoms, then edges. + Within a class the order follows id bytes, which these symbolic names do + not show. + - `EnsureNode T2 {bytes "hello there", lineBreaks 0}` + - `EnsureNode H2 {byteLength 11, lineCount 1, sequence 5}` + - `ReplaceAtom B expected digest(version 7), now {version 8}` + - `EnsureEdge H2 -root-> T2` + - `EnsureEdge H2 -anchor-> I` + - `ReplaceEdge B -canonicalHead-> expected H1, now H2` +6. **Validation**, in [Validation order](#validation-order): + 1. every key is in the root warp, so no portal is crossed; + 2. resolution reads and charges the node records and alpha slots of the + `EnsureNode T2` and `EnsureNode H2` targets and the edge records of + the `EnsureEdge H2.root` and `H2.anchor` targets (all absent, so all + four create); `B`'s node record, for `ReplaceAtom B` and as the + source of `ReplaceEdge`, charged once; the `B.canonicalHead` edge + record; and the endpoint `I`'s node record. `H2`, the source of both + Ensures, is created here and is not read; + 3. the Action is whole-frontier, so no history check runs; + 4. no two effects share a slot; + 5. the schema admits every type: `T2` and `H2` are content types, `B` is + mutable, and each edge's source and target types are admitted; + 6. Echo recomputes `T2` and `H2` as content addresses over their atoms + and the edges this proposal gives them, recomputes the content ids of + `H2.root` and `H2.anchor`, and recomputes the slot id of the resolved + `B.canonicalHead` from its source and type, which the retarget keeps; + 7. the read set, precondition slots, and write set lie inside the + footprint law; + 8. the expected `H1` and version-7 digest hold at `c`, and every endpoint + exists or is created here. + + Its package's footprint law admits range reads, so its validity rule is + `WholeFrontier` whatever this evaluation read. + +7. **Composition.** The write set is the eight target slots `T2`, `T2.atom`, + `H2`, `H2.atom`, `H2.root`, `H2.anchor`, `B.canonicalHead`, and `B.atom`, + plus the range keys `(H2, root)`, `(H2, anchor)`, and `(B, canonicalHead)` + of the edges it creates or retargets. Its reads add the precondition slots: + endpoints `I` and `B` exist, and `B.atom` and `B.canonicalHead` hold their + expected values. No co-scheduled Action reads or writes these. +8. **Patch**, derived by Echo: `UpsertNode T2`, `SetAttachment T2`, + `UpsertNode H2`, `SetAttachment H2`, `UpsertEdge H2.root`, + `UpsertEdge H2.anchor`, `UpsertEdge B.canonicalHead` (same edge id, new + target), `SetAttachment B`. Eight operations, whose actual footprint is + exactly the write set above: each `SetAttachment` writes an atom slot and + each `UpsertEdge` writes its edge and range key. +9. **Decision and durability.** The receipt binds the proposal posture + `Proposed` with the proposal identity, the target-set digest, the patch tag + `Derived` with the write-set and patch digests, the read-set digest, the + validity rule `WholeFrontier`, and the consumed budget. + The decided Tick is written to the WAL, then published. +10. **Visibility.** Coordinate `t` shows `B → H1 → T1`. Coordinate `t+1` shows + `B → H2 → T2`, with `H2 → I`. No coordinate shows `H2` without `T2`. `H1` + and `T1` are no longer reachable from `B`, so they leave the state root, + but they stay records of the state until a patch deletes them (see + [Basis](#basis-budget-retries)). + +A crash before the WAL record loses the Tick entirely; the Action was never +decided, so after recovery it is the same pending submission, evaluated again +when the scheduler selects it. Over the unchanged basis `c` it reproduces the +same proposal. A crash after the WAL record recovers Tick `t+1` by replaying +its patch, re-derives the Action's evaluation over `c` to verify the recorded +proposal posture and digests, and yields the same state root and receipt. + +### Obstructed: stale basis at evaluation + +After coordinate `c`, another edit commits at Tick `u > t` and moves `B` to +head `H3`. Coordinate `c` still shows `H1`; the later coordinate `c'` (Tick +`u`) shows `B -canonicalHead-> H3`. A client that is still displaying `H1` +submits the same invocation, `basisHeadId H1`, and it is admitted at `c'`. + +1. **Admission** at `c'`, as in the committed trace. +2. **Selection.** The scheduler selects the Action while constructing Tick + `u+1` and opens a recording view over `c'`. +3. **Evaluation** reads the `B` atom and the `canonicalHead` edge (to `H3`), + then the authored guard `canonicalHead == basisHeadId` fails. +4. The outcome is the typed obstruction `BasisNotCanonical` with proposal + posture `NoProposal`. There is no proposal identity and no patch. The + receipt records the obstruction and the two-slot read set, so the refusal + is evidence of what the program saw. +5. The state root at `u+1` is unchanged by this Action. The client must issue + a new invocation naming `H3`. + +### Obstructed: conflict at composition + +Two Actions, both evaluated against `H1`, are selected for the same Tick. Both +propose `ReplaceEdge B -canonicalHead-> expected H1`. + +1. Each evaluates and validates on its own. +2. Their write sets overlap on `B.canonicalHead`. In deterministic order the + first joins the Tick; the second gets `RejectedFootprintConflict`. Its + posture is `Proposed` with a `Derived` patch, whose write-set and patch + digests are recorded, but no patch of it is committed. +3. The second Action's `RejectedFootprintConflict` is its final outcome. If + the application submits the edit again, that is a new submission with its + own identity; evaluated at `t+1`, its basis shows `H2`, its guard fails, and + it obstructs with `BasisNotCanonical`. Echo never merges the two edits and + never rewrites the first rejection; reconciling them is the application's + decision. + +## What this design does not do + +- It does not create an opaque patch authority. A program cannot submit a + patch; it can only propose typed effects that Echo validates. +- It does not add application intrinsics, a rope primitive, or a + general-purpose virtual machine. +- It does not decide the state-root definition, and it does not make + admission cost independent of history size. +- It does not implement or imply Continuum transport, comparable-basis + transport, replica import, or distributed settlement. It defines generic + authored effects inside one Echo's existing admission, scheduling, WAL, and + recovery architecture. That Echo can commit an Edict-authored proposal says + nothing about whether a remote history can be imported; those are separate + contracts with their own reviews. + +## Required tests + +Each behaviour below needs a test before the profile that implements it ships. +The first bridge profile must pass the witnesses named in +[What merging accepts](#what-merging-accepts) and every row its scope +exercises. The rows for dependency-scoped validity (Restored value, Scoped +preconditions, Origin resolution, Scoped conflict recovery, Scoped evidence +forms, `OriginOnly` recovery, Scoped basis change, Scoped evaluation +obstruction, Origin reachability) apply only to a later profile that +implements it. A row that pins an exact layout, code, or constant turns that +provisional detail into an obligation when its test lands. + +| Property | Test | +| ------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | +| Atomicity | A failure on the last effect of a multi-node proposal leaves the parent state root and patch unchanged. | +| Ensure identity | Identical existing node: no patch entry. Different existing node: `ContentIdentityConflict`. | +| Partial occupancy | A node record without its atom, or an atom without its record: `CreateNode` obstructs with `PreconditionMismatch` and `EnsureNode` with `ContentIdentityConflict`; neither overwrites the orphan slot. | +| Witnessed footprint | A program that reads a slot outside its law obstructs, even if its writes are in bounds. | +| Stale basis | A `ReplaceAtom` or `ReplaceEdge` whose expected value already disagrees with the value at its evaluation basis obstructs with `PreconditionMismatch`, posture `Proposed`, `NotDerived`, and no patch; when the value instead changed after the origin, a whole-frontier Action obstructs with `BasisChanged` before evaluation and a scoped one at the history check. | +| Budget | Exhausting steps or bytes obstructs with `BudgetExceeded` and `NoProposal`; a proposal whose patch alone exceeds the Action-batch operation limit obstructs with `BudgetExceeded`, posture `Proposed` with its digests, and no committed patch. | +| Effect charges | Each effect is charged one step and its fixed `write_bytes` (64 plus atom bytes for node and atom effects, 128 for edge effects) at emission; a budget one byte short of a proposal's total obstructs with `BudgetExceeded` and `NoProposal`. | +| Atom write bytes | A proposal whose atom bytes exceed the delegated `write_bytes` obstructs with `BudgetExceeded` and `NoProposal`; a whole-frontier `BasisChanged` records zero consumed budget. | +| Validation read budget | A `ReplaceAtom` of a stored atom larger than the remaining `read_bytes` obstructs with `BudgetExceeded`, posture `Proposed`, `NotDerived`, before hashing it; allocation beyond `edict_pure`'s `max_allocated_bytes` obstructs with `BudgetExceeded` and `NoProposal`. | +| Budget-stopped evidence | A scoped proposal whose validation read exhausts the budget records `Compared` with that dependency, and every later one, as not compared; no value past the stop is hashed. | +| Determinism | Same package, invocation, and evaluation basis give byte-identical proposals, proposal identities, read-set and write-set digests, and derived patches, whether the Action is evaluated alone or beside other Actions. Receipts and composite patches are compared only for identical Tick contexts. | +| Canonical order | Emitting the same effects in different orders yields the same canonical `EffectProposal` bytes and proposal identity. | +| Blob-independent order | Two same-kind duplicate effects on one slot with different atoms produce the same canonical image and proposal identity whichever order they were emitted in. | +| Encoding vectors | Fixed byte vectors for every row, the proposal image, every set digest, a bridge table with each posture, validity, evidence, and outcome tag, and `EOACT004` reproduce the specified bytes, sizes, and receipt-v5 digests. | +| In-place validation | Each image validates and reads through a view without heap allocation; an image with nonzero padding, a nonzero unused field, an unsorted section, an out-of-bounds range, or loosely packed blob bytes is refused. | +| No hot-path allocation | With an allocation-counting allocator, a warmed-up Tick of bridge Actions performs zero heap allocations during evaluation, validation, derivation, and composition, and recovery of that Tick allocates nothing per Action. | +| Arena independence | The same Ticks decided on hosts with different initial arena capacities produce byte-identical receipts, WAL records, and state roots. | +| Scratch independence | The same Ticks decided with a freshly allocated (cold) arena and with an arena reused after unrelated earlier Ticks (warm) produce byte-identical receipts, WAL records, retained evidence, and state roots. | +| Range-read entries | An empty observed range encodes as a range entry with count zero, never as an absent outcome, and a nonempty range's entry matches the specified layout byte for byte. | +| Canonical slots | Differently expressed effects on one slot (`EnsureEdge` and `ReplaceEdge` of one edge id; `CreateNode` and `ReplaceAtom` of one node) obstruct with `DuplicateEffectTarget`. | +| Write set | The derived patch's actual footprint equals the write set, including the atom slots of created nodes and the range key of every created or retargeted edge, so a committed `EnsureEdge` and `ReplaceEdge` pass the footprint check. | +| Identity law | A proposed node or edge id that does not match the package's identity law obstructs with `IdentityLawViolation`, posture `Proposed`, `NotDerived`, and recovery reproduces it. | +| Node resolution | A `ReplaceAtom` of a node absent at the evaluation basis obstructs at step 2 with `NodeMissing`, posture `Proposed`, `NotDerived`. | +| Content address | Under `ContentAddressV1`, a node id equal to the specified BLAKE3 over its type, atom, and the edges its creating proposal's `EnsureEdge` effects give it, and an edge id over its endpoints and type, pass; any other id obstructs with `IdentityLawViolation`; fixed vectors pin both derivations. | +| Addressing by type | A `ReplaceAtom` of a node whose type the schema marks content-addressed, or an `EnsureNode` of a mutable type, obstructs with `IdentityLawViolation`; a `ReplaceAtom` of a mutable-type node commits. | +| Edge addressing | An edge from a mutable node keeps its slot id when a `ReplaceEdge` retargets it; a creating `EnsureEdge` from an existing content node, a `CreateNode` of a content type, and a `ReplaceEdge` of an edge from a content node each obstruct with `IdentityLawViolation`. | +| Unreachable warp | An effect naming a key in a missing warp, or in a warp no valid portal chain reaches, obstructs with `UnreachableWarp`, posture `Proposed`, `NotDerived`. | +| Origin reachability | A scoped Action naming a warp unreachable at its origin obstructs with `UnreachableWarp` even when an intervening Tick created the portal that reaches it. | +| Portal permission and cost | At validation step 1, an effect in a descended warp whose chain crosses a portal owned by a type outside `portal_owner_types` obstructs with `FootprintLawViolation`, and a chain whose crossings exceed the remaining budget obstructs with `BudgetExceeded`. | +| Schema | An effect whose node type, atom `type_id`, or edge type the package's schema does not admit obstructs with `SchemaViolation`, posture `Proposed`, `NotDerived`, and recovery reproduces it. | +| Resolved schema | A `ReplaceEdge` whose basis edge type the schema does not admit, or a `ReplaceAtom` whose owner node type does not admit the new atom type, obstructs with `SchemaViolation` after its record is read and charged. | +| Endpoint types | A creating `EnsureEdge` or a `ReplaceEdge` whose source or target node type the schema does not admit for that edge type obstructs with `SchemaViolation`, after its endpoint records are read and charged. | +| Validation order | A proposal that breaks several rules (for example a duplicate target, an unadmitted type, and a missing endpoint) records the obstruction of the earliest step in the validation order, live and on recovery. | +| Conflict before batch limit | A candidate that both overlaps an earlier accepted Action and would exceed the batch operation limit records `RejectedFootprintConflict`, as today's scheduler does. | +| Footprint stages | A target outside the footprint law obstructs with `FootprintLawViolation` and `NotDerived`, and so does a `ReplaceEdge` whose basis edge's range key lies outside the law; a derived patch whose footprint differs from the write set obstructs with `FootprintMismatch` and `Derived`. | +| Resolved footprint | A `ReplaceEdge` whose resolved source node lies outside the footprint law obstructs with `FootprintLawViolation`. | +| Restored value (ABA) | A dependency written A to B and back to A between origin and commit parent is found through the written-slot set and obstructs with `BasisChanged`, including when the intervening patch under-declared its `out_slots`; with one replay patch in the interval missing, the Action obstructs before evaluation as a whole-frontier `BasisChanged`, posture `NoProposal`, with an empty read set. | +| Scoped preconditions | A dependency-scoped Action whose `ReplaceAtom` expected value changed and was restored between its origin and the commit parent obstructs with `BasisChanged`, though the program never read it. | +| Origin resolution | A scoped `ReplaceAtom` whose program never read its node, and whose node is deleted and recreated between origin and commit parent with the same atom, obstructs with `BasisChanged`, because resolution at the origin recorded the node record as a dependency. | +| Scoped conflict recovery | A scoped Action rejected because an earlier Action in its Tick replaced a value it expects recovers as `RejectedFootprintConflict`, not `PreconditionMismatch`. | +| Scoped evidence forms | An evaluation obstruction records `OriginOnly`, a dependency-scoped `BasisChanged` records `HistoryChanged` with no compared values, and every other scoped outcome records `Compared` over commit-parent values; none is compared at a validation position that includes an earlier overlapping write. | +| OriginOnly recovery | A scoped proposal that fails reachability or resolution is recovered by replaying only that failure, with no dependency set rebuilt. | +| Resolution failure evidence | A scoped `ReplaceAtom` whose node is missing at its origin records `OriginOnly` with `NodeMissing`; recovery reproduces it without running the history check. | +| Retry basis | A new submission selected after the head advanced is evaluated at its recorded basis, not at the selection-time state. | +| Receipt digest v5 | A version-5 receipt digest begins with the little-endian `u16` `5` and changes when any bridge field changes, including the validation position, a dependency's comparison mode, or a compared value; version-4 receipt identities are unchanged. | +| Proposal binding | For every `Proposed` outcome class in the recovery matrix, including rejected ones, altering one recorded effect-derived digest or the proposal identity refuses the history. | +| No-proposal evidence | An evaluation that obstructs before proposing records `NoProposal` with its read-set digest and no proposal, write-set, or patch digest. | +| Recovery | Crash before and after the decided-Tick WAL record; fresh-host recovery reproduces the same state root and receipts. | +| Recovered outcomes | A fresh engine recovering a history that holds a committed bridge Action, an obstructed one, and a `RejectedFootprintConflict` reproduces each recorded outcome, receipt, and state root by verification, and records no new admission decision for any of them. | +| Composition | Two Actions with independent witnessed footprints (neither writes a slot the other reads or writes) commit in one Tick. A write/write overlap obstructs the later one, and so does a write/read overlap: A reads X and writes Y, B writes X and Z. | +| Shared structure | Two Actions that `Ensure` the same node already present in the basis both commit in one Tick. | +| Same-Tick identical create | Two Actions that both `Ensure` the same node absent at the commit parent: the later obstructs with `RejectedFootprintConflict` instead of reading the earlier one's write. | +| Referential integrity | An edge to a node neither in the basis nor created by the proposal obstructs with `DanglingReference`; a pre-existing dangling edge elsewhere in the basis does not obstruct an unrelated proposal. | +| Portal chain | An effect in a descended warp records every portal on its root-to-target chain as a footprint and dependency entry, never as a witnessed read; a co-scheduled portal retarget conflicts with it, and a portal changed and restored between origin and commit parent obstructs a scoped Action with `BasisChanged`. | +| Visibility | No published coordinate shows a retargeted head without every node and edge the proposal introduced; pre-existing structure the head reaches is not validated. | +| Witnessed reads | The receipt's read set equals the slots the view resolved, including for a program that reads and then obstructs. | +| Negative reads | An Action that observed a node, atom, or edge set absent obstructs when a co-scheduled Action creates it, including a fresh edge of the observed source and type with a new edge id when the observed set was empty (outgoing-edge range key). | +| Range metering | A range read over a node with more edges than the law's maximum, or than the remaining budget covers, obstructs with `BudgetExceeded` and `NoProposal` before copying any edge; an admissible range charges one step and 64 read bytes per edge. | +| Absent probes | A read that finds nothing records the type it named in `read_type`; a probe for a type outside the law's read permissions obstructs evaluation at once with `FootprintLawViolation`, `NoProposal`, and recovery reproduces the decision from the read set alone. | +| Edge-read basis | An Action whose package's footprint law admits a range read commits only onto its exact evaluation basis, including when this invocation reads no edge. | +| Exact parent | In the first bridge profile, an Action whose evaluation basis is not the commit parent obstructs with whole-frontier `BasisChanged`, posture `NoProposal`, before evaluation; it adds no patch entry and changes no state root, live or on recovery. | +| Final outcomes | A rejected Action's outcome, receipt, and attribution are unchanged after a later submission of the same edit succeeds. | +| Duplicate resubmission | Resubmitting a decided Action's identical content returns `Duplicate` with the original outcome and commits no Tick. | +| Attribution | Every Action in a bridge Tick appears once in the attribution section, mapped to its own receipt entry. | +| One effect per slot | Two effects on one slot (two `ReplaceAtom`, or `EnsureNode` plus `ReplaceAtom` of the same node) obstruct with `DuplicateEffectTarget`, posture `Proposed`, `NotDerived`. | +| Scoped basis change | A dependency-scoped Action evaluated at its origin obstructs with `BasisChanged`, posture `Proposed` with `NotDerived`, and keeps its proposal, read set, and changed dependency when a dependency changed, even if its proposal would also fail validation; an unchanged dependency set lets it commit. | +| Scoped evaluation obstruction | A dependency-scoped Action whose evaluation exhausts its budget, or fails an authored guard, keeps that obstruction with `NoProposal` even when one of its reads changed after the origin; recovery reproduces it. | +| Receipt format | `EPRV0003` records recover byte for byte through the unchanged decoder; a Tick containing a bridge Action is written as `EPRV0004`, with its fixed-profile Actions as all-zero `NotBridge` rows; a Tick of fixed-profile Actions alone stays `EPRV0003` and receipt digest version 4; a history mixing both formats recovers. | +| Package version | A source-compiled package encodes as `ExecutableOperationPackageV2` with a `closure-v2` (no lawpack keys) and a `program-v2-effect`, and its identities use the `v2` domains; a fixed-profile package keeps its V1 bytes and identities exactly. | +| Lawpack by program | A V2 package whose closure carries `lawpack_coordinate` or `lawpack_identity`, or whose program is a fixed profile, is refused at admission. | +| Invocation version | An effect invocation (`invocation-v2-effect`) is admitted only for an effect-program package, and a V1 invocation only for its own fixed profile. | +| Input bounds | An effect invocation whose `application_input_bytes` is not canonical CBOR, or is longer than `max_input_bytes`, is refused at admission; a well-formed one of the wrong shape obstructs evaluation with `InputRejected`. | +| Outcome record | A bridge obstruction, including an authored one such as `BasisNotCanonical`, is retained as `EOACT004` with the same coordinate as its receipt; fixed-profile Actions still write `EOACT003`, and mixed histories recover. | +| Pending recovery | An Action lost with its Tick before the WAL record is recovered as the same submission, not a new one. | +| Ensure resolution | An `EnsureNode` whose identical target already exists is a read, not a write, and the footprint law checks the write set without it; its target read is charged at step 2. | +| Absent endpoint history | An Action whose package admits edge writes keeps the whole-frontier rule, so an endpoint absent at its evaluation basis and created by a later Tick never lets it commit onto that later basis; it obstructs with whole-frontier `BasisChanged`. | +| Bridge result | A committed bridge Action's exact result bytes are retained in `EPRV0004` and `EOACT004` and bound by `result_identity`; recovery refuses re-evaluated bytes that differ. | +| Absent probe row | An absent `ReadRow` carries its expected type in `read_type` and a zero `subject`, and the image validator accepts it. | +| Set encoding | A footprint law or schema with an unsorted or duplicated set is refused at admission; two packages declaring the same sets have identical bytes. | +| Portal owner dependency | A delayed scoped Action whose portal owner's node type changed in an intervening Tick obstructs with `BasisChanged`; the owner read is charged at step 1. | +| Existing edge identity | A `ReplaceEdge` of a basis edge whose id is not its slot id under `ContentAddressV1` obstructs with `IdentityLawViolation`. | +| Unreachable records | A keyed read of a record that a prior Tick made unreachable resolves identically live and after recovery, because the record stays until a patch deletes it. | +| Alpha slot dependency | A scoped `ReplaceAtom` whose owner node record changed in an intervening Tick, with its atom unchanged, obstructs with `BasisChanged` through the resolved node-record dependency. | +| Absent atom probe | An absent atom read records its expected atom `type_id`; a probe for a type outside `atom_types` obstructs evaluation at once with `FootprintLawViolation`, `NoProposal`, before the program sees the result. | +| Content-node adoption | An `EnsureNode` of an existing content node is adopted only when that node's record, atom, and outgoing edges recompute to its id; a node stored under another id obstructs with `IdentityLawViolation`. | +| Schema shape | A footprint law or schema with an unknown, missing, or reordered key, or a node-type entry of any other shape, is refused at admission. | +| Descended read reachability | A scoped Action that only reads a descended warp records that warp's portals and owners as dependencies, enforces `portal_owner_types`, and obstructs with `BasisChanged` when an intervening Tick changes them. | +| Undeclared range read | A range read of an edge type outside `range_edge_types` obstructs evaluation with `FootprintLawViolation`, posture `NoProposal`, before reading anything. | +| Range inspection metering | A range read over a bucket of many edges of other types is charged for every edge in the bucket and obstructs when the bucket length exceeds `max_range_edges`, even when no edge matches. | +| Existing edge source | An identical `EnsureEdge` whose source exists reads and charges the source record, and the edge id is recomputed under the rule its type selects. | +| V2 domains | V2 package, program, invocation, and installed-operation identities use the `v2` schema strings and domains, and differ from V1 identities over the same content. | +| Topology eligibility | An Action whose package's law admits an edge write or a content-node write commits only onto its exact evaluation basis, including when this invocation writes only atoms. | +| Mutable-source alias | A creating `EnsureEdge` or a `ReplaceEdge` from a mutable source that already has another edge of the same type, under any id, obstructs with `IdentityLawViolation`. | +| Beta portal | An effect or read reached only through an edge-owned portal obstructs at step 1 with `FootprintLawViolation`. | +| Program map | An effect program map whose `schema` or `kind` differs from `program-v2-effect`, that has any other key, or whose profile identities differ from the package's, is refused at admission. | +| Dangling source | A creating `EnsureEdge` whose source exists neither at the basis nor in the proposal skips the identity law and obstructs at step 8 with `DanglingReference`. | +| Graph schema binding | A V2 package whose closure names the application's own schema declaration is admitted with a different `graph_schema`; changing `graph_schema` changes the program identity. | +| Output type | A committed result's `result_identity` hashes the program's `output_type`; a program map without `output_type` is refused at admission. | +| Footprint contract | A V2 package whose `footprint_contract_identity` is not the `v2` digest of its `footprint_law` bytes is refused at admission. | +| Authored obstruction | An authored obstruction's `authored_id` follows the specified recipe from its code and canonical detail, and recovery re-derives the same identity. | +| Candidate and composite patches | In a Tick with two accepted bridge Actions, each row's `patch_digest` is its own candidate patch, and the replay patch is their batch composition; recovery verifies both. | +| Bridge decision coordinate | Every `EOACT004` variant carries the 152-byte decision coordinate, and recovery refuses one that does not name the sealed Tick and member index of its receipt entry. | +| Footprint maxima | `max_reads` counts read-set rows, one per slot, or one per named type for an absent slot probed under several types, so two typed probes of one absent slot exceed `max_reads = 1`; `max_writes` counts distinct resolved write slots after Ensure resolution, so an identical `EnsureNode` adds no write; one range read is one row. | +| Effect profiles | A V2 package whose `target_profile_identity` or `application_basis_schema_identity` is not the specified profile digest is refused at admission. | +| Effect basis binding | An effect invocation whose `application_basis_value_identity` is not the digest of its own `application_input_bytes` is refused at admission. | +| Outcome row projection | An `EOACT004` record whose `OutcomeRow` differs from the projection of its receipt-bound `BridgeEntryRow` is refused by recovery. | +| Allocation ceiling | An effect program map without `max_allocated_bytes` is refused; evaluation is bounded by that declaration alone, never by a host's own ceiling. | +| Inherited identities | A V2 package whose input, result, obstruction, interpretation, or evaluation-basis identity differs from its specified profile digest is refused at admission. | +| Evaluation read charges | Node, absent, and atom reads charge one step and 64 `read_bytes`, plus the atom length when present; a read the budget cannot cover obstructs before reading, uncharged. | +| Read types | A present read is authorized by the record's actual type in `read_type`, an absent one by the type it named; recovery reproduces both decisions from the read set. | +| Orphan bucket | Creating a node whose id already has an outgoing bucket left by a non-bridge writer obstructs with `PreconditionMismatch`; a law admitting node creation keeps the whole-frontier rule. | +| Supported profiles | An effect program and package that agree on any interpreter or intrinsic profile other than the specified effect profiles are refused at admission. | +| Id-keyed maps | A graph schema whose `node_types` or `edge_types` keys are out of bytewise order, or repeat an id, is refused at admission. | +| Repeated absent reads | Reading one absent slot under a permitted and a forbidden type yields two rows and `FootprintLawViolation`; reading it twice under one type yields one row. | +| V2 installation record | A retained V2 installation uses schema `echo.operation-installation/v2` and recovers through the V2 decoder; a record with any other schema is refused. | +| Bucket scan charge | A bucket scan charges one step and 128 `read_bytes` per edge for the whole bucket before inspecting any; a scan the budget cannot cover obstructs uncharged. | +| Bridge scope | A bridge Action's receipt entry has the synthetic scope (root warp, invocation identity) and its `scope_hash`; recovery recomputes both from the retained invocation. | +| Mixed batch digests | A Tick of fixed-profile Actions alone keeps its V1 rewrites and composition digests byte for byte; a Tick with a bridge Action uses the `v2` recipes with member kinds, and recovery reproduces them. | +| Evaluation-only proposal cost | The same evaluation at the same origin has the same proposal identity whether validation stops at the history check or runs to the end. | +| Allocation ceiling profile | A program declaring more than `EFFECT_ALLOCATION_CEILING_V1` is refused at admission; a host that cannot provide the declared bytes fails the Tick as a host fault, never obstructing the Action. | +| Range-type refusal recovery | An evaluation-time `FootprintLawViolation` for an undeclared range type recovers as `NoProposal` by re-evaluation, with the same read set. | +| Portal atom read | An atom read of a slot holding a portal records outcome `portal`, the owner's node type as `read_type`, and the portal's digest; it is refused unless that type is in `portal_owner_types`, decided from the row alone. | +| Inherited ceilings | An effect program declaring `max_input_bytes` or `max_result_bytes` above 65,536 is refused at admission; a longer result obstructs with `BudgetExceeded`, `NoProposal`. | +| No result projection | A V2 package carrying `application_result_projection` is refused at admission. | +| Reads authorized before use | A program that reads a node outside its law, then fails an authored guard or exhausts its budget, obstructs with `FootprintLawViolation` at that read; the forbidden value never reaches its obstruction or `authored_id`. | +| Result capacity | A program with a small `max_allocated_bytes` returning input bytes up to `max_result_bytes` fits the pre-sized arena; evaluation never grows it. | +| Read reachability | A read through an unreachable warp, or a chain with a forbidden portal owner, obstructs evaluation at that read with `UnreachableWarp` or `FootprintLawViolation`, `NoProposal`, before the value is visible. | +| Content hash charge | Adopting an existing content node charges its atom hash at step 2; a budget that cannot cover it obstructs there, before the identity law runs. | +| Effect minimum budget | An effect package ceiling or delegated budget below one step is refused at admission; any budget of at least one step is admitted, and shortfalls are `BudgetExceeded` at evaluation. | +| Unreachable read recovery | A read through an unreachable warp recovers as an evaluation-time `UnreachableWarp`, `NoProposal`, by re-evaluation at the origin with the same read set. | +| Footprint law ceilings | A footprint law with `max_reads` above 4,096, `max_writes` above 256, or `max_range_edges` above 65,536 is refused at admission; the arena is sized from the maxima clamped by the delegated budget. | +| ReplaceAtom over a portal | A `ReplaceAtom` whose alpha slot holds a portal obstructs with `PreconditionMismatch` before derivation, even when its expected digest names the portal. | +| Output type coordinate | An effect program whose `output_type` is empty or longer than 1,024 bytes is refused at admission. | +| Effect budget ceilings | A package ceiling or delegated budget above `EFFECT_BUDGET_CEILING_V1` is refused at admission; a program emitting a 1,025th effect, even an identical `Ensure`, obstructs with `BudgetExceeded`, `NoProposal`. | +| Chain charged once | A read whose portal chain the view resolved and charged is not charged again at step 1; a budget covering one traversal suffices. | +| Implied-read permissions | A `ReplaceAtom` whose owner's node type is in `read_node_types` but not `write_node_types` passes the footprint law; one whose owner type is in neither obstructs with `FootprintLawViolation`. | +| Content-scan permissions | Adopting an existing content node whose bucket holds an edge type outside `write_edge_types` and `range_edge_types` obstructs with `FootprintLawViolation`. | +| Content mismatch first | An `EnsureNode` of an existing content node whose atom differs from the proposal's obstructs at step 2 with `ContentIdentityConflict`, never `IdentityLawViolation`. | +| ReplaceAtom current atom | A `ReplaceAtom` whose current atom type is outside `atom_types` obstructs at step 7 with `FootprintLawViolation`; its alpha value is read and charged at step 2. | + +## Open questions + +- How `edict_read` exposes outgoing edges by type to Edict source, and how a + bounded closure read guided by a pure Edict selector is expressed and + budgeted. The metering of a single range read is defined above. +- How Edict source exposes the `ContentAddressV1` inputs; the law itself + is defined above. +- Whether proposals larger than the Action-batch operation limit should ever + be committable. This design says no: such a proposal is still representable + as evidence (`BudgetExceeded`, posture `Proposed` with a `Derived` patch, as + [Basis, budget, retries](#basis-budget-retries) states), but it never + commits and is never split across Ticks. +- When a later bridge profile should adopt dependency-scoped validity. It is + deferred for the first profile; adopting it needs its own executable + evidence, at least the restored-value (ABA) and scoped-precondition + witnesses, and must leave the first profile's recorded outcomes verifiable. +- Which reclamation mechanism, if any, should change what a keyed read of an + unreachable record observes. Until one ships as an explicit, versioned + semantic change, unreachable records stay readable by key. diff --git a/docs/plans/2026-07-18-jim-edict-echo-executable-warp-semantics.md b/docs/plans/2026-07-18-jim-edict-echo-executable-warp-semantics.md index 25fe4a1cb..df3891bf5 100644 --- a/docs/plans/2026-07-18-jim-edict-echo-executable-warp-semantics.md +++ b/docs/plans/2026-07-18-jim-edict-echo-executable-warp-semantics.md @@ -13,6 +13,11 @@ differ from the accepted executable-operation boundary. The accepted campaign is recorded in section 13; the inventory of broader Jim and Echo capabilities does not place those capabilities in scope for the first vertical. +ADR 0023's Jedit lawpack-resource route is itself superseded in part, +effective when flyingrobots/echo#889 merges, by +[Application operation semantics authored in Edict source](../topics/GeneratedRules.md#application-operation-semantics-authored-in-edict-source). +This inventory's lawpack-resource steps are kept as historical evidence. + ## Source basis This report is based on source code, not repository documentation, at these diff --git a/docs/spec/canonical-inbox-sequencing.md b/docs/spec/canonical-inbox-sequencing.md index e02654ace..97406320f 100644 --- a/docs/spec/canonical-inbox-sequencing.md +++ b/docs/spec/canonical-inbox-sequencing.md @@ -49,7 +49,7 @@ Ingress event records are immutable once committed. Processing an event removes ## Decision 6: A Continuum occurrence is part of ingress identity Decision 1 makes content the identity of a local intent. Continuum separates -*what* is intended from *which happening* it is: an `AppliedIntent` has an +_what_ is intended from _which happening_ it is: an `AppliedIntent` has an `appliedDigest`, and an `OccurredIntent` adds an `OccurrenceRef` whose `occurrenceKeyDigest = hash({ issuer, localId })`. Two occurrences of identical content are two acts, and Echo must not collapse them into one submission. @@ -78,10 +78,10 @@ IDs unchanged; a local submission is never matched to an occurrence. Admission applies Continuum's binding law within the target worldline, which is the coordinate lineage an occurrence may be admitted to only once: -| Presented again | Echo's answer | -| --- | --- | -| Same occurrence key, same content, applied digest and writer head | Retry: the existing submission (`Duplicate`) | -| Different occurrence key, identical content | A separate submission, decided and attributed on its own | +| Presented again | Echo's answer | +| --------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------- | +| Same occurrence key, same content, applied digest and writer head | Retry: the existing submission (`Duplicate`) | +| Different occurrence key, identical content | A separate submission, decided and attributed on its own | | Same occurrence key, different content, applied digest or writer head | `RuntimeError::ContinuumOccurrenceConflict`; nothing is admitted and the existing submission is unchanged | The admission mapping from `(worldline, occurrence key)` to submission is @@ -117,13 +117,13 @@ A strand's causal past is the prefix it copied at its fork basis that past does not become a new act because the worldline changed, so the occurrence lineage of a strand includes its inherited prefix: -| Presented on the strand | Echo's answer | -| --- | --- | -| Occurrence decided in the inherited prefix, same binding | `AlreadyPresentInInheritedHistory`, naming the original submission, its head, the fork basis and its receipt when ticketed; nothing is admitted or written | -| Same inherited occurrence key, different binding | `RuntimeError::ContinuumOccurrenceConflict` | -| Occurrence absent from the inherited prefix | Ordinary admission on the strand | -| Occurrence decided on the source after the fork basis | Not inherited | -| Occurrence accepted on the source but undecided at the fork basis | Not inherited: acceptance before the fork is not part of its causal past | +| Presented on the strand | Echo's answer | +| ----------------------------------------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Occurrence decided in the inherited prefix, same binding | `AlreadyPresentInInheritedHistory`, naming the original submission, its head, the fork basis and its receipt when ticketed; nothing is admitted or written | +| Same inherited occurrence key, different binding | `RuntimeError::ContinuumOccurrenceConflict` | +| Occurrence absent from the inherited prefix | Ordinary admission on the strand | +| Occurrence decided on the source after the fork basis | Not inherited | +| Occurrence accepted on the source but undecided at the fork basis | Not inherited: acceptance before the fork is not part of its causal past | When a strand forks, live or while recovery replays the fork, Echo records the submissions its copied ticks attribute. Admission on a strand with no binding of @@ -158,12 +158,12 @@ IDs, and the genuine request is treated as its duplicate. Every envelope now records its `IngressIdentityVersion`: -| Recipe | Version | Domain | Retained as | -| --- | --- | --- | --- | -| Plain intent | `Original` (unchanged) | `ingress:` | `EINGR002` (`EINGR003` with an occurrence) | -| Causal intent, accepted before #885 | `Original` | `ingress:causal:v2\0` | `EINGR002` / `EINGR003` | -| Causal intent, new | `SeparatedCausal` | `echo.ingress.causal.v3\0` | `EINGR004` | -| Continuum occurrence | as its content | `echo.ingress.continuum-occurrence.v1\0` | per content | +| Recipe | Version | Domain | Retained as | +| ----------------------------------- | ---------------------- | ---------------------------------------- | ------------------------------------------ | +| Plain intent | `Original` (unchanged) | `ingress:` | `EINGR002` (`EINGR003` with an occurrence) | +| Causal intent, accepted before #885 | `Original` | `ingress:causal:v2\0` | `EINGR002` / `EINGR003` | +| Causal intent, new | `SeparatedCausal` | `echo.ingress.causal.v3\0` | `EINGR004` | +| Continuum occurrence | as its content | `echo.ingress.continuum-occurrence.v1\0` | per content | `EINGR001` to `EINGR003` are retention formats whose identity interpretation is frozen: they decode to `Original`, including ordinary plain intents, and keep @@ -184,12 +184,12 @@ recipe arrives in the separated form, with a different ingress id. Exact legacy matches take precedence over creating a separated submission, so a resend never becomes a second act: -| Found for the request's original-recipe id on its head | Echo's answer | -| --- | --- | +| Found for the request's original-recipe id on its head | Echo's answer | +| ----------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------------------------- | | A retained submission whose envelope states the same kind, bytes, causal parents, occurrence (both digests) and resolved head | That submission (`Duplicate`, with its original ingress id); staging uses its retained envelope | -| A retained submission whose envelope states something else (an alias) | Not a retry and no reservation: ordinary separated admission | -| A submission without retained envelope material, or committed ingress without a submission | `RuntimeError::OriginalIngressIdentityUnverifiable` | -| Both a legacy and a separated submission of the same request | `RuntimeError::IngressIdentityAmbiguous` | +| A retained submission whose envelope states something else (an alias) | Not a retry and no reservation: ordinary separated admission | +| A submission without retained envelope material, or committed ingress without a submission | `RuntimeError::OriginalIngressIdentityUnverifiable` | +| Both a legacy and a separated submission of the same request | `RuntimeError::IngressIdentityAmbiguous` | The same comparison applies to occurrence retries and to occurrences a strand inherits. The recipe, the retention layout and this lookup are Echo's own; any diff --git a/docs/topics/BenchmarkSceneFixtures.md b/docs/topics/BenchmarkSceneFixtures.md index f7da9cd71..8b29cd72a 100644 --- a/docs/topics/BenchmarkSceneFixtures.md +++ b/docs/topics/BenchmarkSceneFixtures.md @@ -33,11 +33,11 @@ fixture = scene × intent stream × history operation, plus declared outcomes ### Three identities, kept separate -| Identity | Defined by | Changes when | -| --- | --- | --- | -| **Workload identity** | The fixture manifest (below) | The workload changes. Never because Echo changed | -| **Expected-result identity** | Declared outcomes, and any goldens under a named root-format version | Echo's promised semantics or a format version change, with an explanation | -| **Run identity** | Implementation revision, build, environment, machine conditions, raw samples | Every run | +| Identity | Defined by | Changes when | +| ---------------------------- | ---------------------------------------------------------------------------- | ------------------------------------------------------------------------- | +| **Workload identity** | The fixture manifest (below) | The workload changes. Never because Echo changed | +| **Expected-result identity** | Declared outcomes, and any goldens under a named root-format version | Echo's promised semantics or a format version change, with an explanation | +| **Run identity** | Implementation revision, build, environment, machine conditions, raw samples | Every run | An Echo optimization changes the run identity. It must not silently change the workload identity, and it may change the expected-result identity only @@ -99,20 +99,20 @@ nodes, total edges, warps, payload bytes, history length and peak live strands. An illustrative nested-scene declaration: | Tier | Entities | Total nodes | Total edges | Child warps | Payload bytes | Ticks | Peak strands | -| --- | ---: | ---: | ---: | ---: | ---: | ---: | ---: | -| S | 1,000 | ≤ 10,000 | ≤ 12,000 | 1,000 | ≤ 0.5 MB | 600 | 0 | -| M | 10,000 | ≤ 100,000 | ≤ 120,000 | 10,000 | ≤ 5 MB | 600 | 0 | -| L | 100,000 | ≤ 1,000,000 | ≤ 1,200,000 | 100,000 | ≤ 50 MB | 600 | 0 | +| ---- | -------: | ----------: | ----------: | ----------: | ------------: | ----: | -----------: | +| S | 1,000 | ≤ 10,000 | ≤ 12,000 | 1,000 | ≤ 0.5 MB | 600 | 0 | +| M | 10,000 | ≤ 100,000 | ≤ 120,000 | 10,000 | ≤ 5 MB | 600 | 0 | +| L | 100,000 | ≤ 1,000,000 | ≤ 1,200,000 | 100,000 | ≤ 50 MB | 600 | 0 | The figures are illustrative; each fixture's first implementation sets and pins its own. ### Two concurrency modes -| Mode | Purpose | Required control | -| --- | --- | --- | -| **Fixed causal workload** | Compare implementations and execution profiles | Same declared inputs, causal constraints and promised outcome equivalence on every run | -| **Concurrent arrival workload** | Measure admission, queueing and contention | A declared arrival process, captured deliveries, and complete outcome accounting | +| Mode | Purpose | Required control | +| ------------------------------- | ---------------------------------------------- | -------------------------------------------------------------------------------------- | +| **Fixed causal workload** | Compare implementations and execution profiles | Same declared inputs, causal constraints and promised outcome equivalence on every run | +| **Concurrent arrival workload** | Measure admission, queueing and contention | A declared arrival process, captured deliveries, and complete outcome accounting | In both modes the workload is generated before execution, as a logical script. Values the runtime produces, such as commit identities or returned @@ -153,12 +153,12 @@ shared mistakes are still mistakes. Every execution is classified: -| Class | Meaning | May enter a performance comparison | -| --- | --- | --- | -| **Valid** | Generator conformance, required capability coverage and every declared outcome hold. An expected refusal that occurs is a valid outcome | Yes | -| **Invalid** | A declared outcome failed | No; timings are kept for diagnosis only | -| **Unsupported** | A required capability is missing. It never counts as passing coverage | No | -| **Incomplete** | The run stopped before its declared work finished | No; timings are kept for diagnosis only | +| Class | Meaning | May enter a performance comparison | +| --------------- | --------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------- | +| **Valid** | Generator conformance, required capability coverage and every declared outcome hold. An expected refusal that occurs is a valid outcome | Yes | +| **Invalid** | A declared outcome failed | No; timings are kept for diagnosis only | +| **Unsupported** | A required capability is missing. It never counts as passing coverage | No | +| **Incomplete** | The run stopped before its declared work finished | No; timings are kept for diagnosis only | A stubbed operation must never report an impressive zero. @@ -249,17 +249,17 @@ to 93–119 ms while the load average looked ordinary. ## Properties every fixture declares -| Property | Why it matters | -| --- | --- | -| Reachable size: nodes, edges, bytes, separately | The study observed per-node cost rising with scene size on one shape | -| Shape: fan-out, depth, cycles, nodes reached by many paths | Walk queue, revisits, edge filter | -| Warp nesting: count and depth, on nodes and on edges | The walk enters `Descend` on both; no current bench has one | -| Attachment bytes: inline, or a reference to content held outside the graph | Hash bytes against hash structure | -| Writes per tick: count, attachment-only or structural, local or scattered | Incremental-root designs treat these differently | -| Footprints, skew and arrival pattern | Inputs; conflict and refusal rates are outputs | -| Retention obligations: worldlines, strands, pinned readings | What may and may not be reclaimed | -| Readers: count, view size, pinned coordinate | Readings under concurrent writes | -| History: length, strands, suffix size | Log, replay and transport costs | +| Property | Why it matters | +| -------------------------------------------------------------------------- | -------------------------------------------------------------------- | +| Reachable size: nodes, edges, bytes, separately | The study observed per-node cost rising with scene size on one shape | +| Shape: fan-out, depth, cycles, nodes reached by many paths | Walk queue, revisits, edge filter | +| Warp nesting: count and depth, on nodes and on edges | The walk enters `Descend` on both; no current bench has one | +| Attachment bytes: inline, or a reference to content held outside the graph | Hash bytes against hash structure | +| Writes per tick: count, attachment-only or structural, local or scattered | Incremental-root designs treat these differently | +| Footprints, skew and arrival pattern | Inputs; conflict and refusal rates are outputs | +| Retention obligations: worldlines, strands, pinned readings | What may and may not be reclaimed | +| Readers: count, view size, pinned coordinate | Readings under concurrent writes | +| History: length, strands, suffix size | Log, replay and transport costs | ## Implementation principles @@ -284,14 +284,14 @@ Their conformance is checked by `crates/warp-core/tests/scene_fixture_tests.rs`, which CI runs with `native_rule_bootstrap,trusted_runtime`. -| Part | Where | What it establishes | -| --- | --- | --- | -| Generator | `benches/support/fixtures/prng.rs` | SplitMix64 output vectors, cross-checked against an independent implementation; the bounded-integer mapping pinned separately, including a bound above 2^63 | -| Manifests | `benches/support/fixtures/manifest.rs` | `workload_id` and `expectation_id` digested separately, with `edict.canonical-cbor/v1`; a test shows a golden change leaves `workload_id` unchanged | -| Result classes | `benches/support/fixtures/outcome.rs` | Valid, invalid, unsupported and incomplete; only valid results are comparable | -| C1 | `benches/support/fixtures/star.rs` | The star scene built independently of `action_scene`, with identical state roots at 1, 100 and 1,000 cells, and a pinned root | -| F5 | `benches/support/fixtures/think_append.rs` | Append and replay through the trusted host, validated | -| Runner | `benches/scene_fixtures.rs` | A fixed matrix (tiers S and M, seed 7, five rounds each) of classified rounds; a summary only when every round is valid | +| Part | Where | What it establishes | +| -------------- | ------------------------------------------ | ----------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Generator | `benches/support/fixtures/prng.rs` | SplitMix64 output vectors, cross-checked against an independent implementation; the bounded-integer mapping pinned separately, including a bound above 2^63 | +| Manifests | `benches/support/fixtures/manifest.rs` | `workload_id` and `expectation_id` digested separately, with `edict.canonical-cbor/v1`; a test shows a golden change leaves `workload_id` unchanged | +| Result classes | `benches/support/fixtures/outcome.rs` | Valid, invalid, unsupported and incomplete; only valid results are comparable | +| C1 | `benches/support/fixtures/star.rs` | The star scene built independently of `action_scene`, with identical state roots at 1, 100 and 1,000 cells, and a pinned root | +| F5 | `benches/support/fixtures/think_append.rs` | Append and replay through the trusted host, validated | +| Runner | `benches/scene_fixtures.rs` | A fixed matrix (tiers S and M, seed 7, five rounds each) of classified rounds; a summary only when every round is valid | ### F5 append and replay @@ -352,7 +352,7 @@ protocol and tolerance are not yet established. - XYPH: the README on GitHub (`flyingrobots/xyph`), default branch at `f2e6d267` when this revision was written. - Dojo: a documentation snapshot of 2026-10-09, including ADR-0003, the JIT Context Builder design and the Contextual Claims specification. -- James Ross, *CΩMPUTER: The Geometry of All Possible Machines* (2025), +- James Ross, _CΩMPUTER: The Geometry of All Possible Machines_ (2025), prologue and chapters 1–3. - The state-root timing study of 2026-10-17 (`docs/benchmarks/state-root-timing-study.md`, local branch diff --git a/docs/topics/GeneratedRules.md b/docs/topics/GeneratedRules.md index c84d20e4f..f2e93d90d 100644 --- a/docs/topics/GeneratedRules.md +++ b/docs/topics/GeneratedRules.md @@ -307,7 +307,9 @@ all of the following hold: identity, origin basis, commit parent, validation position, each dependency descriptor and comparison mode, and a digest of the compared values. Recovery recomputes the validation at that position and refuses a history whose - result differs; it never trusts the evidence field alone. + result differs; it never trusts the evidence field alone. An Action rejected + as a footprint conflict under the within-one-tick rule above is not + validated, so recovery recomputes its conflict instead. An Action is never re-stamped as if evaluated against its commit parent. A dependency failure names the dependency that changed. The per-tick limit of 64 @@ -387,6 +389,94 @@ boundary. The host/WAL shell must be separated from `native_rule_bootstrap` before Jedit can delete the legacy feature without also losing executable operations. +#### Application operation semantics authored in Edict source + +**Decision 2026-10-15, accepted, effective when +[flyingrobots/echo#889](https://github.com/flyingrobots/echo/pull/889) merges to +`main`; until that merge it is a proposal and ADR 0023 governs unchanged. Tracks +[flyingrobots/jedit#296](https://github.com/flyingrobots/jedit/issues/296). +Supersedes in part [ADR 0023](../adr/0023-admitted-executable-operation-packages.md): +every requirement that assumes the rope law is an imported declarative +resource or lawpack, wherever it appears in ADR 0023 (the rope-law closure, +the package binding direction and obligations, the evidence grades, +Jurisdiction, and Consequences), each marked where it appears and enumerated +in the "Jedit rope-law closure" banner, and its selection under "Alternatives +for Expressing the Rope Law". For bridge Actions, +[Authored Operation Effects](../architecture/authored-operation-effects.md) +also supersedes ADR 0023's prepared-evaluation outcome, as marked there. Every +other provision of ADR 0023 continues to govern, and its original reasoning is +kept. The maintainer decision of 2026-10-17 accepts this authorship decision +and the core architecture of that design on merge, authorizes a bounded +first implementation, and keeps the design's detailed specification +provisional until executable evidence demonstrates it; see +[What merging accepts](../architecture/authored-operation-effects.md#what-merging-accepts).** + +Jedit's persistent-rope `ReplaceRange` law is authored in Jedit-owned Edict +source and compiled by Edict. It is not imported as a declarative executable +resource through a Jedit lawpack, and it is not delegated to a native or +nominally generic sequence-splice capability. + +What does not change: + +- Echo still learns no editor, text, or rope vocabulary. +- The prohibited forms listed under ADR 0023's rope-law closure remain + prohibited: Rust function pointers, callback coordinates, host trait + implementations, Jedit-supplied `MutationPlan`s, a native `replace-range` + intrinsic, and assertions that ambient code implements an operation. +- Jedit must still publish one versioned canonical text-schema declaration + that binds the fact, edge, and attachment propositions, codecs, identity law, + and migration posture, and the package must bind it. +- The evidence-grade table and the handwritten planner's role as test-only + differential evidence are unchanged. + +Evidence for the change, which ADR 0023 did not have on 2026-07-18: + +- The declarative resource route was never implemented. No crate in this + repository decodes or evaluates such a resource, so the route that was chosen + for speed has not delivered a witness. +- Edict source has since grown on its main branch: proven unsigned subtraction, + bounded byte length, slice, and concatenation, and first-order source + functions compiled into authenticated Core. Echo now evaluates those + functions in its pure and bounded-read evaluators (#753). The source route is + no longer the empty-handed alternative ADR 0023 rejected. +- Neither route can produce a committed rope today, for the same reason: no + admitted path turns an evaluated Edict operation into graph writes. The + admitted programs remain single-node compare-and-set and create-if-absent of + caller-supplied bytes. That gap is generic, and it gates every route equally. +- A resource format rich enough to carry rope splitting, joining, balancing, + and obstruction control would itself be an unreviewed second law language. + Authoring in Edict keeps one language for application behavior. + +Consequences: + +- This decision accepts an architectural contract, not an implementation. No + evaluation-to-effect bridge exists until it is built and witnessed. +- The generic evaluation-to-effect boundary must be designed and reviewed + before it is implemented; the design is + [Authored Operation Effects](../architecture/authored-operation-effects.md). + Evaluation proposes effects; it never performs + them. Echo witnesses the actual read and write dependencies, validates basis, + identity, budget, and authority, and commits all proposed effects atomically + within the existing WAL and recovery law, or none. This decision does not + approve an opaque patch authority. +- Edict language features are added only when complete authored source + demonstrates the need. Isolated probes do not justify a feature. +- A native sequence-splice capability is rejected unless the complete authored + implementation demonstrates either a fundamental expressiveness gap that no + small, general language feature closes, or a measured resource problem that + no generic runtime optimization solves without changing authored semantics. + Even then, the logical splice contract must be separated from its + implementation strategy, and the capability requires its own design review. +- Rope completion requires two acceptance targets. The first is semantic + correctness: an Edict-authored `ReplaceRange`, possibly over an inefficient + representation (flat text is acceptable), commits correct bytes with + canonical evidence. Its witness creates content, links it, and moves the + head in one atomic Tick, then recovers that result on a fresh engine. The + second is + persistent-rope correctness: path copying, retained identity for unaffected + subtrees, preserved invariants, and bounded work. The first does not complete + the rope. + ## Footprint Honesty Generated footprints are compile-time claims. Runtime footprint checking in diff --git a/schemas/edict-provider/README.md b/schemas/edict-provider/README.md index 958c9489f..4bf85393c 100644 --- a/schemas/edict-provider/README.md +++ b/schemas/edict-provider/README.md @@ -22,7 +22,6 @@ automatic upgrade from a legacy selection. `provider_source_module_generation` checks that every pre-existing semantic declaration is identical in both variants and that module generation has its owning schema root. - ## Authority The checked source names one authority artifact and one canonical domain for diff --git a/schemas/edict-provider/contracts/source-modules-v1/README.md b/schemas/edict-provider/contracts/source-modules-v1/README.md index cbd99e0b9..823a117e3 100644 --- a/schemas/edict-provider/contracts/source-modules-v1/README.md +++ b/schemas/edict-provider/contracts/source-modules-v1/README.md @@ -8,10 +8,10 @@ These are the exact Edict-owned contract-pack bytes from merge Echo selects this pair only through `ProviderContractPublicationV1::SourceModules`. Earlier selectors retain their existing bytes, bounds and inventories. -| Artifact | SHA-256 | -| --- | --- | +| Artifact | SHA-256 | +| ------------------------------- | ------------------------------------------------------------------ | | `edict-provider-contracts.cddl` | `8f8db4052e1bb85c4f728a0a453c4eb20904bcf2ce81530ffdbfce9351e209bc` | -| `manifest.json` | `29927f6db5e0fe1e5e7475bef3fb2c6e7f0f84ea56304fd97bd1299f1c2bb4be` | +| `manifest.json` | `29927f6db5e0fe1e5e7475bef3fb2c6e7f0f84ea56304fd97bd1299f1c2bb4be` | The publication has twelve contracts, eight domains and five unchanged contract resources. It adds `source-closure` and `edict.source-closure/v1`.