source: src/joint/semantics_blocks.ma @ 2599

Last change on this file since 2599 was 2599, checked in by tranquil, 8 years ago
  • map_opt and map on positive maps are now clean (erase empty subtrees)
  • minor changes to blocks
File size: 5.8 KB
Line 
1include "joint/blocks.ma".
2include "joint/Traces.ma".
3include "joint/semanticsUtils.ma".
4
5include "common/StatusSimulation.ma". (* for trace_any_any_free *)
6
7(* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
8  match b with
9  [ nil ⇒ [ ]
10  | cons hd tl ⇒ step_labels … hd @ seq_list_labels … tl
11  ].*)
12
13definition repeat_eval_seq_no_pc ≝
14  λp : evaluation_params.λcurr_id,curr_fn.
15  m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id curr_fn).
16
17definition taaf_cons : ∀S : abstract_status.∀s1,s2,s3.
18  as_execute S s1 s2 →
19  as_classifier … s1 cl_other →
20  ∀taaf : trace_any_any_free S s2 s3.
21  (if taaf_non_empty … taaf then ¬as_costed … s2 else True) →
22  trace_any_any_free S s1 s3 ≝
23λS,s1,s2,s3,H,I,tl.
24match tl return λs2,s3,tl.
25  as_execute … s1 s2 →
26  if taaf_non_empty … tl then ¬as_costed … s2 else True →
27  trace_any_any_free S s1 s3
28with
29[ taaf_base s2 ⇒ λH.λ_.taaf_step … (taa_base …) H I
30| taaf_step s2 s3 s4 taa H' I' ⇒
31  λH,J.taaf_step … (taa_step … H I J taa) H' I'
32| taaf_step_jump s2 s3 s4 taa H' I' K' ⇒
33  λH,J.taaf_step_jump … (taa_step ???? H I J taa) H' I' K'
34] H.
35
36lemma taaf_cons_non_empty : ∀S,s1,s2,s3,H,I,tl,J.
37bool_to_Prop (taaf_non_empty … (taaf_cons S s1 s2 s3 H I tl J)).
38#S #s1 #s2 #s3 #H #I #tl lapply H -H cases tl
39[ #s #H * % |*: #s2 #s3 #s4 #taa #H' #I' [2: #K'] #H #J % ]
40qed.
41
42let rec produce_trace_any_any_free_aux
43  (p : evaluation_params)
44  (st : state_pc p)
45  curr_id curr_fn
46  (b : list (joint_seq p (globals p))) on b :
47  ∀l : list (code_point p).
48  ∀dst : code_point p.
49  ∀st' : state p.
50  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
51    return 〈curr_id, curr_fn〉 →
52  let src ≝ point_of_pc p (pc … st) in
53  step_list_in_code … (joint_if_code … curr_fn) src b l dst →
54  All ? (no_cost_label …) b →
55  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
56  Σtaaf : trace_any_any_free (joint_abstract_status p) st
57    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
58  (not_empty … b ↔ bool_to_Prop (taaf_non_empty … taaf)) ≝
59  match b
60  return λb.∀l,dst.?→?→?→?→?→ Σtaaf.(not_empty ? b ↔ bool_to_Prop (taaf_non_empty … taaf))
61  with
62  [ nil ⇒
63    λl,dst,st',fd_prf,in_code,all_other,EQ1.
64    «taaf_base (joint_abstract_status p) st
65    ⌈trace_any_any_free ??? ↦ ?⌉,?»
66  | cons hd tl ⇒
67    λl.
68    match l return λx.∀dst,st'.?→?→?→?→Σtaaf.(True ↔ bool_to_Prop (taaf_non_empty … taaf)) with
69    [ nil ⇒ λdst,st',fd_prf,in_code.⊥
70    | cons mid rest ⇒
71      λdst,st',fd_prf,in_code,all_other,EQ1.
72      let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in
73      match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st
74      return λx.eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st = x →
75      Σtaaf : trace_any_any_free (joint_abstract_status p) st
76        (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
77        (True ↔ bool_to_Prop (taaf_non_empty … taaf)) with
78      [ OK st_mid ⇒ λEQ2.
79        let tr_tl ≝ produce_trace_any_any_free_aux ?
80            (mk_state_pc ? st_mid mid_pc (last_pop … st))
81            curr_id curr_fn tl rest dst ????? in
82        «taaf_cons … tr_tl ?,?»
83      | _ ⇒ λEQ2.⊥
84      ] (refl …)
85    ]
86  ]. @hide_prf
87[1,2: [2: % [*] generalize in ⊢ (?(???? (match % with [ _ ⇒ ?])) → ?); ]
88  whd in EQ1 : (??%%);
89  cases l in in_code; whd in ⊢ (%→?); [2,4: #hd #tl * ] #EQ destruct
90  >pc_of_point_of_pc cases st // #a #b #c #e >(K ?? e) normalize nodelta *
91| @in_code
92|12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
93|4: cases tr_tl -tr_tl #tr_tl cases tl in in_code all_other;
94  [ #_ #_ * #_ cases (taaf_non_empty ????)
95    [ #ABS cases (ABS I) | #_ % ]
96  | #hd' #tl' ** #nxt * #EQstmt_at #EQ_nxt cases rest [*] #mid' #rest' *
97    * #nxt' * #EQstmt_at' #EQ_nxt' #_ * #hd_other * #hd_other'
98    #_ * #H #_ >(H I) % whd in ⊢ (%→?);
99    whd in ⊢ (?(??%?)→?); whd in match (as_pc_of ??);
100    >fetch_statement_eq [2: whd in match point_of_pc;
101    normalize nodelta >point_of_offset_of_point @EQstmt_at' |3: @fd_prf |*:]
102    normalize nodelta
103    >(no_label_uncosted … hd_other') * #ABS @ABS %
104  ]
105|7: % [2: #_ %] * @taaf_cons_non_empty
106]
107change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1;
108>EQ2 in EQ1; >m_return_bind
109cases in_code -in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code
110cases all_other -all_other #hd_no_cost #tl_other
111#EQ1
112try assumption
113[2: whd whd in match eval_state; normalize nodelta
114  >(fetch_statement_eq … fd_prf EQ_stmt_at)
115  >m_return_bind
116  whd in match eval_statement_no_pc; normalize nodelta
117  >EQ2 >m_return_bind
118  whd in match eval_statement_advance; normalize nodelta
119  whd in match next; normalize nodelta
120  whd in match succ_pc; normalize nodelta
121  >EQ_mid %
122|1: whd whd in ⊢ (??%?);
123  >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta %
124|3: normalize nodelta >point_of_pc_of_point assumption
125]
126qed.
127
128definition produce_trace_any_any_free :
129  ∀p : evaluation_params.
130  ∀st : state_pc p.
131  ∀curr_id,curr_fn.
132  ∀b : list (joint_seq p (globals p)).
133  ∀l : list (code_point p).
134  ∀dst : code_point p.
135  ∀st' : state p.
136  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
137    return 〈curr_id, curr_fn〉 →
138  let src ≝ point_of_pc p (pc … st) in
139  step_list_in_code … (joint_if_code … curr_fn) src b l dst →
140  All ? (no_cost_label …) b →
141  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
142  trace_any_any_free (joint_abstract_status p) st
143    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝
144  λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3,prf4.
145  produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3 prf4.
Note: See TracBrowser for help on using the repository browser.