Memory access helper lemmas

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_at g address)    
  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 5 --ifuel 0 --fuel 1 --split_queries always"
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 begin
    read_seq_is_correct g (address +^ machine_word) (word_count -^ 1UL) (i -^ 1UL);    

    ()
  end
#pop-options

let qword_of (n: nat{UInt.size n 64}) = UInt64.uint_to_t n

let read_seq_of_words_fast (g:heap)
                           (address: word_aligned_address_for g)
                           (word_count: qword)
  : Pure (s: seq qword { length s == !word_count })
         (requires !address + !word_count * !machine_word <= length g)
         (ensures fun r -> forall (i: qword{ !i < !word_count }). 
                          index r !i == read_word_at g (address +^ (i *^ machine_word))) 
  = Seq.init !word_count (fun i -> read_word_at g (address +^ ((qword_of i)*^machine_word)))


#push-options "--z3rlimit 5 --ifuel 1 --fuel 1 --split_queries always"
let read_seq_of_words_fast_is_correct (g:heap) 
                                      (address: word_aligned_address_for g)
                                      (word_count: qword)
                                      (i:qword)
  : Lemma (requires !address + !word_count * !machine_word <= length g /\ !i < !word_count)
          (ensures index (read_seq_of_words_fast g address word_count) !i
                == read_word_at g (address +^ (i *^ machine_word))) 
  = () //trivial and obvious.
#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

let read_tail_fields_fast (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 || skip = field_count then empty else 
    read_seq_of_words_fast g (header_address +^ machine_word +^ (skip *^ machine_word)) (field_count -^ skip) 


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


/// Very subtle arithmetic difference leads to increased resource usage.
/// Compare how the x+m+(i+skip)*m variant is much harder to prove than x+(1+i+skip)*m
/// despite both always being the same

#push-options "--z3rlimit 15 --ifuel 0 --fuel 0 --split_queries always"
let read_tail_fields_fast_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) <= length g })
                     (skip: qword { !skip <= !field_count })
                     (i: qword { !i < (!field_count - !skip) }) 
  : Lemma (requires True)
          (ensures (
            let final_addr : word_aligned_address_for g = header_address +^ machine_word +^ ((i +^ skip) *^ machine_word) in
            let all = read_tail_fields_fast g header_address field_count skip in
              index all !i == read_word_at g final_addr)) =  
  ()

let read_tail_fields_fast_is_correct_2 (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 })
                     (i: qword { !i < (!field_count - !skip) }) 
  : Lemma (requires True)
          (ensures index (read_tail_fields_fast g header_address field_count skip) !i 
                == read_word g ((header_address /^ machine_word) +^ ((1UL +^ skip +^ i)))) = ()

/// To make the comparison complete, let's also check the read_word_at vs read_word,
/// and make sure these are identical proof-wise.
let read_tail_fields_fast_is_correct_3 (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 })
                     (i: qword { !i < (!field_count - !skip) }) 
  : Lemma (requires True)
          (ensures is_valid_word_aligned_address_for (header_address +^ ((1UL +^ skip +^ i) *^ machine_word)) g /\
                   index (read_tail_fields_fast g header_address field_count skip) !i 
                == read_word_at g (header_address +^ ((1UL +^ skip +^ i) *^ machine_word))) = ()
#pop-options
 

let test (x y: qword) : Lemma (requires UInt.size (!x * !y) 64) (ensures x *^ y == y *^ x) = ()

#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
      let after_skip_proven_to_be_address : word_aligned_address_for g = after_skip in 
      read_seq_is_correct g after_skip_proven_to_be_address (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