Repository navigation
Lower and verify projected compare-and-set Edict operations #763
Description
Activity
E01 execution plan from fresh main
Base:
1589743873450b79acc06d3add9b63e61782c202; isolated branchfeature/edict-projected-cas.Source inspection confirms the work spans provider and runtime admission. The runtime has unprojected compare-and-set, but
EchoOperationInvocationV1::from_valueadmits canonical application input only inPROJECTED_CREATE_INVOCATION_SCHEMA(crates/warp-core/src/echo_operation.rs#2989@1589743873450b79acc06d3add9b63e61782c202).validate_application_input_bindingbinds key and replacement, with no expected-digest binding (crates/warp-core/src/echo_operation.rs#1204@1589743873450b79acc06d3add9b63e61782c202). Simply admitting the CAS program kind in the lowerer would therefore not meet this issue.One coherent implementation/PR, with ordered witnesses:
- Runtime RED: a projected CAS invocation round-trips canonical application input and its expected digest, then admission rejects a substituted expected digest with a stable structured kind. Preserve exact legacy CAS/create bytes and identities. Bind the expected attachment-value digest through an explicit projection path; do not interpret a Keep BlobId as that digest.
- Provider RED: compile a real authored update, lower it and independently reconstruct the package in the verifier. Require exact effect, target intrinsic/profile, footprint, authority, input binding and result projection. Add rejection witnesses for rebound projection and expected-digest metadata. Retain create compatibility controls.
- End-to-end GREEN: public compiler build, verified package admission, matched scheduler-owned update, stale-digest typed noncommit, missing-node and bounded-replacement cases. Assert actual attachment content and commit/outcome evidence; root equality alone does not prove absence of a detached write.
- Recovery witness: persist through the existing WAL lifecycle and reconstruct in a fresh host with the same explicit basis and typed outcomes, without application callbacks.
- Rebuild checked provider components reproducibly; synchronize schemas/package identities and canonical owner
docs/architecture/application-contract-hosting.md; run provider/runtime/host gates, documentation accuracy, Code Lawyer and independent agy review before merge.
This is a test/implementation plan, not executed RED evidence. E02 PR #775 is not a prerequisite on this base; any key-bound contract merged while E01 is underway must be preserved when reconciling main. Reuse the existing guarded workers and aggregate budgets. Runtime data is near its 4 GiB ceiling; preflight must pass before a workload starts, with only verified owned disposable output eligible for cleanup.
E01 native projected compare-and-set boundary
Commit:
74e904d49bc8074462a9b4df4e93452394845062. Issue: #763. Base:1589743873450b79acc06d3add9b63e61782c202. Branch:feature/edict-projected-cas.The native invocation codec now has a distinct projected-CAS schema retaining canonical application input in the invocation identity. Its projection optionally carries
application_input_expected_value_digest_path. Static admission requires this path for projected CAS, exact equality with the invocation's 32-byte expected attachment-value digest, and omission for create. Missing or substituted bindings reportApplicationInputMismatch. Existing legacy encoding branches retain their original field sets.Executed evidence
All Rust runs used the existing guarded Docker worker and stable target. The initial resource preflight refused the source copy; no test ran then. The disposable source archive was loaded into memory and removed after generation, retaining exact source in the worktree and a hash manifest. No budget was raised. A later worker reservation belonged to another agent; this task waited and acquired both canonical worker keys only after release.
- Codec RED:
cargo +1.96.0 test --locked -p warp-core --lib echo_operation::tests::projected_cas_invocation_preserves_application_input_and_identity -- --exactfailed with decoded application inputNoneinstead of the supplied canonical bytes. - The first binding test used the create fixture's smaller budget and returned BudgetExceeded. That is fixture setup evidence, not the final expected-digest RED.
- Corrected binding RED:
cargo +1.96.0 test --locked -p warp-core --lib echo_operation::tests::projected_cas_admissionfailed because static admission accepted an absent digest binding, and the proposed digest projection field was unsupported. The test budget was valid for CAS. - GREEN:
cargo +1.96.0 test --locked -p warp-core --lib echo_operation::testspasses 21 tests. This includes a positive exact-digest static-admission control and structured substitution refusal. cargo +1.96.0 clippy --locked -p warp-core --lib -- -D warnings -D missing_docspasses.git diff --checkpasses. The workspace crate was invalidated with scoped cargo clean before final validation; dependency caches were retained.
The new tests isolate codec/static-admission behavior using a synthetic internal fixture. They do not establish fully admitted compiler-produced CAS package execution, causal-basis correctness, or recovery. Existing create lifecycle tests remain controls. No full Echo gate or independent review is claimed.
Remaining issue work
Add public construction/package production, independent lowerer/verifier CAS derivation and exact metadata refusal; synchronize generated schema/component/package identities; exercise a real public Edict compiler build, matched scheduler update, stale precondition, missing node, bounded replacement and callback-free recovery. Preserve any E02 key contract merged before integration. Request Code Lawyer and agy review of the complete candidate; agy currently remains quota-blocked.
Final measured aggregate usage: build 14296130909 bytes, runtime data 4264047965 bytes, logs 24955084 bytes. Host/VM free space exceeded 600 GiB. Limits remain 20 GiB build, 4 GiB data, 128 MiB logs. Data headroom remains small. The worker was stopped and the reservation released.
- Codec RED:
E01 native provider CAS derivation
Commit
4b94e724891b53fdf51d6e18da1f887af3d86b5aonfeature/edict-projected-cas, following native invocation binding commit74e904d49bc8074462a9b4df4e93452394845062. Issue: #763.The lowerer and structurally separate verifier now select create or compare-and-set explicitly. CAS requires the write operation profile, CAS intrinsic, replace write class, distinct expected-digest input field and at least four steps. Encoding selects the existing CAS runtime identities for basis, footprint, input, result, obstruction and target profile. The verifier reconstructs the expected package and rejects a rebound digest path. Existing create-package regression suites remain passing. No application coordinate selects native code.
Evidence and limits
The first provider witness failed with typed UnsupportedSemantics at the existing create-only boundary. After implementation, the native lowerer emitted a CAS package, and the independent verifier accepted it and rejected a modified digest path. A subsequent RED showed a three-step CAS configuration was accepted; the corrected implementations require the runtime's four-step minimum. Missing expected-digest metadata and aliases to key/replacement fields also refuse through both provider entrypoints.
Final guarded Docker commands:
cargo +1.96.0 test --locked -p echo-edict-provider-verifier --test executable_operation_package: 43 passed.cargo +1.96.0 test --locked -p echo-edict-provider-lowerer --test executable_operation_package: 13 passed.cargo +1.96.0 clippy --locked -p echo-edict-provider-lowerer -p echo-edict-provider-verifier --lib -- -D warnings -D missing_docs: passed.git diff --check: passed.
The fixtures are synthetic, internally rebound semantic closures. They prove native provider selection, package reconstruction and the specified refusals. They do not establish real compiler output compatibility, checked Wasm components, generated schema consistency, scheduler execution or recovery. The package schema and checked component production are still pending in this branch. No PR or merge-ready claim is made for this intermediate commit.
Next: synchronize the generated schema; produce and exercise a real Edict CAS lawpack/build; rebuild both checked components reproducibly; verify admission, matched update, stale digest noncommit, missing node, bounded replacement and callback-free WAL recovery. Preserve any E02 contract merged before final integration. Complete Code Lawyer and independent agy review of the full candidate; agy currently has no available quota or new verdict.
Resource receipt: 14285881856 build bytes; 4138512896 runtime-data bytes; 22960444 log bytes. Limits remain 20 GiB / 4 GiB / 128 MiB. Host and VM free space exceeded 600 GiB. Both shared worker keys were reserved together; the worker is stopped and reservations released. Workspace provider artifacts were invalidated; dependency caches were reused.
E01 reproducible provider production and real Edict build
Commit
8a09a4ab050e24ae4b867e6b732ddf72c2061f80, branchfeature/edict-projected-cas. Issue: #763.The generated schema now admits CAS configuration with explicit expected-digest metadata and a four-step minimum, and the result-projection digest path. The schema tests first failed OwningRootRejected for both valid CAS shapes, then passed after the schema change. Create projection shape remains admitted.
Both provider components were built twice with the designated pinned Rust 1.90 x86_64 toolchain, with scoped component cleaning between rounds. Exact byte comparison passed. Lowerer SHA-256:
b5e621cf20f18bf6cc817c474b404ad29eed9b83d37b560ed5777d47b0f7e036. Verifier:5c2a028215fdb424cd1c5b30e2182c85646eb63e7d5a8ae21ebb773f65a21fc6. Promotion initially refused the old checked pins, then passed after pinning these reproduced candidates. The generated helper's schema identity was updated before building; native helper and real-host agreement pass.Provider package identity:
sha256:bef39ea60891b2bec38643fc8307ea38cadf3915159e9717177bff8ec3335128. Raw manifest SHA-256:fd6797962b164248d1b725ab37de17373c682f1b885534c0fa772d42c1c25fde.Public compiler witness
The authored
examples.cas_echo@1.updateCelluses a derived authenticated lawpack with expected inputBytes<exact=32>, replace write class, CAS intrinsic and explicit input binding. Seed bytes are preserved from Edict commit3f81f759e921a69b04fe8cf8e62e62f8f3dc7b7e; the reproducible recipe rebinds the affected digests rather than manufacturing Core or Target IR.The pinned public Edict compiler from commit
2405a550e93e1e97fff640caa44bbd0f65ffff3c, binary SHA-2563b082d61c8cd23b0f917efb55c4eebd54e75c0df5d31c72f90ad856853678bf5, completed the JSONL application build with exit 0 and zero errors. Its exact outputs are committed undercrates/echo-edict-provider-verifier/tests/fixtures/compiler-produced-cas/built/:- Executable package: 2472 bytes, SHA-256
4d671f8d9515c7d60c82e938103e59231eecab3c60782874f2d6fc2ff27c0d17. - Verification report: 912 bytes, SHA-256
02ff41155c7ad5665633063cc25ec56c9fa7aa04f64fc951eb4cf239d94d7429, decoded outcomeaccepted.
This establishes real compiler/provider production. It does not establish scheduler execution, stale-digest noncommit or fresh-host WAL recovery of this CAS package. Those are the next E01 requirements.
Validation
Guarded Docker runs passed the lowerer executable suite (13), lowerer contract suite (45, one explicitly ignored regeneration entrypoint), verifier executable suite (43), schema suite (2), package suite (17), package corpus (4), and isolated provider-host suites (5 conformance, 6 helper, 23 host, 16 package, 1 resource synchronization). The three ignored host child entrypoints are exercised by parent witnesses. Strict native provider-library Clippy passed. Generated artifacts/package/assets consistency commands passed. No full-project or final review approval is claimed.
Duplicate candidate exports were removed only after matching their hashes to retained checked binaries. Unique source and evidence remain preserved. Cleanup receipt records final aggregate build 14587978946 bytes, runtime data 4139693250 bytes, logs 23044812 bytes; limits remain 20 GiB / 4 GiB / 128 MiB. Host/VM free space exceeded 600 GiB. Workers are stopped and reservations released.
The task remains open for runtime integration, required review and merge. Agy has no new verdict while quota-blocked.
- Executable package: 2472 bytes, SHA-256
E01 compare-and-set PR opened
PR: #776
Issue: #763
Head:4894eb4b6728193b8980095e9d269fde067d0e9f.Five exact-compiler-package runtime integration tests now pass, with strict Clippy. The added fifth witness mutates the expected-digest projection to alias the node-key path and pins the mutated package identity in admission policy. Admission rejects it as
ArtifactInvalid/InvalidStructurebefore installation. This establishes structural refusal rather than merely failure to match the old hash.The fixture README no longer calls runtime recovery pending, and the root README links the exact-byte scheduler/recovery witness. The source and executable tests remain the evidence; documentation edits do not add behavior. Earlier four-test runtime and recovery evidence remains in Reader receipt
9b8620b1-2117-4e28-95ab-1cb06cc68ff1.This run invoked the resource guard directly, with no git-locks wrapper and no container flock, following the user's clarification. Aggregate limits and fail-closed monitoring remained enforced. The worker stopped at completion. Final build/data/log measurements: 14162833675 / 4143509771 / 23188017 bytes.
Current-head CI, complete Code Lawyer audit and independent agy approval remain pending. Agy remains quota-blocked, with no verdict. A semantic audit question remains: confirm that configured input bindings preserve the authored effect argument rather than merely reproducing matching metadata. The happy-path compiler fixture does not establish this general proposition. The PR expressly records this uncertainty; no merge readiness or task completion is claimed.
Next: audit the complete PR against the current mainline and review feedback; reproduce any semantic-binding gap with a valid compiler control; implement justified fixes with RED/GREEN; obtain required validation and reviews before merge. E01 remains one coherent PR, and no Keep adoption is included.
task: E01
type: Feature
title: "Lower and verify projected compare-and-set Edict operations"
status: planned
feedback_items: "5"
audit_commit: 01161c1745baad0d713234ba1a671b9a26923aa4
owner_repository: echo
owner_component: echo-edict-provider-lowerer, echo-edict-provider-verifier, warp-core
source_commit: a93e9d8
prerequisites: []
issue: #763
Feature
1. Background Context
This Echo prerequisite supports the audited Edict author-study repair.
Inspect Echo at
a93e9d82e89455ed1fa0b63447c88de544b9da26.Source:
crates/echo-edict-provider-lowerer/src/executable_operation.rs#1092@a93e9d82e89455ed1fa0b63447c88de544b9da26;crates/echo-edict-provider-verifier/src/executable_operation.rs#1140@a93e9d82e89455ed1fa0b63447c88de544b9da26;crates/warp-core/src/echo_operation.rs#2797@a93e9d82e89455ed1fa0b63447c88de544b9da26.Keep adoption is related architecture, not a prerequisite for this existing runtime path.
2. Problem Description
The generic runtime has compare-and-set. The Edict lowerer and verifier accept only the create effect on this path.
2b. Proposed Solution
Extend the generic lowerer and independent verifier for the existing compare-and-set program. Bind expected attachment-value digest, canonical application input, result projection, authority, footprint, and typed mismatch evidence. Preserve every currently merged input-bound contract and old create packages.
2c. Alternatives considered and rejected
Leave the limitation undocumented: authors cannot identify the contract boundary.
Combine unrelated fixes: a reviewer cannot verify one outcome independently.
2d. Acceptance Criteria
Compile, independently verify, admit, and execute a matched update. Observe typed noncommit for a stale expected digest. Verify explicit basis and replay/recovery. Test missing node, substituted expected digest, invalid projection, and bounded replacement. Neither source nor core receives application-specific callbacks.
2e. Test Plan
Golden: independently verified projected execution. Edges: metadata substitution, invalid input, authority failure, stale basis, and callback-free recovery. Known failure modes: lowerer/verifier disagreement or unsupported metadata ignored by a legacy provider. Fuzz and stress: deterministic bounded witnesses under Echo resource guards.
3. Prerequisites
E01 and E02 have no unconditional dependency. Each must preserve the contracts already merged by the other.
4. Scope
In: Generic Echo provider components, projected invocation/runtime integration, compatible schemas, package production, and complete execution/recovery evidence.
Out: Keep backend adoption, graph ontology changes, application algorithms, general ingress schema validation, and new caller authentication.
5. Why now
The study shows an author cannot safely infer this boundary from the current entry points.
Keep Storage Boundary
Application compare-and-set compares an Echo attachment-value digest under an explicit causal basis.
Keep content-addressed storage verifies a versioned
BlobIdpreimage.These coordinates are not interchangeable. Keep adoption is separate work, tracked by Echo #722 and #760.
Use existing Echo operation interfaces. Do not call Keep directly from authored Edict.
6. Risks
A change can invalidate exact artifact pins or hide independent errors.
Use explicit version and compatibility checks. Do not infer execution from a build receipt.
7. Definition of Done
The acceptance checks pass on the reviewed head.
The task has one merged PR with issue traceability.
Record RED, GREEN, full verification, reviews, and the integration commit.
Update this task and ROADMAP.md with the observed result.
8. Stakeholders
James: project owner and application author.
Edict authors: accurate compiler contracts and usable diagnostics.
Echo maintainers: verified portable artifacts and explicit runtime limits.
9. Related Issues
Study: source feedback.
Audit: claim audit.