M24: durable-memory witness — a cap-path write survives a device round-trip#90
Open
bahadirarda wants to merge 2 commits into
Open
M24: durable-memory witness — a cap-path write survives a device round-trip#90bahadirarda wants to merge 2 commits into
bahadirarda wants to merge 2 commits into
Conversation
…d-trip Folds the deferred "M24 durable spill" into the M13 memory organ (the "M24:" marker is the bakeoff milestone, so this rides M13). `m24_durable_selftest` mounts the durable virtio-blk backing, writes a sentinel through the organ's `write()` (the path `M_MEM_WRITE` dispatches to), FLUSHES it, DROPS the substrate (all in-RAM T2 gone), RE-MOUNTS + rehydrates the T2 journal from the replayed Episodic log, and reads the sentinel back byte-equal -- proving the bytes left RAM, hit the device, and returned on a fresh mount. A round-trip failure is FAIL-CLOSED (withholds the M13 marker, so the durable claim can never hollow-pass); an absent disk is a graceful skip. - push_record persists the full 48-byte EpisodeBody via the Kani-proven blkfmt::episode_encode (was: only the id), so the durable log carries the T2 journal field-for-field. - MemSubstrate::with_backing + rehydrate_from_backing rebuild T2 from the replayed Episodic log on remount; checkpoint() flushes the backing. - engine::mount_durable constructs a VirtioBlkStore backing (engine side; the organ names only the trait, §3.4). persist_selftest moved EPISODIC -> WORKING so the M20 substrate round-trip and this M24 organ round-trip do not collide on the one M20 partition (raw 8-byte sentinels vs 48-byte episodes). - verified_leaf::M24DurableProof + facade; re-export selftests -> organ -> mem. Proves the device round-trip (like the M20 within-boot drop+remount) through the organ/cap path. Build-verified on x86_64, aarch64, and the compile-out lane. Cross-REBOOT survival (M33-style two-boot), the full cap-DISPATCH path, and durable agent homes are follow-ups.
The durable-memory witness emits a new 'durable-mem:' word: token in the agent profile; the substrate lane's negative-census (organs-proven-absent) diffs the live census against this file, so the new family must be registered or the substrate boot reds on census drift. Position derived by gen-witness-census.sh (sorted, between cost: and exittel:).
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.
What
Lands the deferred "M24 durable spill": a capability-mediated memory write now survives a real device round-trip. Folded into the M13 memory organ (the
M24:marker is the bakeoff milestone).m24_durable_selftestmounts the durable virtio-blk backing, writes a sentinel through the organ'swrite()(the pathM_MEM_WRITEdispatches to), FLUSHES it, DROPS the substrate (all in-RAM T2 gone), re-mounts + rehydrates the T2 journal from the replayed Episodic log, and reads the sentinel back byte-equal — proving the bytes left RAM, hit the device, and returned on a fresh mount. A round-trip failure is FAIL-CLOSED (withholds the M13 marker, so the durable claim can never hollow-pass); an absent disk is a graceful skip.How
push_recordpersists the full 48-byteEpisodeBody(Kani-provenblkfmt::episode_encode) — the durable log carries the T2 journal field-for-field.MemSubstrate::with_backing+rehydrate_from_backingrebuild T2 from the replayed Episodic log;checkpoint()flushes the backing.engine::mount_durablebuilds aVirtioBlkStorebacking (engine side; the organ names only the trait, §3.4).persist_selftestmoved EPISODIC → WORKING so the M20 substrate round-trip and this M24 organ round-trip do not collide on the one M20 partition (raw 8-byte sentinels vs 48-byte episodes).verified_leaf::M24DurableProof+ facade; re-export selftests → organ → mem.durable-mem:witness family inwitness-census.txt.Verification
CI green on this branch: both-arch build & boot, compile-out (organ off), substrate profile, clippy, conductor-host, corpus-export, m32-local-infer. The durable round-trip runs in-boot on both arches.
Honest scope (follow-ups)
Proves the device round-trip (like the M20 within-boot drop+remount) through the organ/cap path. NOT yet: cross-REBOOT survival (M33-style two-boot), the full cap-DISPATCH path (this drives
MemSubstrate::writedirectly — the same fn the dispatch arm calls), and durable agent homes (themint_memory_home_with_backingprimitive).