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

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