Retain observed execution footprints for falsification - #716
Draft
flyingrobots wants to merge 8 commits into
Draft
Retain observed execution footprints for falsification#716flyingrobots wants to merge 8 commits into
flyingrobots wants to merge 8 commits into
Conversation
Add docs/topics/FalsificationWitnesses.md as the design doc and roadmap for first-class falsification artifacts: GeneratedPropertyV1, PropertyInstanceV1, CounterexampleProposalV1, and AdmittedFalsificationWitnessV1. Anyone may propose a counterexample; only Echo may admit that it falsifies an exact property instance. Discovery stays outside the admission trust boundary, admission requires fresh-host exact replay, reduction must preserve a typed violation class, and the target worldline is never rewritten — witnesses append to a separate evidence worldline. Every claim is anchored to source at c354d53. Verification against the tree corrected four errors in the source draft and added two roadmap stages that it omitted: - FootprintViolation is a std::panic::panic_any payload, not a returned value, so a property evaluator cannot receive it today. Stage 2 (guard reification) is new. - There is no ExecutableActionEvidence observation projection; the only projections are Head, Snapshot, TruthChannels, and Query, and RecordedTruth admits only TruthChannels. Stage 3 (footprint evidence projection) is new. - WalAppendAuthority::AdmissionKernel already exists and is used by CausalAnchorAdmission; only the transaction kind (next stable code 13) and record kinds (next stable code 32) are new. - The guard reports nine distinct ViolationKind variants, three of which are not read/write footprint violations and must not be merged into one violation class. Also records two coupled edits the roadmap will need: adding ADR 0027 requires updating tests/docs/test_adr_namespace.sh, and wiring the footprint_enforce_release lane into CI requires changing the literal sentence in GeneratedRules.md that test_generated_rule_truth.sh asserts. Index the topic in docs/topics/README.md.
Add docs/adr/0027-first-class-falsification-witnesses.md fixing the boundaries the falsification schemas must respect: the discovery/admission trust boundary, the closed property-outcome sum, fresh-host replay as the admission boundary, typed-violation-preserving reduction, always-qualified minimality, dual identities, the never-rewritten target worldline, durability before publication, and enforcement posture as evidence. Records twelve rejected alternatives. Respecify the footprint blocker in the topic doc after reading FootprintGuard rather than only its violation payload. The guard holds exactly six declared BTreeSets and has no accumulator; every check_* method takes &self, compares one access, and panics on a miss. Nothing in Echo records what an Action actually touched, so the subset relation Actual ⊆ Declared cannot be evaluated at all — catching the panic yields one violating access, not a footprint. Consequences: - Stage 2 becomes accumulation, not unwind-catching. The sink must record every checked access, additively, leaving the panic path unchanged. - Stage 3 becomes execution-evidence delivery rather than a new observation projection. The evaluator already receives execution evidence on a channel separate from the reading, so routing footprints there avoids widening the bound aperture — which the design forbids. - Open question 4 (per-Action vs per-Tick granularity) is closed. The guard is constructed once per rule execution and pre-filtered to one warp, so an accumulator hung off that instance is per-Action by construction. - Two open questions replace it: the pub(crate) guard visibility seam, and the cost of an accumulator on a guard that is live in every debug build. Add a Status column to the roadmap table. Index ADR 0027 in docs/adr/README.md and register it in tests/docs/test_adr_namespace.sh (current_adrs plus current_adr_last=27) as the coupled edit the roadmap predicted. Update CHANGELOG. All four doc-truth tests pass; markdownlint clean.
Add ActualFootprint: an accumulated record of the graph resources an
execution actually touched, comparable against a declared Footprint.
FootprintGuard holds only the six declared BTreeSets. Every check_*
method takes &self, compares one access, and panics on a miss — it
answers "was this access declared?" and immediately forgets. Nothing
recorded what an Action actually touched, so the soundness relation
ActualRead(a) ⊆ DeclaredRead(a)
ActualWrite(a) ⊆ DeclaredWrite(a)
had no left-hand side and could only be observed as a panic. A read-only
property evaluator cannot refute a footprint claim that way.
soundness_violations returns the existing ViolationKind vocabulary in a
fixed axis order — node reads, edge reads, attachment reads, then the
three write axes — canonically within each axis, so the same execution
yields the same violation sequence on every host.
from_ops derives the write axis from an emitted op sequence via
op_write_targets, the same extraction enforcement uses, so a recorded
write set and an enforced write check cannot disagree about what an op
mutates. Cross-warp and instance-level concerns are excluded on purpose:
CrossWarpEmission and UnauthorizedInstanceOp are scope and authority
questions the guard already reports, and recording them as local writes
would misreport them as footprint-subset failures.
The read axis is not derivable from ops and is left unwired. Reads reach
the guard through GraphView, whose guards live in WorkUnit and are shared
across worker threads, so an accumulator inside the guard would make
WorkUnit !Sync and break parallel execution. That fork is documented for
review rather than decided here.
Enforcement behaviour is unchanged. Recording is additive and never
panics; the guard's panic remains the correct response to an undeclared
access during ordinary execution.
14 unit tests cover subset semantics, superset soundness, axis
separation, per-warp scoping, canonical ordering, idempotence,
order-independence, op-derived writes, cross-warp exclusion, and the
edge-writes-imply-from-node adjacency rule.
Also add #[allow(clippy::panic)] to the external_action test module,
matching the convention in other in-src test modules. That failure was
pre-existing and blocked `cargo clippy -p warp-core --all-targets`.
ActualFootprint landed the write axis. The read axis is blocked on a genuine architecture decision rather than on effort. Reads reach the guard through GraphView, and guards live in WorkUnit.guards, which worker threads share by reference. A RefCell accumulator inside FootprintGuard would make WorkUnit !Sync and break parallel execution. Three ways out, each with a real cost: a Mutex in the guard (lock per guarded read in every debug build), a sink threaded through GraphView (no locks, guard stays pure, but GraphView carries an explicit DO-NOT-add-interior-mutability prohibition and check_* signatures change), or a thread-local accumulator (rejected outright — global mutable state on a deterministic path, forbidden by ADR 0004 and enforced by CI). Recorded for review rather than settled unilaterally: this is a hot path and one option brushes an explicit architectural prohibition.
The previous revision offered a Mutex-in-the-guard option and framed the read axis as needing synchronization. That was wrong. execute_work_queue claims unit indices with next_unit.fetch_add, so each unit goes to exactly one worker, and items within a unit execute serially. A guard is never touched concurrently. The scheduler already provides the exclusivity a lock would buy; adding one would re-implement a guarantee Echo already makes. The real constraint is type-level, not runtime: s.spawn over &[WorkUnit] requires WorkUnit: Sync because the borrow checker cannot see the atomic-claim protocol. A RefCell inside FootprintGuard fails to compile for that reason alone. So the resolution is to keep mutable state out of the shared structure: an accumulator owned by the worker's frame in execute_item_enforced is already exclusive, never crosses a thread, and leaves WorkUnit: Sync untouched. Only one question remains, and it is a judgment call rather than a constraint — whether a worker-local accumulator reference in GraphView is inside the intent of its DO-NOT-add-interior-mutability prohibition, whose listed items all concern mutable access to graph state. Also record a finding that surfaced while checking this: execute_serial constructs no guard at all, and execute_item_enforced has exactly one call site. A serial verification replay runs with enforcement inert and would report an empty actual footprint for an execution that touched everything — the false negative acceptance criterion 21 exists to prevent.
An LSN names a WAL frame. Acquiring a writer epoch persists ledger
evidence and emits no frame, so an epoch that committed nothing spent
nothing. `acquire_fresh_writer_epoch` nonetheless applied `checked_next`
to the predecessor's `started_at_lsn` when that predecessor had no final
committed LSN, and `validate_writer_epoch_request` enforced the fiction
by rejecting equality against an empty predecessor's start.
Every open-and-close therefore minted a phantom coordinate. 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 `recover_from_frames_and_
commits` failed closed with `LsnContinuityMismatch` for every reader
thereafter. `inverse_intent_resolves_one_admitted_transition_after_
restart` reproduced exactly this: two inspect-only hosts, two holes, and
recovery refusing the WAL at LSN 18.
An epoch's start LSN is the next unallocated frame coordinate. It is
non-regressing, not universally strictly increasing:
previous epoch committed frames:
successor.start = previous.final_lsn + 1
previous epoch committed no frames:
successor.start = previous.start
Epoch-chain advancement stays strict, carried by epoch identity,
ordinal, fencing token, and lease evidence — none of which changed.
`filesystem_writer_lease_refuses_overlap_before_takeover` had grown a
second policy as a barnacle: it asserted the start LSN advanced past an
empty predecessor. That assertion is dropped; the test's subject is
lease overlap and takeover linkage. Empty-epoch cursor semantics move to
three named tests that also witness the distinction an empty closure
hides — a predecessor with committed frames, and a predecessor whose
frames were written but never committed.
Also declares `required-features` for eight test targets whose contents
sit behind an inner `#![cfg(feature = ...)]`. Without it `cargo test -p
warp-core` compiled an empty crate and printed "running 0 tests ... test
result: ok", so the failure above was invisible to a per-crate run.
`ActualFootprint` landed the write axis. The read axis was blocked on a
real constraint: reads reach the guard through `GraphView`, whose
accessors take `&self`, so recording would need to mutate through a
shared reference. Interior mutability is what that costs, and `GraphView`
forbids it by contract and would lose `Sync` — which `s.spawn` over
`&[WorkUnit]` requires, since the borrow checker cannot see the atomic
unit-claim protocol that already makes access exclusive.
No lock is warranted. The scheduler hands each unit to exactly one
worker and runs items within a unit serially, so guards are never touched
concurrently; a `Mutex` would re-implement a guarantee that already
holds, and `UnsafeCell` plus a manual `Sync` would turn an observation
feature into a scheduler-soundness theorem every future refactor must
preserve.
The shape adopted moves the mutable execution frame — not the declared
guard — into exclusive worker ownership:
Shared prepared work WorkUnit { items, guards } immutable
Worker-local frame ActualFootprint, TickDelta exclusive
Executor capability ExecutionGraphView borrows both
`ExecutionGraphView` is not `Copy` and not `Clone`, and its accessors
take `&mut self`. That is inherited mutability expressing exactly what
the scheduler already guarantees: one executor owns one observation
session, and it cannot be casually shared. `GraphView` keeps its
contract, its `Copy`, and its `Sync`; nothing in `WorkUnit` changes.
Accessors record *before* consulting the guard. The guard panics, so
checking first would unwind before the violating coordinate entered the
record, leaving Echo holding a purported actual footprint that omits the
very access that falsifies it. The recorded axis mirrors enforcement
rather than inventing a finer one — `edges_from` records a node read,
because a node in `n_read` grants its outbound adjacency — and an absent
resource is still a recorded coordinate, so a rule cannot probe
undeclared coordinates for free by choosing empty ones.
`ActualFootprintPosture` makes lane provenance a value. An empty
violation set means the declaration covered the execution only when the
lane recorded *and* enforced; from an unobserved lane it means only that
nothing was compared. `read_axis_is_complete` keeps an empty read axis
readable as unknown rather than as "read nothing", which is the false
negative acceptance criterion 21 exists to block, and
`build_footprint_posture` caps every lane by the enforcement the binary
compiled.
`serial_execution_is_an_unobserved_lane` pins the serial replay hole by
contrast: one executor reading one undeclared node runs through
`execute_serial` without panicking and without leaving a trace, while the
identical read through `ExecutionGraphView` is recorded and reported.
Two lanes, identical behaviour, different evidence.
Differential tests run the recorded write set and the enforced write
check over the same ops and declaration, closing an assumption the design
had only asserted, and pin the two deliberate disagreements: cross-warp
emission and unauthorized instance ops stay scope and authority classes
rather than collapsing into footprint-subset failures.
No production executor reaches the new capability yet; `ExecuteFn` still
passes `GraphView` by value. That migration is the next unit of work.
Contributor
|
Important Review skippedDraft detected. Please check the settings in the CodeRabbit UI or the ⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Plus Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
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. Comment |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Goal
Establish the scheduler-side evidence foundation for first-class falsification witnesses: retain a canonical per-Action actual read/write footprint without weakening the ordinary enforcement panic or widening
FootprintGuard.Plan
Current status
Stages 1 and 2 of the 14-stage falsification roadmap are implemented. Stage 2 is complete locally: native and generated rules use the observed ABI, provider-v1 remains legacy, serial execution retains no evidence, and the scheduler stores canonical per-Action evidence before propagating ordinary panics.
Validation is green for the full workspace tests, all-target Clippy with warnings denied, formatting, documentation lint/dead-link checks, release builds with and without
footprint_enforce_release, theunsafe_graphbuild, and release enforcement footprint tests.Stage 3—delivering these records to the read-only property evaluator—is intentionally outside this PR's implemented boundary.
Open questions