Extended_Reals : Theory
Begin

  extended_real? : PRED[number]

  Extended_Real : Type = (extended_real?)

  number_field_in_extended_real : Axiom
    Forall (n : number_field) : extended_real?(n)

  value? : PRED[Extended_Real]
  nan?   : {P : PRED[Extended_Real] | disjoint?(P, value?)}

  qnan?  : set[(nan?)]
  snan?  : {P : PRED[(nan?)] | disjoint?(P, qnan?)}

End Extended_Reals

Cpp_Type : Datatype With Subtypes Fundamental, Compound, Hardware
Begin
  % fundamental C++ types
  %-----------------------
  bool  : bool?  : Fundamental
  char  : char?  : Fundamental
  short : short? : Fundamental
  int   : int?   : Fundamental
  % ...

  enum(typ : Fundamental) : enum? : Compound
  % ...
    
  % hardware types
  %----------------
  bit     : bit?     : Hardware
  byte    : byte?    : Hardware
  word    : word?    : Hardware
  address : address? : Hardware
End Cpp_Type


Toy_Syntax_Pre : Theory
Begin

  Importing Extended_Reals, Cpp_Type

  % Addresses
  %===========

  max_GP        : posnat
  max_Temporary : posnat

  Register_ID : Datatype 
  Begin
    Phys_Mem                  : Phys_Mem?
    Gp_Reg(x : below[max_GP]) : Gp_Reg?
    % ...
    % special purpose regs
    % ...
    Premature                                            : Premature?
    Temporary(id : below[max_Temporary], typ : Cpp_Type) : Temporary?
  End Register_ID 

  Address : Type = [# register : Register_ID, offset : int #]

  a : Var Address
  i : Var int

  +(a, i) : Address = a With [(offset) := offset(a) + i]
  
  valid? : [Register_ID -> finite_set[int]]

  Physical_Address : Type = {a : Address | Phys_Mem?(register(a))}

  Bit : Type = below[2]

  Virtual_Address : Type = int

  temporary?(typ : Cpp_Type)(a : Address) : bool = 
    Temporary?(register(a)) And (typ(register(a)) = typ)

  min_page_size : posnat

  % Datatype Semantics
  %====================

  Interpreted_Data_Type : Type = [#
    range     : nonempty_set[Extended_Real], 
    alignment : posnat, 
    size      : {p : posnat | p <= min_page_size},
    support   : nonempty_set[below[size]],
    to_bits    : [(range) -> [(support) -> Bit]], 
    from_bits  : [[(support) -> Bit] -> (range)]
  #]

  idt?(dt : Interpreted_Data_Type) : bool = 
    % from_bit is left inverse of to_bit
    (Forall (d : (range(dt))) : value?(d) Implies dt`from_bits(dt`to_bits(d)) = d)

  dt : {f : [Cpp_Type -> (idt?)] | f(bool)`range(1) And 
                                   subset?(f(address)`range, 
            extend[Extended_Real, Virtual_Address, bool, false](fullset[Virtual_Address]) )}

  dt_address_type : Lemma
    Forall (val : [(support(dt(address))) -> Bit]) : 
    number_field_pred(dt(address)`from_bits(val)) And
      Forall (n : nat) : 
        real_pred(dt(address)`from_bits(val) + n) And
        rational_pred(dt(address)`from_bits(val) + n) And
        integer_pred(dt(address)`from_bits(val) + n) 

  % Commands
  %==========

  Binary_Op : Type
  Unary_Op  : Type
  Marker    : Type

End Toy_Syntax_Pre

Command : Datatype With Subtypes Expression, Statement
Begin

    Importing Toy_Syntax_Pre

    % Expression
    %------------

    const (typ : Cpp_Type, t_res : (temporary?(typ)), 
           c : (range(dt(typ))))                                    : const?     : Expression

    read_reg (typ : Cpp_Type, t_res : (temporary?(typ)),
              addr : Address)                                       : read_reg?  : Expression

    read_mem (typ : Cpp_Type, t_res : (temporary?(typ)),
              vaddr : Virtual_Address)                              : read_mem?  : Expression

    read_ptr (typ : Cpp_Type, t_res : (temporary?(typ)),
              taddr : (temporary?(address)))                        : read_ptr?  : Expression

    binary_op (typ : Cpp_Type, t_res : (temporary?(typ)),
               bin_op : Binary_Op, l, r : (temporary?(typ)))        : binary_op? : Expression

    unary_op (typ : Cpp_Type, t_res : (temporary?(typ)),
              un_op : Unary_Op, value : (temporary?(typ)))          : unary_op?  : Expression

    cast (typ : Cpp_Type, t_res : (temporary?(typ)), 
          from_typ : Cpp_Type, from_value : (temporary?(from_typ))) : cast?      : Expression

    % Statements
    %------------

    skip(n : posnat) : skip? : Statement

    e2s (exp : Expression) : e2s? : Statement
    
    write_reg (typ : Cpp_Type, value : (temporary?(typ)), 
               addr : Address)                              : write_reg?    : Statement

    write_mem (typ : Cpp_Type, value : (temporary?(typ)), 
               vaddr : Virtual_Address)                     : write_mem?    : Statement

    write_ptr (typ : Cpp_Type, value : (temporary?(typ)), 
               taddr : (temporary?(address)))               : write_ptr?    : Statement

    if_then_else (condition : (temporary?(bool)), 
                  stm_if, 
                  stm_else : {s : Statement | Not nil?(s)}) : if_then_else? : Statement
 
    seq (stm1, stm2 : {s : Statement | Not nil?(s)})        : seq?          : Statement

    parallel (m : Marker, id : nat, 
              stm1, stm2 : {s : Statement | Not nil?(s)})   : parallel?     : Statement

    % Helper Statements
    %-------------------

    ndet (m : Marker, 
          stm1, stm2 : {s : Statement | Not nil?(s)})       : ndet?         : Statement

    nil                                                     : nil?          : Statement

End Command

Toy_Syntax : Theory
Begin

  Importing Command, Toy_Syntax_Pre, Command_adt

  count(c : Command) : Recursive nat = 
    Cases c Of
      % Statements
      skip(n)                           : n,
      e2s(exp)                          : count(exp),
      write_reg(typ, val, addr)         : 1,
      write_mem(typ, val, addr)         : 1,
      write_ptr(typ, val, addr)         : 1,
      if_then_else(c, stm_if, stm_else) : 1 + max(count(stm_if), count(stm_else)),
      seq(stm1, stm2)                   : count(stm1) + count(stm2),
      parallel(m, id, stm1, stm2)       : count(stm1) + count(stm2),
      nil                               : 0,
      ndet(m, stm1, stm2)               : max(count(stm1), count(stm2))
   Else
     % Expressions
     1
   EndCases
  Measure c by <<;

  cmd_measure(c : Command) : Recursive nat = 
    Cases c Of
      % Statements
      skip(n)                           : n,
      e2s(exp)                          : 1 + cmd_measure(exp),
      write_reg(typ, val, addr)         : 1,
      write_mem(typ, val, addr)         : 1,
      write_ptr(typ, val, addr)         : 1,
      if_then_else(c, stm_if, stm_else) : 
        2 + max(1 + cmd_measure(stm_if) + max(count(stm_else) - count(stm_if), 0),
                1 + cmd_measure(stm_else) + max(count(stm_if) - count(stm_else), 0)),
      seq(stm1, stm2)                   : 1 + cmd_measure(stm1) + cmd_measure(stm2),
      parallel(m, id, stm1, stm2)       : 1 + cmd_measure(stm1) + cmd_measure(stm2),
      nil                               : 0,
      ndet(m, stm1, stm2)               : 
        1 + max(1 + cmd_measure(stm1) + max(count(stm2) - count(stm1), 0),
                1 + cmd_measure(stm2) + max(count(stm1) - count(stm2), 0))
   Else
     % Expressions
     1
   EndCases
  Measure c by <<;

  cmd_measure_count : Lemma
    Forall (c : Command) : 
      count(c) <= cmd_measure(c)

  not_parallel?(c : Command) : Recursive bool = 
    Cases c Of 
      seq(stm1, stm2) : 
        not_parallel?(stm1) And not_parallel?(stm2),

      if_then_else(condition, stm_if, stm_else) : 
        not_parallel?(stm_if) And not_parallel?(stm_else),

      ndet(m, stm1, stm2) :
        not_parallel?(stm1) And not_parallel?(stm2),
 
      parallel(m, id, stm1, stm2) : 
        False
    Else
      True
    EndCases
   Measure c by <<

  % Syntactic Sugar
  %-----------------
  if_then (condition : (temporary?(bool)), stm : {s : Statement | Not nil?(s)}) : Statement = 
    if_then_else(condition, stm, skip(1))

  indet (m : Marker, stm1, stm2 : {s : Statement | Not nil?(s)}) : Statement = 
    ndet(m, seq(stm1, stm2), seq(stm2, stm1))

  skip(n : nat) : Statement = 
    If n = 0 Then nil Else skip(n) Endif

  seq_nil(stm1 : {s : Statement | Not nil?(s)}, 
          stm2 : Statement) : {s : Statement | Not nil?(s)} = 
    If nil?(stm2) Then
      stm1
    Else
      seq(stm1, stm2)
    Endif


  while_n (n : nat, condition : (temporary?(bool)), 
                    body : {s : Statement | Not nil?(s)}) : 
                                     Recursive {s : Statement | Not nil?(s)} =
    If n = 0 Then 
      skip(1)
    Else
      if_then(condition, seq(body, while_n(n - 1, condition, body)))
    Endif
   Measure n;

  count_skip_n : Lemma
    Forall (n : nat) : count(skip(n)) = n

  count_pos : Lemma 
    Forall (stm : Statement) : Not nil?(stm) Implies count(stm) > 0

  count_nil : Lemma
    Forall (c : Command) : 
      count(c) = 0 IFF nil?(c)

End Toy_Syntax


Memory : Theory
Begin

  Importing Toy_Syntax, Subtype_Order

  vm  : {f : [Virtual_Address -> Physical_Address] |
             Forall (v1, v2 : Virtual_Address) : v1 < v2 And v2 - v1 < min_page_size 
               Implies f(v1) /= f(v2)}

  readable? : PRED[Address] 
  writable? : PRED[Address] 

  effect    : (partial_preorder?((readable?), (writable?)))

  % Locks
  Lock : Type

  locks            : [nat -> PRED[Lock]]
  locked_addresses : [Lock -> PRED[Address]]

  local?(n : nat)(a : Address) : bool = 
    Exists (l : Lock) : locks(n)(l) And locked_addresses(l)(a)

  not_local?(n : nat)(a : Address) : bool = 
    Not local?(n)(a)

End Memory

Memory_Ops [T : Type] : Theory
Begin

  Importing Memory

  singleton_support : Lemma
    Forall (t : Cpp_Type, x, a : Address) : 
      (Exists (i: (support(dt(t)))): x = a + i) Implies
         singleton?({i: (support(dt(t))) | x = a + i})

  singleton_support2 : Lemma
    Forall (t : Cpp_Type, x : Address, a : Virtual_Address) : 
      (Exists (i: (support(dt(t)))): x = vm(a + i)) Implies
         singleton?({i: (support(dt(t))) | x = vm(a + i)})

  read_bits(t : Cpp_Type, a : Address)(mem : [Address -> T]) : [(support(dt(t))) -> T] = 
    Lambda (n : (support(dt(t)))) : mem(a + n)

  write_bits(t : Cpp_Type, a : Address, value : [(support(dt(t))) -> T])
            (mem : [Address -> T]) : [Address -> T] = 
    Lambda (x : Address) : 
      If Exists (i : (support(dt(t)))) : x = a + i Then
        value(singleton_elt({i : (support(dt(t))) | x = a + i}))
      Else
        mem(x)
      Endif

  read_bits(t : Cpp_Type, a : Virtual_Address)(mem : [Address -> T]) : [(support(dt(t))) -> T] = 
    Lambda (n : (support(dt(t)))) : mem(vm(a + n))

  write_bits(t : Cpp_Type, a : Virtual_Address, value : [(support(dt(t))) -> T])
            (mem : [Address -> T]) : [Address -> T] = 
    Lambda (x : Address) : 
      If Exists (i : (support(dt(t)))) : x = vm(a + i) Then
        value(singleton_elt({i : (support(dt(t))) | x = vm(a + i)}))
      Else
        mem(x)
      Endif

End Memory_Ops

Toy_Semantics : Theory
Begin

  Importing Toy_Syntax, 
            Memory_Ops[Bit]

  % State
  State : Type = [#
    ip : nat, 
    mem : [Address -> Bit] 
  #]

  % Oracles
  %---------

  Input_Oracle : Type = [nat -> [Address -> lift[Bit]]]
  Control_Flow_Oracle : Type = [Marker, nat -> bool]

  external(io : Input_Oracle)(s : State) : State = 
    s With [(ip)  := s`ip + 1,
            (mem) := Lambda (a : Address) : 
                       If Phys_Mem?(register(a)) And up?(io(s`ip)(a)) And
                          not_local?(s`ip)(a) And writable?(a) 
                       Then
                         down(io(s`ip)(a))
                       Else
                         s`mem(a)
                       Endif]
                          
  % Semantics of Toy Expressions
  %
  step_const (io : Input_Oracle, exp : (const?))(s0 : State) : State = 
    Let s = external(io)(s0) In 
      s With [(mem) := write_bits(typ(exp), t_res(exp),  
                                dt(typ(exp))`to_bits(c(exp)))(s`mem)]


  step_read_reg (io : Input_Oracle, exp : (read_reg?))(s0 : State) : State =
    Let s = external(io)(s0) In 
      s With [(mem) := write_bits(typ(exp), t_res(exp), 
                                  read_bits(typ(exp), addr(exp))(s`mem))(s`mem)]

  step_read_mem (io : Input_Oracle, exp : (read_mem?))(s0 : State) : State = 
    Let s = external(io)(s0) In 
      s With [(mem) := write_bits(typ(exp), t_res(exp), 
                                  read_bits(typ(exp), vaddr(exp))(s`mem))(s`mem)]

  step_read_ptr (io : Input_Oracle, exp : (read_ptr?))(s0 : State) : State = 
    Let s = external(io)(s0), 
        vaddr = dt(address)`from_bits(read_bits(address, taddr(exp))(s`mem)) In
      step_read_mem(io, read_mem(typ(exp), t_res(exp), vaddr))(s0)

  bin_op_sem : [Binary_Op, typ : Cpp_Type, (range(dt(typ))), (range(dt(typ))) -> (range(dt(typ)))]

  step_binary_op (io : Input_Oracle, exp : (binary_op?))(s0 : State) : State = 
    Let s = external(io)(s0), 
        left  = dt(typ(exp))`from_bits(read_bits(typ(exp), l(exp))(s`mem)),
        right = dt(typ(exp))`from_bits(read_bits(typ(exp), r(exp))(s`mem)) In
      s With [(mem) := write_bits(typ(exp), t_res(exp),
                         dt(typ(exp))`to_bits(bin_op_sem(bin_op(exp), typ(exp), left, right)))(s`mem)]
      
  unary_op_sem : [Unary_Op, typ : Cpp_Type, (range(dt(typ))) -> (range(dt(typ)))]

  step_unary_op (io : Input_Oracle, exp : (unary_op?))(s0 : State) : State = 
    Let s = external(io)(s0),
        value = dt(typ(exp))`from_bits(read_bits(typ(exp), value(exp))(s`mem)) In
      s With [(mem) := write_bits(typ(exp), t_res(exp),
                         dt(typ(exp))`to_bits(unary_op_sem(un_op(exp), typ(exp), value)))(s`mem)]
 
  cast_op_sem : [typ : Cpp_Type, from_typ : Cpp_Type, (range(dt(from_typ))) -> (range(dt(typ)))]

  step_cast (io : Input_Oracle, exp : (cast?))(s0 : State) : State =
    Let s = external(io)(s0),
        value = dt(from_typ(exp))`from_bits(read_bits(from_typ(exp), from_value(exp))(s`mem)) In
      s With [(mem) := write_bits(typ(exp), t_res(exp),
                         dt(typ(exp))`to_bits(cast_op_sem(typ(exp), from_typ(exp), value)))(s`mem)]

  step_exp (io : Input_Oracle, exp : Expression)(s : State) : State = 
    Cases exp Of
      const (typ, t_res, value)        : step_const     (io, exp)(s), 
      read_reg (typ, t_res, addr)      : step_read_reg  (io, exp)(s), 
      read_mem (typ, t_res, addr)      : step_read_mem  (io, exp)(s), 
      read_ptr (typ, t_res, addr)      : step_read_ptr  (io, exp)(s), 
      binary_op (typ, t_res, op, l, r) : step_binary_op (io, exp)(s), 
      unary_op (typ, t_res, op, val)   : step_unary_op  (io, exp)(s), 
      cast (typ, t_res, from_typ, from_val) : step_cast      (io, exp)(s)
    EndCases
          
  % Semantics of Toy Statements
  %
  io     : Var Input_Oracle
  pick   : Var Control_Flow_Oracle
  s, s0  : Var State

  step_e2s(io, pick)(stm : (e2s?), s) : [Statement, State] = 
    (nil, step_exp(io, exp(stm))(s))

  step_skip(io, pick)(stm : (skip?), s) : [Statement, State] = 
    If n(stm) = 1 Then 
      (nil, external(io)(s))
    Else 
      (skip(n(stm) - 1), external(io)(s))
    Endif

  step_write_reg(io, pick)(stm : (write_reg?), s0) : [Statement, State] = 
    (nil, Let s = external(io)(s0) In
            s With [(mem) := write_bits(typ(stm), addr(stm), 
                               read_bits(typ(stm), value(stm))(s`mem))(s`mem)])

  step_write_mem(io, pick)(stm : (write_mem?), s0) : [Statement, State] = 
    (nil, Let s = external(io)(s0) In
            s With [(mem) := write_bits(typ(stm), vaddr(stm), 
                               read_bits(typ(stm), value(stm))(s`mem))(s`mem)])

  step_write_ptr(io, pick)(stm : (write_ptr?), s0) : [Statement, State] = 
    (nil, Let s = external(io)(s0), 
              vaddr = dt(address)`from_bits(read_bits(address, taddr(stm))(s`mem)) In
            s With [(mem) := write_bits(typ(stm), vaddr, 
                               read_bits(typ(stm), value(stm))(s`mem))(s`mem)])

  step_if(io, pick)(stm : (if_then_else?), s0) : [Statement, State] = 
    Let (stm_nil, s) = step_skip(io, pick)(skip(1), s0), 
        b = dt(bool)`from_bits(read_bits(bool, condition(stm))(s`mem)) In 
    If b = 1 Then
      (seq_nil(stm_if(stm), skip(max(count(stm_else(stm)) - count(stm_if(stm)), 0))), s)
    Else
      (seq_nil(stm_else(stm), skip(max(count(stm_if(stm)) - count(stm_else(stm)), 0))), s)
    Endif

  step_nil(io, pick)(stm : (nil?), s) : [Statement, State] = 
    (nil, s)

  step(io, pick)(stm : Statement, s) : Recursive [Statement, State] = 
    Cases stm Of
      skip(n)                           : step_skip(io, pick)(stm, s),
      e2s(exp)                          : step_e2s(io, pick)(stm, s),
      write_reg(typ, val, addr)         : step_write_reg(io, pick)(stm, s),
      write_mem(typ, val, addr)         : step_write_mem(io, pick)(stm, s),
      write_ptr(typ, val, addr)         : step_write_ptr(io, pick)(stm, s),
      if_then_else(c, stm_if, stm_else) : step_if(io, pick)(stm, s),
      nil                               : step_nil(io, pick)(stm, s),
      ndet(m, stm1, stm2)               : 
        If pick(m(stm), 0) Then 
          step(io, pick)
              (seq_nil(stm1(stm), skip(max(count(stm2(stm)) - count(stm1(stm)), 0))), s)
        Else
          step(io, pick)
              (seq_nil(stm2(stm), skip(max(count(stm1(stm)) - count(stm2(stm)), 0))), s)
        Endif,

      seq(stm1, stm2)                   : Let res = step(io, pick)(stm1, s) In
                                            If nil?(res`1) Then 
                                              (stm2, res`2)
                                            Else
                                              (seq(res`1, stm2), res`2)
                                            Endif,
      parallel(m, id, stm1, stm2)       : If pick(m, id) Then
                                            Let res = step(io, pick)(stm1, s) In
                                              If nil?(res`1) Then 
                                                (stm2, res`2)
                                              Else 
                                                (parallel(m, id + 1, res`1, stm2), res`2)
                                              Endif
                                          Else
                                            Let res = step(io, pick)(stm2, s) In
                                              If nil?(res`1) Then 
                                                (stm1, res`2)
                                              Else 
                                                (parallel(m, id + 1, stm1, res`1), res`2)
                                              Endif
                                          Endif
    EndCases
   Measure cmd_measure(stm)

  step_count : Lemma
    Forall (stm : {s : Statement | Not nil?(s)}): 
      step(io, pick)(stm, s)`2`ip = s`ip + 1

  step_count_seq : Lemma
    Forall (stm1, stm2 : {s : Statement | Not nil?(s)}): 
      Not nil?(step(io, pick)(stm1, s)`1) Implies 
        count(step(io, pick)(seq(stm1, stm2), s)`1) = count(seq(step(io, pick)(stm1,s)`1, stm2))

  step_count2 : Lemma
    Forall (stm : {s : Statement | Not nil?(s)}): 
      count(stm) = count(step(io, pick)(stm, s)`1) + 1

  step_cmd_measure_seq : Lemma
    Forall (stm1, stm2 : {s : Statement | Not nil?(s)}): 
      cmd_measure(stm1) > cmd_measure(step(io, pick)(stm1, s)`1) Implies
        cmd_measure(seq(stm1, stm2)) > cmd_measure(step(io, pick)(seq(stm1, stm2), s)`1)

  step_cmd_measure : Lemma
    Forall (stm : {s : Statement | Not nil?(s)}): 
      cmd_measure(stm) > cmd_measure(step(io, pick)(stm, s)`1)

  run(io, pick)(max : nat)(stm : Statement, s) : Recursive [Statement, State] = 
    If max = 0 Or nil?(stm) Then 
      (stm, s)
    Else
      run(io, pick)(max - 1)(step(io, pick)(stm, s)) 
    Endif
   Measure cmd_measure(stm)

  run_count : Lemma
    Forall (stm : Statement, max : nat) : 
      max <= count(stm) Implies
        count(run(io, pick)(max)(stm, s)`1) = count(stm) - max

  run_split : Lemma
    Forall (stm : Statement, i, max : nat) : i < max Implies
      run(io, pick)(max)(stm, s) = run(io, pick)(max - i)(run(io, pick)(i)(stm, s))

  run_nil : Lemma 
    Forall (stm : Statement) : 
      nil?(run(io, pick)(count(stm))(stm, s)`1)

  run_seq1 : Lemma
    Forall (stm1, stm2 : {s : Statement | Not nil?(s)}, max : nat): max <= count(stm1) Implies
      run(io, pick)(max)(seq(stm1, stm2), s)`2 = run(io, pick)(max)(stm1, s)`2

  run_seq2a : Lemma
    Forall (stm1, stm2 : {s : Statement | Not nil?(s)}, max : nat): max >= count(stm1) Implies
      run(io, pick)(max)(seq(stm1, stm2), s)`1 = 
        run(io, pick)(max - count(stm1))(stm2, run(io, pick)(count(stm1))(stm1, s)`2)`1

  run_seq2 : Lemma
    Forall (stm1, stm2 : {s : Statement | Not nil?(s)}, max : nat): max >= count(stm1) Implies
      run(io, pick)(max)(seq(stm1, stm2), s)`2 = 
        run(io, pick)(max - count(stm1))(stm2, run(io, pick)(count(stm1))(stm1, s)`2)`2

  run_skip : Lemma
    Forall (i, j, max : nat) : max <= i Implies
      run(io, pick)(max)(skip(i), s)`2 = run(io, pick)(max)(skip(i + j), s)`2

  run_skip2 : Lemma
    Forall (i, j : nat) : 
      run(io, pick)(i)(skip(i + j), s)`1 = skip(j)

  run_count2_seq : Lemma
    Forall (stm1, stm2 : {s : Statement | Not nil?(s)}, max : nat) : 
      (Forall (s : State, max : nat) : 
         run(io, pick)(max)(stm1, s)`2`ip = s`ip + min(max, count(stm1))) And
      (Forall (s : State, max : nat) : 
         run(io, pick)(max)(stm2, s)`2`ip = s`ip + min(max, count(stm2)))
    Implies
      run(io, pick)(max)(seq(stm1, stm2), s)`2`ip = s`ip + min(max, count(seq(stm1, stm2)))

  run_count2_skip_n : Lemma
    Forall (n, max : nat) : 
      run(io, pick)(max)(skip(n), s)`2`ip = s`ip + min(max, count(skip(n)))

  run_count2 : Lemma
    Forall (stm : {s : Statement | not_parallel?(s)}, max : nat) : 
      run(io, pick)(max)(stm, s)`2`ip = s`ip + min(max, count(stm))

  skip_n_memory : Lemma
    Forall (n, max : nat, s, t : State, a : Address) : 
      s`ip = t`ip And s`mem(a) = t`mem(a) 
    Implies
      run(io, pick)(max)(skip(n), s)`2`mem(a) = run(io, pick)(max)(skip(n), t)`2`mem(a) 

End Toy_Semantics