include "costs.ma". include "basics/lists/list.ma". include "../src/utilities/option.ma". include "basics/jmeq.ma". lemma bind_inversion : ∀A,B : Type[0].∀m : option A. ∀f : A → option B.∀y : B. ! x ← m; f x = return y → ∃ x.(m = return x) ∧ (f x = return y). #A #B * [| #a] #f #y normalize #EQ [destruct] %{a} %{(refl …)} // qed. record assembler_params : Type[1] ≝ { seq_instr : Type[0] ; jump_condition : Type[0] ; io_instr : Type[0] ; entry_of_function : FunctionName → ℕ ; call_label_fun : list (ℕ × CallCostLabel) ; return_label_fun : list (ℕ × ReturnPostCostLabel) }. inductive AssemblerInstr (p : assembler_params) : Type[0] ≝ | Seq : seq_instr p → option (NonFunctionalLabel) → AssemblerInstr p | Ijmp: ℕ → AssemblerInstr p | CJump : jump_condition p → ℕ → NonFunctionalLabel → NonFunctionalLabel → AssemblerInstr p | Iio : NonFunctionalLabel → io_instr p → NonFunctionalLabel → AssemblerInstr p | Icall: FunctionName → AssemblerInstr p | Iret: AssemblerInstr p. record AssemblerProgram (p : assembler_params) : Type[0] ≝ { instructions : list (AssemblerInstr p) ; endmain : ℕ ; endmain_ok : endmain < |instructions| }. definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝ λp,l,n. nth_opt ? n (instructions … l). definition stackT: Type[0] ≝ list (nat). record sem_params (p : assembler_params) : Type[1] ≝ { m : monoid ; asm_store_type : Type[0] ; eval_asm_seq : seq_instr p → asm_store_type → option asm_store_type ; eval_asm_cond : jump_condition p → asm_store_type → option bool ; eval_asm_io : io_instr p → asm_store_type → option asm_store_type ; cost_of_io : io_instr p → asm_store_type → m ; cost_of : AssemblerInstr p → asm_store_type → m }. record vm_state (p : assembler_params) (p' : sem_params p) : Type[0] ≝ { pc : ℕ ; asm_stack : stackT ; asm_store : asm_store_type … p' ; asm_is_io : bool ; cost : m … p' }. definition label_of_pc ≝ λL.λl.λpc.find … (λp.let 〈x,y〉 ≝ p in if eqb x pc then Some L y else None ? ) l. definition option_pop ≝ λA.λl:list A. match l with [ nil ⇒ None ? | cons a tl ⇒ Some ? (〈a,tl〉) ]. inductive vmstep (p : assembler_params) (p' : sem_params p) (prog : AssemblerProgram p) : ActionLabel → relation (vm_state p p') ≝ | vm_seq : ∀st1,st2 : vm_state p p'.∀i,l. fetch … prog (pc … st1) = return (Seq p i l) → asm_is_io … st1 = false → eval_asm_seq p p' i (asm_store … st1) = return asm_store … st2 → asm_stack … st1 = asm_stack … st2 → asm_is_io … st1 = asm_is_io … st2 → S (pc … st1) = pc … st2 → op … (cost … st1) (cost_of p p' (Seq p i l) (asm_store … st1)) = cost … st2 → vmstep … (cost_act l) st1 st2 | vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ. fetch … prog (pc … st1) = return (Ijmp p new_pc) → asm_is_io … st1 = false → asm_store … st1 = asm_store … st2 → asm_stack … st1 = asm_stack … st2 → asm_is_io … st1 = asm_is_io … st2 → new_pc = pc … st2 → op … (cost … st1) (cost_of p p' (Ijmp … new_pc) (asm_store … st1)) = cost … st2 → vmstep … (cost_act (None ?)) st1 st2 | vm_cjump_true : ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse. eval_asm_cond p p' cond (asm_store … st1) = return true→ fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) → asm_is_io … st1 = false → asm_store … st1 = asm_store … st2 → asm_stack … st1 = asm_stack … st2 → asm_is_io … st1 = asm_is_io … st2 → pc … st2 = new_pc → op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 → vmstep … (cost_act (Some ? ltrue)) st1 st2 | vm_cjump_false : ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse. eval_asm_cond p p' cond (asm_store … st1) = return false→ fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) → asm_is_io … st1 = false → asm_store … st1 = asm_store … st2 → asm_stack … st1 = asm_stack … st2 → asm_is_io … st1 = asm_is_io … st2 → S (pc … st1) = pc … st2 → op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 → vmstep … (cost_act (Some ? lfalse)) st1 st2 | vm_io_in : ∀st1,st2 : vm_state p p'.∀lin,io,lout. fetch … prog (pc … st1) = return (Iio p lin io lout) → asm_is_io … st1 = false → asm_store … st1 = asm_store … st2 → asm_stack … st1 = asm_stack … st2 → true = asm_is_io … st2 → pc … st1 = pc … st2 → cost … st1 = cost … st2 → vmstep … (cost_act (Some ? lin)) st1 st2 | vm_io_out : ∀st1,st2 : vm_state p p'.∀lin,io,lout. fetch … prog (pc … st1) = return (Iio p lin io lout) → asm_is_io … st1 = true → eval_asm_io … io (asm_store … st1) = return asm_store … st2 → asm_stack … st1 = asm_stack … st2 → false = asm_is_io … st2 → S (pc … st1) = pc … st2 → op … (cost … st1) (cost_of_io p p' io (asm_store … st1)) = cost … st2 → vmstep … (cost_act (Some ? lout)) st1 st2 | vm_call : ∀st1,st2 : vm_state p p'.∀f,lbl. fetch … prog (pc … st1) = return (Icall p f) → asm_is_io … st1 = false → asm_store … st1 = asm_store … st2 → S (pc … st1) :: asm_stack … st1 = asm_stack … st2 → asm_is_io … st1 = asm_is_io … st2 → entry_of_function p f = pc … st2 → op … (cost … st1) (cost_of p p' (Icall p f) (asm_store … st1)) = cost … st2 → label_of_pc ? (call_label_fun p) (entry_of_function p f) = return lbl → vmstep … (call_act f lbl) st1 st2 | vm_ret : ∀st1,st2 : vm_state p p'.∀newpc,lbl. fetch … prog (pc … st1) = return (Iret p) → asm_is_io … st1 = false → asm_store … st1 = asm_store … st2 → asm_stack … st1 = newpc :: asm_stack … st2 → asm_is_io … st1 = asm_is_io … st2 → newpc = pc … st2 → label_of_pc ? (return_label_fun p) newpc = return lbl → op … (cost … st1) (cost_of p p' (Iret p) (asm_store … st1)) = cost … st2 → vmstep … (ret_act (Some ? lbl)) st1 st2. definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p. AssemblerProgram p → vm_state p p' → option (ActionLabel × (vm_state p p')) ≝ λp,p',prog,st. ! i ← fetch … prog (pc … st); match i with [ Seq x opt_l ⇒ if asm_is_io … st then None ? else ! new_store ← eval_asm_seq p p' x (asm_store … st); return 〈cost_act opt_l, mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false (op … (cost … st) (cost_of p p' (Seq p x opt_l) (asm_store … st)))〉 | Ijmp newpc ⇒ if asm_is_io … st then None ? else return 〈cost_act (None ?), mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false (op … (cost … st) (cost_of p p' (Ijmp … newpc) (asm_store … st)))〉 | CJump cond newpc ltrue lfalse ⇒ if asm_is_io … st then None ? else ! b ← eval_asm_cond p p' cond (asm_store … st); if b then return 〈cost_act (Some ? ltrue), mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉 else return 〈cost_act (Some ? lfalse), mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉 | Iio lin io lout ⇒ if asm_is_io … st then ! new_store ← eval_asm_io … io (asm_store … st); return 〈cost_act (Some ? lout), mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false (op … (cost … st) (cost_of_io p p' io (asm_store … st)))〉 else return 〈cost_act (Some ? lin), mk_vm_state ?? (pc … st) (asm_stack … st) (asm_store … st) true (cost … st)〉 | Icall f ⇒ if asm_is_io … st then None ? else ! lbl ← label_of_pc ? (call_label_fun p) (entry_of_function p f); return 〈call_act f lbl, mk_vm_state ?? (entry_of_function p f) ((S (pc … st)) :: (asm_stack … st)) (asm_store … st) false (op … (cost … st) (cost_of p p' (Icall p f) (asm_store … st)))〉 | Iret ⇒ if asm_is_io … st then None ? else ! 〈newpc,tl〉 ← option_pop … (asm_stack … st); ! lbl ← label_of_pc ? (return_label_fun p) newpc; return 〈ret_act (Some ? lbl), mk_vm_state ?? newpc tl (asm_store … st) false (op … (cost … st) (cost_of p p' (Iret p) (asm_store … st)))〉 ]. lemma eval_vmstate_to_Prop : ∀p,p',prog,st1,st2,l. eval_vmstate p p' prog st1 = return 〈l,st2〉 → vmstep … prog l st1 st2. #p #p' #prog #st1 #st2 #l whd in match eval_vmstate; normalize nodelta #H cases(bind_inversion ????? H) -H * normalize nodelta [ #seq #opt_l * #EQfetch inversion(asm_is_io ???) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) #newstore * #EQnewstore whd in ⊢ (??%% → ?); #EQ destruct @vm_seq // | #newpc * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio [ whd in ⊢ (??%% → ?); #EQ destruct] whd in ⊢ (??%% → ?); #EQ destruct @vm_ijump // | #cond #new_pc #ltrue #lfase * #EQfetch inversion(asm_is_io ???) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) -H * normalize nodelta * #EQcond whd in ⊢ (??%% → ?); #EQ destruct [ @(vm_cjump_true … EQfetch) // | @(vm_cjump_false … EQfetch) //] | #lin #io #lout * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio [ #H cases(bind_inversion ????? H) -H #newstore * #EQnewstore ] whd in ⊢ (??%% → ?); #EQ destruct [ @(vm_io_out … EQfetch) // | @(vm_io_in … EQfetch) // ] | #f * #EQfetch inversion(asm_is_io ???) #EQio normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct ] #H cases (bind_inversion ????? H) -H #lbl * #EQlb whd in ⊢ (??%% → ?); #EQ destruct @(vm_call … EQfetch) // | * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H * #newpc #tl * whd in match option_pop; normalize nodelta inversion(asm_stack ???) normalize nodelta [#_ whd in ⊢ (??%% → ?); #EQ destruct] #newpc1 #tl1 #_ #EQstack whd in ⊢ (??%% → ?); #EQ destruct #H cases(bind_inversion ????? H) #lbl * #EQlbl whd in ⊢ (??%% → ?); #EQ destruct @vm_ret // ] qed. lemma vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 → eval_vmstate p p' prog st1 = return 〈l,st2〉. #p #p' #prog * #pc1 #stack1 #store1 #io1 #cost1 * #pc2 #stack2 #store2 #io2 #cost2 #l #H inversion H [ #s1 #s2 #i #opt_l #EQfetch #EQio #EQstore #EQstack #EQio1 #EQpc #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio normalize nodelta >EQstore >m_return_bind EQio EQstack >EQcost % | #s1 #s2 #newpc #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta EQio1 >EQstore >EQstack EQstore % |3,4: #s1 #s2 #cond #newoc #ltrue #lfalse #EQev_cond #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewoc #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta >EQev_cond >m_return_bind normalize nodelta EQio2 >EQstore >EQstack EQstore [%] >EQnewoc % |5,6: #s1 #s2 #lin #io #lout #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQpc #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta >EQstack EQcost [ >EQstore EQstore >m_return_bind EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta >EQlab_pc >m_return_bind >EQentry >EQcost EQio1 EQstore % | #s1 #s2 #newpc #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc #EQlab_pc #EQcosts #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta >EQstack whd in match option_pop; normalize nodelta >m_return_bind >EQlab_pc >m_return_bind >EQcosts >EQstore EQio1 % ] qed. coercion vm_step_to_eval. include "../src/utilities/hide.ma". discriminator option. definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p → abstract_status ≝ λp,p',prog.mk_abstract_status (vm_state p p') (λl.λst1,st2 : vm_state p p'.(eqb (pc ?? st1) (endmain … prog)) = false ∧ vmstep p p' prog l st1 st2) (λ_.λ_.True) (λs.match fetch … prog (pc … s) with [ Some i ⇒ match i with [ Seq _ _ ⇒ cl_other | Ijmp _ ⇒ cl_other | CJump _ _ _ _ ⇒ cl_jump | Iio _ _ _ ⇒ if asm_is_io … s then cl_io else cl_other | Icall _ ⇒ cl_other | Iret ⇒ cl_other ] | None ⇒ cl_other ] ) (λ_.true) (λs.eqb (pc ?? s) O) (λs.eqb (pc … s) (endmain … prog)) ???. @hide_prf [ #s1 #s2 #l inversion(fetch ???) normalize nodelta [ #_ #EQ destruct] * normalize nodelta [ #seq #lbl #_ | #n #_ | #cond #newpc #ltrue #lfalse #EQfetch | #lin #io #lout #_ cases (asm_is_io ??) normalize nodelta | #f #_ | #_ ] #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind normalize nodelta cases(asm_is_io ??) normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H * * #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct % // | #s1 #s2 #l inversion(fetch ???) normalize nodelta [ #_ #EQ destruct] * normalize nodelta [ #seq #lbl #_ | #n #_ | #cond #newpc #ltrue #lfalse #_ | #lin #io #lout #EQfetch inversion (asm_is_io ??) #EQio normalize nodelta | #f #_ | #_ ] #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate; normalize nodelta #H cases(bind_inversion ????? H) -H * [ #seq1 #lbl1 | #n1 | #cond1 #newpc1 #ltrue1 #lfalse1 | #lin1 #io1 #lout1 | #f | ] normalize nodelta * #_ cases(asm_is_io ??) normalize nodelta [1,3,5,9,11: whd in ⊢ (??%% → ?); #EQ destruct |2,6,7,10,12: #H cases(bind_inversion ????? H) -H #x * #_ [2: cases x normalize nodelta |5: #H cases(bind_inversion ????? H) -H #y * #_ ] ] whd in ⊢ (??%% → ?); #EQ destruct destruct % // | #s1 #s2 #l inversion(fetch ???) normalize nodelta [ #_ #EQ destruct] * normalize nodelta [ #seq #lbl #_ | #n #_ | #cond #newpc #ltrue #lfalse #_ | #lin #io #lout #EQfetch inversion(asm_is_io ??) normalize nodelta #EQio | #f #_ | #_ ] #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio normalize nodelta #H cases(bind_inversion ????? H) -H #x * #_ whd in ⊢ (??%% → ?); #EQ destruct % // qed. definition asm_concrete_trans_sys ≝ λp,p',prog.mk_concrete_transition_sys … (asm_operational_semantics p p' prog) (m … p') (cost …). definition emits_labels ≝ λp.λinstr : AssemblerInstr p.match instr with [ Seq _ opt_l ⇒ match opt_l with [ None ⇒ Some ? (λpc.S pc) | Some _ ⇒ None ? ] | Ijmp newpc ⇒ Some ? (λ_.newpc) | _ ⇒ None ? ]. definition fetch_state : ∀p,p'.AssemblerProgram p → vm_state p p' → option (AssemblerInstr p) ≝ λp,p',prog,st.fetch … prog (pc … st). definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m. mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t … (fetch_state p p' prog) instr_m. definition non_empty_list : ∀A.list A → bool ≝ λA,l.match l with [ nil ⇒ false | _ ⇒ true ]. let rec block_cost (p : assembler_params) (prog: AssemblerProgram p) (abs_t : monoid) (instr_m : AssemblerInstr p → abs_t) (program_counter: ℕ) (program_size: ℕ) on program_size: option abs_t ≝ match program_size with [ O ⇒ None ? | S program_size' ⇒ if eqb program_counter (endmain … prog) then return e … abs_t else ! instr ← fetch … prog program_counter; ! n ← (match emits_labels … instr with [ Some f ⇒ block_cost … prog abs_t instr_m (f program_counter) program_size' | None ⇒ return e … ]); return (op … abs_t (instr_m … instr) n) ]. record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝ { map_type :> Type[0] ; empty_map : map_type ; get_map : map_type → dom → option codom ; set_map : map_type → dom → codom → map_type ; get_set_hit : ∀k,v,m.get_map (set_map m k v) k = return v ; get_set_miss : ∀k1,k2,v,m.(k1 == k2) = false → get_map (set_map m k1 v) k2 = get_map m k2 }. definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (CostLabel × ℕ) ≝ λp,i,program_counter. match i with [ Seq _ opt_l ⇒ match opt_l with [ Some lbl ⇒ [〈(a_non_functional_label lbl),S program_counter〉] | None ⇒ [ ] ] | Ijmp _ ⇒ [ ] | CJump _ newpc ltrue lfalse ⇒ [〈(a_non_functional_label ltrue),newpc〉; 〈(a_non_functional_label lfalse),S program_counter〉] | Iio lin _ lout ⇒ [〈(a_non_functional_label lin),program_counter〉; 〈(a_non_functional_label lout),S program_counter〉] | Icall f ⇒ [ ] | Iret ⇒ [ ] ]. let rec labels_pc (p : assembler_params) (prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝ match prog with [ nil ⇒ [〈i_act,O〉] @ map … (λx.let〈y,z〉 ≝ x in 〈(a_call z),y〉) (call_label_fun … p) @ map … (λx.let〈y,z〉 ≝ x in 〈(a_return_post z),y〉) (return_label_fun … p) | cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is (S program_counter) ]. lemma labels_pc_ok : ∀p,prog,i,lbl,pc,m. fetch p prog pc = return i → mem ? lbl (labels_pc_of_instr … i (m+pc)) → mem ? lbl (labels_pc p (instructions … prog) m). #p * #instrs #end_main #Hend_main #i #lbl #pc whd in match fetch; normalize nodelta lapply pc -pc -end_main elim instrs [ #pc #m whd in ⊢ (??%% → ?); #EQ destruct] #x #xs #IH * [|#pc'] #m whd in ⊢ (??%% → ?); [ #EQ destruct #lbl_addr whd in match (labels_pc ???); /2 by mem_append_l1/ | #EQ #H2 whd in match (labels_pc ???); @mem_append_l2 @(IH … EQ) // ] qed. lemma labels_pc_return: ∀p,prog,x1,x2. label_of_pc ReturnPostCostLabel (return_label_fun p) x1=return x2 → ∀m. mem … 〈(a_return_post x2),x1〉 (labels_pc p (instructions p prog) m). #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l [ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?); elim (return_label_fun ?) in H; [ whd in ⊢ (??%% → ?); #EQ destruct] * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim normalize nodelta [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/ | #NEQ #H2 %2 @IH // ] | #hd #tl #IH #m @mem_append_l2 @IH ] qed. lemma labels_pc_call: ∀p,prog,x1,x2. label_of_pc CallCostLabel (call_label_fun p) x1=return x2 → ∀m. mem … 〈(a_call x2),x1〉 (labels_pc p (instructions p prog) m). #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l [ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?); elim (call_label_fun ?) in H; [ whd in ⊢ (??%% → ?); #EQ destruct] * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim normalize nodelta [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/ | #NEQ #H2 %2 @IH // ] | #hd #tl #IH #m @mem_append_l2 @IH ] qed. (* lemma labels_pc_bounded : ∀p.∀prog : AssemblerProgram p.∀lbl,pc.∀m. mem ? 〈lbl,pc〉 (labels_pc p (instructions … prog) m) → (m + pc) < (|(instructions … prog)|). #p * #instr #endmain #_ #H1 #H2 elim instr [ #H3 @⊥ /2/ ] #x #xs #IH #_ #lbl #pc #m whd in match (labels_pc ???); #H cases(mem_append ???? H) -H [ whd in match labels_pc_of_instr; normalize nodelta cases x normalize nodelta [ #seq * [|#lab] | #newpc | #cond #newpc #ltrue #lfalse | #lin #io #lout | #f | ] normalize [1,3,6,7: *] * [2,4,6: * [2,4:*] ] #EQ destruct *) let rec m_foldr (M : Monad) (X,Y : Type[0]) (f : X→Y→M Y) (l : list X) (y : Y) on l : M Y ≝ match l with [ nil ⇒ return y | cons x xs ⇒ ! z ← m_foldr M X Y f xs y; f x z ]. definition static_analisys : ∀p : assembler_params.∀abs_t : monoid.(AssemblerInstr p → abs_t) → ∀mT : cost_map_T DEQCostLabel abs_t.AssemblerProgram p → option mT ≝ λp,abs_t,instr_m,mT,prog. let prog_size ≝ S (|instructions … prog|) in m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m w prog_size; return set_map … m z k) (labels_pc … (instructions … prog) O) (empty_map ?? mT). include "basics/lists/listb.ma". (*doppione da mettere a posto*) let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝ match l with [ nil ⇒ True | cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs ]. definition asm_no_duplicates ≝ λp,prog.no_duplicates … (map ?? \fst … (labels_pc … (instructions p prog) O)). (*falso: necessita di no_duplicates*) definition eq_deq_prod : ∀D1,D2 : DeqSet.D1 × D2 → D1 × D2 → bool ≝ λD1,D2,x,y.\fst x == \fst y ∧ \snd x == \snd y. definition DeqProd ≝ λD1 : DeqSet.λD2 : DeqSet. mk_DeqSet (D1 × D2) (eq_deq_prod D1 D2) ?. @hide_prf * #x1 #x2 * #y1 #y2 whd in match eq_deq_prod; normalize nodelta % [2: #EQ destruct @andb_Prop >(\b (refl …)) %] inversion (? ==?) #EQ1 whd in match (andb ??); #EQ2 destruct >(\P EQ1) >(\P EQ2) % qed. (* unification hint 0 ≔ D1,D2 ; X ≟ DeqProd D1 D2 (* ---------------------------------------- *) ⊢ D1 × D2 ≡ carr X. unification hint 0 ≔ D1,D2,p1,p2; X ≟ DeqProd D1 D2 (* ---------------------------------------- *) ⊢ eq_deq_prod D1 D2 p1 p2 ≡ eqb X p1 p2. definition deq_prod_to_prod : ∀D1,D2 : DeqSet.DeqProd D1 D2 → D1 × D2 ≝ λD1,D2,x.x. coercion deq_prod_to_prod. *) lemma map_mem : ∀A,B,f,l,a.mem A a l → ∃b : B.mem B b (map A B f l) ∧ b = f a. #A #B #f #l elim l [ #a *] #x #xs #IH #a * [ #EQ destruct %{(f x)} % // % // | #H cases(IH … H) #b * #H1 #EQ destruct %{(f a)} % // %2 // ] qed. lemma static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map. asm_no_duplicates p prog → static_analisys p abs_t instr_m mT prog = return map → mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) O) → get_map … map lbl = block_cost … prog abs_t instr_m pc (S (|(instructions … prog)|)) ∧ block_cost … prog abs_t instr_m pc (S (|(instructions … prog)|)) ≠ None ?. #p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta whd in match asm_no_duplicates; normalize nodelta lapply (labels_pc ???) #l #endmain #Hendmain elim l [ #x #y #z #w #h * ] * #hd1 #hd2 #tl #IH #lbl #pc #map * #H1 #H2 #H cases(bind_inversion ????? H) -H #map1 * #EQmap1 normalize nodelta #H cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); #EQ destruct * [ #EQ destruct % [ >get_set_hit >EQelem % | >EQelem % whd in ⊢ (??%% → ?); #EQ destruct] | #H % [ >get_set_miss [ @(proj1 … (IH …)) //] inversion (? == ?) [2: #_ %] #ABS cases H1 -H1 #H1 @⊥ @H1 >(\P ABS) >mem_to_memb // cases(map_mem … \fst … H) #z1 * #Hz1 #EQ destruct @Hz1 | @(proj2 … (IH …)) // ] ] qed. include "Simulation.ma". record terminated_trace (S : abstract_status) (R_s2 : S) : Type[0] ≝ { R_post_step : option (ActionLabel × S) ; R_fin_ok : match R_post_step with [ None ⇒ bool_to_Prop (as_final … R_s2) | Some x ⇒ let 〈l,R_post_state〉≝ x in (is_costlabelled_act l ∨ is_labelled_ret_act l) ∧ (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧ as_execute … l R_s2 R_post_state ] }. definition big_op: ∀M: monoid. list M → M ≝ λM. foldl … (op … M) (e … M). lemma big_op_associative: ∀M:monoid. ∀l1,l2. big_op M (l1@l2) = op M (big_op … l1) (big_op … l2). #M #l1 whd in match big_op; normalize nodelta generalize in match (e M) in ⊢ (? → (??%(??%?))); elim l1 [ #c #l2 whd in match (append ???); normalize lapply(neutral_r … c) generalize in match c in ⊢ (??%? → ???%); lapply c -c lapply(e M) elim l2 normalize [ #c #c1 #c2 #EQ @sym_eq // | #x #xs #IH #c1 #c2 #c3 #EQ act_neutral // | #hd #tl #IH #l2 #x change with ([?]@(tl@l2)) in match ([?]@(tl@l2)); >big_op_associative >act_op >IH change with ([hd]@tl) in match ([hd]@tl); >big_op_associative >act_op in ⊢ (???%); % ] qed. lemma monotonicity_of_block_cost : ∀p,prog,abs_t,instr_m,pc,size,k. block_cost p prog abs_t instr_m pc size = return k → ∀size'.size ≤ size' → block_cost p prog abs_t instr_m pc size' = return k. #p #prog #abs_t #instr_m #pc #size lapply pc elim size [ #pc #k whd in ⊢ (??%% → ?); #EQ destruct] #n #IH #pc #k whd in ⊢ (??%% → ?); @eqb_elim [ #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct #size' * [2: #m #_] whd in ⊢ (??%%); @eqb_elim try( #_ %) * #H @⊥ @H % | #Hpc normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi #H cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); #EQ destruct #size' * [ whd in ⊢ (??%?); @eqb_elim [ #EQ @⊥ @(absurd ?? Hpc) assumption ] #_ normalize nodelta >EQi >m_return_bind >EQelem % | #m #Hm whd in ⊢ (??%?); @eqb_elim [ #EQ @⊥ @(absurd ?? Hpc) assumption ] #_ normalize nodelta >EQi >m_return_bind cases (emits_labels ??) in EQelem; normalize nodelta [ whd in ⊢ (??%%→ ??%%); #EQ destruct %] #f #EQelem >(IH … EQelem) [2: /2/ ] % ] ] qed. lemma step_emit : ∀p,p',prog,st1,st2,l,i. fetch p prog (pc … st1) = return i → eval_vmstate p p' … prog st1 = return 〈l,st2〉 → emits_labels … i = None ? → ∃x. match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with  [call_act f c ⇒ [a_call c] |ret_act x ⇒ match x with [None⇒[]|Some c⇒[a_return_post c]] |cost_act x ⇒ match x with [None⇒[]|Some c⇒[a_non_functional_label c]] ] = [x] ∧ (mem … 〈x,pc … st2〉 (labels_pc p (instructions … prog) O)). #p #p' #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta >EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta [ #seq * [|#lab] | #newpc | #cond #newpc #ltrue #lfalse | #lin #io #lout | #f | ] #EQi cases(asm_is_io ???) normalize nodelta [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1 [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2 ] ] whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels; normalize nodelta #EQ destruct % [2,4,6,8,10,12,14: % try % |*:] [1,2,4,5,7: @(labels_pc_ok … EQi) normalize /3 by or_introl,or_intror/ ] /2 by labels_pc_return, labels_pc_call/ qed. lemma step_non_emit : ∀p,p',prog,st1,st2,l,i,f. fetch p prog (pc … st1) = return i → eval_vmstate p p' … prog st1 = return 〈l,st2〉 → emits_labels … i = Some ? f → match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with  [call_act f c ⇒ [a_call c] |ret_act x ⇒ match x with [None⇒[]|Some c⇒[a_return_post c]] |cost_act x ⇒ match x with [None⇒[]|Some c⇒[a_non_functional_label c]] ] = [ ] ∧ pc … st2 = f (pc … st1). #p #p' #prog #st1 #st2 #l #i #f #EQi whd in match eval_vmstate; normalize nodelta >EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta [ #seq * [|#lab] | #newpc | #cond #newpc #ltrue #lfalse | #lin #io #lout | #f | ] #EQi cases(asm_is_io ???) normalize nodelta [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1 [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2 ] ] whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels; normalize nodelta #EQ destruct /2 by refl, conj/ qed. lemma labels_of_trace_are_in_code : ∀p,p',prog.∀st1,st2 : vm_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2. ∀lbl. mem … lbl (get_costlabels_of_trace … t) → mem … (lbl) (map ?? \fst … (labels_pc … (instructions p prog) O)). #p #p' #prog #st1 #st2 #t elim t [ #st #lbl * | #st1 #st2 #st3 #l * #H1 #H2 #tl #IH #lbl whd in match (get_costlabels_of_trace ????); #H cases(mem_append ???? H) -H [2: #H @IH //] lapply(vm_step_to_eval … H2) whd in match eval_vmstate; normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi #_ inversion(emits_labels … i) [ #EQemit cases(step_emit … (vm_step_to_eval … H2)) // #x * #EQ1 #EQ2 >EQ1 * [2: *] #EQ destruct cases(map_mem … \fst … EQ2) #y * #H3 #EQ destruct // | #f #EQemit >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H2) … EQemit)) * ] ] qed. let rec dependent_map (A,B : Type[0]) (l : list A) (f : ∀a : A.mem … a l → B) on l : list B ≝ (match l return λx.l=x → ? with [ nil ⇒ λ_.nil ? | cons x xs ⇒ λprf.(f x ?) :: dependent_map A B xs (λx,prf1.f x ?) ])(refl …). [ >prf %% | >prf %2 assumption] qed. lemma dependent_map_append : ∀A,B,l1,l2,f. dependent_map A B (l1 @ l2) (λa,prf.f a prf) = (dependent_map A B l1 (λa,prf.f a ?)) @ (dependent_map A B l2 (λa,prf.f a ?)). [2: @hide_prf /2/ | 3: @hide_prf /2/] #A #B #l1 elim l1 normalize /2/ qed. lemma rewrite_in_dependent_map : ∀A,B,l1,l2,f. ∀EQ:l1 = l2. dependent_map A B l1 (λa,prf.f a prf) = dependent_map A B l2 (λa,prf.f a ?). [2: >EQ // | #A #B #l1 #l2 #f #EQ >EQ in f; #f % ] qed. lemma static_dynamic : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog. ∀abs_t : abstract_transition_sys (m … p').∀instr_m. ∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1. ∀EQmap : static_analisys p ? instr_m mT prog = return map1. ∀st1,st2 : vm_state p p'. ∀ter : terminated_trace (asm_operational_semantics p p' prog) st2. ∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2. ∀k. pre_measurable_trace … t → block_cost p prog … instr_m (pc … st1) (S (|(instructions … prog)|)) = return k → ∀a1.rel_galois … good st1 a1 → let stop_state ≝ match R_post_step … ter with [None ⇒ st2 | Some x ⇒ \snd x ] in ∀costs. costs = dependent_map CostLabel ? (get_costlabels_of_trace … t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) → rel_galois … good stop_state (act_abs … abs_t (big_op … costs) (act_abs … abs_t k a1)). [2: @hide_prf cases(mem_map ????? (labels_of_trace_are_in_code … prf)) * #lbl' #pc * #Hmem #EQ destruct >(proj1 … (static_analisys_ok … no_dup … EQmap … Hmem)) @(proj2 … (static_analisys_ok … no_dup … EQmap … Hmem)) ] #p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t lapply ter -ter elim t [ #st #ter inversion(R_post_step … ter) normalize nodelta [| * #lbl #st3 ] #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) #a1 #rel_st_a1 whd in match (map ????); #costs #EQ >EQ >act_neutral >act_neutral assumption | ** #H1 #H2 * #H3 #H4 whd in ⊢ (??%% → ?); >H3 normalize nodelta #H cases(bind_inversion ????? H) -H * [ #seq * [|#lbl1] | #newpc | #cond #newpc #ltrue #lfalse | #lin #io #lout | #f | ] * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind normalize nodelta cases(asm_is_io ??) normalize nodelta [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_ [3: cases x normalize nodelta |6: #H cases(bind_inversion ????? H) -H #y * #_ ] ] whd in ⊢ (??%% → ?); #EQ destruct [4,8: cases H1 [1,3: * |*: * #y #EQ destruct]] >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ >EQ >neutral_r >act_neutral @(instr_map_ok … good … EQfetch … good_st_a1) /2/ ] | -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????); whd #costs >dependent_map_append (*change with (list_cost_to_list_initcost ?) in match (list_cost_to_list_initcost ?);*) #EQ destruct whd in H2 : (??%?); lapply H2 >H3 in ⊢ (% → ?); -H2 normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi inversion(emits_labels ??) [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct >big_op_associative >act_op @IH | #f #EQemits normalize nodelta #H cases(bind_inversion ????? H) -H #k' * #EQk' whd in ⊢ (??%% → ?); #EQ destruct(EQ) >act_op whd in match (append ???); @IH ] [1,5: inversion H in ⊢ ?; [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H * ] // | cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx >(rewrite_in_dependent_map … EQx) whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??); >neutral_l @opt_safe_elim #elem #EQget cases (static_analisys_ok … x … (pc … st2) … no_dup … EQmap) // #EQ #_ neutral_r @(instr_map_ok … good … EQi … good_a1) /2/ | % | >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) >(monotonicity_of_block_cost … EQk') // | @(instr_map_ok … good … EQi … good_a1) /2/ | lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) #EQ >(rewrite_in_dependent_map … EQ) % ] ] qed. definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝ λa.match a with [ call_act f l ⇒ [a_call l] | ret_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_return_post l]] | cost_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_non_functional_label l]] ]. definition get_costlabels_of_measurable_trace : ∀S : abstract_status.measurable_trace S → list CostLabel ≝ λS,t. match L_label … t with [ None ⇒ [i_act] | Some l ⇒ actionlabel_to_costlabel l ] @ get_costlabels_of_trace … (trace … t). (*get_costlabels_of_measurable_trace deve aggiungere la label iniziale.*) theorem static_dynamic_meas : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog. ∀abs_t : abstract_transition_sys (m … p').∀instr_m. ∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1. ∀EQmap : static_analisys p ? instr_m mT prog = return map1. ∀t : measurable_trace (asm_operational_semantics p p' prog). ∀a1.rel_galois … good (L_s1 … t) a1 → let stop_state ≝ match R_post_state … t with [None ⇒ R_s2 … t | Some x ⇒ x ] in ∀abs_trace. abs_trace = dependent_map CostLabel ? (get_costlabels_of_measurable_trace … t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) → rel_galois … good stop_state (act_abs … abs_t (big_op … abs_trace) a1). [2: @hide_prf whd in match get_costlabels_of_measurable_trace in prf; normalize nodelta in prf; cases(mem_append ???? prf) -prf [2: #prf cases(mem_map ????? (labels_of_trace_are_in_code … prf)) * #lbl' #pc * #Hmem #EQ destruct >(proj1 … (static_analisys_ok … no_dup … EQmap … Hmem)) @(proj2 … (static_analisys_ok … no_dup … EQmap … Hmem)) | inversion(L_label … t) normalize nodelta [| #lbl'] #EQleft [ * [2: *] #EQ destruct cases daemon (* i_act sta sempre nel codice *) | (* per inversione su as_execute *) cases daemon ] ] ] #p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap1 #t #a1 #rel_galois #abs_trace #EQabs_trace xxxxxx lapply(static_dynamic … (trace …t) … abs_trace) try //