verifier.mm1

import "compiler.mm1";
import "mm0.mm1";

---------------------------------------
-- Specification of a valid verifier --
---------------------------------------

--| The actual verifier ELF
def Verifier: string;

--| The verifier file is a valid ELF file
theorem Verifier_basicElf: $ isBasicElf Verifier $;

--| Given `mm0_file` on input, the verifier always terminates,
--| ensuring that the final input is empty (the entire input was consumed),
--| the output is empty (it outputs nothing), and the theorems in the
--| mm0 file are derivable.
theorem Verifier_terminates {mm0_file output: nat} (k: nat):
  $ initialConfig Verifier k ->
    terminates_ensuring k (S\ mm0_file, {output |
      output = 0 /\ Valid mm0_file}) $;

--| Unpacking the above claim: if we set up an initial configuration
--| such that `mm0_file` is on standard in, and it runs to completion
--| having consumed the input and produced no output with exit code 0,
--| then the theorems in the input are derivable.
theorem Verifier_Valid (k mm0_file: nat):
  $ initialConfig Verifier k /\ succeeds k mm0_file 0 ->
    Valid mm0_file $ =
(named '(anrd @ sylib (elsabe @ elabed @ aneqd (eqeq1d anr) @ Valideqd anl) @
  sylan terminates_ensuring_succeeds (anwl Verifier_terminates) anr));

def Represents (env a_sorts a_terms a_thms: nat) = $ T. $;

do {
  -- Import some constants from MM1
  (mmc-add @ map (fn (x) '(const {{,x : u64} := (pure ,x)}))
    '(O_RDONLY O_WRONLY O_CREAT O_TRUNC
      MAP_FAILED MAP_PRIVATE MAP_ANONYMOUS))

  -- This is just a scratchpad for now, some thoughts on MMC syntax and primitives.
  (mmc-add '(
    (intrinsic struct CStr
      {(ghost len) : nat}
      {buf : (array u8 {len + 1})}
      {eq0 : (pure $ A. i (nth buf i = suc 0 <-> i = len) $)})

    (intrinsic struct Stat
      {st_dev : u64} {st_ino : u64} {st_nlink : u64}
      {st_mode : u32} {st_uid : u32} {st_gid : u32} {_ : i32}
      {st_rdev : u64} {st_size : i64}
      {st_blksize : i64} {st_blocks : i64}
      {st_atime : i64} {st_atime_nsec : i64}
      {st_mtime : i64} {st_mtime_nsec : i64}
      {st_ctime : i64} {st_ctime_nsec : i64}
      {_ : (array i64 3)})

    (intrinsic proc (sys_fstat {fd : u32}
      (mut {(ghost buf) : (? Stat)}) {p : (&sn buf)} :
      (out {buf : Stat})
      u32))
    (intrinsic proc (sys_open
      {fname : (& CStr)}
      {flags : {(sn O_RDONLY) or (sn {O_WRONLY + O_CREAT + O_TRUNC})}} :
      u32))
    (intrinsic proc (sys_mmap {pos : (sn {0 : u64})} {len : u64} {prot : u32}
      {(ghost anon) : bool}
      {flags : (sn {(if anon MAP_PRIVATE {MAP_PRIVATE + MAP_ANONYMOUS}) : u64})}
      {fd : (if anon (sn {(- 1) : i64}) i64)}
      {off : (sn {0 : u64})} :
      {ret : (or
        (struct {err : i64} (pure $ isIOError err $))
        (own @ struct {ret : (array u8 len)} (pure $ anon -> all (sn 0) ret $)))}))

    (struct File
      (implicit @ ghost {len : nat})
      {file : (& (array u8 len))}
      {end : (sn {{file + len} : u64})})

    (global {{F : (? File)} := uninit})

    (struct Header0
      {magic : u32} {version : u8} {num_sorts : u8} {_ : u16}
      {num_terms : u32} {num_thms : u32}
      {p_terms : u32} {p_thms : u32}
      {p_proof : u32} {_ : u32}
      {p_index : u64})

    (struct Header {h : Header0} {sorts : (array u8 (h . num_sorts))})

    (const {{MM0B_MAGIC : u32} := 0x42304D4D})
    (const {{MM0B_VERSION : u8} := 1})
    (const {{MAX_SORTS : u8} := 128})
    (const {{CMD_END : u8} := 0})

    (struct Term0 {num_args : u16} {sort : u8} {_ : u8} {p_args : u32})
    (struct Thm0 {num_args : u16} {_ : u16} {p_args : u32})

    (struct (CData A)
      (implicit @ ghost {max : nat})
      {buf : (& (array A max))})

    (struct (MData A {c : (CData A)})
      {cur : u32}
      {dat : (ref (array A cur))}
      {eq : {(c . buf) :> (&sn dat)}}
      {le : {cur <= (c . max)}})

    (struct Env {e : nat} {h : (pure $ Env e $)})

    (struct CState
      {sorts : (CData u8)}
      {terms : (CData Term0)}
      {thms : (CData Thm0)})

    (struct (MState {c : CState})
      {sorts : (MData u8 (c . sorts))}
      {terms : (MData Term0 (c . terms))}
      {thms : (MData Thm0 (c . thms))}
      {env : Env}
      {env2 : Env}
      {ext : (pure $ EnvExtend env env2 $)}
      {repr : (pure
        {sorts := (sorts . dat)}
        {terms := (terms . dat)}
        {thms := (thms . dat)}
        $ Represents env2 sorts terms thms $)})

    (global {{C : (? CState)} := uninit})
    (global {{M : (? (MState (cast C)))} := uninit})

    (func (cmd_unpack {cmd : (& (array u8 5))} : u8 u8 u32)
      {v := (index cmd 0)}
      {w := {v band 0x3F}}
      (match {v shr 6}
        {0 => (return w 1 0)}
        {1 => (return w 2 {(index cmd 1) as u32})}
        {2 => (return w 3 {{(pun @ slice cmd 1 2) : u16} as u32})}
        {3 => (return w 5 {(pun @ slice cmd 1 4) : u32})}
        {_ => (unreachable _)}))

    (proc (parse_until
      (global {C : CState})
      (mut @ global {M : (MState C)})
      {stmt_type : u8}
      {h : (match stmt_type
        {CMD_STMT_SORT => {((M . sorts) . cur) < ((C . sorts) . max)}}
        {_ => #f})} :
      (out M {M2 : (MState C)})
      {_ : (match stmt_type
        {CMD_STMT_SORT => {((M2 . sorts) . cur) = {((M . sorts) . cur) + 1}}}
        {_ => #f})}
      ))

    (proc (verify
        (global {F : File})
        (mut @ ghost {input : Input}) :
        (pure $ Valid input $))
      {(len file end) := (ref F)}
      {{p : (& Header0)} := (pun file (assert {(sizeof Header0) <= len}))}
      (assert {(p . magic) = MM0B_MAGIC})
      (assert {(p . version) = MM0B_VERSION})
      {nsorts := (p . num_sorts)}
      {h2 := (assert {nsorts <= MAX_SORTS})}
      {{C : CState} <- (list
        (list (& (slice file (sizeof Header) nsorts)))
        (list (& (slice file (p . p_terms) (p . num_terms))))
        (list (& (slice file (p . p_thms) (p . num_thms)))))}
      {(dat eq) := (typeof (& (slice ((C . sorts) . buf) 0 0)))}
      {(M . sorts) <- (list 0 dat eq)}
      {(dat eq) := (typeof (& (slice ((C . terms) . buf) 0 0)))}
      {(M . terms) <- (list 0 dat eq)}
      {(dat eq) := (typeof (& (slice ((C . thms) . buf) 0 0)))}
      {(M . thms) <- (list 0 dat eq)}
      {(M . env) <- _}
      {(M . env2) <- _}
      {(M . ext) <- _}
      {(M . repr) <- _}
      {(ref M) : (MState C)}
      {(ghost remainder) := {len - (p . p_proof)}}
      {remainder_bd := (assert {{(p . p_proof) + 5} <= len})}
      {stmt := (& (slice file (p . p_proof) remainder (entail remainder_bd _)))}
      {{suff : {{stmt + remainder} = end}} := _}

      (while {(index stmt 0 (entail remainder_bd _)) != CMD_END}
        (variant {(p . p_proof) + 5} <= len := remainder_bd)

        {((w sz data) h_unpack) := (sn (cmd_unpack stmt))}
        {{remainder <- {remainder - data}} with {remainder -> old_rem}}
        {next_stmt_bd := (assert {{stmt + data + 5} <= end})}
        {remainder_bd <- (entail next_stmt_bd _)}
        {next_stmt := (& (slice stmt data remainder
          (entail next_stmt_bd suff _)))}

        (match w
          {CMD_STMT_SORT => (begin
            (assert {data = sz})
            {h := (assert {((M . sorts) . cur) < ((C . sorts) . max)})}
            {(h_sorts repr2) := (parse_until CMD_STMT_SORT h)}
            {((M . sorts) . cur) <- (cast {((M . sorts) . cur) + 1} (entail h _))}
            {((M . sorts) . le) <- (cast ((M . sorts) . le) _)}
          )}

          {{CMD_STMT_DEF or CMD_STMT_LOCAL_DEF} => (begin
              _ -- this marks unfinished code, the compiler will give an error
                -- and provide the current type context
          )}
        )

        {stmt <- next_stmt}
        {suff <- (entail suff _)}
        (continue
          (variant (entail h_unpack remainder
            -- proof of
            -- w, sz, data = cmd_unpack (* stmt),
            -- remainder = old_rem - data |- remainder < old_rem
            _))))
      (assert {((M . sorts) . cur) = ((C . sorts) . max)})
      (assert {((M . terms) . cur) = ((C . terms) . max)})
      (assert {((M . thms) . cur) = ((C . thms) . max)})
      (entail (parse_until CMD_END) _))

    (proc (main
        {argc : u32}
        {args : (& (array (& CStr) argc))}
        (mut @ ghost {input : Input})
        (mut @ ghost {output : (sn {0 : Output})}) :
        (out {output : Output})
        (pure $ output = 0 /\ Valid input $))
      {(output2 oz) := output}
      {output <- output2}
      {fd := (sys_open (index args 1) O_RDONLY)}
      (assert {0 <= {fd as i64}})
      {{buf : (? Stat)} := uninit}
      (begin
        {n := (sys_fstat fd buf _)}
        (assert {0 <= {n as i64}}))
      {len := (buf . st_size)}
      {(ptr h) := (typeof! (sys_mmap 0 len PROT_READ #f MAP_PRIVATE {fd as i64} 0))}
      {{((ghost buf) file) : (own (array u8 len))} :=
        (pun ptr (entail h (assert {ptr != MAP_FAILED})
          -- proof of
          -- ptr :: (union (sn {MAP_FAILED : u64})
          --   (own (struct {ret : (array u8 len)} $ fd = bitsNeg 32 1 -> all (sn 0) ret $))) /\
          -- ptr != MAP_FAILED
          -- |- (ptr :: (own (array u8 len))
          _))}
      {{F : File} <- (list file (sn {(& (slice file len 0)) as u64}))}
      (list oz (verify input)))
  ))
};