Changeset 3486 for LTS/Vm.ma


Ignore:
Timestamp:
Sep 24, 2014, 2:49:14 PM (5 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3485 r3486  
    1515{ seq_instr : Type[0]
    1616; jump_condition : Type[0]
    17 ; io_instr : Type[0]
    18 ; entry_of_function : FunctionName → ℕ
    19 ; call_label_fun : list (ℕ × CallCostLabel)
    20 ; return_label_fun : list (ℕ × ReturnPostCostLabel)
    21 }.
     17; io_instr : Type[0] }.
    2218
    2319inductive AssemblerInstr (p : assembler_params) : Type[0] ≝
     
    2925| Iret: AssemblerInstr p.
    3026
     27definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (CostLabel × ℕ) ≝
     28λp,i,program_counter.
     29match i with
     30  [ Seq _ opt_l ⇒ match opt_l with
     31                  [ Some lbl ⇒ [〈(a_non_functional_label lbl),S program_counter〉]
     32                  | None ⇒ [ ]
     33                  ]
     34  | Ijmp _ ⇒ [ ]
     35  | CJump _ newpc ltrue lfalse ⇒ [〈(a_non_functional_label ltrue),newpc〉;
     36                                  〈(a_non_functional_label lfalse),S program_counter〉]
     37  | Iio lin _ lout ⇒ [〈(a_non_functional_label lin),program_counter〉;
     38                      〈(a_non_functional_label lout),S program_counter〉]
     39  | Icall f ⇒ [ ]
     40  | Iret ⇒ [ ]
     41  ].
     42
     43let rec labels_pc (p : assembler_params)
     44(prog : list (AssemblerInstr p)) (call_label_fun : list (ℕ × CallCostLabel))
     45              (return_label_fun : list (ℕ × ReturnPostCostLabel)) (i_act : NonFunctionalLabel)
     46              (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝
     47match prog with
     48[ nil ⇒ [〈a_non_functional_label (i_act),O〉] @
     49        map … (λx.let〈y,z〉 ≝ x in 〈(a_call z),y〉) (call_label_fun) @
     50        map … (λx.let〈y,z〉 ≝ x in 〈(a_return_post z),y〉) (return_label_fun)
     51| cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is call_label_fun return_label_fun i_act (S program_counter)
     52].
     53
     54include "basics/lists/listb.ma".
     55
     56(*doppione da mettere a posto*)
     57let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝
     58match l with
     59[ nil ⇒ True
     60| cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs
     61].
     62
     63
    3164record AssemblerProgram (p : assembler_params) : Type[0] ≝
    3265{ instructions : list (AssemblerInstr p)
    3366; endmain : ℕ
    3467; endmain_ok : endmain < |instructions|
     68; entry_of_function : FunctionName → ℕ
     69; call_label_fun : list (ℕ × CallCostLabel)
     70; return_label_fun : list (ℕ × ReturnPostCostLabel)
     71; in_act : NonFunctionalLabel
     72; asm_no_duplicates : no_duplicates … (map ?? \fst … (labels_pc … instructions call_label_fun return_label_fun in_act O))
    3573}.
     74
    3675
    3776definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝
     
    137176           S (pc … st1) ::  asm_stack … st1 = asm_stack … st2 →
    138177           asm_is_io … st1 = asm_is_io … st2 →
    139            entry_of_function p f = pc … st2 →
     178           entry_of_function … prog f = pc … st2 →
    140179           op … (cost … st1) (cost_of p p' (Icall p f) (asm_store … st1)) = cost … st2 →
    141            label_of_pc ? (call_label_fun p) (entry_of_function p f) = return lbl →
     180           label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f) = return lbl →
    142181           vmstep … (call_act f lbl) st1 st2
    143182| vm_ret :
     
    149188           asm_is_io … st1 = asm_is_io … st2 →
    150189           newpc = pc … st2 →
    151            label_of_pc ? (return_label_fun p) newpc = return lbl →
     190           label_of_pc ? (return_label_fun … prog) newpc = return lbl →
    152191           op … (cost … st1) (cost_of p p' (Iret p) (asm_store … st1)) = cost … st2 →
    153192           vmstep … (ret_act (Some ? lbl)) st1 st2.
     
    202241      None ?
    203242    else
    204       ! lbl ← label_of_pc ? (call_label_fun p) (entry_of_function p f);
     243      ! lbl ← label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f);
    205244      return 〈call_act f lbl,
    206               mk_vm_state ?? (entry_of_function p f)
     245              mk_vm_state ?? (entry_of_function … prog f)
    207246                             ((S (pc … st)) :: (asm_stack … st))
    208247                             (asm_store … st) false
     
    212251         else
    213252            ! 〈newpc,tl〉 ← option_pop … (asm_stack … st);
    214             ! lbl ← label_of_pc ? (return_label_fun p) newpc;
     253            ! lbl ← label_of_pc ? (return_label_fun … prog) newpc;
    215254            return 〈ret_act (Some ? lbl),
    216255                    mk_vm_state ?? newpc tl (asm_store … st) false   
     
    291330discriminator option.
    292331
     332inductive vm_ass_state  (p : assembler_params) (p' : sem_params p) : Type[0] ≝
     333| INITIAL : vm_ass_state p p'
     334| FINAL : vm_ass_state p p'
     335| STATE : vm_state p p' → vm_ass_state p p'.
     336
    293337definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p →  abstract_status ≝
    294 λp,p',prog.mk_abstract_status
    295                 (vm_state p p')
    296                 (λl.λst1,st2 : vm_state p p'.(eqb (pc ?? st1) (endmain … prog)) = false ∧
    297                                vmstep p p' prog l st1 st2)
     338λp,p',prog.let init_act ≝ cost_act (Some ? (in_act … prog)) in
     339           let end_act ≝ cost_act (Some ? (in_act … prog)) in
     340    mk_abstract_status
     341                (vm_ass_state p p')
     342                (λl.λs1,s2 : vm_ass_state p p'.
     343                    match s1 with
     344                    [ STATE st1 ⇒
     345                        match s2 with
     346                        [ STATE st2 ⇒ 
     347                            (eqb (pc ?? st1) (endmain … prog)) = false ∧ vmstep p p' prog l st1 st2
     348                        | INITIAL ⇒ False
     349                        | FINAL ⇒ eqb (pc … st1) (endmain … prog) = true ∧ l = end_act
     350                        ]
     351                    | INITIAL ⇒ match s2 with
     352                                [ STATE st2 ⇒ eqb (pc … st2) O = true ∧ l = init_act
     353                                | _ ⇒ False
     354                                ]
     355                    | FINAL ⇒ False
     356                    ])
    298357                (λ_.λ_.True)
    299                 (λs.match fetch … prog (pc … s) with
    300                     [ Some i ⇒ match i with
     358                (λst.match st with
     359                    [ INITIAL ⇒ cl_other | FINAL ⇒ cl_other |
     360                     STATE s ⇒
     361                      match fetch … prog (pc … s) with
     362                      [ Some i ⇒ match i with
    301363                               [ Seq _ _ ⇒ cl_other
    302364                               | Ijmp _ ⇒ cl_other
     
    306368                               | Iret ⇒ cl_other
    307369                               ]
    308                     | None ⇒ cl_other
     370                     | None ⇒ cl_other
     371                     ]
    309372                    ]
    310373                )
    311374                (λ_.true)
    312                 (λs.eqb (pc ?? s) O)
    313                 (λs.eqb (pc … s) (endmain … prog))
     375                (λs.match s with [ INITIAL ⇒ true | _ ⇒ false])
     376                (λs.match s with [ FINAL ⇒ true | _ ⇒ false])
    314377                ???.
    315 @hide_prf
     378@hide_prf cases daemon qed. (*
    316379[ #s1 #s2 #l inversion(fetch ???) normalize nodelta
    317380  [ #_ #EQ destruct] * normalize nodelta
     
    366429  normalize nodelta #H cases(bind_inversion ????? H) -H #x * #_
    367430  whd in ⊢ (??%% → ?); #EQ destruct % //
    368 qed.
     431qed.*)
    369432
    370433definition asm_concrete_trans_sys ≝
    371434λp,p',prog.mk_concrete_transition_sys …
    372              (asm_operational_semantics p p' prog) (m … p') (cost …).
     435             (asm_operational_semantics p p' prog) (m … p')
     436             (λs.match s with [STATE st ⇒ cost … st | _ ⇒ e …] ).
    373437
    374438definition emits_labels ≝
     
    387451definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m.
    388452mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t
    389  … (fetch_state p p' prog) instr_m.
     453 … (λs.match s with [ STATE st ⇒ fetch_state p p' prog st | _ ⇒ None ? ]) instr_m.
    390454
    391455definition non_empty_list : ∀A.list A → bool ≝
     
    395459 (prog: AssemblerProgram p) (abs_t : monoid)
    396460 (instr_m : AssemblerInstr p → abs_t)
    397  (program_counter: ℕ)
     461 (prog_c: option ℕ)
    398462    (program_size: ℕ)
    399463        on program_size: option abs_t ≝
    400 match program_size with
    401   [ O ⇒ None ?
    402   | S program_size' ⇒
    403     if eqb program_counter (endmain … prog) then
    404        return e … abs_t
    405     else
    406     ! instr ← fetch … prog program_counter;
    407     ! n ← (match emits_labels … instr with
    408           [ Some f ⇒ block_cost … prog abs_t instr_m (f program_counter) program_size'
    409           | None ⇒ return e …
    410           ]);
    411     return (op … abs_t (instr_m … instr) n)
    412   ].
     464match prog_c with
     465[ None ⇒ return e … abs_t
     466| Some program_counter ⇒
     467  match program_size with
     468    [ O ⇒ None ?
     469    | S program_size' ⇒
     470       if eqb program_counter (endmain … prog) then
     471        return e … abs_t
     472      else
     473      ! instr ← fetch … prog program_counter;
     474      ! n ← (match emits_labels … instr with
     475            [ Some f ⇒ block_cost … prog abs_t instr_m (Some ? (f program_counter)) program_size'
     476            | None ⇒ return e …
     477            ]);
     478      return (op … abs_t (instr_m … instr) n)
     479    ]
     480].
    413481
    414482
     
    422490}.
    423491
    424 definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (CostLabel × ℕ) ≝
    425 λp,i,program_counter.
    426 match i with
    427   [ Seq _ opt_l ⇒ match opt_l with
    428                   [ Some lbl ⇒ [〈(a_non_functional_label lbl),S program_counter〉]
    429                   | None ⇒ [ ]
    430                   ]
    431   | Ijmp _ ⇒ [ ]
    432   | CJump _ newpc ltrue lfalse ⇒ [〈(a_non_functional_label ltrue),newpc〉;
    433                                   〈(a_non_functional_label lfalse),S program_counter〉]
    434   | Iio lin _ lout ⇒ [〈(a_non_functional_label lin),program_counter〉;
    435                       〈(a_non_functional_label lout),S program_counter〉]
    436   | Icall f ⇒ [ ]
    437   | Iret ⇒ [ ]
    438   ].
    439 
    440 let rec labels_pc (p : assembler_params)
    441 (prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝
    442 match prog with
    443 [ nil ⇒ [〈i_act,O〉] @
    444         map … (λx.let〈y,z〉 ≝ x in 〈(a_call z),y〉) (call_label_fun … p) @
    445         map … (λx.let〈y,z〉 ≝ x in 〈(a_return_post z),y〉) (return_label_fun … p)
    446 | cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is (S program_counter)
    447 ].
    448 
    449 lemma labels_pc_ok : ∀p,prog,i,lbl,pc,m.
     492
     493
     494lemma labels_pc_ok : ∀p,prog,l1,l2,i_act,i,lbl,pc,m.
    450495nth_opt ? pc prog = return i →
    451496mem ? lbl (labels_pc_of_instr … i (m+pc)) →
    452 mem ? lbl (labels_pc p prog m).
    453 #p #instrs #i #lbl #pc
     497mem ? lbl (labels_pc p prog l1 l2 i_act m).
     498#p #instrs #l1 #l2 #iact #i #lbl #pc
    454499whd in match fetch; normalize nodelta lapply pc -pc
    455500elim instrs
    456501[ #pc #m whd in ⊢ (??%% → ?); #EQ destruct]
    457 #x #xs #IH * [|#pc'] #m whd in ⊢ (??%% → ?);
     502#x #xs #IH * [|#pc'] #m  whd in ⊢ (??%% → ?);
    458503[ #EQ destruct #lbl_addr whd in match (labels_pc ???);
    459504  /2 by mem_append_l1/
     
    462507qed.
    463508
    464 lemma labels_pc_return: ∀p,prog,x1,x2.
    465  label_of_pc ReturnPostCostLabel (return_label_fun p) x1=return x2 →
     509lemma labels_pc_return: ∀p,prog,l1,l2,iact,x1,x2.
     510 label_of_pc ReturnPostCostLabel l2 x1=return x2 →
    466511 ∀m.
    467    mem … 〈(a_return_post x2),x1〉 (labels_pc p prog m).
    468  #p #l whd in match (labels_pc ???); #x1 #x2 #H elim l
     512   mem … 〈(a_return_post x2),x1〉 (labels_pc p prog l1 l2 iact m).
     513 #p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l
    469514[ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?);
    470   elim (return_label_fun ?) in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
     515  elim l2 in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
    471516  * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim
    472517  normalize nodelta
     
    476521qed.
    477522
    478 lemma labels_pc_call: ∀p,prog,x1,x2.
    479  label_of_pc CallCostLabel (call_label_fun p) x1=return x2 →
     523lemma labels_pc_call: ∀p,prog,l1,l2,iact,x1,x2.
     524 label_of_pc CallCostLabel l1 x1=return x2 →
    480525 ∀m.
    481    mem … 〈(a_call x2),x1〉 (labels_pc p prog m).
    482  #p #l whd in match (labels_pc ???); #x1 #x2 #H elim l
     526   mem … 〈(a_call x2),x1〉 (labels_pc p prog l1 l2 iact m).
     527 #p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l
    483528[ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?);
    484   elim (call_label_fun ?) in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
     529  elim l1 in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
    485530  * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim
    486531  normalize nodelta
     
    520565λp,abs_t,instr_m,mT,prog.
    521566let prog_size ≝ S (|instructions … prog|) in
    522 m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m w prog_size; 
    523                                return set_map … m z k) (labels_pc … (instructions … prog) O)
     567m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m (Some ? w) prog_size; 
     568                               return set_map … m z k) (labels_pc … (instructions … prog)
     569                                         (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)
    524570      (empty_map ?? mT).
    525571     
    526 
    527 include "basics/lists/listb.ma".
    528 
    529 (*doppione da mettere a posto*)
    530 let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝
    531 match l with
    532 [ nil ⇒ True
    533 | cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs
    534 ].
    535 
    536 definition asm_no_duplicates ≝
    537 λp,prog.no_duplicates … (map ?? \fst … (labels_pc … (instructions p prog) O)).
    538572
    539573(*falso: necessita di no_duplicates*)
     
    577611
    578612lemma static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map.
    579 asm_no_duplicates p prog →
    580613static_analisys p abs_t instr_m mT prog = return map →
    581 mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) O) →
     614mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) (call_label_fun … prog)
     615                   (return_label_fun … prog) (in_act … prog) O) →
    582616get_map … map lbl =
    583 block_cost … prog abs_t instr_m pc (S (|(instructions … prog)|)) ∧
    584 block_cost … prog abs_t instr_m pc (S (|(instructions … prog)|)) ≠ None ?.
     617block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ∧
     618block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ≠ None ?.
    585619#p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta
    586 whd in match asm_no_duplicates; normalize nodelta lapply (labels_pc ???)
    587 #l #endmain #Hendmain elim l [ #x #y #z #w #h * ]
    588 * #hd1 #hd2 #tl #IH #lbl #pc #map * #H1 #H2 #H
     620#endmain #Hendmain #entry_fun #call_label_fun #return_label_fun #inact
     621#nodup generalize in match nodup in ⊢ (∀_.∀_.∀_. (??(????%??)?) → %); #Hnodup lapply nodup -nodup
     622lapply (labels_pc ??????) #l elim l [ #x #y #z #w #h * ]
     623* #hd1 #hd2 #tl #IH * #H1 #H2 #lbl #pc #map #H
    589624cases(bind_inversion ????? H) -H #map1 * #EQmap1 normalize nodelta #H
    590625cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); #EQ
     
    602637include "Simulation.ma".
    603638
    604 record terminated_trace (S : abstract_status) (R_s2 : S) : Type[0] ≝
    605 {  R_post_step : option (ActionLabel × S)
    606  ; R_fin_ok : match R_post_step with
    607                [ None ⇒ bool_to_Prop (as_final … R_s2)
    608                | Some x ⇒ let 〈l,R_post_state〉≝ x in
    609                           (is_costlabelled_act l ∨ is_labelled_ret_act l) ∧
    610                           (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧
    611                           as_execute … l R_s2 R_post_state
    612                ]
    613  }.
     639definition terminated_trace : ∀S : abstract_status.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝
     640λS,s1,s3,t.bool_to_Prop (as_final … s3) ∨
     641       ∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind ? s2 s3 s3 l prf … (t_base … s3))
     642∧ ((is_costlabelled_act l ∨ is_labelled_ret_act l) ∧
     643   (is_call_act l → bool_to_Prop (is_call_post_label … s2))).
    614644
    615645definition big_op: ∀M: monoid. list M → M ≝
     
    643673
    644674lemma monotonicity_of_block_cost : ∀p,prog,abs_t,instr_m,pc,size,k.
    645 block_cost p prog abs_t instr_m pc size = return k →
     675block_cost p prog abs_t instr_m (Some ? pc) size = return k →
    646676∀size'.size ≤ size' →
    647 block_cost p prog abs_t instr_m pc size' = return k.
     677block_cost p prog abs_t instr_m (Some ? pc) size' = return k.
    648678#p #prog #abs_t #instr_m #pc #size lapply pc elim size
    649679[ #pc #k whd in ⊢ (??%% → ?); #EQ destruct]
     
    678708   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
    679709] = [x] ∧
    680  (mem … 〈x,pc … st2〉 (labels_pc p (instructions … prog) O)).
     710 (mem … 〈x,pc … st2〉 (labels_pc p (instructions … prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)).
    681711#p #p' #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta
    682712>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
     
    733763
    734764lemma labels_of_trace_are_in_code :
    735 ∀p,p',prog.∀st1,st2 :  vm_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
     765∀p,p',prog.∀st1,st2 :  vm_ass_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
    736766∀lbl.
    737767mem … lbl (get_costlabels_of_trace … t) →
    738 mem … (lbl) (map ?? \fst … (labels_pc … (instructions p prog) O)).
     768mem … (lbl) (map ?? \fst … (labels_pc … (instructions p prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)).
     769cases daemon (*
    739770#p #p' #prog #st1 #st2 #t elim t
    740771[ #st #lbl *
     
    749780    *
    750781  ]
    751 
     782*)
    752783qed.
    753784
     
    774805qed.
    775806
    776 
    777 lemma static_dynamic : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog.
     807definition get_pc : ∀p,p'.vm_ass_state p p' → ℕ → option ℕ ≝
     808λp,p',st,endmain.match st with
     809[ STATE s ⇒ Some ? (pc … s)
     810| INITIAL ⇒ None ?
     811| FINAL ⇒ Some ? endmain
     812].
     813
     814
     815lemma static_dynamic : ∀p,p',prog.
    778816∀abs_t : abstract_transition_sys (m … p').∀instr_m.
    779817∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
    780818∀EQmap : static_analisys p ? instr_m mT prog = return map1.
    781 ∀st1,st2 : vm_state p p'.
    782 ∀ter : terminated_trace (asm_operational_semantics p p' prog) st2.
     819∀st1,st2 : vm_ass_state p p'.
    783820∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
     821terminated_trace … t →
    784822∀k.
    785823pre_measurable_trace … t →
    786 block_cost p prog … instr_m (pc … st1) (S (|(instructions … prog)|)) = return k →
     824block_cost p prog … instr_m (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k →
    787825∀a1.rel_galois … good st1 a1 →
    788 let stop_state ≝ match R_post_step … ter with [None ⇒ st2 | Some x ⇒ \snd x ] in
    789 ∀costs.
    790 costs = dependent_map CostLabel ? (get_costlabels_of_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
    791 rel_galois … good stop_state (act_abs … abs_t (big_op … costs) (act_abs … abs_t k a1)).
     826∀labels.
     827labels = dependent_map CostLabel ? (get_costlabels_of_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
     828rel_galois … good st2 (act_abs … abs_t (big_op … labels) (act_abs … abs_t k a1)).
    792829[2: @hide_prf
    793830    cases(mem_map ????? (labels_of_trace_are_in_code … prf)) *
    794831    #lbl' #pc * #Hmem #EQ destruct   
    795     >(proj1 … (static_analisys_ok … no_dup … EQmap … Hmem))
    796     @(proj2 … (static_analisys_ok … no_dup … EQmap … Hmem))
    797 ]
    798 #p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t
    799 lapply ter -ter elim t
    800 [ #st #ter inversion(R_post_step … ter) normalize nodelta [| * #lbl #st3 ]
     832    >(proj1 … (static_analisys_ok … EQmap … Hmem))
     833    @(proj2 … (static_analisys_ok … EQmap … Hmem))
     834]
     835#p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t elim t
     836[ #st * [| * #st3 * #t1 * #l * #prf * #ABS @⊥ cases t1 in ABS; ]
    801837  #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta
    802838  [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st
Note: See TracChangeset for help on using the changeset viewer.