(* Type of values used in the dynamic semantics of the back-end intermediate
   languages, and the memory model for the whole compiler. Inspired by
   common/Values.ma, adapted from Compcert *)

include "common/Pointers.ma".
include "utilities/hide.ma".

record part (*r: region*): Type[0] ≝
 { part_no:> nat
 ; part_no_ok: part_no < size_pointer (*r*)
 }.

(* Byte-sized values used in the back-end.
   Values larger than a single Byte are represented via their parts.
   Values are either:
  - machine integers (Bytes)
  - parts of a pointer seen as a triple giving the representation of the
    pointer (in terms of the memory regions such a pointer could address),
    a memory address and an integer offset with respect to this address;
  - a null pointer: the region denotes the pointer size
  - the [BVundef] value denoting an arbitrary bit pattern, such as the
    value of an uninitialized variable
  - the [BVnonzero] value denoting an arbitrary but non-zero bit pattern,
    which arise in the RTLabs → RTL pass when translating equality comparisons
    between pointers (which get translated to multiple XORs between pointer
    parts).    
*)

inductive beval: Type[0] ≝
  | BVundef: beval
  | BVnonzero: beval
  | BVByte: Byte → beval
  | BVnull: (*∀r:region.*) part  → beval
  | BVptr: block → ∀p:part.Vector Byte (S p) → beval.

definition eq_beval: beval → beval → bool ≝
 λv1,v2.
  match v1 with
   [ BVundef      ⇒ match v2 with [ BVundef      ⇒ true                           | _ ⇒ false ]
   | BVnonzero    ⇒ match v2 with [ BVnonzero    ⇒ true                           | _ ⇒ false ]
   | BVByte b1    ⇒ match v2 with [ BVByte b2    ⇒ eq_bv … b1 b2                  | _ ⇒ false ]
   | BVnull p1    ⇒ match v2 with [ BVnull p2    ⇒ eqb p1 p2                      | _ ⇒ false ]
   | BVptr b1 p1 o1  ⇒
      match v2 with
      [ BVptr b2 p2 o2  ⇒
        eq_block … b1 b2 ∧ eqb p1 p2 ∧
          (* equivalent to equality if p1 = p2 *)
          vprefix … (eq_bv 8) o1 o2
      | _ ⇒ false
      ]
   ].

include alias "arithmetics/nat.ma".

axiom CorruptedPointer: String.

let rec pointer_of_bevals_aux (b:block) (part: nat) (acc : BitVector (part*8))
  (l: list beval) on l : res pointer ≝
 match l with
  [ nil ⇒
     If eqb part (size_pointer (*ptype p*)) then with prf do
      return mk_pointer b (mk_offset (acc⌈BitVector (part*8)↦?⌉))
     else
      Error … [MSG CorruptedPointer]
  | cons v tl ⇒
     match v with
      [ BVptr b' part' o' ⇒
        let acc' ≝ vflatten … o' in
        if eq_block b b' ∧
           eqb part part' ∧
           vsuffix … eq_b acc acc' then
           pointer_of_bevals_aux b (S part') acc' tl
         else
          Error … [MSG CorruptedPointer]
      | _ ⇒ Error … [MSG CorruptedPointer]
      ]
  ].
  @hide_prf
  >commutative_times_fast
  lapply prf @(eqb_elim part) #H * >H % qed.

(* CSC: use vectors in place of lists? Or even better products of tuples
   (more easily pattern matchable in the finite case)? requires one more parameter *)
definition pointer_of_bevals: list beval → res pointer ≝
 λl.
 match l with
  [ nil ⇒ Error … [MSG CorruptedPointer]
  | cons he tl ⇒
     match he with
      [ BVptr b part o ⇒
         if eqb part 0 then
           pointer_of_bevals_aux b (S part) (vflatten … o) tl
         else Error … [MSG CorruptedPointer]
      | _ ⇒ Error … [MSG CorruptedPointer]
      ]
  ].

(* CSC: use vectors in place of lists? Or even better products of tuples
   (more easily pattern matchable in the finite case)? *)
let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) on n: n + part = size_pointer (*ptype p*) → list beval ≝
 match n with
  [ O ⇒ λ_.[]
  | S m ⇒ λpr': S m + part = ?.
    let postfix ≝ rvsplit … (\snd (vsplit bool (m*8) (S part*8) (offv (poff p) ⌈BitVector ?↦?⌉))) in
    (BVptr (pblock p) (mk_part … part …) postfix)::bevals_of_pointer_aux p (S part) m ?
  ].
@hide_prf
[3: change with (?*?) in match offset_size;
  <pr' >(commutative_times_fast ? 8) >(commutative_times_fast ? 8)
  <distributive_times_plus_fast <plus_n_Sm_fast %
] -postfix
/3 by lt_plus_to_minus_r, lt_plus_to_lt_l/ qed.

definition bevals_of_pointer: pointer → list beval ≝
 λp. bevals_of_pointer_aux p 0 (size_pointer (*ptype p*)) ….
@hide_prf @plus_n_O qed.

lemma pointer_of_bevals_bevals_of_pointer:
 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p.
* #pbl * #voff
whd in match (bevals_of_pointer ?);
@vsplit_elim #pre #post
normalize nodelta
#EQ >EQ
whd in match (bevals_of_pointer_aux ????);
@vsplit_elim #pre' #post'
normalize nodelta
>(Vector_O … pre') #EQ' normalize in EQ'; <EQ' -pre' -post'
whd in ⊢ (??%?);
>eq_block_b_b >eqb_n_n
>vflatten_rvsplit >vflatten_rvsplit
>vsuffix_true
[2: change with (bool_to_Prop (eq_bv ???)) >eq_bv_refl % ]
normalize nodelta %
qed.

(* CSC: move elsewhere *)
(* CSC: Wrong data-type? Use products of products *)
definition list_to_pair: ∀A:Type[0]. ∀l:list A. length … l = 2 → A × A.
 #A #l cases l [2: #a #tl cases tl [2: #b #tl' cases tl' [1: #_ @〈a,b〉 | #c #tl'']]]
 #abs normalize in abs; destruct
qed.

axiom NotATwoBytesPointer: String.

(* Fails if the address is not representable as a pair *)
definition beval_pair_of_pointer: pointer → res (beval × beval) ≝
 λp. OK … (list_to_pair … (bevals_of_pointer p) ?).
(*
 λp. match p with [ mk_pointer pty pbl pok poff ⇒
  match pty with
   [ XData ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer XData pbl pok poff)) ?)
   | Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?)
   | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*)
% qed.

definition beval_pair_of_code_pointer: (Σp:pointer. ptype p = Code) → beval × beval ≝
 λp. list_to_pair ? (bevals_of_pointer p) ?.
(*
 λp. match p return λp. ptype p = Code → ? with [ mk_pointer pty pbl pok poff ⇒
  match pty return λpty. ? → pty = Code → ? with
   [ Code ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer Code pbl ? poff)) ?
   | _ ⇒ λpok'.λabs. ⊥] pok] ?.
[@(pi2 … p) |7: // |8: %] destruct (abs)*) %
qed.


axiom NotACodePointer: String.
definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝
 λp.
  let 〈v1,v2〉 ≝ p in
  do p ← pointer_of_bevals [v1;v2] ;
  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
  [ Code ⇒ λE.OK ? (mk_Sig … p ?)
  | _ ⇒ λ_.Error … [MSG NotACodePointer]] ?.
// qed.

axiom ValueNotABoolean: String.

definition bool_of_beval: beval → res bool ≝
 λv.match v with
  [ BVundef ⇒ Error … [MSG ValueNotABoolean]
  | BVnonzero ⇒ OK … true
  | BVByte b ⇒ OK … (eq_bv … (zero …) b)
  | BVnull y ⇒  OK … false
  | BVptr p q o ⇒ OK ? true ].

definition Byte_of_val: String → beval → res Byte ≝ (*CSC: move elsewhere *)
 λerr,b.match b with
  [ BVByte b ⇒ OK … b
  | _ ⇒ Error … [MSG err]].

axiom NotAnInt32Val: String.
definition Word_of_list_beval: list beval → res int ≝
 λl.
  let first_byte ≝ λl.
   match l with
    [ nil ⇒ Error ? [MSG NotAnInt32Val]
    | cons hd tl ⇒ do b ← Byte_of_val NotAnInt32Val hd ; OK ? 〈b,tl〉 ] in
  do 〈b1,l〉 ← first_byte l ;
  do 〈b2,l〉 ← first_byte l ;
  do 〈b3,l〉 ← first_byte l ;
  do 〈b4,l〉 ← first_byte l ;
   match l with
    [ nil ⇒ OK ? (b4 @@ b3 @@ b2 @@ b1)
    | _ ⇒ Error ? [MSG NotAnInt32Val] ].

inductive bebit : Type[0] ≝
| BBbit : bool → bebit
| BBundef : bebit
| BBptrcarry :
  (* is add *) bool → block → ∀p : part.Vector Byte (S p) → Vector Byte (S p) → bebit.

definition eq_bebit: bebit → bebit → bool ≝
 λv1,v2.
  match v1 with
   [ BBundef      ⇒ match v2 with [ BBundef      ⇒ true                           | _ ⇒ false ]
   | BBbit b1    ⇒ match v2 with [ BBbit b2    ⇒ eq_b b1 b2                  | _ ⇒ false ]
   | BBptrcarry is_add1 b1 p1 o1 by1  ⇒
      match v2 with
      [ BBptrcarry is_add2 b2 p2 o2 by2  ⇒
        eq_b is_add1 is_add2 ∧ eq_block … b1 b2 ∧ eqb p1 p2 ∧
          (* equivalent to equality if p1 = p2 *)
          vprefix … (eq_bv 8) o1 o2 ∧
          vprefix … (eq_bv 8) by1 by2
      | _ ⇒ false
      ]
   ].

definition Bit_of_val: String → bebit → res Bit ≝ (*CSC: move elsewhere *)
 λerr,b.match b with
  [ BBbit b ⇒ OK … b
  | _ ⇒ Error … [MSG err]].