source: src/joint/lineariseProof.ma @ 2446

(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "joint/linearise.ma".
include "common/StatusSimulation.ma".   
include "joint/Traces.ma".
include "joint/SemanticUtils.ma".

definition graph_prog_params:
  ∀p:unserialized_params. 
  (∀F.sem_unserialized_params p F) →
    joint_program (mk_graph_params p) →
   prog_params
 ≝
 λp,p',prog.
  (mk_prog_params
   (make_sem_graph_params (mk_graph_params p) p')
   prog).

definition lin_prog_params:
  ∀p:unserialized_params. 
  (∀F.sem_unserialized_params p F) →
    joint_program (mk_lin_params p) →
   prog_params
 ≝
 λp,p',prog.
  (mk_prog_params
   (make_sem_lin_params (mk_lin_params p) p')
   prog).

(*CSC: Paolo, come to the rescue*)
axiom choose_sigma:
  ∀p:unserialized_params. 
  (∀F.sem_unserialized_params p F) →
    joint_program (mk_graph_params p) →
   identifier LabelTag → option ℕ.

(*CSC: Paolo, come to the rescue*)
axiom linearise_code_spec:
 ∀p : unserialized_params.
 ∀p':(∀F.sem_unserialized_params p F).
 ∀graph_prog:joint_program (mk_graph_params p).
 ∀graph_fun:joint_closed_internal_function (mk_graph_params p)
                           (globals (graph_prog_params p p' graph_prog)).
 let sigma ≝ choose_sigma p p' graph_prog in
 let lin_fun ≝ linearise_int_fun … graph_fun in
 let g ≝ joint_if_code ?? (pi1 … graph_fun) in
 let c ≝ joint_if_code ?? (pi1 … lin_fun) in
 ∀entry : (Σl.bool_to_Prop (code_has_label … g l)).
      code_closed … c ∧
      sigma entry = Some ? 0 ∧
      ∀l,n.sigma l = Some ? n →
        ∃s. lookup … g l = Some ? s ∧
          opt_Exists ?
            (λls.let 〈lopt, ts〉 ≝ ls in
              opt_All ? (eq ? l) lopt ∧
              ts = graph_to_lin_statement … s ∧
              opt_All ?
                (λnext.Or (sigma next = Some ? (S n))
                (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
                (stmt_implicit_label … s)) (nth_opt … n c). 
   
definition graph_abstract_status:
 ∀p:unserialized_params. 
  (∀F.sem_unserialized_params p F) →
    joint_program (mk_graph_params p) →
     abstract_status
 ≝
 λp,p',prog.
  joint_abstract_status (graph_prog_params p p' prog).

definition lin_abstract_status:
 ∀p:unserialized_params. 
  (∀F.sem_unserialized_params p F) →
    joint_program (mk_lin_params p) →
     abstract_status
 ≝
 λp,p',prog.
  joint_abstract_status (lin_prog_params p p' prog).

(*CSC: BUG, the natural must be ≤ 2^16! *)
(*CSC: already defined? *)
definition pointer_of_block_and_lin_offset :
 ∀b:block. block_region b = Code → nat → cpointer ≝
  λb,p,n. «mk_pointer b (mk_offset (bitvector_of_nat … n)), p».

definition well_formed_status:
 ∀p,p',graph_prog.
  ∀sigma: identifier LabelTag → option ℕ. 
  graph_abstract_status p p' graph_prog → Prop
 ≝
 λp,p',graph_prog,sigma,s.
  sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))
   ≠ None ….

definition sigma_pc_of_status:
 ∀p,p',graph_prog.
  ∀sigma: identifier LabelTag → option ℕ.
   ∀s:graph_abstract_status p p' graph_prog.
    well_formed_status … sigma s → ℕ
 ≝
  λp,p',prog,sigma,s.
   match sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))
   return λx. x ≠ None ? → ℕ
   with
   [ None ⇒ λprf.⊥
   | Some n ⇒ λ_.n ].
 @(absurd ?? prf) //
qed.

lemma sigma_pc_of_status_ok:
  ∀p,p',graph_prog.
  ∀sigma: identifier LabelTag → option ℕ.
   ∀s:graph_abstract_status p p' graph_prog.
    ∀prf:well_formed_status … sigma s.
     sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))
     = Some … (sigma_pc_of_status … prf).
 #p #p' #prog #sigma #s whd in ⊢ (% → ?);
 whd in match sigma_pc_of_status; normalize nodelta cases (sigma ?) //
 #abs cases (absurd ?? abs)
qed.

definition linearise_status_fun:
 ∀p,p',graph_prog.
  ∀sigma: identifier LabelTag → option ℕ.
   let lin_prog ≝ linearise ? graph_prog in
    ∀s:graph_abstract_status p p' graph_prog.
     well_formed_status … sigma s →
      lin_abstract_status p p' lin_prog
≝
 λp,p',graph_prog,sigma,s,prf.
  mk_state_pc ??
   (pointer_of_block_and_lin_offset (pblock (pc ? s)) …
    (sigma_pc_of_status … sigma … prf)).
[2: cases (pc ??) * normalize //
| cases daemon (* TODO *) ]
qed.

axiom sigma_pc_commute:
 ∀p,p',graph_prog,s1,prf.
 sigma_pc_of_status p p' graph_prog (choose_sigma p p' graph_prog) s1 prf =
 point_of_pointer (lin_prog_params p p' (linearise p graph_prog))
 (lin_prog_params p p' (linearise p graph_prog))
  (pc (lin_prog_params p p' (linearise p graph_prog))
   (linearise_status_fun p p' graph_prog (choose_sigma p p' graph_prog) s1 prf)).

definition linearise_status_rel:
 ∀p,p',graph_prog.
  ∀sigma: identifier LabelTag → option ℕ.
  let lin_prog ≝ linearise ? graph_prog in
   status_rel
    (graph_abstract_status p p' graph_prog)
    (lin_abstract_status p p' lin_prog)
 ≝ λp,p',graph_prog,sigma.mk_status_rel …
    (λs1,s2.
     ∃prf: well_formed_status … sigma s1.
      s2 = linearise_status_fun p p' graph_prog sigma s1 prf) ….
 cases daemon (* TODO *)
qed.

axiom fetch_function_sigma_commute:
 ∀p,p',graph_prog,sigma,st1.
 ∀prf:well_formed_status ??? sigma st1.
 let lin_prog ≝ linearise ? graph_prog in
  fetch_function
   (lin_prog_params p p' lin_prog)
   (globals (lin_prog_params p p' lin_prog))
   (ev_genv (lin_prog_params p p' lin_prog))
   (pc (lin_prog_params p p' lin_prog)
    (linearise_status_fun p p' graph_prog sigma st1 prf))
 =
  m_map …
   (linearise_int_fun ??)
   (fetch_function
    (graph_prog_params p p' graph_prog)
    (globals (graph_prog_params p p' graph_prog))
    (ev_genv (graph_prog_params p p' graph_prog))
    (pc (graph_prog_params p p' graph_prog) st1)).

lemma stm_at_sigma_commute:
 ∀p,p',graph_prog,graph_fun,s1.
 let lin_prog ≝ linearise ? graph_prog in
 let sigma ≝ choose_sigma p p' graph_prog in
 ∀prf:well_formed_status ??? sigma s1.
  stmt_at (lin_prog_params p p' (linearise p graph_prog))
   (globals (lin_prog_params p p' (linearise p graph_prog)))
   (joint_if_code (lin_prog_params p p' (linearise p graph_prog))
    (globals (lin_prog_params p p' (linearise p graph_prog)))
    (linearise_int_fun p (globals (graph_prog_params p p' graph_prog)) graph_fun))
   (point_of_pointer (lin_prog_params p p' (linearise p graph_prog))
    (lin_prog_params p p' (linearise p graph_prog))
    (pc (lin_prog_params p p' (linearise p graph_prog))
     (linearise_status_fun p p' graph_prog sigma s1 prf)))
 =
  option_map …
   (graph_to_lin_statement …)
   (stmt_at (graph_prog_params p p' graph_prog)
    (globals (graph_prog_params p p' graph_prog))
    (joint_if_code (graph_prog_params p p' graph_prog)
     (globals (graph_prog_params p p' graph_prog)) graph_fun)
    (point_of_pointer (graph_prog_params p p' graph_prog)
     (graph_prog_params p p' graph_prog)
     (pc (graph_prog_params p p' graph_prog) s1))).
 #p #p' #graph_prog #graph_fun #s1 #prf
 whd in match (stmt_at ????);
 whd in match (stmt_at ????);
 cases (linearise_code_spec … p' graph_prog graph_fun
         (joint_if_entry … graph_fun))
 * #lin_code_closed #sigma_entry_is_zero #sigma_spec
 lapply (sigma_spec
         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1)))
 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ]
 -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok
 whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec;
 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_
 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
 <sigma_pc_commute >lin_lookup_ok //
qed.

lemma fetch_statement_sigma_commute:
 ∀p,p',graph_prog,st1.
 let sigma ≝ choose_sigma p p' graph_prog in
 let lin_prog ≝ linearise ? graph_prog in
 ∀prf.
  fetch_statement
   (lin_prog_params p p' lin_prog)
   (lin_prog_params p p' lin_prog)
   (globals (lin_prog_params p p' lin_prog))
   (ev_genv (lin_prog_params p p' lin_prog))
   (pc (lin_prog_params p p' lin_prog)
    (linearise_status_fun p p' graph_prog sigma st1 prf))
 =
  m_map …
   (λfun_stm.
     let 〈fun,stm〉 ≝ fun_stm in
      〈linearise_int_fun ?? fun, graph_to_lin_statement ?? stm〉)
   (fetch_statement
    (graph_prog_params p p' graph_prog)
    (graph_prog_params p p' graph_prog)
    (globals (graph_prog_params p p' graph_prog))
    (ev_genv (graph_prog_params p p' graph_prog))
    (pc (graph_prog_params p p' graph_prog) st1)).
 #p #p' #graph_prog #s1 #prf
 whd in match fetch_statement; normalize nodelta
 >fetch_function_sigma_commute
 cases (fetch_function ????) [2://]
 #graph_fun whd in ⊢ (??%%);
 whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?]));
 >stm_at_sigma_commute cases (stmt_at ????) //
qed.

lemma linearise_ok:
 ∀p,p',graph_prog.
  let lin_prog ≝ linearise ? graph_prog in
   status_simulation
    (graph_abstract_status p p' graph_prog)
    (lin_abstract_status p p' lin_prog) ≝
 λp,p',graph_prog.
  let sigma ≝ choose_sigma p p' graph_prog in
   mk_status_simulation … (linearise_status_rel p p' graph_prog sigma) ….
#st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl
cases cl in classified_st1_cl; -cl #classified_st1_cl whd
[4:
 cases rel_st1_st2 -rel_st1_st2 #wf_st1 #rel_st1_st2 >rel_st1_st2 -st2
 whd in move_st1_st1';
 letin lin_prog ≝ (linearise ? graph_prog)
 letin st2' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) …
               (ev_genv (lin_prog_params p p' lin_prog))
               (linearise_status_fun … sigma st1 wf_st1))
 whd in st2';
 whd in match (fetch_statement ?????) in st2';
 >fetch_function_sigma_commute in st2';
 whd in match (fetch_function ????) in st2';
 XXX
 check fetch_statement
 CSC
 %{}

whd in classified_st1_cl;
whd in classified_st1_cl:(??%?);
inversion (fetch_statement ?????) in classified_st1_cl;

<classified_st1_cl -cl 
whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ] ?);
inversion (fetch_statement ?????)

inversion (fetch_statement ?????)
qed.