Newer version of address shift properties

Sheera.fst

module Sheera

open FStar.Seq
open FStar.Seq.Base

open FStar.IntegerIntervals

open FStar.Mul

//Name Your Variables Properly!

module U64 = FStar.UInt64
module U8 = FStar.UInt8
module U32 = FStar.UInt32

unfold let bytes_in_word = 8UL
unfold let bytes_in_heap = 1024UL

open FStar.UInt64

let ulong = UInt64.t

let (!) (x: ulong) : int = UInt64.v x 

type aligned_address = h:ulong { h <^ bytes_in_heap /\ rem h bytes_in_word == 0UL }

let previous_address (address: aligned_address) 
  : Pure aligned_address 
         (requires !address > 0) 
         (ensures fun result -> !result == (!address - !bytes_in_word))
  = address -^ bytes_in_word
  
let next_address (address: aligned_address)
  : Pure aligned_address
         (requires !address + !bytes_in_word < !bytes_in_heap)
         (ensures fun result -> !result == (!address + !bytes_in_word))
  = address +^ bytes_in_word


let next_of_previous_is_id (address: aligned_address)
  : Lemma (requires !address > 0)
          (ensures next_address (previous_address address) == address) = ()
          
let previous_of_next_is_id (address: aligned_address)
  : Lemma (requires !address + !bytes_in_word < !bytes_in_heap)
          (ensures previous_address (next_address address) == address) = ()

let rec is_set (l: seq ulong) : Tot (bool) (decreases length l)
  = if length l = 0 then true else not(mem (head l) (tail l)) && is_set (tail l)
 
let can_be_shifted_forward (f: seq aligned_address)
  = forall x. mem x f ==> !x + !bytes_in_word < !bytes_in_heap

let can_be_shifted_backward (f: seq aligned_address)
  = forall x. mem x f ==> !x > 0

let rec shift_addresses_forward (addresses: seq aligned_address)
  : Pure (seq aligned_address) 
         (requires forall x. mem x addresses ==> !x + !bytes_in_word < !bytes_in_heap)
         (ensures fun result -> length result == length addresses /\ 
                             can_be_shifted_backward result /\
                             (forall (i: under (length result)). 
                                index result i == next_address (index addresses i)))
         (decreases length addresses) =
  if length addresses = 0 then empty else  
  let result_head = next_address (head addresses) in 
  let result_tail = shift_addresses_forward (tail addresses) in
  let result = cons result_head result_tail in    
  let aux (x:aligned_address{mem x result}) : Lemma (!x > 0) = 
    let _ = index_mem x result in ()
    in Classical.forall_intro aux; 
  result 

let rec shift_addresses_backward (addresses: seq aligned_address)
  : Pure (seq aligned_address) 
         (requires forall x. mem x addresses ==> !x > 0)
         (ensures fun result -> length result == length addresses /\ 
                             can_be_shifted_forward result /\
                             (forall (i: under (length result)). 
                                index result i == previous_address (index addresses i)))
         (decreases length addresses) =
  if length addresses = 0 then empty else  
  let result_head = previous_address (head addresses) in 
  let result_tail = shift_addresses_backward (tail addresses) in
  let result = cons result_head result_tail in    
  let aux (x:aligned_address{mem x result}) : Lemma (!x + !bytes_in_word < !bytes_in_heap) = 
    let _ = index_mem x result in ()
    in Classical.forall_intro aux; 
  result

let shift_addresses_forward_tail (addresses: seq aligned_address)
  : Lemma (requires length addresses > 0 /\ can_be_shifted_forward addresses) 
          (ensures shift_addresses_forward (tail addresses) == tail (shift_addresses_forward addresses))
          (decreases length addresses)
  = shift_addresses_forward (tail addresses) `lemma_eq_elim` tail (shift_addresses_forward addresses) 
  
let shift_addresses_backward_tail (addresses: seq aligned_address)
  : Lemma (requires length addresses > 0 /\ can_be_shifted_backward addresses) 
          (ensures shift_addresses_backward (tail addresses) == tail (shift_addresses_backward addresses))
          (decreases length addresses)
  = shift_addresses_backward (tail addresses) `lemma_eq_elim` tail (shift_addresses_backward addresses) 
   

let rec backward_of_forward_is_id (f: seq aligned_address)
  : Lemma (requires forall x. mem x f ==> !x + !bytes_in_word < !bytes_in_heap)
          (ensures (shift_addresses_backward (shift_addresses_forward f) == f))
          (decreases length f) = 
  let g = shift_addresses_backward (shift_addresses_forward f) in 
  if length f = 0 then lemma_eq_elim f g
  else begin
    backward_of_forward_is_id (tail f);
    assert (equal g f)
  end 
   
let rec forward_of_backward_is_id (f: seq aligned_address)
  : Lemma (requires forall x. mem x f ==> !x > 0)
          (ensures (shift_addresses_forward (shift_addresses_backward f) == f))
          (decreases length f) = 
  let g =  shift_addresses_forward(shift_addresses_backward f) in  
  if length f = 0 then lemma_eq_elim f g
  else begin
    forward_of_backward_is_id (tail f);  
    shift_addresses_backward_tail f; 
    shift_addresses_forward_tail (shift_addresses_backward f); 
    next_of_previous_is_id (head f) 
  end