Retain observed execution footprints for falsification

CHANGELOG.md

@@ -7,6 +7,72 @@
 
 ### 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.
+- ADR 0027 proposes first-class falsification witnesses, and
+  `docs/topics/FalsificationWitnesses.md` carries the design and delivery
+  roadmap. Anyone may propose a counterexample; only Echo may admit that it
+  falsifies an exact property instance. Discovery stays outside the admission
+  trust boundary, property evaluation returns a closed outcome sum, admission
+  requires fresh-host exact replay, reduction must preserve a typed violation
+  class under a declared equivalence policy, minimality is always qualified,
+  semantic counterexample identity is separate from the evidence-envelope
+  identity, and the target worldline is never rewritten—witnesses append to a
+  separate evidence worldline under the existing admission-kernel append
+  authority. The first vertical is footprint honesty, whose blocking gap is now
+  documented: the footprint guard compares each access against the declared set
+  and panics, accumulating nothing, so no actual per-Action footprint exists for
+  a property to compare against.
 - Strict filesystem WAL stores now persist a checksummed writer-epoch ledger
   containing the active epoch, its exact latest closed predecessor, and final
   LSN and commit-digest evidence. Bounded retention keeps ledger writes and
@@ -1628,6 +1694,25 @@ Applied, Rejected, Obstructed}` with receipt evidence and typed contract
 
 ### Fixed
 
+- A writer epoch that commits nothing no longer consumes an LSN. An LSN names a
+  WAL frame; acquiring an epoch persists ledger evidence and emits no frame, so
+  an epoch's start LSN is the next unallocated frame coordinate and is
+  non-regressing rather than universally strictly increasing. After a
+  predecessor with committed frames the successor still starts at
+  `final_lsn + 1`, but after an empty predecessor it resumes at the
+  predecessor's own start. Previously every barren open-and-close minted a
+  phantom coordinate, so a host that reopened a filesystem WAL only to inspect
+  it left a permanent hole; the next writer's frames landed past the gap and
+  every later recovery failed closed with `LsnContinuityMismatch`. Epoch-chain
+  advancement remains strict and is carried by epoch identity, ordinal, fencing
+  token, and lease evidence, none of which changed.
+- `cargo test -p warp-core` no longer reports a green result for eight test
+  files it never ran. Each sits behind an inner `#![cfg(feature = ...)]`, so
+  without the feature cargo compiled an empty crate and printed
+  "running 0 tests ... test result: ok". They now declare `required-features`,
+  matching the convention the manifest already used for five other targets, so
+  cargo skips the target with an explicit message instead of manufacturing
+  coverage. Under `--workspace`, feature unification runs them as before.
 - 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.

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,