 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 |
|