Preserve typed result projections for Echo targets by flyingrobots · Pull Request #174 · flyingrobots/edict

flyingrobots · 2026-07-29T12:20:30Z

Plain-English Walkthrough

TL;DR

[claim:compiler-owned-result-projection, confidence:1.00] Edict now preserves an application operation's authored result assembly as a bounded, canonical edict.result-projection/v1 artifact derived from exact Core and Target IR. The public application build independently verifies that artifact and passes the same bytes and digest into both provider component closures.

This closes the compiler-side contract required by Echo #698. It does not evaluate the projection, reconstruct an application result in native code, or add runtime authority.

Walkthrough

Previously, Target IR retained the intent result expression, but the executable-operation provider closure did not carry a separately typed, canonical description of how the public application result is assembled. Echo therefore had no compiler-owned result contract to evaluate or recover.

[claim:projection-dataflow, confidence:1.00] The new flow keeps result authorship in Edict and makes every boundary explicit:

flowchart LR
    A[Edict source and lawpack closure] --> B[Core result]
    B --> C[Target IR result]
    C --> D[Bounded canonical projection]
    D --> E[Independent reverse verification]
    E --> F[Lowerer and verifier semantic-input closures]

Caption: Compiler-owned result projection flow

Real Edict source and its complete lawpack closure produce Core and matching Target IR.
The compiler emits a closed projection over declared application input and capability-step results.
A structurally reverse verifier decodes the bytes, recomputes identity, reconstructs the complete semantic closure and result expression, and compares both source artifacts.
Only the accepted bytes and digest enter the checked provider component requests.

The provider receives data, not an application callback. Projection emission and verification have no filesystem, network, process, model, or runtime imports.

[claim:closed-and-bounded, confidence:1.00] The v1 expression language permits records, declared application input, capability results addressed by Target IR step identity, and bounded field paths. Unsupported calls, undeclared locals, shape mismatches, zero or exceeded bounds, noncanonical bytes, substituted digests, altered Target results, and altered Core or lawpack closure identities fail with structured rejection kinds.

[claim:independent-verification, confidence:1.00] Verification does not call the emitter. It decodes and reproduces canonical bytes, recomputes the domain-framed identity, reconstructs the complete Core-derived semantic closure, reverse-maps projection sources to Core, and requires the reconstructed result to equal both Core and Target IR.

[claim:provider-closure-binding, confidence:1.00] The standalone application build requires exactly one admitted projection, independently verifies it, then binds the same canonical artifact into both lowerer and verifier semantic-input sets under role 07-result-projection. A provider that does not declare the domain refuses at the existing schema-admission boundary.

Compatibility and ownership

[claim:target-ir-compatibility, confidence:1.00] General Target IR remains available for operations outside the first projection subset: per-intent projection failures are reported separately and legacy artifacts without an explicit semantic closure claim neither a projection nor a projection failure. The executable application build is intentionally stricter and refuses a missing, ambiguous, or failed projection.

Echo #698 owns generic package inclusion, runtime evaluation, durable result binding, and recovery. The current external Hello Echo build therefore reaches the expected UnsupportedArtifactDomain refusal at Echo's six-input provider package; no provisional Echo-owned projection format is introduced here. Hello Echo #18 owns the later concrete GreetingCreated witness.

No dependencies were added.

RED / GREEN evidence

Boundary	RED	GREEN
Projection artifact and verifier	`cargo test -p edict-syntax --test result_projection` failed at the committed `NotImplemented` boundary in `6a422147`	16/16 projection tests pass at this head
Target emission	`echo_target_lowering_emits_the_verified_result_projection` failed before `3d98675f`	Target lowering emits the exact reviewed bytes and digest
Provider closure	`compiler_result_projection_is_bound_into_the_provider_closure` failed with `ResultProjectionUnavailable` before `d88f8a8`	Both provider requests carry the compiler artifact
Complete closure	`mutated_target_lawpack_closure_fails_closed` failed at `f4bdc39e`	A substituted lawpack digest now fails closed
Repository gate	—	`cargo xtask verify` passed: format, clippy, all workspace tests and doctests, goldens, provider fixtures/contracts, dependency boundary, contract graph, and diff check

Appendix: Citations

Claim	Evidence	Confidence	Notes
`claim:compiler-owned-result-projection`	`crates/edict-syntax/src/result_projection.rs#187@8cd6bbe201ad963cf0e253be4b7378e1947afc86`; `exact_core_and_target_ir_emit_the_typed_hello_echo_projection` in `crates/edict-syntax/tests/result_projection.rs`	1.00	Canonical bytes and digest are checked against generator-owned fixtures.
`claim:projection-dataflow`	`crates/edict-syntax/src/target_ir.rs#297@8cd6bbe201ad963cf0e253be4b7378e1947afc86`; `crates/edict-cli/src/application_build.rs#304@8cd6bbe201ad963cf0e253be4b7378e1947afc86`	1.00	Target lowering emits the projection; application build admits it.
`claim:closed-and-bounded`	`crates/edict-syntax/src/result_projection.rs#180@8cd6bbe201ad963cf0e253be4b7378e1947afc86`; `docs/topics/result-projections/test-plan.md#36@8cd6bbe201ad963cf0e253be4b7378e1947afc86`	1.00	Golden, failure, boundary, fixed-seed property, and bounded stress cases are executable.
`claim:independent-verification`	`crates/edict-syntax/src/result_projection.rs#249@8cd6bbe201ad963cf0e253be4b7378e1947afc86`; `crates/edict-syntax/src/result_projection.rs#443@8cd6bbe201ad963cf0e253be4b7378e1947afc86`; `independent_verifier_reconstructs_the_authored_core_result` in `crates/edict-syntax/tests/result_projection.rs`	1.00	Reverse reconstruction and closure mutation tests cover the independent path.
`claim:provider-closure-binding`	`crates/edict-cli/src/application_build.rs#314@8cd6bbe201ad963cf0e253be4b7378e1947afc86`; `crates/edict-cli/src/application_build.rs#918@8cd6bbe201ad963cf0e253be4b7378e1947afc86`; `crates/edict-cli/src/application_build.rs#984@8cd6bbe201ad963cf0e253be4b7378e1947afc86`; `crates/edict-cli/src/application_build.rs#1112@8cd6bbe201ad963cf0e253be4b7378e1947afc86`	1.00	The same verified artifact is bound into both component requests.
`claim:target-ir-compatibility`	`crates/edict-syntax/src/target_ir.rs#317@8cd6bbe201ad963cf0e253be4b7378e1947afc86`; `target_lowering_exposes_an_unsupported_result_projection_without_claiming_one` in `crates/edict-syntax/tests/result_projection.rs`	1.00	Unsupported projection does not erase otherwise valid Target IR.
`claim:full-local-gate`	`cargo xtask verify` — passed at `8cd6bbe201ad963cf0e253be4b7378e1947afc86`	1.00	Complete repository verification command and observed result.

Closes #173.

flyingrobots · 2026-07-29T12:20:56Z

@coderabbitai review

coderabbitai · 2026-07-29T12:20:57Z

Walkthrough

Adds a compiler-owned edict.result-projection/v1 artifact with canonical encoding, digest identity, Core/Target verification, Target lowering outputs, provider closure binding, contract schemas, fixtures, documentation, and extensive validation.

Changes

Result projection support

Layer / File(s)	Summary
Projection contract and canonical encoding `crates/edict-syntax/src/result_projection.rs`, `crates/edict-syntax/src/lib.rs`, `docs/abi/edict-result-projection.cddl`	Defines the bounded projection model, canonical CBOR representation, digesting, Core/Target derivation, reverse verification, and structured failures.
Target lowering and projection outcomes `crates/edict-syntax/src/target_ir.rs`, `crates/edict-syntax/tests/result_projection.rs`	Emits per-intent projections, records unsupported-result failures, and validates mutation, shape, identity, bound, determinism, and stress cases.
Application admission and provider closure binding `crates/edict-cli/src/application_build.rs`	Requires exactly one verified projection and adds its canonical bytes and digest to lowering and verification semantic inputs.
Provider contract-pack integration `crates/edict-provider-schema/...`, `fixtures/provider-contracts/v1/...`, `xtask/src/provider_contract_pack.rs`, `xtask/src/tests.rs`	Adds the result-projection schema, contract root, digest domain, manifest entries, representative values, and drift checks.
Golden artifacts and contract documentation `xtask/src/lawpack_goldens.rs`, `fixtures/lawpack/hello-echo/*`, `docs/topics/...`, `CHANGELOG.md`	Generates Hello Echo projection goldens and documents the projection, CLI closure, Target IR, fixture, and test-plan contracts.

Estimated code review effort: 4 (Complex) | ~60 minutes

Sequence Diagram(s)

sequenceDiagram
  participant Compiler
  participant TargetLowering
  participant ApplicationBuild
  participant Provider
  Compiler->>TargetLowering: derive Core/Target result projection
  TargetLowering->>ApplicationBuild: return projection or failure
  ApplicationBuild->>ApplicationBuild: verify exactly one projection
  ApplicationBuild->>Provider: bind canonical bytes and digest
  Provider->>Provider: consume seven semantic inputs

Possibly related PRs

flyingrobots/edict#67: Established the Target IR lowering path extended with result-projection outputs.
flyingrobots/edict#162: Introduced the provider contract-pack infrastructure extended with the new schema.
flyingrobots/edict#170: Established the application-build provider invocation path extended with projection binding.

Poem

Core shapes a result,
Target gives it a name,
Canonical bytes march onward,
Digests guard the frame.
Echo carries seven inputs—
No phantom fields remain.

🚥 Pre-merge checks | ✅ 4 | ❌ 1

❌ Failed checks (1 warning)

Check name	Status	Explanation	Resolution
Docstring Coverage	⚠️ Warning	Docstring coverage is 72.60% which is insufficient. The required threshold is 80.00%.	Write docstrings for the functions missing them to satisfy the coverage threshold.

✅ Passed checks (4 passed)

Check name	Status	Explanation
Linked Issues check	✅ Passed	The implementation matches `#173`: projections are Core-derived, bounded, independently verified, and fail closed for invalid or unsupported cases.
Out of Scope Changes check	✅ Passed	The added docs, tests, fixtures, and build wiring all support result projections; no unrelated changes stand out.
Title check	✅ Passed	The title is concise and accurately captures the main change: preserving typed result projections for Echo targets.
Description check	✅ Passed	The description is directly about the same result-projection changes and matches the implemented work.

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

_{Comment @coderabbitai help to get the list of available commands.}

flyingrobots · 2026-07-29T12:21:01Z

@codex please review

coderabbitai · 2026-07-29T12:21:01Z

✅ Action performed

Review finished.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 07e9c8c4c7

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

coderabbitai

Actionable comments posted: 15

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@crates/edict-cli/src/application_build.rs`:
- Around line 1048-1067: Add RED/GREEN unit coverage in the existing tests
module and update the owning test-plan.md for the negative paths enforced by
single_result_projection and with_result_projection_input: zero projections,
multiple projections, failures alongside a valid projection, and a digest
mismatch. Construct deterministic small BTreeMap fixtures and a mutated artifact
digest, verify the expected ResultProjectionUnavailable or
ResultProjectionDigestMismatch errors, then implement only the minimal changes
needed for the tests to pass and mark the plan cases implemented.

In `@crates/edict-syntax/src/result_projection.rs`:
- Around line 275-294: Remove the explicit validate_projection_bounds call from
decode_result_projection and rely on encode_result_projection’s existing
validation during the canonical round-trip check. Preserve the current error
propagation and exact-byte comparison behavior.
- Around line 412-434: Replace the bare "arg.0" literal in
resolve_application_input with a named constant representing the Core lowering’s
single application-input local, shared with or explicitly tied to the Core
emitter. Document the invariant that this local must use that name, and preserve
the existing matching and duplicate-rejection behavior.
- Around line 37-45: Make ResultProjection and ResultProjectionArtifact fields
private to preserve canonical and digest invariants, matching the encapsulation
used by VerifiedResultProjection. Add or retain read-only accessors and update
consumers such as verify_result_projection and application_build to use them,
while preserving construction and validation behavior.
- Around line 932-978: Add a remaining expression-depth parameter or counter to
projection_from_value and expression_from_value, decrementing it before
recursively parsing nested record field expressions and rejecting when the
configured MAX_RESULT_PROJECTION_NODES limit is exhausted. Propagate this state
through every projection-expression parsing call so deeply nested records fail
before further recursion, while preserving existing parsing behavior within the
limit.
- Around line 687-693: Update resolve_type to avoid constructing a formatted
prefix during each lookup: after the direct core.types lookup misses, derive the
relative coordinate by checking for core.coordinate followed by a '.' and
stripping that prefix without allocation, then retry core.types with the
relative value. Preserve the existing absolute-key precedence and fallback
behavior.
- Around line 695-698: Introduce a dedicated named recursion-depth constant for
the type-compatibility walk, separate from MAX_RESULT_PROJECTION_PATH_SEGMENTS.
Update types_are_compatible to use the new constant while preserving its
existing fail-closed behavior, leaving the field-path limit unchanged for
source-reference validation.

In `@crates/edict-syntax/src/target_ir.rs`:
- Around line 305-329: Update lower_result_projections and
emit_result_projection to reuse target_ir.semantic_closure or a precomputed
ProjectionSemantics basis, rather than constructing it from
semantic_closure_for_core for each intent. Preserve the existing per-intent
projection and failure collection while ensuring the Core module closure and
digest are computed only once.
- Around line 177-178: Document the public fields result_projections and
result_projection_failures in Lowered, explicitly stating that a Lowered report
may contain zero projections while still carrying non-empty projection failures,
and that an empty failures collection does not imply any projections exist. Make
clear that admission of these results is the caller’s responsibility.

In `@crates/edict-syntax/tests/result_projection.rs`:
- Around line 416-457: Expand the negative coverage around result_projection.rs
by splitting path_text_artifact_and_structure_bounds_fail_closed into focused
tests. Add cases that assert empty text rejects as InvalidCanonicalArtifact,
decoded zero maxOutputBytes rejects as InvalidOutputBound, an absent target-IR
step rejects as UnknownCapabilityStep, and missing or duplicate arg.0
application-input intent rejects as InvalidApplicationInput. Construct each case
through the relevant encode_result_projection or decode_result_projection path
and assert the specific failure kind.
- Around line 460-494: Replace the vacuous BTreeMap insertion-order loop in
canonical_encoding_is_insertion_order_independent_for_fixed_seed_cases with a
test that constructs a CanonicalValue::Map in deliberately non-canonical order
and verifies encode_canonical_cbor normalizes it. Include keys such as "z" and
"aa" to cover the canonical length-boundary ordering difference, and assert the
resulting encoded bytes or structured artifact against the canonical expectation
rather than relying on BTreeMap ordering.

In `@docs/abi/edict-result-projection.cddl`:
- Line 18: Update the canonical CDDL schema for result-projection paths and
field maps to encode the same occurrence limits enforced by
validate_expression_bounds: cap path segments at
MAX_RESULT_PROJECTION_PATH_SEGMENTS and field entries according to
MAX_RESULT_PROJECTION_NODES. Use the exact constant values and add comments
referencing both constants so future changes remain synchronized.
- Line 10: Add a projection fixture covering maxOutputBytes set to zero and
assert that validation returns SchemaMismatch. Reuse the existing maxOutputBytes
fixture structure or generated-field variant, preserving the missing-field
coverage while directly exercising the uint .gt 0 constraint.

In `@docs/topics/cli/README.md`:
- Around line 76-82: Rewrite the singleton executable-operation paragraph in the
documentation to distinguish target lowering from application build: lowering
carries a per-intent projection map and failure map, while
single_result_projection in application_build.rs enforces exactly one projection
and rejects recorded failures before independently invoking
verify_result_projection. Preserve the existing provider semantic-input and Echo
`#698` details, but attribute cardinality and verification to the build route
rather than lowering.

In `@fixtures/provider-contracts/v1/edict-provider-contracts.cddl`:
- Around line 798-826: Update the result-projection CDDL definitions around
result-projection, result-projection-record, and result-projection-source to
mirror validate_projection_bounds exactly: bound maxOutputBytes, record nesting
and field counts, source path segments, and total artifact size. Add
provider-schema validation tests proving each over-limit projection is rejected,
while valid boundary values remain accepted.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

Push a commit to this branch (recommended)
Create a new PR with the fixes

ℹ️ Review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 9410e446-d3ff-486e-be28-91bd647f4626

📥 Commits

Reviewing files that changed from the base of the PR and between 296bf1f and 07e9c8c.

📒 Files selected for processing (22)

CHANGELOG.md
crates/edict-cli/src/application_build.rs
crates/edict-provider-schema/src/contract_pack.rs
crates/edict-provider-schema/tests/provider_contract_pack.rs
crates/edict-syntax/src/lib.rs
crates/edict-syntax/src/result_projection.rs
crates/edict-syntax/src/target_ir.rs
crates/edict-syntax/tests/result_projection.rs
docs/abi/edict-result-projection.cddl
docs/topics/README.md
docs/topics/cli/README.md
docs/topics/result-projections/README.md
docs/topics/result-projections/test-plan.md
docs/topics/target-ir/README.md
fixtures/lawpack/hello-echo/README.md
fixtures/lawpack/hello-echo/create-greeting.result-projection.cbor
fixtures/lawpack/hello-echo/create-greeting.result-projection.sha256
fixtures/provider-contracts/v1/edict-provider-contracts.cddl
fixtures/provider-contracts/v1/manifest.json
xtask/src/lawpack_goldens.rs
xtask/src/provider_contract_pack.rs
xtask/src/tests.rs

📜 Review details

⏰ Context from checks skipped due to timeout. (3)

GitHub Check: supply-chain (cargo-deny)
GitHub Check: rust stable (fmt · clippy · test)
GitHub Check: rust msrv 1.94.0 (fmt · clippy · test)

🧰 Additional context used

📓 Path-based instructions (6)

**/*