(* 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".


definition cpointer ≝ Σp.ptype p = Code.
definition xpointer ≝ Σp.ptype p = XData.
unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer 	(λp.ptype p = XData).


(* this is like a code pointer, but with unbounded offset.
   used only in the back-end, they become code pointers in LIN → ASM *)
record program_counter : Type[0] ≝
  { pc_block : Σb : block.block_region b = Code
  ; pc_offset : Pos
  }.

definition eq_program_counter : program_counter → program_counter → bool ≝
λpc1,pc2.eq_block (pc_block pc1) (pc_block pc2) ∧
         eqb (pc_offset pc1) (pc_offset pc2).

lemma eq_program_counter_elim : ∀P:bool→Prop.
  ∀pc1,pc2.(pc1=pc2→P true)→(pc1≠pc2→P false)→P (eq_program_counter pc1 pc2).
#P ** #bl1 #H1 #o1 ** #bl2 #H2 #o2
#Heq #Hneq whd in ⊢ (?%);
@eq_block_elim #EQ1
[ @eqb_elim #EQ2 ]
[ @Heq destruct %
|*: @Hneq % #ABS destruct
  [ @(absurd ?? EQ2) | @(absurd ?? EQ1) ] %
] qed.

lemma reflexive_eq_program_counter : ∀pc.eq_program_counter pc pc = true.
** #bl1 #H1 #o1 whd in ⊢ (??%?); >eq_block_b_b >eqb_n_n % qed.

definition bitvector_from_pos :
  ∀n.Pos → BitVector n ≝
  λn,p.bitvector_of_Z n (Zpred (pos p)).

definition pos_from_bitvector :
  ∀n.BitVector n → Pos ≝
  λn,v.
  match Zsucc (Z_of_unsigned_bitvector n v)
  return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?
  with
  [ OZ ⇒ λprf.⊥
  | pos x ⇒ λ_. x
  | neg x ⇒ λprf.⊥
  ] (refl …).
@hide_prf
elim v in prf;
[2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.

definition cpointer_of_pc : program_counter → option cpointer ≝
  λpc.
  let pc_off ≝ pc_offset pc in
  if leb pc_off (two_power_nat offset_size) then
    return «mk_pointer (pc_block pc) (mk_offset (bitvector_from_pos … pc_off)),?»
  else
    None ?.
elim (pc_block pc) #bl #H @H qed.

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

definition part_from_sig : (Σn:ℕ.n<size_pointer) → part ≝
λn_sig : Σn.n<size_pointer.mk_part n_sig (pi2 … n_sig).

coercion sig_to_part : ∀n_sig:Σn:ℕ.n<size_pointer.part ≝
part_from_sig on _n_sig:Σn.n<size_pointer to part.

(* 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
  - [BVXor] is a formal XOR between (possibly null) pointer parts
  - [BVnonzero] is any nonzero value
*)

inductive beval: Type[0] ≝
  | BVundef: beval
  | BVnonzero: beval
  | BVXor: option pointer → option pointer → part → beval (* option pointer ≈ pointer + null *)
  | BVByte: Byte → beval
  | BVnull: (*∀r:region.*) part  → beval
  | BVptr: pointer → part → beval
  | BVpc: program_counter → part → beval. (* only used in back end, needed to separate
                                      program counters that go in the stack from
                                      function pointers, as they are linked with
                                      different relations in some passes *)

definition eq_bv_suffix : ∀n,m,p.
  BitVector (n + p) → BitVector (m + p) → bool ≝
λn,m,p,v1,v2.
let b1 ≝ \snd (vsplit … v1) in
let b2 ≝ \snd (vsplit … v2) in
eq_bv … b1 b2.

include alias "arithmetics/nat.ma".

(* 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 bv1 tl ⇒
    match tl with
    [ nil ⇒ Error … [MSG CorruptedPointer]
    | cons bv2 tl' ⇒
      match tl' with
      [ cons _ _ ⇒ Error … [MSG CorruptedPointer]
      | nil ⇒
        match bv1 with
        [ BVptr ptr1 p1 ⇒
          match bv2 with
          [ BVptr ptr2 p2 ⇒
            if eqb p1 0 ∧ eqb p2 1 ∧ eq_block (pblock ptr1) (pblock ptr2) ∧
               eq_bv_suffix 8 8 8 (offv (poff ptr1)) (offv (poff ptr2))
            then
              return ptr2
            else Error … [MSG CorruptedPointer]
          | _ ⇒ Error … [MSG CorruptedPointer]
          ]
        | _ ⇒ Error … [MSG CorruptedPointer]
        ]
      ]
    ]
  ].

definition pc_of_bevals: list beval → res program_counter ≝
 λl.
 match l with
  [ nil ⇒ Error … [MSG CorruptedPointer]
  | cons bv1 tl ⇒
    match tl with
    [ nil ⇒ Error … [MSG CorruptedPointer]
    | cons bv2 tl' ⇒
      match tl' with
      [ cons _ _ ⇒ Error … [MSG CorruptedPointer]
      | nil ⇒
        match bv1 with
        [ BVpc ptr1 p1 ⇒
          match bv2 with
          [ BVpc ptr2 p2 ⇒
            if eqb p1 0 ∧ eqb p2 1 ∧ eq_program_counter ptr1 ptr2 then
              return ptr2
            else Error … [MSG CorruptedPointer]
          | _ ⇒ Error … [MSG CorruptedPointer]
          ]
        | _ ⇒ Error … [MSG CorruptedPointer]
        ]
      ]
    ]
  ].

definition bevals_of_pointer ≝
 λp:pointer.
 map ?? (λn_sig.BVptr p (part_from_sig n_sig)) (range_strong size_pointer).

definition bevals_of_pc ≝
 λp:program_counter.
 map ?? (λn_sig.BVpc p (part_from_sig n_sig)) (range_strong size_pointer).

lemma pointer_of_bevals_bevals_of_pointer:
 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p.
#ptr
whd in match (bevals_of_pointer ?);
whd in ⊢ (??%?);
>eq_block_b_b
change with (eq_bv ???) in match (eq_bv_suffix ?????);
>eq_bv_refl %
qed.

lemma pc_of_bevals_bevals_of_pc:
 ∀p. pc_of_bevals (bevals_of_pc p) = OK … p.
#ptr
whd in match (bevals_of_pc ?);
whd in ⊢ (??%?);
>reflexive_eq_program_counter
%
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.

(* Should fail if the address is not representable as a pair
   As we only have 16 bit addresses atm, it never fails *)
definition beval_pair_of_pointer: pointer → (* res *) (beval × beval) ≝
 λp.list_to_pair … (bevals_of_pointer p) (refl …).
(*
 λ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].*)

definition beval_pair_of_pc: program_counter → beval × beval ≝
 λp. list_to_pair ? (bevals_of_pc p) (refl …).

(*
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 E)
  | _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …). *)

definition bool_of_beval: beval → res bool ≝
 λv.match v with
  [ BVundef ⇒ Error … [MSG ValueNotABoolean]
  | BVXor _ _ _ ⇒ Error … [MSG ValueNotABoolean] (* even if in some cases we can
                                                   tell the value, we will always
                                                   call bool_of_beval after a
                                                   series of XORs has been
                                                   completed *)
  | BVpc _ _ ⇒ Error … [MSG ValueNotABoolean] (* we should never test on a pc *)
  | BVByte b ⇒ OK … (¬eq_bv … (zero …) b)
  | BVnull _ ⇒  OK … false
  | _ ⇒ OK ? true
  ].

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

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 add_or_sub : Type[0] ≝
| do_add : add_or_sub
| do_sub : add_or_sub.

definition eq_add_or_sub : add_or_sub → add_or_sub → bool ≝
λx,y.match x with
[ do_add ⇒ match y with [ do_add ⇒ true | _ ⇒ false ]
| do_sub ⇒ match y with [ do_sub ⇒ true | _ ⇒ false ]
].

inductive bebit : Type[0] ≝
| BBbit : bool → bebit
| BBundef : bebit
| BBptrcarry :
  add_or_sub → pointer → ∀p : part.BitVector (8*S p) → bebit.

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

definition eq_option_map : ∀A: Type[0].(A → A → bool) → option A → option A → bool ≝ 
λA,eq,a1,a2.
match a1 with
[ Some x ⇒ match a2 with [Some y ⇒ eq x y | _ ⇒ false ]
| None ⇒ match a2 with [None ⇒ true | _ ⇒ false]
].

lemma eq_option_map_elim : ∀A : Type[0].∀P:bool → Prop.∀eq,
x,y. (∀P:bool → Prop.∀z,w.(z = w → P true) → (z ≠w → P false) → P (eq z w)) → 
(x = y → P true) → (x ≠ y → P false) → P (eq_option_map A eq x y).
#A #P #eq * [|#x] * [1,3:|*: #y] normalize #H #H1 #H2 
[@H1 % |2,3: @H2 % #EQ destruct(EQ)] @H 
[ #EQ @H1 >EQ % 
| * #H3 @H2 % #EQ destruct @H3 %
]
qed.


definition eq_beval : beval → beval → bool ≝ 
λbv1,bv2.
match bv1 with
[ BVundef ⇒ match bv2 with [ BVundef ⇒ true | _ ⇒ false ]
| BVnonzero ⇒ match bv2 with [ BVnonzero ⇒ true | _ ⇒ false ]
| BVXor pt1 pt1' p1 ⇒ 
  match bv2 with 
  [ BVXor pt2 pt2' p2 ⇒ eq_option_map … eq_pointer pt1 pt2 ∧ 
                        eq_option_map … eq_pointer pt1' pt2' ∧ 
                        eqb (part_no … p1) (part_no … p2)
  | _ ⇒ false
  ]
| BVByte b1 ⇒ match bv2 with [ BVByte b2 ⇒ eq_bv … b1 b2 | _ ⇒ false]
| BVnull p1 ⇒ match bv2 with 
              [ BVnull p2 ⇒ eqb (part_no … p1) (part_no … p2) | _ ⇒ false ]
| BVptr ptr1 p1 ⇒ match bv2 with 
                 [ BVptr ptr2 p2 ⇒ eq_pointer ptr1 ptr2 ∧ 
                                   eqb (part_no … p1) (part_no … p2) 
                 | _ ⇒ false 
                 ]
| BVpc pc1 p1 ⇒ match bv2 with 
                [ BVpc pc2 p2 ⇒ eq_program_counter pc1 pc2 ∧ 
                  eqb (part_no … p1) (part_no … p2) 
                | _⇒ false 
                ]
].

lemma eq_beval_elim : ∀P:bool → Prop.∀x,y.
(x = y → P true) → (x ≠ y → P false) → P (eq_beval x y).
#P *
[|| #pt1 #pt1' #p1 | #b1 | #p1 | #ptr1 #p1 | #pc1 #p1 ]
*
[1,8,15,22,29,36,43:
|2,9,16,23,30,37,44:
|3,10,17,24,31,38,45: #pt2 #pt2' #p2
|4,11,18,25,32,39,46: #b2
|5,12,19,26,33,40,47: #p2
|6,13,20,26,34,41,48: #ptr2 #p2
|*: #pc2 #p2
]
normalize nodelta #H1 #H2 try(@H1 %) try(@H2 % #EQ destruct)
whd in match eq_beval; normalize nodelta
[ @eq_option_map_elim 
 [ @eq_pointer_elim 
 |3: * #H whd in match (andb ??); @H2 % #EQ destruct(EQ) @H %
 | normalize nodelta #EQ destruct(EQ) @eq_option_map_elim
 [ @eq_pointer_elim
 |3: * #H whd in match (andb ??); @H2 % #EQ destruct(EQ) @H %
 | #EQ destruct(EQ) cases p1 in H1 H2; -p1 cases p2 -p2
   #p2 #prf #p1 #prf1 #H1 #H2 @eqb_elim
  [ #EQ destruct(EQ) @H1 %
  | * #H @H2 % #EQ destruct(EQ) @H %
  ]
 ]
 ]
| @eq_bv_elim [#EQ destruct(EQ) @H1 % | * #H @H2 % #EQ destruct(EQ) @H %]
| cases p1 in H1 H2; -p1 cases p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim
 [ #EQ destruct(EQ) @H1 %
 | * #H @H2 % #EQ destruct @H %
 ]
| @eq_pointer_elim [2: * #H @H2 % #EQ destruct @H %] #EQ destruct(EQ)
  cases p1 in H1 H2; -p1 cases p2 -p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim
  [#EQ destruct @H1 %
  | * #H @H2 % #EQ destruct @H %
  ]
| @eq_program_counter_elim [2: * #H @H2 % #EQ destruct @H %] #EQ destruct
  cases p1 in H1 H2; -p1 cases p2 -p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim
  [ #EQ destruct @H1 %
  | * #H @H2 % #EQ destruct @H %
  ]
]
qed.