(* Memory model used in the dynamic semantics of the back-end intermediate
   languages. Inspired by common/Mem.ma, adapted from Compcert *)

(* * This file develops the memory model that is used in the dynamic
  semantics of all the languages used in the compiler.
  It defines a type [mem] of memory states, the following 4 basic
  operations over memory states, and their properties:
- [load]: read a memory chunk at a given address;
- [store]: store a memory chunk at a given address;
- [alloc]: allocate a fresh memory block;
- [free]: invalidate a memory block.
*)

include "common/ByteValues.ma".
include "common/GenMem.ma".

definition bemem ≝ mem.

definition is_addressable : region → bool ≝ λr.match r with
  [ XData ⇒ true | Code ⇒ true | _ ⇒ false ].

definition is_address : (beval × beval) → Prop ≝ λa.
  ∃b : Σb.bool_to_Prop (is_addressable (block_region b)).
  ∃p0,p1,o0,o1.
    \fst a = BVptr b p0 o0 ∧ part_no … p0 = 0 ∧
    \snd a = BVptr b p1 o1 ∧ part_no … p1 = 1 ∧
    bool_to_Prop (vsuffix … (eq_bv 8) o0 o1).

(*
definition is_addressb : (beval × beval) → bool ≝ λa.
  let 〈a0,a1〉 ≝ a in
  match a0 with
  [ BVptr b0 part0 o0 ⇒
      is_addressable (block_region b0) ∧ eqb part0 0 ∧
        match a1 with
        [ BVptr b1 part1 o1 ⇒
          eq_block b0 b1 ∧ eqb part1 1 ∧ subvector_with … (eq_bv 8) o0 o1
        | _ ⇒ false
        ]
  | _ ⇒ false
  ].

lemma is_addressb_elim : ∀P : bool → Prop.∀a : beval × beval.
  (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a).
#P * * [||#b0|(*#r0*)#part0|#b0#part0#o0] #a1
[5: whd in match is_addressb; normalize nodelta
  elim (true_or_false_Prop (is_addressable (block_region b0)))
  #H >H
  [ @(eqb_elim part0 0) #Heq
    [ cases a1 [||#b1|(*#r1*)#part1|#b1#part1#o1] whd in match (?∧?);
      [5: @eq_block_elim #Heq'
        [ @(eqb_elim part1 1) #Heq''
          [ elim (true_or_false_Prop (subvector_with … (eq_bv 8) o0 o1)) #Heq''' >Heq'''
            [ #Ptrue #_ @Ptrue destruct
              %{b1} [assumption] %{part0} %{part1} %{o0} %{o1}
              % [ % [ % [ % ]]] try assumption %
            ]
          ]
        ]
      ]
    ]
  ]
]
#_ #Pfalse @Pfalse % ** #b0' #H' * #part0' * #part1' * #o0' * #o1' ****
#H0 #H1 #H2 #H3 #H4 destruct /2 by absurd/
qed.
*)

(* CSC: only pointers to XRAM or code memory ATM *)
definition address ≝ beval × beval.

(* definition safe_address ≝ Sig address is_address.
unification hint 0 ≔ ;
P ≟ Prod beval beval
(*------------------*)⊢
safe_address ≡ Sig P is_address. *)

definition eq_address: address → address → bool ≝
 λaddr1,addr2.
  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).

definition pointer_of_address: address → res pointer ≝
 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].

lemma bevals_of_pointer_is_address :
  ∀p.is_address (list_to_pair … (bevals_of_pointer p) (refl …)).
* #b * #o whd in ⊢ (?%); whd
%{b} [ elim (block_region b) % ] %{(mk_part 0 ?)} [ %2 %1 ] %{(mk_part 1 ?)} [ %1 ]
@(vsplit_elim … 8 8 o) #o1 #o0 #EQ >EQ -o
%{[[o0]]} %{[[o1;o0]]}
% [2: change with (bool_to_Prop (if eq_bv ??? then ? else ?))
      >eq_bv_refl % ]
%%[2: normalize nodelta @vsplit_elim #pre >(Vector_O … pre) #post #EQ
      normalize in EQ; <EQ -pre -post
      whd in match (rvsplit ????);
      <(vsplit_prod … (refl …)) normalize nodelta
  | % [2: % ]
  ]
whd in match (rvsplit ????);
try <(vector_append_empty … o0) in ⊢ (??%?);
<(vsplit_prod … (refl …)) normalize nodelta %
qed.

lemma is_address_to_pointer : ∀a.is_address a → ∃p.pointer_of_address a = return p.
* #a0 #a1 ** #bl #bl_prf ** #p0 #p0_prf ** #p1 #p1_prf * #o0' * #o1o0 ****
#EQ1 #EQ2 #EQ3 #EQ4 destruct
@(Vector_pair_elim … o1o0) #o1 #o0 #EQ >EQ -o1o0
@(Vector_singl_elim … o0') #o0'' #EQ >EQ -o0'
whd in ⊢ (?%→?);
@eq_bv_elim #EQ * >EQ -o0''
whd in match (pointer_of_address ?);
>eq_block_b_b >(eqb_n_n 1)
>vsuffix_vflatten
[2: change with (bool_to_Prop (vsuffix ????? ([[?]]@@[[?]])))
  @vsuffix_true change with (bool_to_Prop (if eq_bv ? o0 o0 then ? else ?))
  >eq_bv_refl % ]
normalize nodelta
whd in ⊢ (??(λ_.??%?));
% [2: % |]
qed.

(* For full 8051 memory spaces 
definition pointer_compat' ≝ λb,r.
  match b with
  [ mk_block r' z ⇒
    if eq_region r' r then True
    else
      match r with
      [ Any ⇒ True
      | XData ⇒ match r' with
        [ PData ⇒ True
        | _ ⇒ False
        ]
      | _ ⇒ False
      ]
   ].

lemma pointer_compat_to_ind : ∀b,r.pointer_compat' b r → pointer_compat b r.
** #z ** //
qed.

lemma pointer_compat_from_ind : ∀b,r.pointer_compat b r → pointer_compat' b r.
#b #r #H inversion H
[ #s #id #EQ1 #EQ2 #EQ3 whd >reflexive_eq_region %
| #id #EQ1 #EQ2 #EQ3 %
| #r #id #EQ1 #EQ2 #EQ3 whd @eq_region_elim #EQ4 destruct(EQ4) %
]
qed.
*)
(*lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
** #a0 #a1 ***** #z #o
#Hr
(*
** #a0 #a1 ***** #r #z #Hr #o * lapply (pointer_compat_from_ind ?? Hr)
cases r in Hr ⊢ %; #Hr *
*)
** #part0 #H0 ** #part1 #H1 *** #EQa0 #EQpart0 #EQa1 #EQpart1
destruct normalize
@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
change with (eq_bv ???) in match (eq_v ?????);
@eq_bv_elim [2,4,6: * #ABS elim (ABS (refl …))]
#_ #_ normalize %
qed.*)
    
definition address_of_pointer : pointer → res address ≝ beval_pair_of_pointer.

example address_of_pointer_OK_to_safe :
  ∀p,a.address_of_pointer p = OK … a → is_address a.
#p #a whd in match address_of_pointer; normalize nodelta
#EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
//
qed.

(*definition safe_address_of_pointer: pointer → res safe_address ≝ λp.
  do a as EQ ← address_of_pointer p ; return «a ,address_of_pointer_OK_to_safe ?? EQ».

lemma address_of_pointer_is_safe :
  ∀p.address_of_pointer p = ! a ← safe_address_of_pointer p ; return (a : address).
#p normalize % qed.
(*
****#z #H
lapply (pointer_compat_from_ind ?? H) * #o
normalize %
qed.*)

definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝
code_pointer_of_beval_pair.

definition address_of_code_pointer: (Σp:pointer. ptype p = Code) → address ≝ beval_pair_of_code_pointer.

definition safe_address_of_code_pointer: (Σp:pointer. ptype p = Code) → safe_address ≝ address_of_code_pointer.
cases H -H * #b #o normalize cases b * #z #EQ destruct
%{«mk_pointer  (mk_block Code z)  o,I»}
% [2: % [2: % [ % [ % ]]]] %
qed.
(*
cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
%{«mk_pointer ? (mk_block Code z) H o,I»}
% [2: % [2: % [ % [ % ]] % |]|]
qed.*)
*)

(* Paolo: why only code pointers and not XRAM too? *)
(*definition addr_add: address → nat → res address ≝
 λaddr,n.
  do ptr ← code_pointer_of_address addr ;
  OK … (address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
normalize cases ptr #p #E @E
qed.

definition safe_addr_add: safe_address → nat → res safe_address ≝
 λaddr,n.
  do ptr ← code_pointer_of_address addr ;
  OK … (safe_address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
normalize cases ptr #p #E @E
qed.

definition addr_sub: address → nat → res address ≝
 λaddr,n.
  do ptr ← code_pointer_of_address addr ;
  OK … (address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
normalize cases ptr #p #E @E
qed.

definition safe_addr_sub: safe_address → nat → res safe_address ≝
 λaddr,n.
  do ptr ← code_pointer_of_address addr ;
  OK … (safe_address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
normalize cases ptr #p #E @E
qed.
*)