source: src/joint/as_semantics.ma @ 2160

include "joint/semantics_paolo.ma".
include "common/StructuredTraces.ma".

definition stmt_classifier :
  ∀p : params.∀globals.
    (ext_step p → status_class) →
    (ext_fin_stmt p → status_class) →
    joint_statement p globals → status_class
  ≝ λp,globals,ext_step_classifier,ext_fin_step_classifier,s.
  match s with
  [ sequential stp _ ⇒
    match stp with
    [ COND _ _ ⇒ cl_jump
    | extension ext_s ⇒ ext_step_classifier ext_s
    | CALL_ID _ _ _ ⇒ cl_call (* Paolo : this does not take into account external calls! *)
    | _ ⇒ cl_other
    ]
  | final stp ⇒
    match stp with
    [ RETURN ⇒ cl_return
    | extension_fin ext_s ⇒ ext_fin_step_classifier ext_s
    | _ ⇒ cl_other
    ]
  ].

definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
*#p1 #EQ1 * #p2 #EQ2 @eq_pointer_elim
[ #EQ destruct % #H %
| * #NEQ % #ABS destruct elim (NEQ ?) %
]
qed.
  
definition joint_abstract_status :
 ∀p : evaluation_parameters.
 (ext_step p → status_class) →
 (ext_fin_stmt p → status_class) →
 abstract_status ≝ 
 λp,ext_step_cl,ext_fin_step_cl.
 mk_abstract_status
   (* as_status ≝ *) (state_pc p)
   (* as_execute ≝ *) (λs1,s2.eval_state … p (genv2 p) s1 = return s2)
   (* as_pc ≝ *) cpointerDeq
   (* as_pc_of ≝ *) (pc …)
   (* as_classifier ≝ *)
    (λs,cl.∃stmt.fetch_statement ? p … (genv2 p) (pc … s) = return stmt ∧
     stmt_classifier … ext_step_cl ext_fin_step_cl stmt = cl)
   (* as_label_of_pc ≝ *)
    (λpc.
      match fetch_statement ? p … (genv2 p) pc with
      [ OK stmt ⇒
        match stmt with
        [ sequential s _ ⇒
          match s with
          [ COST_LABEL l ⇒ Some ? l
          | _ ⇒ None ?
          ]
        | _ ⇒ None ?
        ]
      | _ ⇒ None ?
      ])
   (* as_after_return ≝ *)
    (λs1,s2. (* Paolo: considering sequential calls, tailcalls are out of the picture for now *)
      ∃stp,nxt.fetch_statement ? p … (genv2 p) (pc … s1) = return (sequential ?? stp nxt) ∧
      succ_pc p p (pc … s1) nxt = return pc … s2)
   (* as_final ≝ *) (λs.is_final (globals ?) p (genv2 p) (exit p) s ≠ None ?).