source: src/joint/semanticsUtils_paolo.ma @ 1948

include "joint/semantics_paolo.ma".
include alias "common/Identifiers.ma".

(*** Store/retrieve on pseudo-registers ***)

axiom BadRegister : String.

definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.

definition reg_retrieve : register_env beval → register → res beval ≝
 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).

(*** Store/retrieve on hardware registers ***)

definition init_hw_register_env: address → hw_register_env ≝
 λaddr.
  let 〈dpl,dph〉 ≝ addr in
  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
   hwreg_store RegisterDPL dpl env.

(******************************** GRAPHS **************************************)

definition graph_pointer_of_label : cpointer → label → res cpointer ≝
  λoldpc,l.
  return (mk_pointer Code
   (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))) : cpointer). 
% qed.

definition graph_label_of_pointer: pointer → res label ≝
 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).

definition graph_fetch_statement:
 ∀pars : graph_params.
 ∀sem_pars : sem_state_params.
 ∀globals.
  genv globals pars →
  cpointer →
  res (joint_statement pars globals) ≝
 λpars,sem_pars,globals,ge,p.
  do f ← fetch_function … ge p ;
  do l ← graph_label_of_pointer p;
  opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).

definition make_sem_graph_params :
  ∀pars : graph_params.
  ∀g_pars : more_sem_genv_params pars.
  sem_params ≝
  λpars,g_pars.
  mk_sem_params
    pars
    (mk_more_sem_params
      pars
      g_pars
      graph_pointer_of_label
      (λ_.λ_.graph_pointer_of_label)
      (graph_fetch_statement ? g_pars)
    ).
    
(******************************** LINEAR **************************************)
check mk_pointer
definition lin_succ_p: cpointer → unit → res cpointer :=
 λptr.λ_.return «mk_pointer Code (pblock ptr) ? (mk_offset (offv (poff ptr) + 1)), ?».
[%| cases ptr //] qed.

axiom BadLabel: String.

definition lin_pointer_of_label:
 ∀pars : lin_params.
 ∀globals. genv globals pars → cpointer → label → res cpointer ≝
 λpars,globals,ge,old,l.
  do fn ← fetch_function … ge old ;
  do pos ←
   opt_to_res ? [MSG BadLabel]
    (position_of ?
      (λs. let 〈l',x〉 ≝ s in
        match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false])
     (joint_if_code … pars fn)) ;
  OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
% qed.

definition lin_fetch_statement:
 ∀pars : lin_params.
 ∀sem_pars : sem_state_params.
 ∀globals.
 genv globals pars → cpointer → res (joint_statement pars globals) ≝
 λpars,sem_pars,globals,ge,ppc.
  do fn ← fetch_function … ge ppc ;
  let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)
  do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ;
  return (\snd found).

definition make_sem_lin_params :
  ∀pars : lin_params.
  ∀g_pars : more_sem_genv_params pars.
  sem_params ≝
  λpars,g_pars.
  mk_sem_params
    pars
    (mk_more_sem_params
      pars
      g_pars
      lin_succ_p
      (lin_pointer_of_label ?)
      (lin_fetch_statement ? g_pars)
    ).
    
definition step_unbranching : ∀p,globals.joint_step p globals → bool ≝
  λp,globals,stp.match stp with
  [ COND _ _ ⇒ false
  | CALL_ID _ _ _ ⇒ false
  | extension c' ⇒ (* FIXME: does not care about calling extensions!! *)
    match ext_step_labels … c' with
    [ nil ⇒ true
    | _ ⇒ false
    ]
  | _ ⇒ true
  ].

definition is_not_seq : ∀p,globals.joint_statement p globals → bool ≝
  λp,globals,stp.match stp with
  [ sequential _ _ ⇒ false
  | _ ⇒ true
  ].

inductive s_block (p : params) (globals : list ident) : Type[0] ≝
  | Skip : s_block p globals
  | FinStep : (Σs.bool_to_Prop (¬step_unbranching p globals s)) → s_block p globals
  | FinStmt : (Σs.bool_to_Prop (is_not_seq p globals s)) → s_block p globals
  | Cons : (Σs.bool_to_Prop (step_unbranching p globals s)) → s_block p globals → s_block p globals.

include "utilities/bind_new.ma".

definition Block ≝ λp : params.λglobals.bind_new (localsT p) (s_block p globals).

definition Bcons ≝ λp : params.λglobals.
    λs : Σs.bool_to_Prop (step_unbranching p globals s).
    λB : Block p globals.
    ! b ← B ; return Cons ?? s b.

interpretation "block cons" 'vcons hd tl = (Bcons ??? hd tl).

let rec is_unbranching p globals (b1 : s_block p globals) on b1 : bool ≝
  match b1 with
  [ Skip ⇒ true
  | FinStep _ ⇒ false
  | FinStmt _ ⇒ false
  | Cons _ tl ⇒ is_unbranching ?? tl
  ].

let rec Is_unbranching p globals (b1 : Block p globals) on b1 : Prop ≝
  match b1 with
  [ bret b ⇒ bool_to_Prop (is_unbranching … b)
  | bnew f ⇒ ∀x.Is_unbranching … (f x)
  ].

let rec s_block_append_aux p globals (b1 : s_block p globals) (b2 : s_block p globals) on b1 : is_unbranching … b1 → s_block p globals ≝
  match b1 return λx.is_unbranching ?? x → ? with
  [ Skip ⇒ λ_.b2
  | Cons x tl ⇒ λprf.Cons ?? x (s_block_append_aux ?? tl b2 prf)
  | _ ⇒ Ⓧ
  ].

definition s_block_append ≝
  λp,globals.λb1 : Σb.bool_to_Prop (is_unbranching … b).λb2.
  match b1 with
  [ mk_Sig b1 prf ⇒ s_block_append_aux p globals b1 b2 prf ].

definition Is_to_is_unbr : ∀p,globals.(ΣB.Is_unbranching p globals B) →
  bind_new (localsT p) (Σb.bool_to_Prop (is_unbranching p globals b)) ≝
  λp,globals. ?.
* #b elim b -b
[ #b #H @bret @b @H
| #f #IH #H @bnew #x @(IH x) @H
]
qed.

lemma Is_to_is_unbr_OK : ∀p,globals,B.! b ← Is_to_is_unbr p globals B ; return pi1 … b = pi1 … B.
#p #globals * #b elim b
[ //
| #f #IH #H @bnew_proper
  #x @IH
]
qed.
  
definition Block_append ≝
  λp,globals.λB : Σb.Is_unbranching … b.λB'.
  ! b1 ← Is_to_is_unbr … B;
  ! b2 ← B';
  return s_block_append p globals b1 b2.

definition all_unbranching ≝ λp,globals.All ? (λs.bool_to_Prop (step_unbranching p globals s)).

let rec step_list_to_s_block (p : params) globals (l : list (joint_step p globals)) on l :
    s_block p globals ≝
  match l  with
  [ nil ⇒ Skip ??
  | cons hd tl ⇒
    If step_unbranching … hd then with prf do
      Cons ?? hd (step_list_to_s_block ?? tl)
    else with prf do
      FinStep ?? hd
  ]. [assumption | >prf % ] qed.
  
definition step_list_to_block : ∀R,p,g.? → Block R p g ≝
  λR,p,globals,l.bret R ? (step_list_to_s_block p globals l).

record sem_rel (p1 : sem_params) (p2 : sem_params) (globals : list ident) : Type[0] ≝
  { function_rel : joint_function globals p1 → joint_function globals p2 → Prop
  ; genv_rel : genv globals p1 → genv globals p2 → Prop
  ; pc_rel : cpointer → cpointer → Prop
  ; st_rel : state p1 → state p2 → Prop
  ; stmt_rel : joint_statement p1 globals → Block 
  (* TODO: state what do we need of genv_rel (like finding the same symbols and what relation to above rels ) *)
  ; st_to_pc_rel : ∀st1,st2.st_rel st1 st2 → pc_rel (pc ? st1) (pc ? st2)
  }.
  
(* move *)
definition beval_pair_of_xdata_pointer: (Σp:pointer. ptype p = XData) → beval × beval ≝
 λp. match p return λp. ptype p = XData → ? with [ mk_pointer pty pbl pok poff ⇒
  match pty return λpty. ? → pty = XData → ? with
   [ XData ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer XData pbl ? poff)) ?
   | _ ⇒ λpok'.λabs. ⊥] pok] ?.
[@(pi2 … p) |6: // |7: %] destruct (abs)
qed.

definition safe_address_of_xdata_pointer: (Σp:pointer. ptype p = XData) → safe_address ≝ beval_pair_of_xdata_pointer.
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 ? z) H o,I»}
% [2,4: % [2,4: % [1,3: % [1,3: % ]] % |*:]|*:]
qed.

definition state_rel : ∀p1,p2.∀R : sem_rel p1 p2.good_state p1 → good_state p2 → Prop ≝
  λp1,p2,R,st1,st2.
    frames_rel p1 p2 R (st_frms … st1) (st_frms … st2) ∧
    pc_rel p1 p2 R (pc … st1) (pc … st2) ∧
    sp_rel p1 p2 R
      (safe_address_of_xdata_pointer (sp … st1))
      (safe_address_of_xdata_pointer (sp … st2)) ∧
    isp_rel p1 p2 R
      (safe_address_of_xdata_pointer (isp … st1))
      (safe_address_of_xdata_pointer (isp … st2)) ∧
    sp_rel p1 p2 R
      (safe_address_of_xdata_pointer (sp … st1))
      (safe_address_of_xdata_pointer (sp … st2)) ∧
    carry … st1 = carry … st2 ∧
    regs_rel p1 p2 R (regs … st1) (regs … st2) ∧
    mem_rel p1 p2 R (m … st1) (m … st2).
elim st1 -st1 #st1 ** #good_pc1 #good_sp1 #good_isp1
elim st2 -st2 #st2 ** #good_pc2 #good_sp2 #good_isp2
assumption
qed.
 elim st2
-st1 -st2 #st2 ** #good_pc2 # ∧
    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
    frames_rel … R (st_frms … st1) (st_frms … st2) ∧