12 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
james	f044a95a6b	feat(snapshot): prove promotion preserves unselected snapshot contents	2026-11-02 02:49:18 +00:00
james	97648de5fc	refactor(layout): relocate proof guest and host build inputs	2026-08-31 17:48:00 +01:00
james	36fd34c522	test(pager): check recycling preserves isolation after remapping	2026-08-20 21:27:00 +01:00
james	be965f3fac	feat(checker): check guest observations against exported pager semantics	2026-08-10 18:34:00 +01:00
james	034f655e01	feat(pager): resolve write faults and recycle scrubbed frames	2026-07-29 20:16:00 +01:00
james	d5ec9d43bb	feat(export): export checked pager transitions as executable ocaml	2026-07-15 19:52:00 +01:00
james	7a0a28f1bf	feat(reuse): preserve zeroed unmapped frames across pool operations	2026-07-03 22:19:00 +01:00
james	c0ba93474c	feat(snapshot): preserve source frames across valid edit traces	2026-06-21 16:43:00 +01:00
james	86650c76e9	feat(protocol): equate fault resolution and retry with atomic stores	2026-06-09 21:08:00 +01:00
james	72727aec95	feat(execution): enforce access bounds and allocation capacity	2026-05-27 18:26:00 +01:00
james	087436dffa	feat(isolation): refine shared storage to private byte memories	2026-05-14 20:37:00 +01:00
james	8607a1f020	feat(model): formalise writable frame exclusivity	2026-05-04 19:14:00 +01:00