source: src/joint/as_semantics.ma @ 2125

Last change on this file since 2125 was 1976, checked in by tranquil, 8 years ago
  • monads: just changed some defs, which had to be propagated in some files
  • ASM/CostProof.ma: linked cost as defined there to the one in StructuredTraces? that uses fold
  • added a library for permutations of lists (useful with fold AC ops on lists)
  • first draft of abstract_status implementation for joint languages (file joint/as_semantics.ma)
File size: 2.1 KB
Line 
1include "joint/semantics_paolo.ma".
2include "common/StructuredTraces.ma".
3
4definition stmt_classifier :
5  ∀p : params.∀globals.
6    (ext_step p → status_class) →
7    (ext_fin_stmt p → status_class) →
8    joint_statement p globals → status_class
9  ≝ λp,globals,ext_step_classifier,ext_fin_step_classifier,s.
10  match s with
11  [ sequential stp _ ⇒
12    match stp with
13    [ COND _ _ ⇒ cl_jump
14    | extension ext_s ⇒ ext_step_classifier ext_s
15    | CALL_ID _ _ _ ⇒ cl_call (* Paolo : this does not take into account external calls! *)
16    | _ ⇒ cl_other
17    ]
18  | final stp ⇒
19    match stp with
20    [ RETURN ⇒ cl_return
21    | extension_fin ext_s ⇒ ext_fin_step_classifier ext_s
22    | _ ⇒ cl_other
23    ]
24  ].
25
26definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
27*#p1 #EQ1 * #p2 #EQ2 @eq_pointer_elim
28[ #EQ destruct % #H %
29| * #NEQ % #ABS destruct elim (NEQ ?) %
30]
31qed.
32 
33definition joint_abstract_status :
34 ∀p : evaluation_parameters.
35 (ext_step p → status_class) →
36 (ext_fin_stmt p → status_class) →
37 abstract_status ≝
38 λp,ext_step_cl,ext_fin_step_cl.
39 mk_abstract_status
40   (* as_status ≝ *) (state_pc p)
41   (* as_execute ≝ *) (λs1,s2.eval_state … p (genv2 p) s1 = return s2)
42   (* as_pc ≝ *) cpointerDeq
43   (* as_pc_of ≝ *) (pc …)
44   (* as_classifier ≝ *)
45    (λs,cl.∃stmt.fetch_statement ? p … (genv2 p) (pc … s) = return stmt ∧
46     stmt_classifier … ext_step_cl ext_fin_step_cl stmt = cl)
47   (* as_label_of_pc ≝ *)
48    (λpc.
49      match fetch_statement ? p … (genv2 p) pc with
50      [ OK stmt ⇒
51        match stmt with
52        [ sequential s _ ⇒
53          match s with
54          [ COST_LABEL l ⇒ Some ? l
55          | _ ⇒ None ?
56          ]
57        | _ ⇒ None ?
58        ]
59      | _ ⇒ None ?
60      ])
61   (* as_after_return ≝ *)
62    (λs1,s2. (* Paolo: considering sequential calls, tailcalls are out of the picture for now *)
63      ∃stp,nxt.fetch_statement ? p … (genv2 p) (pc … s1) = return (sequential ?? stp nxt) ∧
64      succ_pc p p (pc … s1) nxt = return pc … s2)
65   (* as_final ≝ *) (λs.is_final (globals ?) p (genv2 p) (exit p) s ≠ None ?).
Note: See TracBrowser for help on using the repository browser.