Changeset 2760


Ignore:
Timestamp:
Mar 2, 2013, 1:29:41 AM (7 years ago)
Author:
sacerdot
Message:
  1. Many files repaired.
  2. 3 new daemons: 2 in Assembly.ma, 1 in StructuredTraces?.ma
Location:
src
Files:
11 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2757 r2760  
    11021102; code : list labelled_instruction
    11031103; renamed_symbols : list (Identifier × ident)
    1104 ; final_index : Word
     1104; final_label : Identifier
    11051105(* properties *)
    11061106; asm_injective_costlabels :
     
    11131113definition symboltable_type ≝ BitVectorTrie ident 16.
    11141114record labelled_object_code : Type[0] ≝
    1115 { oc :> object_code
     1115{ oc : object_code
    11161116; costlabels : costlabel_map
    11171117; symboltable : symboltable_type
  • src/ASM/ASMCosts.ma

    r2756 r2760  
    1414    mk_abstract_status
    1515      (Status code_memory)
    16       (λs. return (execute_1 … s))
    17       ?
     16      (λs1,s2. execute_1 … s1 = s2)
    1817      word_deqset
    1918      (program_counter …)
     
    391390      ]
    392391    ]
    393   change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;
     392  change with (ASM_classify0 ? = ?) in classifier_assm;
    394393  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    395394  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     
    450449    #final_status_refl #the_trace_refl destruct @⊥
    451450  ]
    452   change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;
     451  change with (ASM_classify0 ? = ?) in classifier_assm;
    453452  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    454453  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     
    587586    ]
    588587  ]
    589   try (change with (Some ? (ASM_classify0 ?) = ? ∨ Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
    590   try (change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
     588  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
     589  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
    591590  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    592591  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     
    636635    #classifier_assm
    637636    destruct @⊥
    638     change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;
     637    change with (ASM_classify0 ? = ?) in classifier_assm;
    639638    cases (current_instruction ??) in classifier_assm;
    640639    [7: #preinstruction cases preinstruction ]
    641     try(#addr1 #addr2 #absurd destruct(absurd))
    642     try(#addr #absurd destruct(absurd))
    643     #absurd destruct(absurd)
     640    try(#addr1 #addr2 #absurd normalize in absurd; destruct(absurd))
     641    try(#addr #absurd normalize in absurd; destruct(absurd))
     642    #absurd normalize in absurd; destruct(absurd)
    644643  |5:
    645644    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     
    653652    #final_status_refl #the_trace_refl destruct @⊥
    654653  ]
    655   try (change with (Some ? (ASM_classify0 ?) = ? ∨ Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
    656   try (change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
     654  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
     655  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
    657656  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    658657  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
  • src/ASM/ASMCostsSplit.ma

    r2754 r2760  
    11include "ASM/ASMCosts.ma".
    22include "ASM/UtilBranch.ma".
     3include alias "ASM/Arithmetic.ma".
    34include alias "arithmetics/nat.ma".
    45include alias "basics/logic.ma".
     
    329330definition ASM_cost_map :
    330331  ∀p: labelled_object_code.
    331   let code_memory ≝ load_code_memory (\fst p) in
    332   let a_s ≝ ASM_abstract_status code_memory (\fst (\snd p)) in
    333   ? → as_cost_map a_s ≝
     332  let code_memory ≝ load_code_memory (oc p) in
     333  let a_s ≝ ASM_abstract_status code_memory (costlabels p) in
     334  as_cost_map a_s ≝
    334335  λp.
    335   λcost_labels_injective.
    336   let cost_map ≝ compute_costs (\fst p) (\fst (\snd p)) cost_labels_injective in
     336  let cost_map ≝ compute_costs (oc p) (costlabels p) (oc_injective_costlabels … p) in
    337337  λl_sig.
    338338  lookup_present … cost_map (as_cost_get_label ? l_sig) ?.
  • src/ASM/Assembly.ma

    r2754 r2760  
    642642  λpolicy: Word → bool.
    643643  sigma (zero …) = zero … ∧
    644   let instr_list ≝ \snd program in
    645   let preamble ≝ \fst program in
     644  let instr_list ≝ code program in
     645  let preamble ≝ preamble program in
    646646  ∀ppc: Word. ∀ppc_ok: nat_of_bitvector … ppc < |instr_list|.
    647647    let pc ≝ sigma ppc in
     
    810810      Σres:labelled_object_code.
    811811       sigma_policy_specification p sigma policy →
    812        let 〈preamble,instr_list〉 ≝ p in
     812       let preamble ≝ preamble p in
     813       let instr_list ≝ code p in
    813814       |instr_list| ≤ 2^16 →
    814        let 〈assembled,costs〉 ≝ res in
     815       let assembled ≝ oc res in
    815816       |assembled| ≤ 2^16 ∧
    816817       (nat_of_bitvector … (sigma (bitvector_of_nat … (|instr_list|))) = |assembled| ∨
     
    833834  λsigma.
    834835  λpolicy.
    835   deplet 〈preamble, instr_list〉 as p_refl ≝ p in
    836   deplet 〈labels_to_ppc,ppc_to_costs〉 as eq_create_label_cost_map ≝ create_label_cost_map instr_list in
     836  deplet 〈labels_to_ppc,ppc_to_costs〉 as eq_create_label_cost_map ≝ create_label_cost_map (code p) in
     837  let preamble ≝ preamble p in
     838  let instr_list ≝ code p in
    837839  let datalabels ≝ construct_datalabels preamble in
    838840  let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
     
    842844      (option Identifier × pseudo_instruction)
    843845      (λpre. Σppc_code:(Word × (list Byte)).
    844        sigma_policy_specification 〈preamble,instr_list〉 sigma policy →
     846       sigma_policy_specification p sigma policy →
    845847        |instr_list| ≤ 2^16 →
    846848        let 〈ppc,code〉 ≝ ppc_code in
     
    870872      〈(zero ?), [ ]〉)
    871873    in
    872      〈reverse … revcode,
    873       〈fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??),
    874        foldl ??
    875         (λsymboltable,newident_oldident.
    876           let ppc ≝ lookup_labels (\fst newident_oldident) in
    877            insert … (sigma ppc) (\snd newident_oldident) symboltable) (Stub ??) (\snd preamble)〉〉.
     874     mk_labelled_object_code
     875     (reverse … revcode)
     876     (fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??))
     877     (foldl ??
     878      (λsymboltable,newident_oldident.
     879        let ppc ≝ lookup_labels (\fst newident_oldident) in
     880         insert … (sigma ppc) (\snd newident_oldident) symboltable) (Stub ??) (renamed_symbols p))
     881     ? ?.
    878882  [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode
    879883    >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok
     
    887891      [ #Hfold5 <Hfold5 % >Hfold1 %
    888892      | * #Hfold51 #Hfold52 %2 <Hfold1 assumption ]]
     893  | cases daemon
     894  | cases daemon
    889895  | * #sigma_pol_ok1 #_ #instr_list_ok %
    890896    [ % % [%] // >sigma_pol_ok1 % ]
     
    970976      [3: @le_S_S @le_O_n
    971977      |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H
    972       |4: <prf <p_refl in instr_list_ok; #H @H ]
     978      |4: <prf @instr_list_ok ]
    973979      #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2 %
    974980      [ >length_reverse >length_append >length_reverse // ]
  • src/ASM/CostsProof.ma

    r2754 r2760  
    451451 ]
    452452qed.
    453    
     453
    454454let rec compute_trace_label_return_using_paid_ok_with_trace
    455455 (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
     
    504504  | #si #sl #sf #tr1 #tr2 #unrepeating_witness #dom_codom
    505505    whd in ⊢ (??%?);
    506     whd in match (flatten_trace_label_return ????);
     506    whd in match flatten_trace_label_return; normalize nodelta
     507    whd in match (observables_trace_label_return ?????);
     508    >costlabels_of_observables_append
    507509    >append_length >bigop_sum_rev >commutative_plus @eq_f2
    508510    [ >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
     
    565567    #classifier_assm #after_return_assm #trace_label_return #costed_assm #unrepeating_witness
    566568    whd in ⊢ (??%?);
    567     @(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
    568     assumption
     569    >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
     570    //
     571    whd in match flatten_trace_any_label; normalize nodelta
     572    whd in match (observables_trace_any_label ??????);
     573    >(costlabels_of_observables_append … [?]) [2: normalize /2/]
     574    >length_append whd in match (? + ?);
     575    whd in match flatten_trace_label_return; normalize nodelta
     576    >costlabels_of_observables_trace_label_return_id_irrelevant //
    569577  |6:
    570578    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    571579    #classifier_assm #trace_label_return #unrepeating_witness
    572580    whd in ⊢ (??%?);
    573     @(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
    574     assumption
     581    >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
     582    //
     583    whd in match flatten_trace_any_label; normalize nodelta
     584    whd in match (observables_trace_any_label ??????);
     585    >(costlabels_of_observables_append … [?]) [2: normalize /2/]
     586    >length_append whd in match (? + ?);
     587    whd in match flatten_trace_label_return; normalize nodelta
     588    >costlabels_of_observables_trace_label_return_id_irrelevant //
    575589  |7:
    576590    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     
    582596      >(compute_trace_any_label_using_paid_ok_with_trace … cost_map … codom_dom … dom_codom)
    583597      [1:
     598        whd in match flatten_trace_any_label in ⊢ (???%); normalize nodelta
     599        whd in match (observables_trace_any_label ??????);
     600        >costlabels_of_observables_append
     601        >(costlabels_of_observables_append … [?]) [2: normalize /2/]
    584602        >length_append >bigop_sum_rev >commutative_plus @eq_f2
    585603        [ @same_bigop [2: #i #H #_ -dom_codom @tech_cost_of_label_shift assumption
    586604                      |1: #i #H % ]
    587         | @same_bigop [#i #H %] #i #H #_ @(tech_cost_of_label_prefix … H)
     605        | >length_append whd in match (|?|+?);
     606          >costlabels_of_observables_trace_label_return_id_irrelevant
     607          [@same_bigop [#i #H %] #i #H #_ @(tech_cost_of_label_prefix … H) | skip]
    588608        ]
    589609      |2:
     
    674694lemma tech_cost_sum_eq_as_cost :
    675695  ∀compiled_code: labelled_object_code.
    676   let cost_labels ≝ \fst (\snd compiled_code) in
    677   ∀cost_labels_injective:
    678    (∀pc,pc',l.
    679      lookup_opt … pc cost_labels = Some … l
    680      → lookup_opt … pc' cost_labels = Some … l → pc = pc').
    681   let cost_map ≝ compute_costs (\fst compiled_code) (\fst (\snd compiled_code)) cost_labels_injective in
     696  let cost_labels ≝ costlabels compiled_code in
     697  let cost_map ≝ compute_costs (oc compiled_code) (costlabels compiled_code) (oc_injective_costlabels compiled_code) in
    682698  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … k).
    683699  ∀trace.
    684700  (Σ_{i < |trace|}(tech_cost_of_label cost_labels (map_of_sigma_map … cost_map) codom_dom trace i)) =
    685   (Σ_{l ∈ trace}(ASM_cost_map compiled_code cost_labels_injective l)).
    686 * #ccode1 #ccode2 #cost_labels_injective #codom_dom #trace
     701  (Σ_{l ∈ trace}(ASM_cost_map compiled_code l)).
     702#ccode #codom_dom #trace
    687703@(list_elim_left … trace)
    688704[ %
     
    692708  <tech_cost_of_label_shift [2: //]
    693709  cut (∀x,y,z,w.x = y → z = w → x + z = y + w) [ // ] #APP @APP -APP
    694   [ cases tl -tl #tl #Htl
    695     change with (lookup_present ????? = ?)
    696     whd in ⊢ (???(%???)); normalize nodelta
    697     generalize in ⊢ (???(?????%)); #p
    698     @costlabel_map_of_as_cost_labels_map_ok
     710  [ cases tl -tl #tl #Htl @costlabel_map_of_as_cost_labels_map_ok
    699711  | @sym_eq @same_bigop /2 by tech_cost_of_label_prefix/
    700712  ]
  • src/ASM/Interpret.ma

    r2756 r2760  
    11931193  let s ≝
    11941194    match instr with
    1195     [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels (\snd cm) x) instr s
     1195    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels (code cm) x) instr s
    11961196    | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
    11971197    | Cost cst ⇒ s
    11981198    | Jmp jmp ⇒
    11991199       let s ≝ set_clock … s (\fst ticks + clock … s) in
    1200         set_program_counter … s (address_of_word_labels (\snd cm) jmp)
     1200        set_program_counter … s (address_of_word_labels (code cm) jmp)
    12011201    | Jnz acc dst1 dst2 ⇒
    12021202       if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
    12031203        let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    1204          set_program_counter … s (address_of_word_labels (\snd cm) dst1)
     1204         set_program_counter … s (address_of_word_labels (code cm) dst1)
    12051205       else
    12061206        let s ≝ set_clock ?? s (\snd ticks + clock … s) in
    1207          set_program_counter … s (address_of_word_labels (\snd cm) dst2)
     1207         set_program_counter … s (address_of_word_labels (code cm) dst2)
    12081208    | MovSuccessor dst ws lbl ⇒
    12091209      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    1210       let addr ≝ address_of_word_labels (\snd cm) lbl in
     1210      let addr ≝ address_of_word_labels (code cm) lbl in
    12111211      let 〈high, low〉 ≝ vsplit ? 8 8 addr in
    12121212      let v ≝ match ws with [ HIGH ⇒ high | LOW ⇒ low ] in
     
    12141214    | Call call ⇒
    12151215      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    1216       let a ≝ address_of_word_labels (\snd cm) call in
     1216      let a ≝ address_of_word_labels (code cm) call in
    12171217      let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    12181218      let s ≝ set_8051_sfr … s SFR_SP new_sp in
     
    12251225    | Mov dptr ident ⇒
    12261226      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    1227       let the_preamble ≝ \fst cm in
     1227      let the_preamble ≝ preamble cm in
    12281228      let data_labels ≝ construct_datalabels the_preamble in
    12291229        set_arg_16 … s (get_arg_16 … s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
     
    12351235
    12361236definition execute_1_pseudo_instruction:
    1237  ∀cm. (∀ppc:Word. nat_of_bitvector … ppc < |\snd cm| → nat × nat) → ∀s:PseudoStatus cm.
    1238    nat_of_bitvector 16 (program_counter pseudo_assembly_program cm s) <|\snd  cm| →
     1237 ∀cm. (∀ppc:Word. nat_of_bitvector … ppc < |code cm| → nat × nat) → ∀s:PseudoStatus cm.
     1238   nat_of_bitvector 16 (program_counter pseudo_assembly_program cm s) <|code cm| →
    12391239    PseudoStatus cm
    12401240
    12411241  λcm,ticks_of,s,pc_ok.
    1242   let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) pc_ok in
     1242  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (code cm) (program_counter … s) pc_ok in
    12431243  let ticks ≝ ticks_of (program_counter … s) pc_ok in
    12441244   execute_1_pseudo_instruction0 ticks cm s instr pc.
  • src/LIN/LINToASM.ma

    r2754 r2760  
    373373     ! symboltable ← get_symboltable … ;
    374374     (* atm no data identifier is used in the code, so preamble must be empty *)
    375      return 〈[ ], symboltable, code〉).
     375     return
     376      (mk_pseudo_assembly_program [ ] code symboltable exit_label ? ?)).
     377cases daemon
     378qed.
  • src/RTLabs/MeasurableTraces.ma

    r2601 r2760  
    66  RTLabs_fullexec
    77  (λ_.RTLabs_cost)
    8   (λ_. RTLabs_classify).
     8  (λ_. RTLabs_classify) ?.
    99
    1010notation "hbox(‘ ident i ’)" non associative with precedence 90 for @{ (let (${ident i} : unit) ≝ it in ?) }.
  • src/RTLabs/RTLabs_traces.ma

    r2757 r2760  
    22712271#ge #pre #post #CL #ret #callee #AF
    22722272cases pre in CL AF ⊢ %;
    2273 * [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?); whd in CL:(??(??%)?);
     2273* [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?); whd in CL:(??%?);
    22742274    cases (next_instruction f) in CL;
    22752275    normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct
     
    25082508#ge #flX #s1X #s2X *
    25092509[ #s1 #s2 #EX *
    2510   [ whd in ⊢ (% → ?); #CL #CS #CL' @⊥  change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
     2510  [ whd in ⊢ (% → ?); #CL #CS #CL' @⊥  change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL' in CL; #CL destruct
    25112511  | #CL #CS #CL' @eq_true_to_b @memb_hd
    25122512  ]
    2513 | #s1 #s2 #EX #CL whd in CL; #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
    2514 | #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
     2513| #s1 #s2 #EX #CL whd in CL; #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL' in CL; #CL destruct
     2514| #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL' in CL; #CL destruct
    25152515| #s1 #s2 #s3 #EX #CL @⊥ @(RTLabs_notail' … CL)
    2516 | #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
     2516| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL' in CL; #CL destruct
    25172517| #fl #s1 #s2 #s3 #EX #tal #CL #CS #CL' @eq_true_to_b @memb_hd
    25182518] qed.
     
    27702770| @no_loops_in_tal // @simplify_cl @CL
    27712771] qed.
    2772 
  • src/common/StructuredTraces.ma

    r2757 r2760  
    829829].
    830830
     831lemma filter_map_append:
     832 ∀X,Y,f,l1,l2. filter_map X Y f (l1@l2) = filter_map … f l1 @ filter_map … f l2.
     833 #X #Y #f #l1 elim l1 // #hd #tl #IH #l2 normalize >IH //
     834qed.
     835
    831836lemma map_to_filter_map : ∀X,Y,f,l.map X Y f l = filter_map X Y (λx.Some ? (f x)) l.
    832837#X #Y #f #l elim l normalize // qed.
     
    856861λA,P,l.list_distribute_sig_aux … l (pi2 … l).
    857862
     863lemma list_distribute_sig_append:
     864 ∀A,P,l1,l2,prf1,prf2,prf3.
     865  list_distribute_sig A P «l1@l2,prf3» =
     866   list_distribute_sig … «l1,prf1» @ list_distribute_sig … «l2,prf2».
     867 #A #P #l1 whd in match list_distribute_sig; normalize nodelta elim l1 //
     868 #hd #tl #IH normalize #l2 #prf1 #prf2 #prf3 <IH //
     869qed.
     870
    858871let rec list_factor_sig X P (l : list (Σx.P x)) on l : Σl.All X P l ≝
    859872match l with
     
    868881    | _ ⇒ λ_.None ?
    869882    ] (pi2 … ev)) (list_distribute_sig … l).
     883
     884axiom costlabels_of_observables_trace_label_return_id_irrelevant:
     885 ∀S,s1,s2,tr,id1,id2.
     886  costlabels_of_observables S (observables_trace_label_return S s1 s2 tr id1) =
     887  costlabels_of_observables S (observables_trace_label_return S s1 s2 tr id2).
     888
     889lemma costlabels_of_observables_append:
     890 ∀S:abstract_status. ∀tr1,tr2: as_trace S.
     891  costlabels_of_observables S (tr1 @ tr2) =
     892   costlabels_of_observables … tr1 @ costlabels_of_observables … tr2.
     893[ #S #tr1 #tr2 whd in match costlabels_of_observables; normalize nodelta
     894  <filter_map_append <list_distribute_sig_append //
     895| @All_append [ @(pi2 … tr1) | @(pi2 … tr2) ]]
     896qed.
    870897
    871898(* JHM: base case now passes the termination checker *)
     
    10351062  costlabels_of_observables … (observables_trace_label_label … tll dummy).
    10361063
     1064definition flatten_trace_any_label ≝
     1065  λS,flag,st1,st2.λtll : trace_any_label S flag st1 st2.
     1066  (* as cost events do not depend on current function identifier, we
     1067     can use a dummy one *)
     1068  let dummy ≝ an_identifier ? one in
     1069  costlabels_of_observables … (observables_trace_any_label … tll dummy).
     1070
    10371071lemma lift_cost_map_same_cost_tlr :
    10381072  ∀S_in, S_out, dec, m_out, start_in, start_out, end_in, end_out.
  • src/joint/semantics_blocks.ma

    r2688 r2760  
    4141
    4242lemma produce_step_trace :
    43   ∀p : evaluation_params.
     43  ∀p : prog_params.
    4444  ∀st : state_pc p.
    4545  ∀curr_id,curr_fn.
     
    6767
    6868let rec produce_trace_any_any_free_aux
    69   (p : evaluation_params)
     69  (p : prog_params)
    7070  (st : state_pc p)
    7171  curr_id curr_fn
     
    154154
    155155definition produce_trace_any_any_free :
    156   ∀p : evaluation_params.
     156  ∀p : prog_params.
    157157  ∀st : state_pc p.
    158158  ∀curr_id,curr_fn.
     
    173173(* when a seq_list is coerced to a step_block *)
    174174definition produce_trace_any_any_free_coerced :
    175   ∀p : evaluation_params.
     175  ∀p : prog_params.
    176176  ∀st : state_pc p.
    177177  ∀curr_id,curr_fn.
Note: See TracChangeset for help on using the changeset viewer.