Backward-forward shift is identity on applicable domain

ShiftProperties.fst

module ShiftProperties

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 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)


/// f_address_seq_of_f = empty, if f is empty
///                    = Seq.cons f_address (Seq.head f) (f_address_seq_of_f (Seq.tail f))
///
/// f_address_seq_of_f_rev = empty if f is empty
///                        = Seq.cons hd_address (Seq.head f) (f_address_seq_of_f_rev (Seq.tail f))
/// --------------------------------------------------------------------------------------------------------------------------------------------------------

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 shift_addresses_forward (f: seq aligned_address)
  : Pure (seq aligned_address) 
         (requires forall x. mem x f ==> !x + !bytes_in_word < !bytes_in_heap)
         (ensures fun g -> length g == length f /\ can_be_shifted_backward g) =
  let g = init (length f) (fun i -> next_address (index f i)) in
  let aux (x: aligned_address{mem x g}) : Lemma (!x > 0) = 
    let _ = index_mem x g in () 
    in Classical.forall_intro aux;
  g
   
let shift_addresses_backward (f: seq aligned_address)
  : Pure (seq aligned_address) 
         (requires forall x. mem x f ==> !x > 0)
         (ensures fun g -> length g == length f /\ can_be_shifted_forward g) = 
  let g = init (length f) (fun i -> previous_address (index f i)) in
  let aux (x: aligned_address{mem x g}) : Lemma (!x + !bytes_in_word < !bytes_in_heap) = 
    let _ = index_mem x g in () 
    in Classical.forall_intro aux;
  g
  
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 = init (length f) (fun i -> previous_address (next_address (index f i))) in
  lemma_eq_elim g (shift_addresses_backward(shift_addresses_forward f));
  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 = init (length f) (fun i -> next_address (previous_address (index f i))) in
  lemma_eq_elim g (shift_addresses_forward(shift_addresses_backward f));  
  if length f = 0 then lemma_eq_elim f g
  else begin
    forward_of_backward_is_id (tail f);
    assert (equal g f)
  end