Asserted read/write over F* sequences

ArrayTest.fst

module ArrayTest

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

let block_size = 1024

let word_size = 8

let read_word (byte_array: FStar.Endianness.bytes{Seq.Base.length byte_array = block_size}) 
              (index: nat{index < (block_size / word_size)}) =  
  let byte_index = index * word_size in
  let word_array = slice byte_array byte_index (byte_index + word_size) in
  uint64_of_le word_array

let replace_range (source: bytes) 
                  (start_index: under (length source)) 
                  (replacement: bytes) 
  : Pure bytes (requires length replacement <= length source - start_index) 
               (ensures fun result -> length result == length source /\ 
                        (forall (i: under (length source)). 
                          index result i == (
                            if i >= start_index && i < start_index + (length replacement) 
                            then (index replacement (i-start_index)) 
                            else index source i))) =
  let before_start = slice source 0 start_index in
  let after_end = slice source (start_index + (length replacement)) (length source) in
  append before_start (append replacement after_end)
 
let write_word (byte_array: bytes{Seq.Base.length byte_array = block_size})
               (word_index: nat{word_index < (block_size/word_size)})
               (value: UInt64.t)
  : Pure (result: bytes{length result == length byte_array}) 
    (requires True)
    (ensures fun r -> read_word r word_index == value) =  
  let byte_index = word_index * word_size in
  let bytes = FStar.Endianness.le_of_uint64 value in
  let result = replace_range byte_array byte_index bytes in
  lemma_eq_elim (slice result byte_index (byte_index+word_size)) bytes; 
  result
  
let read_and_write_are_valid (byte_array: bytes {length byte_array = block_size})
                             (word_index: under (block_size / word_size))
                             (value: UInt64.t)
  : Lemma (read_word (write_word byte_array word_index value) word_index == value) = ()