F* Memory read/write helpers

MemorySandbox.fst

module MemorySandbox
open FStar.Mul 
open FStar.Bytes
open FStar.Endianness
open FStar.Seq
open FStar.IntegerIntervals


type qword = UInt64.t

let (!) (x: qword) = UInt64.v x

let is_qword (x:nat) = UInt.size x (UInt64.n)

let (+^) (x y: qword) 
  : Pure qword (requires UInt.size (!x + !y) UInt64.n)  
               (ensures fun c -> !x + !y = !c)
    = UInt64.add x y
    
let (-^) (x y: qword) 
  : Pure qword (requires UInt.size (!x - !y) UInt64.n)  
               (ensures fun c -> !x - !y = !c)
    = UInt64.sub x y

let (/^) (x:qword) (y: qword {!y <> 0}) = UInt64.div x y

let ( *^ ) (x y: qword)
  : Pure qword (requires UInt.size (!x * !y) UInt64.n)  
               (ensures fun c -> !x * !y = !c)
  = UInt64.mul x y
 
let heap_size = 1024UL

let heap = byte_array: FStar.Endianness.bytes { length byte_array = !heap_size }

assume val well_formed_heap2 (h: heap) : prop
assume val well_formed_allocated_blocks (h: heap) : prop

let machine_word = 8UL

let is_valid_word_aligned_address_for (addr: qword) (h: heap) 
  = !addr + !machine_word <= length h /\ 
    ((!addr) % (!machine_word)) == 0

let word_aligned_address_for (h: heap) = addr: qword { addr `is_valid_word_aligned_address_for` h }

let read_word (byte_array: heap) 
              (index: qword{(!index * !machine_word + !machine_word) <= !heap_size}) =  
  let byte_index = !index * !machine_word in
  let word_array = slice byte_array byte_index (byte_index + !machine_word) in
  uint64_of_le word_array

let read_word_at (byte_array: heap) 
                 (address: word_aligned_address_for byte_array) =  
  let word_array = slice byte_array !address (!address + !machine_word) in
  uint64_of_le word_array

let read_word_equivalence (byte_array: heap)
                          (address: word_aligned_address_for byte_array)
  : Lemma (read_word_at byte_array address == read_word byte_array (address /^ machine_word)) = ()
 
let rec read_seq_of_words (g: heap)
                          (address: word_aligned_address_for g)
                          (word_count: qword { !address + !word_count * !machine_word <= length g }) 
  : Tot (s: seq qword { length s == !word_count }) 
         (decreases !word_count) = 
  if !word_count = 0 then empty 
  else if !word_count = 1 then begin
    FStar.Seq.create 1 (read_word g (address /^ machine_word))    
  end else begin 
    let next_address : word_aligned_address_for g = address +^ machine_word in
    let tail = read_seq_of_words g (address +^ machine_word) (word_count -^ 1UL) in 
    cons (read_word_at g address) tail
end

#push-options "--z3rlimit 10 --ifuel 1 --fuel 1"
let rec read_seq_is_correct (g: heap)
                            (address: word_aligned_address_for g)
                            (word_count: qword { !address + ((!word_count) * (!machine_word)) <= length g })
                            (i: qword { !i < !word_count })
  : Lemma (ensures index (read_seq_of_words g address word_count) !i
           == read_word_at g (address +^ (i *^ machine_word)))
          (decreases !i) = 
  if (!i = 0) then () else begin
    read_seq_is_correct g (address +^ machine_word) (word_count -^ 1UL) (i -^ 1UL);    
    ()
  end
#pop-options

let read_tail_fields (g: heap{ well_formed_heap2 g /\ well_formed_allocated_blocks g })
                     (header_address: word_aligned_address_for g)
                     (field_count: qword { !header_address + ((1 + !field_count) * !machine_word) <= length g })
                     (skip: qword { !skip <= !field_count })
  : Tot (s: seq qword { length s == !field_count - !skip }) = 
  if !field_count = 0 then empty else begin
    if skip = field_count then empty else begin
      let after_header : word_aligned_address_for g = header_address +^ machine_word in
      let after_skip : qword = after_header +^ (skip *^ machine_word) in
      assert (!(after_header +^ (field_count *^ machine_word)) <= length g);
      let asa : word_aligned_address_for g = after_skip in
      read_seq_of_words g asa (field_count -^ skip)
    end
  end

//ignore this
let math_aux_test (h:heap) (x: word_aligned_address_for h) (n: qword) 
  : Lemma (requires is_qword (!n * !machine_word) /\
                    is_qword (!x + !n * !machine_word) /\
                    !x + !n * !machine_word < length h) 
  (ensures (x +^ (n *^ machine_word)) `is_valid_word_aligned_address_for` h) = 
  let t : qword = x +^ (n *^ machine_word) in
  assert (!t % !machine_word == 0);
  assert (!x + !n * !machine_word <= length h);
  assert (!t == !(x +^ (n *^ machine_word)));
  assert (!x + !n * !machine_word == !t);
  let tt = x +^ (n *^ machine_word) in
  assert (!tt == !t);
  assert (!tt % !machine_word == 0);
  assert (!tt + !machine_word <= length h);
  ()

let math_eq_lemma (h:heap) (x: word_aligned_address_for h) (n: qword {!n * !machine_word <= length h})
  : Lemma ((!x) + (!(n *^ machine_word)) == !x + ((!n) * (!machine_word))) = ()

let math_speedup_lemma (h: heap) (x:word_aligned_address_for h) (n: qword)
  : Lemma ((!x + !n * !machine_word) % !machine_word == 0) =
  Math.Lemmas.modulo_addition_lemma !x !machine_word !n;  
  ()

#push-options "--z3rlimit 50 --ifuel 0 --fuel 0 --split_queries always" 
let read_tail_fields_is_correct_internal (g: heap{ well_formed_heap2 g /\ well_formed_allocated_blocks g })
                                         (header_address: word_aligned_address_for g)
                                         (field_count: qword { !header_address + ((1 + !field_count) * !machine_word) <= Seq.length g })
                                         (skip: qword { !skip <= !field_count })
                                         (i: qword { !i < (!field_count - !skip) })
  : Lemma (index (read_tail_fields g header_address field_count skip) !i ==
           read_word_at g (header_address +^ ((1UL +^ skip +^ i) *^ machine_word))) = 
  if !field_count = 0 then () else begin
    if skip = field_count then () else begin      
      let after_header : word_aligned_address_for g = header_address +^ machine_word in
      let after_skip : qword = after_header +^ (skip *^ machine_word) in
      
//      assert (!(after_header +^ (field_count *^ machine_word)) <= length g);
      let asa : word_aligned_address_for g = after_skip in
      let ait : qword = asa +^ (i *^ machine_word) in
//      assert (!asa % !machine_word == 0);
      //math_speedup_lemma g asa i;
//      assert (!ait % 8 == 0); 
      read_seq_is_correct g asa (field_count -^ skip) i;
      ()
    end
  end
#pop-options

let read_tail_fields_is_correct (g: heap{ well_formed_heap2 g /\ well_formed_allocated_blocks g })
                                (header_address: word_aligned_address_for g)
                                (field_count: qword { !header_address + ((1 + !field_count) * !machine_word) <= Seq.length g })
                                (skip: qword { !skip <= !field_count })
                                (i: qword { !i < (!field_count - !skip) })
  : Lemma (ensures index (read_tail_fields g header_address field_count skip) !i 
                == read_word g ((header_address /^ machine_word) +^ ((1UL +^ skip +^ i)))) 
  = read_tail_fields_is_correct_internal g header_address field_count skip i