refactor(layout): relocate proof guest and host build inputs

test(pager): check recycling preserves isolation after remapping

feat(checker): check guest observations against exported pager semantics

feat(pager): resolve write faults and recycle scrubbed frames

feat(export): export checked pager transitions as executable ocaml

feat(reuse): preserve zeroed unmapped frames across pool operations

feat(snapshot): preserve source frames across valid edit traces

feat(protocol): equate fault resolution and retry with atomic stores

feat(execution): enforce access bounds and allocation capacity

feat(isolation): refine shared storage to private byte memories

feat(model): formalise writable frame exclusivity