Changeset 2264 for src/ASM


Ignore:
Timestamp:
Jul 26, 2012, 12:38:42 AM (9 years ago)
Author:
sacerdot
Message:

1) Major change: we now always use the efficient way of resolving labels

for the interpretation of pseudo assembly code. The inefficient way is
only used locally in ASM/Interpret.ma to prove some properties more easily.

2) AssemblyProofSplitSplit?.ma partially repaired. In particular, the main

lemma is now called correctly thanks to the previous change.

Location:
src/ASM
Files:
8 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Assembly.ma

    r2221 r2264  
    582582
    583583 
    584 (* label_map: identifier ↦ pseudo program counter *)
    585 definition label_map ≝ identifier_map ASMTag ℕ.
    586 
    587584(* Labels *)
    588585definition is_label ≝
    … …  
    617614   ]
    618615 ]
    619 qed.
    620 
    621 (* The function that creates the label-to-address map *)
    622 definition create_label_cost_map0: ∀program:list labelled_instruction.
    623   (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
    624     let 〈labels,costs〉 ≝ labels_costs in
    625     ∀l.occurs_exactly_once ?? l program →
    626     And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
    627      address_of_word_labels_code_mem program l)
    628      (lookup_def ?? labels l 0 < |program|)
    629   ) ≝
    630   λprogram.
    631   \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
    632   (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ.
    633     let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
    634     ppc = |prefix| ∧
    635     ∀l.occurs_exactly_once ?? l prefix →
    636     And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
    637      address_of_word_labels_code_mem prefix l)
    638      (lookup_def ?? labels l 0 < |program|))
    639   program
    640   (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
    641    let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in
    642    let 〈label,instr〉 ≝ x in
    643    let labels ≝
    644      match label with
    645      [ None   ⇒ labels
    646      | Some l ⇒ add … labels l ppc
    647      ] in
    648    let costs ≝
    649      match instr with
    650      [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs
    651      | _ ⇒ costs ] in
    652       〈labels,costs,S ppc〉
    653    ) 〈(empty_map …),(Stub ??),0〉)).
    654 [ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta * #IH1 #IH2
    655   -labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %]
    656  inversion label [#EQ | #l #EQ]
    657  [ #lbl #Hocc <address_of_word_labels_code_mem_None [2: @Hocc] normalize nodelta
    658    >occurs_exactly_once_None in Hocc; @(IH2 lbl)
    659  | #lbl normalize nodelta inversion (eq_identifier ? lbl l)
    660    [ #Heq #Hocc >(eq_identifier_eq … Heq) @conj
    661      [ >address_of_word_labels_code_mem_Some_hit
    662        [ >IH1 >lookup_def_add_hit %
    663        | <(eq_identifier_eq … Heq) in Hocc; //
    664        ]
    665      | >lookup_def_add_hit >IH1 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    666      ]
    667    | #Hneq #Hocc lapply (IH2 lbl ?)
    668      [ >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym >Hneq //
    669      | #IH3 @conj
    670        [ <address_of_word_labels_code_mem_Some_miss
    671          [ >lookup_def_add_miss
    672            [ @(proj1 ?? IH3)
    673            | % @neq_identifier_neq @Hneq
    674            ] 
    675          | @Hocc
    676          | >eq_identifier_sym @Hneq
    677          ]
    678        | >lookup_def_add_miss
    679          [ @(proj2 ?? IH3)
    680          | % @neq_identifier_neq @Hneq
    681          ]
    682        ]
    683      ]
    684    ]
    685  ]
    686 | @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try %
    687   #l #abs cases (abs)
    688 | cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta *
    689   #_ #H @H
    690 ]
    691 qed.
    692 
    693 (* The function that creates the label-to-address map *)
    694 definition create_label_cost_map: ∀program:list labelled_instruction.
    695   label_map × (BitVectorTrie costlabel 16) ≝
    696     λprogram.
    697       pi1 … (create_label_cost_map0 program).
    698 
    699 theorem create_label_cost_map_ok:
    700  ∀pseudo_program: pseudo_assembly_program.
    701    let 〈labels, costs〉 ≝ create_label_cost_map (\snd pseudo_program) in
    702     ∀id. occurs_exactly_once ??  id (\snd pseudo_program) → And
    703      (bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id)
    704      (lookup_def ?? labels id 0 < |\snd pseudo_program|).
    705  #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2
    706616qed.
    707617

  • src/ASM/AssemblyProofSplitSplit.ma

    r2140 r2264  
    3838  >(eq_bv_eq … relevant) %
    3939qed.
    40  
     40
    4141theorem main_thm:
    4242  ∀M, M': internal_pseudo_address_map.
    4343  ∀program: pseudo_assembly_program.
    4444  ∀program_in_bounds: |\snd program| ≤ 2^16.
    45   ∀addr_of: Identifier → PreStatus pseudo_assembly_program program → BitVector 16.
     45  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
     46  let addr_of ≝ λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O) in
    4647  ∀is_well_labelled: is_well_labelled_p (\snd program).
    4748  ∀sigma: Word → Word.
    … …  
    5354      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
    5455        status_of_pseudo_status M' …
    55           (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy.
    56     #M #M' * #preamble #instr_list #program_in_bounds #addr_of
     56          (execute_1_pseudo_instruction program (ticks_of program (λid. addr_of id ps) sigma policy) ps program_counter_in_bounds) sigma policy.
     57    #M #M' * #preamble #instr_list #program_in_bounds
     58    @pair_elim #labels #cost #create_label_cost_refl
    5759    #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps
    5860    letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds
    5961    change with (next_internal_pseudo_address_map0 ?????? = ? → ?)
    6062    generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 program_in_bounds sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?;
    61     @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
     63    >create_label_cost_refl normalize nodelta
    6264    @pair_elim #assembled #costs' #assembly_refl normalize nodelta
    6365    lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
    … …  
    8789      (* XXX: we give the existential *)
    8890      %{0}
     91      whd in match execute_1_pseudo_instruction0; normalize nodelta
     92      change with (status_of_pseudo_status ????? = ?) cases daemon (*CSC: ???
    8993      whd in match (execute_1_pseudo_instruction0 ?????);
    9094      (* XXX: work on the left hand side of the equality *)
    9195      whd in ⊢ (??%?);
    9296      @split_eq_status try %
    93       /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *)
     97      /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *) *)
    9498    |6: (* Mov *)
    9599      #arg1 #arg2 #_
    … …  
    114118      #fetch_many_assm whd in fetch_many_assm;
    115119      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
    116       destruct whd in ⊢ (??%?);
     120      destruct
    117121      (* XXX: now we start to work on the mk_PreStatus equality *)
    118122      (* XXX: lhs *)
    119123      change with (set_arg_16 ????? = ?)
    120       >set_program_counter_mk_Status_commutation
    121       >set_clock_mk_Status_commutation
    122       >set_arg_16_mk_Status_commutation
    123       (* XXX: rhs *)
    124       change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
    125       >set_program_counter_mk_Status_commutation
    126       >set_clock_mk_Status_commutation
    127       >set_arg_16_mk_Status_commutation in ⊢ (???%);
    128       (* here we are *)
    129       @split_eq_status try %
    130       [1:
    131         assumption
    132       |2:
    133         @special_function_registers_8051_set_arg_16 %
    134       ]
     124      @set_arg_16_status_of_pseudo_status
     125      [3: @(subaddressing_mode_elim … arg1) %
     126      |2: %
     127      | @sym_eq @set_clock_status_of_pseudo_status
     128        [ @sym_eq @set_program_counter_status_of_pseudo_status [<EQnewpc % | %]
     129        | % ]]
    135130    |1: (* Instruction *)
    136       #instr #pi_refl #EQP #EQnext #fetch_many_assm
    137       @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness
    138         ps ppc ? ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
    139         EQnewppc instr ? (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
    140         (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
    141         (refl …) ? (refl …))
    142       [1,2:
    143         assumption
    144       |3:
    145         %
    146       |4:
    147         >fetch_pseudo_refl @pi_refl
    148       |5:
    149         <EQP %
    150       |6:
    151         >assembly_refl assumption
    152       |7:
    153         <EQassembled assumption
    154       ]
     131      #instr #pi_refl
     132      change with (execute_1_preinstruction ???????) in match (execute_1_pseudo_instruction0 ?????);
     133      >EQassembled whd in match address_of_word_labels; normalize nodelta
     134        >create_label_cost_refl in ⊢ (? → ? → ? → %);
     135       @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness
     136        ps ppc ? ? labels cost create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
     137        EQnewppc instr ? ? (refl …) ? (refl …)
     138        (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
     139        (refl …) ? (refl …))
     140        try % try assumption >fetch_pseudo_refl assumption
    155141    |4: (* Jmp *)
    156142      #arg1 #pi_refl

  • src/ASM/Fetch.ma

    r2124 r2264  
    33include "ASM/ASM.ma".
    44include "basics/russell.ma".
     5
     6(***** Pseudo-code ******)
     7
     8definition inefficient_address_of_word_labels_code_mem ≝
     9  λcode_mem : list labelled_instruction.
     10  λid: Identifier.
     11    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).
     12
     13lemma inefficient_address_of_word_labels_None: ∀i,id,instr_list.
     14 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
     15  inefficient_address_of_word_labels_code_mem instr_list id =
     16  inefficient_address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
     17 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
     18 >(index_of_internal_None ?????? H) %
     19qed.
     20
     21lemma inefficient_address_of_word_labels_Some_miss: ∀i,id,id',instr_list.
     22 eq_identifier ? id' id = false →
     23  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
     24   inefficient_address_of_word_labels_code_mem instr_list id =
     25   inefficient_address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
     26 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
     27 >(index_of_internal_Some_miss ???????? H) [ @refl | // ]
     28qed.
     29
     30lemma inefficient_address_of_word_labels_Some_hit: ∀i,id,instr_list.
     31  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
     32   inefficient_address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
     33   = bitvector_of_nat … (|instr_list|).
     34 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
     35 >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl
     36qed.
     37
     38(* label_map: identifier ↦ pseudo program counter *)
     39definition label_map ≝ identifier_map ASMTag ℕ.
     40
     41(* The function that creates the label-to-address map *)
     42definition create_label_cost_map0: ∀program:list labelled_instruction.
     43  (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
     44    let labels ≝ \fst labels_costs in
     45    (∀l.occurs_exactly_once ?? l program →
     46      bitvector_of_nat ? (lookup_def ?? labels l 0) =
     47       inefficient_address_of_word_labels_code_mem program l) ∧
     48    (∀l.occurs_exactly_once ?? l program →lookup_def ?? labels l 0 < |program|)
     49  ) ≝
     50  λprogram.
     51  \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
     52  (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ.
     53    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
     54    ppc = |prefix| ∧
     55    ((∀l.occurs_exactly_once ?? l prefix →
     56      bitvector_of_nat ? (lookup_def ?? labels l 0) =
     57       inefficient_address_of_word_labels_code_mem prefix l) ∧
     58    (∀l.occurs_exactly_once ?? l prefix → lookup_def ?? labels l 0 < |program|)))
     59  program
     60  (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
     61   let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in
     62   let 〈label,instr〉 ≝ x in
     63   let labels ≝
     64     match label with
     65     [ None   ⇒ labels
     66     | Some l ⇒ add … labels l ppc
     67     ] in
     68   let costs ≝
     69     match instr with
     70     [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs
     71     | _ ⇒ costs ] in
     72      〈labels,costs,S ppc〉
     73   ) 〈(empty_map …),(Stub ??),0〉)).
     74[ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta *
     75  #IH1 * #IH2 #IH3 -labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %]
     76 inversion label [#EQ | #l #EQ]
     77 [ % #lbl
     78   [ #Hocc <inefficient_address_of_word_labels_None [2: @Hocc] normalize nodelta
     79     >occurs_exactly_once_None in Hocc; @IH2
     80   | #Hocc normalize nodelta >occurs_exactly_once_None in Hocc; @IH3 ]
     81 | %
     82   #lbl normalize nodelta inversion (eq_identifier ? lbl l)
     83    [1,3: #Heq #Hocc >(eq_identifier_eq … Heq)
     84     [ >inefficient_address_of_word_labels_Some_hit
     85       [ >IH1 >lookup_def_add_hit %
     86       | <(eq_identifier_eq … Heq) in Hocc; //
     87       ]
     88     | >lookup_def_add_hit >IH1 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     89     ]
     90    |*: #Hneq #Hocc
     91     cut (occurs_exactly_once … lbl prefix)
     92     [1,3: >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym >Hneq // ]
     93     #Hocc' lapply (IH2 lbl ?) try assumption
     94     [ <inefficient_address_of_word_labels_Some_miss //
     95       >lookup_def_add_miss // % @neq_identifier_neq @Hneq
     96     | >lookup_def_add_miss /2/
     97     ]
     98   ]
     99 ]
     100| @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try %
     101  #l #abs cases (abs)
     102| cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta *
     103  #_ #H @H
     104]
     105qed.
     106
     107(* The function that creates the label-to-address map *)
     108definition create_label_cost_map: ∀program:list labelled_instruction.
     109  label_map × (BitVectorTrie costlabel 16) ≝
     110    λprogram.
     111      pi1 … (create_label_cost_map0 program).
     112
     113theorem create_label_cost_map_ok:
     114 ∀instr_list.
     115   let labels ≝ \fst (create_label_cost_map instr_list) in
     116    ((∀id. occurs_exactly_once ??  id instr_list →
     117     (bitvector_of_nat ? (lookup_def ?? labels id 0) = inefficient_address_of_word_labels_code_mem instr_list id))
     118    ∧
     119     (∀id. occurs_exactly_once ?? id instr_list → lookup_def ?? labels id 0 < |instr_list|)).
     120 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?);
     121 @pi2
     122qed.
     123
     124definition address_of_word_labels :
     125 list labelled_instruction → Identifier → Word
     126≝
     127  λcode_mem : list labelled_instruction.
     128  λid: Identifier.
     129   let labels ≝ \fst (create_label_cost_map code_mem) in
     130    bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O).
     131
     132lemma address_of_word_labels_None: ∀i,id,instr_list.
     133 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
     134  address_of_word_labels instr_list id =
     135  address_of_word_labels (instr_list@[〈None …,i〉]) id.
     136 #i #id #instr_list #H
     137 whd in match address_of_word_labels; normalize nodelta
     138 lapply (create_label_cost_map_ok (instr_list@[〈None …,i〉])) * #K' #_
     139 lapply (create_label_cost_map_ok instr_list) * #K #_
     140 >K' // >K // <inefficient_address_of_word_labels_None //
     141qed.
     142
     143lemma address_of_word_labels_Some_miss: ∀i,id,id',instr_list.
     144 eq_identifier ? id' id = false →
     145  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
     146   address_of_word_labels instr_list id =
     147   address_of_word_labels (instr_list@[〈Some … id',i〉]) id.
     148 #i #id #id' #instr_list #H1 #H2
     149 whd in match address_of_word_labels; normalize nodelta
     150 lapply (create_label_cost_map_ok (instr_list@[〈Some … id',i〉])) * #K' #_
     151 lapply (create_label_cost_map_ok instr_list) * #K #_
     152 >K' // >K
     153 [2: lapply (occurs_exactly_once_Some ?????? H2) >H1 #H @H ]
     154 @inefficient_address_of_word_labels_Some_miss //
     155qed.
     156
     157lemma address_of_word_labels_Some_hit: ∀i,id,instr_list.
     158  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
     159   address_of_word_labels (instr_list@[〈Some … id,i〉]) id
     160   = bitvector_of_nat … (|instr_list|).
     161 #i #id #instr_list #H
     162 whd in match address_of_word_labels; normalize nodelta
     163 lapply (create_label_cost_map_ok (instr_list@[〈Some … id,i〉])) * #K #_
     164 >K // @inefficient_address_of_word_labels_Some_hit //
     165qed.
     166
     167(***** Object-code *******)
    5168
    6169definition bitvector_max_nat ≝

  • src/ASM/Interpret.ma

    r2212 r2264  
    11901190  let s ≝
    11911191    match instr with
    1192     [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels cm x) instr s
     1192    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels (\snd cm) x) instr s
    11931193    | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
    11941194    | Cost cst ⇒ s
    11951195    | Jmp jmp ⇒
    11961196       let s ≝ set_clock … s (\fst ticks + clock … s) in
    1197         set_program_counter … s (address_of_word_labels cm jmp)
     1197        set_program_counter … s (address_of_word_labels (\snd cm) jmp)
    11981198    | Call call ⇒
    11991199      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    1200       let a ≝ address_of_word_labels cm call in
     1200      let a ≝ address_of_word_labels (\snd cm) call in
    12011201      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    12021202      let s ≝ set_8051_sfr … s SFR_SP new_sp in

  • src/ASM/Policy.ma

    r2230 r2264  
    3030          ] (refl … z)
    3131  ] (refl … n).
    32 [5: cases labels #label_map #spec #id #id_ok cases (spec … id_ok) //
     32[5: #l #_ %
    3333| normalize nodelta cases (jump_expansion_start program (create_label_map program))
    3434  #x cases x -x
    … …  
    262262  | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc
    263263  ].
    264 [2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) // ]
     264[2: #l #_ %]
    265265#program #policy #l elim l -l;
    266266[ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ]
    … …  
    332332  [ None ⇒ True
    333333  | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → sigma_jump_equal program policy p ].
    334 [2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) //]
     334[2: #l #_ %]
    335335#program #policy inversion (jump_expansion_step ???)
    336336#p cases p -p #ch #pol normalize nodelta cases pol

  • src/ASM/PolicyFront.ma

    r2235 r2264  
    315315  (Σlabels:label_map.
    316316    ∀l.occurs_exactly_once ?? l program →
    317     And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
    318      address_of_word_labels_code_mem program l)
    319     (lookup_def ?? labels l 0 < |program|)
     317    (*And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
     318     address_of_word_labels program l)
     319    ( *)lookup_def ?? labels l 0 < |program|(*)*)
    320320  ) ≝
    321321 λprogram.
    322322   \fst (create_label_cost_map program).
    323  #l #Hl lapply (pi2 ?? (create_label_cost_map0 program)) @pair_elim
    324  #labels #costs #EQ normalize nodelta #H whd in match create_label_cost_map;
    325  normalize nodelta >EQ @(H l Hl)
     323 #l #Hl cases (create_label_cost_map_ok program) #_ #X @(X … Hl)
    326324qed.
    327325
    … …  
    667665              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    668666              [1,3: cases (create_label_map program) #clm #Hclm
    669                 @le_S_to_le @(proj2 ?? (Hclm x ?))
     667                @le_S_to_le @(Hclm x ?)
    670668                [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
    671669                |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
    … …  
    696694              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    697695              [1,3,5,7: cases (create_label_map program) #clm #Hclm
    698                 @le_S_to_le @(proj2 ?? (Hclm x ?))
     696                @le_S_to_le @(Hclm x ?)
    699697                [1,2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
    700698                |3,4: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
    … …  
    728726               lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    729727              [#x #Heq cases (create_label_map program) #clm #Hclm
    730                @le_S_to_le @(proj2 ?? (Hclm x ?))
     728               @le_S_to_le @(Hclm x ?)
    731729               @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
    732730               [ >nat_of_bitvector_bitvector_of_nat_inverse

  • src/ASM/PolicyStep.ma

    r2248 r2264  
    10671067    occurs_exactly_once ?? l program →
    10681068    bitvector_of_nat ? (lookup_def … lm l 0) =
    1069     address_of_word_labels_code_mem program l).
     1069    address_of_word_labels program l).
    10701070  ∀old_policy:(Σpolicy:ppc_pc_map.
    10711071    (* out_of_program_none program policy *)

  • src/ASM/Status.ma

    r2247 r2264  
    11011101        occurs_exactly_once ASMTag pseudo_instruction id instr_list.
    11021102
    1103 definition address_of_word_labels_code_mem ≝
    1104   λcode_mem : list labelled_instruction.
    1105   λid: Identifier.
    1106     bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).
    1107 
    1108 lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
    1109  occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
    1110   address_of_word_labels_code_mem instr_list id =
    1111   address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
    1112  #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
    1113  >(index_of_internal_None ?????? H) %
    1114 qed.
    1115 
    1116 lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
    1117  eq_identifier ? id' id = false →
    1118   occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
    1119    address_of_word_labels_code_mem instr_list id =
    1120    address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
    1121  #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
    1122  >(index_of_internal_Some_miss ???????? H) [ @refl | // ]
    1123 qed.
    1124 
    1125 lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
    1126   occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
    1127    address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
    1128    = bitvector_of_nat … (|instr_list|).
    1129  #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
    1130  >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl
    1131 qed.
    1132 
    1133 definition address_of_word_labels ≝
    1134   λpr: pseudo_assembly_program.
    1135   λid: Identifier.
    1136     address_of_word_labels_code_mem (\snd pr) id.
    1137 
    11381103definition construct_datalabels: preamble → ? ≝
    11391104  λthe_preamble: preamble.
Note: See TracChangeset for help on using the changeset viewer.