Verified Commit d5ec9d43 authored by james's avatar james
Browse files

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

parent 7a0a28f1

Export.thy

0 → 100644
+16 −0
Changes for Export.thy: 16 added lines, 0 removed lines.
Original line number Diff line number Diff line 
theory Export

  imports Reuse

begin



definition seed :: memory where

  "seed frame offset = (frame * 17 + offset) mod 256"



definition boot :: pager where "boot = initial 4 seed"



definition read_byte :: "pager \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where

  "read_byte s k offset = view s k offset"



export_code boot initial read_byte checked frontier ptable writable prepare reserve reclaim

  Read Write Suc in OCaml module_name Split file_prefix split



end

ROOT

+1 −0
Changes for ROOT: 1 added line, 0 removed lines.
Original line number Diff line number Diff line
@@ -7,3 +7,4 @@ session Split = HOL + 
    Protocol

    Snapshot

    Reuse

    Export