Retain observed execution footprints (first part of #716)

CHANGELOG.md

@@ -14,6 +14,59 @@
 
 ### Added
 
+- `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.
@@ -1784,6 +1837,11 @@ Applied, Rejected, Obstructed}` with receipt evidence and typed contract
 
 ### Changed
 
+- `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.
+
 - 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,

crates/echo-dind-tests/src/rules.rs

@@ -13,9 +13,9 @@ use crate::type_ids::{
 use echo_wasm_abi::unpack_intent_v1;
 use warp_core::{
     make_edge_id, make_node_id, make_type_id, AtomPayload, AtomView, AttachmentKey, AttachmentSet,
-    AttachmentValue, ConflictPolicy, EdgeId, EdgeRecord, EdgeSet, Footprint, GraphStore, GraphView,
-    Hash, NodeId, NodeKey, NodeRecord, NodeSet, PatternGraph, RewriteRule, TickDelta, TypeId,
-    WarpId, WarpOp,
+    AttachmentValue, ConflictPolicy, EdgeId, EdgeRecord, EdgeSet, ExecutionGraphView, Footprint,
+    GraphStore, GraphView, Hash, NodeId, NodeKey, NodeRecord, NodeSet, PatternGraph, RewriteRule,
+    RuleExecutor, TickDelta, TypeId, WarpId, WarpOp,
 };
 
 const TYPE_VIEW_OP: &str = "sys/view/op";
@@ -61,13 +61,15 @@ pub fn route_push_rule() -> RewriteRule {
         name: ROUTE_PUSH_RULE_NAME,
         left: PatternGraph { nodes: vec![] },
         matcher: |s, scope| matcher_for_op(s, scope, ops::route_push::OP_ID),
-        executor: |s, scope, delta| {
-            if let Some(args) =
-                decode_op_args::<ops::route_push::Args>(s, scope, ops::route_push::decode_vars)
-            {
+        executor: RuleExecutor::observed(|s, scope, delta| {
+            if let Some(args) = decode_observed_op_args::<ops::route_push::Args>(
+                s,
+                scope,
+                ops::route_push::decode_vars,
+            ) {
                 emit_route_push(s.warp_id(), delta, args.path);
             }
-        },
+        }),
         compute_footprint: |s, scope| {
             // Only declare full footprint if args decode succeeds (mirrors executor).
             if decode_op_args::<ops::route_push::Args>(s, scope, ops::route_push::decode_vars)
@@ -92,13 +94,15 @@ pub fn set_theme_rule() -> RewriteRule {
         name: SET_THEME_RULE_NAME,
         left: PatternGraph { nodes: vec![] },
         matcher: |s, scope| matcher_for_op(s, scope, ops::set_theme::OP_ID),
-        executor: |s, scope, delta| {
-            if let Some(args) =
-                decode_op_args::<ops::set_theme::Args>(s, scope, ops::set_theme::decode_vars)
-            {
+        executor: RuleExecutor::observed(|s, scope, delta| {
+            if let Some(args) = decode_observed_op_args::<ops::set_theme::Args>(
+                s,
+                scope,
+                ops::set_theme::decode_vars,
+            ) {
                 emit_set_theme(s.warp_id(), delta, args.mode);
             }
-        },
+        }),
         compute_footprint: |s, scope| {
             // Only declare full footprint if args decode succeeds (mirrors executor).
             if decode_op_args::<ops::set_theme::Args>(s, scope, ops::set_theme::decode_vars)
@@ -123,9 +127,9 @@ pub fn toggle_nav_rule() -> RewriteRule {
         name: TOGGLE_NAV_RULE_NAME,
         left: PatternGraph { nodes: vec![] },
         matcher: |s, scope| matcher_for_op(s, scope, ops::toggle_nav::OP_ID),
-        executor: |s, _scope, delta| {
+        executor: RuleExecutor::observed(|s, _scope, delta| {
             emit_toggle_nav(s, delta);
-        },
+        }),
         compute_footprint: |s, scope| footprint_for_state_node(s, scope, "sim/state/navOpen"),
         factor_mask: 0,
         conflict_policy: ConflictPolicy::Abort,
@@ -142,9 +146,9 @@ pub fn toast_rule() -> RewriteRule {
         name: TOAST_RULE_NAME,
         left: PatternGraph { nodes: vec![] },
         matcher: |s, scope| matcher_for_op(s, scope, ops::toast::OP_ID),
-        executor: |s, scope, delta| {
+        executor: RuleExecutor::observed(|s, scope, delta| {
             if let Some(args) =
-                decode_op_args::<ops::toast::Args>(s, scope, ops::toast::decode_vars)
+                decode_observed_op_args::<ops::toast::Args>(s, scope, ops::toast::decode_vars)
             {
                 // Use intent scope (NodeId) for deterministic view op sequencing.
                 // This ensures the same intent always produces the same view op ID,
@@ -157,7 +161,7 @@ pub fn toast_rule() -> RewriteRule {
                     scope,
                 );
             }
-        },
+        }),
         compute_footprint: |s, scope| {
             // Only declare full footprint if args decode succeeds (mirrors executor).
             if decode_op_args::<ops::toast::Args>(s, scope, ops::toast::decode_vars).is_none() {
@@ -190,7 +194,7 @@ pub fn drop_ball_rule() -> RewriteRule {
         name: DROP_BALL_RULE_NAME,
         left: PatternGraph { nodes: vec![] },
         matcher: |s, scope| matcher_for_op(s, scope, ops::drop_ball::OP_ID),
-        executor: |view, _scope, delta| {
+        executor: RuleExecutor::observed(|view, _scope, delta| {
             let warp_id = view.warp_id();
             let ball_id = make_node_id("ball");
             // Q32.32 fixed-point: 1 unit = 1 << 32
@@ -215,7 +219,7 @@ pub fn drop_ball_rule() -> RewriteRule {
                 }),
                 value: Some(AttachmentValue::Atom(atom)),
             });
-        },
+        }),
         compute_footprint: |s, _scope| {
             // Minimal footprint: executor only creates the ball node and its attachment.
             // No sim/state hierarchy or edges are created by this rule.
@@ -249,8 +253,8 @@ pub fn ball_physics_rule() -> RewriteRule {
             }
             false
         },
-        executor: |view, scope, delta| {
-            if let Some(m) = MotionV2View::try_from_node(&view, scope) {
+        executor: RuleExecutor::observed(|view, scope, delta| {
+            if let Some(m) = MotionV2View::try_from_execution_node(view, scope) {
                 let mut pos = m.pos_raw();
                 let mut vel = m.vel_raw();
 
@@ -276,7 +280,7 @@ pub fn ball_physics_rule() -> RewriteRule {
                     ))),
                 });
             }
-        },
+        }),
         compute_footprint: |s, scope| {
             echo_dry_tests::FootprintBuilder::from_view(s)
                 .reads_writes_node_alpha(*scope)
@@ -301,13 +305,13 @@ pub fn put_kv_rule() -> RewriteRule {
         name: PUT_KV_RULE_NAME,
         left: PatternGraph { nodes: vec![] },
         matcher: |s, scope| matcher_for_op(s, scope, ops::put_kv::OP_ID),
-        executor: |s, scope, delta| {
+        executor: RuleExecutor::observed(|s, scope, delta| {
             if let Some(args) =
-                decode_op_args::<ops::put_kv::Args>(s, scope, ops::put_kv::decode_vars)
+                decode_observed_op_args::<ops::put_kv::Args>(s, scope, ops::put_kv::decode_vars)
             {
                 emit_put_kv(s.warp_id(), delta, args.key, args.value);
             }
-        },
+        }),
         compute_footprint: |s, scope| {
             if let Some(args) =
                 decode_op_args::<ops::put_kv::Args>(s, scope, ops::put_kv::decode_vars)
@@ -347,6 +351,18 @@ fn decode_op_args<T>(
     decode_fn(vars)
 }
 
+fn decode_observed_op_args<T>(
+    view: &mut ExecutionGraphView<'_, '_>,
+    scope: &NodeId,
+    decode_fn: fn(&[u8]) -> Option<T>,
+) -> Option<T> {
+    let AttachmentValue::Atom(a) = view.node_attachment(scope)? else {
+        return None;
+    };
+    let (_, vars) = unpack_intent_v1(&a.bytes).ok()?;
+    decode_fn(vars)
+}
+
 impl<'a> MotionV2View<'a> {
     /// Attempt to construct a motion v2 view from a node's attachment.
     pub fn try_from_node(view: &'a GraphView<'a>, node: &NodeId) -> Option<Self> {
@@ -355,6 +371,17 @@ impl<'a> MotionV2View<'a> {
         };
         Self::try_from_payload(p)
     }
+
+    /// Attempt to construct a motion v2 view through an observed executor view.
+    pub fn try_from_execution_node<'store>(
+        view: &mut ExecutionGraphView<'store, '_>,
+        node: &NodeId,
+    ) -> Option<MotionV2View<'store>> {
+        let AttachmentValue::Atom(p) = view.node_attachment(node)? else {
+            return None;
+        };
+        MotionV2View::try_from_payload(p)
+    }
 }
 
 /// Returns a minimal footprint for decode-only access.
@@ -533,7 +560,7 @@ fn emit_set_theme(warp_id: WarpId, delta: &mut TickDelta, mode: crate::codecs::T
 }
 
 /// Emit ops for a toggle nav operation.
-fn emit_toggle_nav(view: GraphView<'_>, delta: &mut TickDelta) {
+fn emit_toggle_nav(view: &mut ExecutionGraphView<'_, '_>, delta: &mut TickDelta) {
     let warp_id = view.warp_id();
     let (_, sim_state_id) = emit_state_base(warp_id, delta);
     let id = make_node_id("sim/state/navOpen");

crates/echo-dry-tests/src/demo_rules.rs

@@ -8,11 +8,14 @@ use warp_core::{
     decode_motion_atom_payload_q32_32, decode_motion_payload, encode_motion_atom_payload,
     encode_motion_payload, encode_motion_payload_q32_32, make_node_id, make_type_id,
     motion_payload_type_id, pack_port_key, AtomPayload, AttachmentKey, AttachmentSet,
-    AttachmentValue, ConflictPolicy, EdgeSet, Engine, Footprint, GraphStore, GraphView, Hash,
-    NodeId, NodeKey, NodeRecord, NodeSet, PatternGraph, PortSet, RewriteRule, TickDelta, WarpId,
-    WarpOp,
+    AttachmentValue, ConflictPolicy, EdgeSet, Engine, ExecutionGraphView, Footprint, GraphStore,
+    GraphView, Hash, NodeId, NodeKey, NodeRecord, NodeSet, PatternGraph, PortSet, RewriteRule,
+    RuleExecutor, TickDelta, WarpId, WarpOp,
 };
 
+#[cfg(test)]
+use warp_core::ActualFootprint;
+
 // =============================================================================
 // Motion Rule
 // =============================================================================
@@ -54,7 +57,7 @@ mod motion_scalar_backend {
 
 use motion_scalar_backend::{scalar_from_raw, scalar_to_raw};
 
-fn motion_executor(view: GraphView<'_>, scope: &NodeId, delta: &mut TickDelta) {
+fn motion_executor(view: &mut ExecutionGraphView<'_, '_>, scope: &NodeId, delta: &mut TickDelta) {
     if view.node(scope).is_none() {
         return;
     }
@@ -187,7 +190,7 @@ pub fn motion_rule() -> RewriteRule {
         name: MOTION_RULE_NAME,
         left: PatternGraph { nodes: vec![] },
         matcher: motion_matcher,
-        executor: motion_executor,
+        executor: RuleExecutor::observed(motion_executor),
         compute_footprint: compute_motion_footprint,
         factor_mask: 0,
         conflict_policy: ConflictPolicy::Abort,
@@ -222,7 +225,7 @@ fn port_matcher(_: GraphView<'_>, _: &NodeId) -> bool {
     true
 }
 
-fn port_executor(view: GraphView<'_>, scope: &NodeId, delta: &mut TickDelta) {
+fn port_executor(view: &mut ExecutionGraphView<'_, '_>, scope: &NodeId, delta: &mut TickDelta) {
     if view.node(scope).is_none() {
         return;
     }
@@ -306,7 +309,7 @@ pub fn port_rule() -> RewriteRule {
         name: PORT_RULE_NAME,
         left: PatternGraph { nodes: vec![] },
         matcher: port_matcher,
-        executor: port_executor,
+        executor: RuleExecutor::observed(port_executor),
         compute_footprint: compute_port_footprint,
         factor_mask: 0,
         conflict_policy: ConflictPolicy::Abort,
@@ -353,9 +356,10 @@ mod tests {
             Some(AttachmentValue::Atom(encode_motion_atom_payload(pos, vel))),
         );
 
-        let view = GraphView::new(&store);
+        let mut actual = ActualFootprint::new();
+        let mut view = ExecutionGraphView::new(&store, &mut actual);
         let mut delta = TickDelta::new();
-        port_executor(view, &node_id, &mut delta);
+        port_executor(&mut view, &node_id, &mut delta);
 
         assert!(delta.is_empty(), "no-op update should not emit a delta op");
     }

crates/echo-dry-tests/src/rules.rs

@@ -9,7 +9,8 @@ use crate::hashes::make_rule_id;
 #[cfg(test)]
 use warp_core::GraphStore;
 use warp_core::{
-    ConflictPolicy, Footprint, GraphView, Hash, NodeId, PatternGraph, RewriteRule, TickDelta,
+    ConflictPolicy, ExecutionGraphView, Footprint, GraphView, Hash, NodeId, ObservedExecuteFn,
+    PatternGraph, RewriteRule, RuleExecutor, TickDelta,
 };
 
 /// Type alias for join functions matching warp-core's `JoinFn`.
@@ -35,7 +36,7 @@ pub fn scope_exists(view: GraphView<'_>, scope: &NodeId) -> bool {
 // --- Executor Functions ---
 
 /// Executor that does nothing.
-pub fn noop_exec(_: GraphView<'_>, _: &NodeId, _: &mut TickDelta) {}
+pub fn noop_exec(_: &mut ExecutionGraphView<'_, '_>, _: &NodeId, _: &mut TickDelta) {}
 
 // --- Footprint Functions ---
 
@@ -113,7 +114,7 @@ impl NoOpRule {
 pub type MatcherFn = for<'a> fn(GraphView<'a>, &NodeId) -> bool;
 
 /// Type alias for Phase 5 parallel execution executor functions.
-pub type ExecutorFn = for<'a> fn(GraphView<'a>, &NodeId, &mut TickDelta);
+pub type ExecutorFn = ObservedExecuteFn;
 
 /// Type alias for Phase 5 parallel execution footprint functions.
 pub type FootprintFn = for<'a> fn(GraphView<'a>, &NodeId) -> Footprint;
@@ -233,7 +234,7 @@ impl SyntheticRuleBuilder {
             name: self.name,
             left: PatternGraph { nodes: vec![] },
             matcher: self.matcher,
-            executor: self.executor,
+            executor: RuleExecutor::observed(self.executor),
             compute_footprint: self.footprint,
             factor_mask: self.factor_mask,
             conflict_policy: self.conflict_policy,