proof/ROOT

session Split = HOL +
  options [document = false]
  theories
    Model
    Isolation
    Execution
    Protocol
    Snapshot
    Reuse
    Export
feat(model): formalise writable frame exclusivity 2026-05-04 19:14:00 +01:00			`session Split = HOL +`
			`options [document = false]`
			`theories`
			`Model`
feat(isolation): refine shared storage to private byte memories 2026-05-14 20:37:00 +01:00			`Isolation`
feat(execution): enforce access bounds and allocation capacity 2026-05-27 18:26:00 +01:00			`Execution`
feat(protocol): equate fault resolution and retry with atomic stores 2026-06-09 21:08:00 +01:00			`Protocol`
feat(snapshot): preserve source frames across valid edit traces 2026-06-21 16:43:00 +01:00			`Snapshot`
feat(reuse): preserve zeroed unmapped frames across pool operations 2026-07-03 22:19:00 +01:00			`Reuse`
feat(export): export checked pager transitions as executable ocaml 2026-07-15 19:52:00 +01:00			`Export`