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

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 14 additions & 7 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,9 @@
recovered work while constructing one singleton Tick. Publication follows
only after the decided-Tick WAL commit. A second fresh filesystem host
recovers the package, Action, Tick, state, typed outcome, and Receipt.
Repeating creation yields the typed precondition obstruction with no hidden
mutation, while a changed initial state produces the typed
Repeating creation yields the package-declared, lawpack-qualified typed
obstruction with no hidden mutation, while a changed initial state produces
the typed
`echo-operation-execution-mismatch/action-basis` recovery refusal. Admission
binds the accepted verification report's Target IR to the package semantic
closure, selects target configuration only from the package-supported target
Expand Down Expand Up @@ -49,12 +50,12 @@
coordinate-framed exports and adapter references independently from their
provider-envelope domains. Its lowerer and verifier components were
independently reproduced in copy-only, mount-free designated `linux/amd64`
containers and promoted at 230,297 bytes /
`f800df20b95c5a3dbb7682d3dbe545ac0fde29ad67430ab7038954a08b54047b`
and 247,766 bytes /
`edbef0fee8bb8b661b457674ce4d7eeb75e842f39eb823ae121ddb412ad20a56`,
containers and promoted at 230,875 bytes /
`08277d4ba7d98e0b143c06c208abc306f133bda510caa5393da08aa490334a6e`
and 248,221 bytes /
`744a511137608634b88abf7bd7e61da9bf81a5cacff7b190fc2530c346ba36cc`,
respectively. The resulting 25-file package has provider identity
`sha256:d8d433725fbece1ba657cd456720c1b788344f9034b1735ab99cf209d835038a`.
`sha256:a7ab6bfbbedc3a6b61a8559dc6506cfc3d2836b46dac3cc825e5b05b16b94fa5`.
This package build proves generic compiler/provider lowering and independent
verification. The separate `run-edict-operation` witness now consumes that
crossing through Echo-owned runtime execution.
Expand Down Expand Up @@ -1517,6 +1518,12 @@ Applied, Rejected, Obstructed}` with receipt evidence and typed contract

### Fixed

- Generic executable-operation lowering and independent verification now
resolve source-local obstruction constructor aliases through the exact
digest-locked lawpack import before encoding or comparing the package.
Runtime duplicate outcomes therefore retain the capability-owned obstruction
coordinate instead of exposing an application-local alias or collapsing it
into the generic precondition-mismatch class.
- Provider-native installation now applies the same pure structural validation
used to reconstruct retained invocation evidence before mutating any Echo
engine index. Empty operation or Target IR coordinates, empty Target IR
Expand Down
11 changes: 7 additions & 4 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -186,7 +186,10 @@ 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.
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.
Comment on lines +190 to +192

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Describe the coordinate as package-bound, not scheduler-reported

For consumers of TrustedRuntimeHost::echo_operation_action_outcome_v1, an EchoOperationActionOutcomeV1::Obstructed value exposes only the generic obstruction kind and package/installation identities; the scheduler outcome has no obstruction-coordinate field or accessor. The xtask witness obtains the displayed coordinate separately by parsing the package and substituting it after observing PreconditionMismatch, so this current-state claim overstates the runtime API; either propagate the coordinate into the typed outcome or describe it as indirectly bound by the package.

AGENTS.md reference: AGENTS.md:L144-L150

Useful? React with 👍 / 👎.


That generic runtime witness is not yet the Jim/Jedit vertical. A standalone
application-owned Edict operation now crosses it through a compiler-produced
Expand Down Expand Up @@ -270,9 +273,9 @@ conflicting or obstructed Actions retain typed outcomes without hidden
mutation. A standalone application-owned Edict create-if-absent operation now
crosses this route as an exact compiler-produced package and independently
accepted verification report through `cargo xtask run-edict-operation`. That
witness is one Action in one Tick; it does not claim external multi-Action Tick
composition, a product-ready application runner, a Jedit operation, or a Graft
operation.
witness proves its package-declared typed obstruction and one Action in one
Tick; it does not claim external multi-Action Tick composition, a product-ready
application runner, a Jedit operation, or a Graft operation.

## Contracts And Boundaries

Expand Down
9 changes: 6 additions & 3 deletions crates/echo-edict-provider-lowerer/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,10 @@ exact digest-bound source, Core, lawpack, lawpack-exports, target-adapter,
target-configuration, and Target IR artifacts. It derives the operation
coordinate from the authored Core package and intent, validates the complete
portable capability closure, and emits canonical `echo.operation-package/v1`
bytes for Echo's bounded anchored create-if-absent profile. Application
bytes for Echo's bounded anchored create-if-absent profile. Both the effect and
obstruction coordinates are resolved from source-local aliases through the
exact digest-locked lawpack import, so the package retains stable
lawpack-qualified identities. Application
coordinates, intent names, effect names, failure names, type profiles, and
authority profiles remain opaque artifact data; production lowering contains
no application-specific dispatch or native callback.
Expand Down Expand Up @@ -111,8 +114,8 @@ proposal constructor supports mutations and refuses a `Query`; authored reads
remain a separate bounded observer/optic path and must never be represented as
synthetic mutations.

The refreshed 230,285-byte checked lowerer component has SHA-256
`9575ca8c843f3dfe4e5550ecdc40a8a8584c1aa7012b5b6f6a76e3f05f1b68f3` and has
The refreshed 230,875-byte checked lowerer component has SHA-256
`08277d4ba7d98e0b143c06c208abc306f133bda510caa5393da08aa490334a6e` and has
crossed the reproducible promotion boundary. The pinned Edict host admits its
generated envelope under the owning `generated-artifact` CDDL root, and the
isolated host fixture exercises the exact helper binding, typed codecs, EINT
Expand Down
28 changes: 24 additions & 4 deletions crates/echo-edict-provider-lowerer/src/executable_operation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,7 @@ struct ProgramConfiguration<'a> {
struct ApplicationIntent<'a> {
name: &'a str,
operation_coordinate: String,
obstruction_coordinate: &'a str,
effect_coordinate: &'a str,
failure_name: &'a str,
}
Expand Down Expand Up @@ -100,7 +101,9 @@ pub(super) fn lower(request: &LoweringRequestV1) -> Result<LoweringSuccessV1, Pr

let source = validate_source(&source, closure.source, &request.core)?;
let semantic_effect =
semantic_effect_coordinate(source, closure.lawpack, intent.effect_coordinate)?;
semantic_lawpack_member_coordinate(source, closure.lawpack, intent.effect_coordinate)?;
let semantic_obstruction =
semantic_lawpack_member_coordinate(source, closure.lawpack, intent.obstruction_coordinate)?;
validate_exports(&exports, &intent, &semantic_effect)?;
validate_lawpack(
&lawpack,
Expand All @@ -121,7 +124,13 @@ pub(super) fn lower(request: &LoweringRequestV1) -> Result<LoweringSuccessV1, Pr
)?;
let configuration = validate_configuration(&configuration)?;

let package = encode_package(request, &closure, &intent, configuration)?;
let package = encode_package(
request,
&closure,
&intent,
&semantic_obstruction,
configuration,
)?;
let _ = request.limits;
Ok(LoweringSuccessV1 {
outputs: vec![LoweringOutputArtifact {
Expand Down Expand Up @@ -246,12 +255,18 @@ fn validate_core<'a>(
return Err(super::unsupported_semantics(coordinate));
}
let effect_coordinate = required_text(node, "effect", coordinate)?;
let (failure_name, _) =
let (failure_name, obstruction_arm) =
single_text_map_entry(required_map(node, "obstructionMap", coordinate)?)
.ok_or_else(|| super::unsupported_semantics(coordinate))?;
let obstruction_value = required_map(obstruction_arm, "value", coordinate)?;
let obstruction_coordinate = required_text(obstruction_value, "callee", coordinate)?;
if obstruction_coordinate.is_empty() {
return Err(super::unsupported_semantics(coordinate));
}
Ok(ApplicationIntent {
name: intent_name,
operation_coordinate: format!("{coordinate}.{intent_name}"),
obstruction_coordinate,
effect_coordinate,
failure_name,
})
Expand Down Expand Up @@ -369,7 +384,7 @@ fn validate_adapter(
Ok(())
}

fn semantic_effect_coordinate(
fn semantic_lawpack_member_coordinate(
source: &str,
lawpack: &SemanticInput,
core_effect: &str,
Expand Down Expand Up @@ -553,6 +568,7 @@ fn encode_package(
request: &LoweringRequestV1,
closure: &ClosureInputs<'_>,
intent: &ApplicationIntent<'_>,
obstruction_coordinate: &str,
configuration: ProgramConfiguration<'_>,
) -> Result<Vec<u8>, ProviderRefusalV1> {
let program = canonical_map([
Expand Down Expand Up @@ -670,6 +686,10 @@ fn encode_package(
"obstruction_interpretation_identity",
hash_value(profile_digest(OBSTRUCTION_INTERPRETATION)),
),
(
"obstruction_coordinate",
canonical_text(obstruction_coordinate),
),
(
"operation_coordinate",
canonical_text(&intent.operation_coordinate),
Expand Down
4 changes: 2 additions & 2 deletions crates/echo-edict-provider-lowerer/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -809,7 +809,7 @@ pub mod echo_dpo {
pub const PROVIDER_SCHEMA_COORDINATE: &str = "echo.provider-artifacts.cddl@1";
/// Raw SHA-256 of the exact self-contained provider CDDL bytes.
pub const PROVIDER_SCHEMA_SHA256_HEX: &str =
"c604b7bf9e20db02dac9c010a01470d711335953cb31e6a603fb1e9cb818e8fa";
"6b9076ae02730797fddf60a93606df3de245a1c6bfbd845486799b7310d002a2";
/// Exact generated-artifact profile coordinate owning operation schemas.
pub const GENERATED_ARTIFACT_PROFILE: &str = "echo.dpo.registration/v1";
/// Digest-framing domain for the generated-artifact profile.
Expand Down Expand Up @@ -846,7 +846,7 @@ pub mod echo_dpo {

const MUTATION_RULE_NAME: &str = concat!(
"cmd/contract/",
"c604b7bf9e20db02dac9c010a01470d711335953cb31e6a603fb1e9cb818e8fa",
"6b9076ae02730797fddf60a93606df3de245a1c6bfbd845486799b7310d002a2",
"/3389142194/a.b@1.t"
);
const PROVIDER_OPERATIONS: [ProviderOperationV1<'static>; 1] = [ProviderOperationV1 {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -107,6 +107,14 @@ fn one_provider_binary_lowers_two_unrelated_application_vocabularies() {
text_field(&beta_decoded, "operation_coordinate"),
Some("notes.beta@7.createNote")
);
assert_eq!(
text_field(&alpha_decoded, "obstruction_coordinate"),
Some(ALPHA.obstruction)
);
assert_eq!(
text_field(&beta_decoded, "obstruction_coordinate"),
Some(BETA.obstruction)
);
}

#[test]
Expand Down Expand Up @@ -272,7 +280,21 @@ fn core(names: FixtureNames<'_>) -> CanonicalValueV1 {
"obstructionMap",
dynamic_map([(
names.failure,
owned_map([("callee", text(names.obstruction))]),
owned_map([(
"value",
owned_map([(
"callee",
text(format!(
"{}.{}",
names.alias,
names
.obstruction
.rsplit_once('.')
.expect("fixture obstruction has a member",)
.1
)),
)]),
)]),
)]),
),
])]),
Expand Down Expand Up @@ -472,6 +494,7 @@ fn expected_package(
let core_identity = hash(&request.core.reference.digest);
ExecutableOperationPackageV1::new(
format!("{}.{}", names.application, names.intent),
names.obstruction,
EchoOperationSemanticClosureV1::new(
hash(&source.reference.digest),
core_identity,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ pub mod echo_dpo {
pub const PROVIDER_SCHEMA_COORDINATE: &str = "echo.provider-artifacts.cddl@1";
/// Raw SHA-256 of the exact self-contained provider CDDL bytes.
pub const PROVIDER_SCHEMA_SHA256_HEX: &str =
"c604b7bf9e20db02dac9c010a01470d711335953cb31e6a603fb1e9cb818e8fa";
"6b9076ae02730797fddf60a93606df3de245a1c6bfbd845486799b7310d002a2";
/// Exact generated-artifact profile coordinate owning operation schemas.
pub const GENERATED_ARTIFACT_PROFILE: &str = "echo.dpo.registration/v1";
/// Digest-framing domain for the generated-artifact profile.
Expand Down Expand Up @@ -108,7 +108,7 @@ pub mod echo_dpo {

const MUTATION_RULE_NAME: &str = concat!(
"cmd/contract/",
"c604b7bf9e20db02dac9c010a01470d711335953cb31e6a603fb1e9cb818e8fa",
"6b9076ae02730797fddf60a93606df3de245a1c6bfbd845486799b7310d002a2",
"/3389142194/a.b@1.t"
);
const PROVIDER_OPERATIONS: [ProviderOperationV1<'static>; 1] = [ProviderOperationV1 {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ const REVIEW_MEDIA_TYPE: &str = "application/json";
const GENERATED_SOURCE_PATH: &str = "generated/echo_dpo.rs";
const REVIEW_PATH: &str = "review/echo_dpo.json";
const EXPECTED_PROVIDER_SCHEMA_SHA256_HEX: &str =
"c604b7bf9e20db02dac9c010a01470d711335953cb31e6a603fb1e9cb818e8fa";
"6b9076ae02730797fddf60a93606df3de245a1c6bfbd845486799b7310d002a2";
const EXPECTED_OPERATION_ID_LAW: &str = "echo.semantic-operation-id.fnv1-32/v1";
const EXPECTED_OPERATION_ID: u32 = 3_389_142_194;

Expand Down
8 changes: 5 additions & 3 deletions crates/echo-edict-provider-verifier/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -26,14 +26,16 @@ configuration, Target IR, and compiler-emitted package as digest-bound inputs,
then reconstructs the expected generic package without importing or calling
the lowerer. Exact equality yields an accepted
`echo.operation-package-verifier-report/v1`; a rebound or otherwise
self-consistent package mutation yields a typed rejected report. Application
self-consistent package mutation yields a typed rejected report. The verifier
independently resolves source-local effect and obstruction aliases through the
exact lawpack import before comparing the canonical package. Application
vocabulary is treated only as opaque authored data.

The `wasm32` guest adapter vendors Edict's exact frozen
`edict:target-provider/verifier@1.0.0` WIT world and performs only exhaustive
transport-to-model conversion. Its reproducibly built 247,754-byte checked
transport-to-model conversion. Its reproducibly built 248,221-byte checked
component has SHA-256
`d87f3df6cdeca0b14032a23b614e9b9ba1f53ea3955a5a0aebda6c61450c3e51`.
`744a511137608634b88abf7bd7e61da9bf81a5cacff7b190fc2530c346ba36cc`.
Component identity and admitted host replay remain separate propositions: the
pinned Edict host preflights the request artifacts and declared output schema,
invokes the checked component, then admits and manifests each returned accepted
Expand Down
28 changes: 24 additions & 4 deletions crates/echo-edict-provider-verifier/src/executable_operation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,7 @@ struct ProgramConfiguration<'a> {
struct ApplicationIntent<'a> {
name: &'a str,
operation_coordinate: String,
obstruction_coordinate: &'a str,
effect_coordinate: &'a str,
failure_name: &'a str,
}
Expand Down Expand Up @@ -111,7 +112,9 @@ pub(super) fn verify(

let source = validate_source(&source, closure.source, &request.core)?;
let semantic_effect =
semantic_effect_coordinate(source, closure.lawpack, intent.effect_coordinate)?;
semantic_lawpack_member_coordinate(source, closure.lawpack, intent.effect_coordinate)?;
let semantic_obstruction =
semantic_lawpack_member_coordinate(source, closure.lawpack, intent.obstruction_coordinate)?;
validate_exports(&exports, &intent, &semantic_effect)?;
validate_lawpack(
&lawpack,
Expand All @@ -125,7 +128,13 @@ pub(super) fn verify(
validate_adapter(&adapter, closure.configuration, &intent, &semantic_effect)?;
validate_target_ir(&target_ir, request, closure.lawpack, &intent)?;
let configuration = validate_configuration(&configuration)?;
let expected = encode_expected_package(request, &closure, &intent, configuration)?;
let expected = encode_expected_package(
request,
&closure,
&intent,
&semantic_obstruction,
configuration,
)?;
let actual = encode_canonical_cbor_v1(&package)
.map_err(|_| invalid_artifact(PACKAGE_COORDINATE, "package could not be re-encoded"))?;

Expand Down Expand Up @@ -276,12 +285,18 @@ fn validate_core<'a>(
return Err(super::unsupported_semantics(coordinate));
}
let effect_coordinate = required_text(node, "effect", coordinate)?;
let (failure_name, _) =
let (failure_name, obstruction_arm) =
single_text_map_entry(required_map(node, "obstructionMap", coordinate)?)
.ok_or_else(|| super::unsupported_semantics(coordinate))?;
let obstruction_value = required_map(obstruction_arm, "value", coordinate)?;
let obstruction_coordinate = required_text(obstruction_value, "callee", coordinate)?;
if obstruction_coordinate.is_empty() {
return Err(super::unsupported_semantics(coordinate));
}
Ok(ApplicationIntent {
name: intent_name,
operation_coordinate: format!("{coordinate}.{intent_name}"),
obstruction_coordinate,
effect_coordinate,
failure_name,
})
Expand Down Expand Up @@ -406,7 +421,7 @@ fn validate_adapter(
Ok(())
}

fn semantic_effect_coordinate(
fn semantic_lawpack_member_coordinate(
source: &str,
lawpack: &SemanticInput,
core_effect: &str,
Expand Down Expand Up @@ -589,6 +604,7 @@ fn encode_expected_package(
request: &VerificationRequestV1,
closure: &ClosureInputs<'_>,
intent: &ApplicationIntent<'_>,
obstruction_coordinate: &str,
configuration: ProgramConfiguration<'_>,
) -> Result<Vec<u8>, ProviderRefusalV1> {
let program = canonical_map([
Expand Down Expand Up @@ -703,6 +719,10 @@ fn encode_expected_package(
"obstruction_interpretation_identity",
hash_value(profile_digest(OBSTRUCTION_INTERPRETATION)),
),
(
"obstruction_coordinate",
canonical_text(obstruction_coordinate),
),
(
"operation_coordinate",
canonical_text(&intent.operation_coordinate),
Expand Down
Loading
Loading