Changeset 2264

Timestamp:

07/26/12 00:38:42 (10 months 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:

• Assembly.ma (modified) (2 diffs)
• AssemblyProofSplitSplit.ma (modified) (4 diffs)
• Fetch.ma (modified) (1 diff)
• Interpret.ma (modified) (1 diff)
• Policy.ma (modified) (3 diffs)
• PolicyFront.ma (modified) (4 diffs)
• PolicyStep.ma (modified) (1 diff)
• Status.ma (modified) (1 diff)

src/ASM/Assembly.ma

@@ -582 +582 @@
 
   
-(* label_map: identifier ↦ pseudo program counter *)
-definition label_map ≝ identifier_map ASMTag ℕ.
-
 (* Labels *) 
 definition is_label ≝ 
@@ -617 +614 @@
    ]
  ]
-qed.
-
-(* The function that creates the label-to-address map *)
-definition create_label_cost_map0: ∀program:list labelled_instruction.
-  (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
-    let 〈labels,costs〉 ≝ labels_costs in
-    ∀l.occurs_exactly_once ?? l program →
-    And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
-     address_of_word_labels_code_mem program l)
-     (lookup_def ?? labels l 0 < |program|)
-  ) ≝
-  λprogram.
-  \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
-  (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ.
-    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
-    ppc = |prefix| ∧
-    ∀l.occurs_exactly_once ?? l prefix →
-    And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
-     address_of_word_labels_code_mem prefix l)
-     (lookup_def ?? labels l 0 < |program|))
-  program
-  (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
-   let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in
-   let 〈label,instr〉 ≝ x in
-   let labels ≝
-     match label with
-     [ None   ⇒ labels
-     | Some l ⇒ add … labels l ppc
-     ] in
-   let costs ≝
-     match instr with
-     [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs
-     | _ ⇒ costs ] in
-      〈labels,costs,S ppc〉
-   ) 〈(empty_map …),(Stub ??),0〉)).
-[ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta * #IH1 #IH2
-  -labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %]
- inversion label [#EQ | #l #EQ]
- [ #lbl #Hocc <address_of_word_labels_code_mem_None [2: @Hocc] normalize nodelta 
-   >occurs_exactly_once_None in Hocc; @(IH2 lbl)
- | #lbl normalize nodelta inversion (eq_identifier ? lbl l) 
-   [ #Heq #Hocc >(eq_identifier_eq … Heq) @conj
-     [ >address_of_word_labels_code_mem_Some_hit 
-       [ >IH1 >lookup_def_add_hit %
-       | <(eq_identifier_eq … Heq) in Hocc; //
-       ]
-     | >lookup_def_add_hit >IH1 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
-     ]
-   | #Hneq #Hocc lapply (IH2 lbl ?)
-     [ >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym >Hneq //
-     | #IH3 @conj
-       [ <address_of_word_labels_code_mem_Some_miss
-         [ >lookup_def_add_miss 
-           [ @(proj1 ?? IH3)
-           | % @neq_identifier_neq @Hneq
-           ]  
-         | @Hocc
-         | >eq_identifier_sym @Hneq
-         ]
-       | >lookup_def_add_miss
-         [ @(proj2 ?? IH3)
-         | % @neq_identifier_neq @Hneq
-         ]
-       ]
-     ]
-   ]
- ]
-| @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try %
-  #l #abs cases (abs)
-| cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta *
-  #_ #H @H
-]
-qed.
-
-(* The function that creates the label-to-address map *)
-definition create_label_cost_map: ∀program:list labelled_instruction.
-  label_map × (BitVectorTrie costlabel 16) ≝
-    λprogram.
-      pi1 … (create_label_cost_map0 program).
-
-theorem create_label_cost_map_ok:
- ∀pseudo_program: pseudo_assembly_program.
-   let 〈labels, costs〉 ≝ create_label_cost_map (\snd pseudo_program) in
-    ∀id. occurs_exactly_once ??  id (\snd pseudo_program) → And
-     (bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id)
-     (lookup_def ?? labels id 0 < |\snd pseudo_program|).
- #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2
 qed.
 

src/ASM/AssemblyProofSplitSplit.ma

@@ -38 +38 @@
   >(eq_bv_eq … relevant) %
 qed.
-  
+
 theorem main_thm:
   ∀M, M': internal_pseudo_address_map.
   ∀program: pseudo_assembly_program.
   ∀program_in_bounds: |\snd program| ≤ 2^16.
-  ∀addr_of: Identifier → PreStatus pseudo_assembly_program program → BitVector 16.
+  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
+  let addr_of ≝ λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O) in
   ∀is_well_labelled: is_well_labelled_p (\snd program).
   ∀sigma: Word → Word.
@@ -53 +54 @@
       ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
         status_of_pseudo_status M' … 
-          (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy.
-    #M #M' * #preamble #instr_list #program_in_bounds #addr_of
+          (execute_1_pseudo_instruction program (ticks_of program (λid. addr_of id ps) sigma policy) ps program_counter_in_bounds) sigma policy.
+    #M #M' * #preamble #instr_list #program_in_bounds
+    @pair_elim #labels #cost #create_label_cost_refl
     #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps
     letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds
     change with (next_internal_pseudo_address_map0 ?????? = ? → ?)
     generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 program_in_bounds sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?;
-    @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
+    >create_label_cost_refl normalize nodelta
     @pair_elim #assembled #costs' #assembly_refl normalize nodelta
     lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
@@ -87 +89 @@
       (* XXX: we give the existential *)
       %{0}
+      whd in match execute_1_pseudo_instruction0; normalize nodelta
+      change with (status_of_pseudo_status ????? = ?) cases daemon (*CSC: ???
       whd in match (execute_1_pseudo_instruction0 ?????);
       (* XXX: work on the left hand side of the equality *)
       whd in ⊢ (??%?);
       @split_eq_status try %
-      /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *)
+      /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *) *)
     |6: (* Mov *)
       #arg1 #arg2 #_
@@ -114 +118 @@
       #fetch_many_assm whd in fetch_many_assm;
       lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
-      destruct whd in ⊢ (??%?);
+      destruct
       (* XXX: now we start to work on the mk_PreStatus equality *)
       (* XXX: lhs *)
       change with (set_arg_16 ????? = ?)
-      >set_program_counter_mk_Status_commutation
-      >set_clock_mk_Status_commutation
-      >set_arg_16_mk_Status_commutation
-      (* XXX: rhs *)
-      change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
-      >set_program_counter_mk_Status_commutation
-      >set_clock_mk_Status_commutation
-      >set_arg_16_mk_Status_commutation in ⊢ (???%);
-      (* here we are *)
-      @split_eq_status try %
-      [1:
-        assumption
-      |2:
-        @special_function_registers_8051_set_arg_16 %
-      ]
+      @set_arg_16_status_of_pseudo_status
+      [3: @(subaddressing_mode_elim … arg1) %
+      |2: %
+      | @sym_eq @set_clock_status_of_pseudo_status
+        [ @sym_eq @set_program_counter_status_of_pseudo_status [<EQnewpc % | %]
+        | % ]]
     |1: (* Instruction *)
-      #instr #pi_refl #EQP #EQnext #fetch_many_assm
-      @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness
-        ps ppc ? ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
-        EQnewppc instr ? (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
-        (λ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)))
-        (refl …) ? (refl …))
-      [1,2:
-        assumption
-      |3:
-        %
-      |4:
-        >fetch_pseudo_refl @pi_refl
-      |5:
-        <EQP %
-      |6:
-        >assembly_refl assumption
-      |7:
-        <EQassembled assumption
-      ]
+      #instr #pi_refl
+      change with (execute_1_preinstruction ???????) in match (execute_1_pseudo_instruction0 ?????);
+      >EQassembled whd in match address_of_word_labels; normalize nodelta
+        >create_label_cost_refl in ⊢ (? → ? → ? → %);
+       @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness
+        ps ppc ? ? labels cost create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
+        EQnewppc instr ? ? (refl …) ? (refl …)
+        (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
+        (refl …) ? (refl …)) 
+        try % try assumption >fetch_pseudo_refl assumption
     |4: (* Jmp *)
       #arg1 #pi_refl

src/ASM/Fetch.ma

@@ -3 +3 @@
 include "ASM/ASM.ma".
 include "basics/russell.ma".
+
+(***** Pseudo-code ******)
+
+definition inefficient_address_of_word_labels_code_mem ≝
+  λcode_mem : list labelled_instruction.
+  λid: Identifier.
+    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).
+
+lemma inefficient_address_of_word_labels_None: ∀i,id,instr_list.
+ occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
+  inefficient_address_of_word_labels_code_mem instr_list id =
+  inefficient_address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
+ #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
+ >(index_of_internal_None ?????? H) %
+qed.
+
+lemma inefficient_address_of_word_labels_Some_miss: ∀i,id,id',instr_list.
+ eq_identifier ? id' id = false →
+  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
+   inefficient_address_of_word_labels_code_mem instr_list id =
+   inefficient_address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
+ #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
+ >(index_of_internal_Some_miss ???????? H) [ @refl | // ]
+qed.
+
+lemma inefficient_address_of_word_labels_Some_hit: ∀i,id,instr_list.
+  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
+   inefficient_address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
+   = bitvector_of_nat … (|instr_list|).
+ #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
+ >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl
+qed.
+
+(* label_map: identifier ↦ pseudo program counter *)
+definition label_map ≝ identifier_map ASMTag ℕ.
+
+(* The function that creates the label-to-address map *)
+definition create_label_cost_map0: ∀program:list labelled_instruction.
+  (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
+    let labels ≝ \fst labels_costs in
+    (∀l.occurs_exactly_once ?? l program →
+      bitvector_of_nat ? (lookup_def ?? labels l 0) =
+       inefficient_address_of_word_labels_code_mem program l) ∧
+    (∀l.occurs_exactly_once ?? l program →lookup_def ?? labels l 0 < |program|)
+  ) ≝
+  λprogram.
+  \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
+  (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ.
+    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
+    ppc = |prefix| ∧
+    ((∀l.occurs_exactly_once ?? l prefix →
+      bitvector_of_nat ? (lookup_def ?? labels l 0) =
+       inefficient_address_of_word_labels_code_mem prefix l) ∧
+    (∀l.occurs_exactly_once ?? l prefix → lookup_def ?? labels l 0 < |program|)))
+  program
+  (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
+   let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in
+   let 〈label,instr〉 ≝ x in
+   let labels ≝
+     match label with
+     [ None   ⇒ labels
+     | Some l ⇒ add … labels l ppc
+     ] in
+   let costs ≝
+     match instr with
+     [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs
+     | _ ⇒ costs ] in
+      〈labels,costs,S ppc〉
+   ) 〈(empty_map …),(Stub ??),0〉)).
+[ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta *
+  #IH1 * #IH2 #IH3 -labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %]
+ inversion label [#EQ | #l #EQ]
+ [ % #lbl
+   [ #Hocc <inefficient_address_of_word_labels_None [2: @Hocc] normalize nodelta 
+     >occurs_exactly_once_None in Hocc; @IH2
+   | #Hocc normalize nodelta >occurs_exactly_once_None in Hocc; @IH3 ]
+ | %
+   #lbl normalize nodelta inversion (eq_identifier ? lbl l) 
+    [1,3: #Heq #Hocc >(eq_identifier_eq … Heq)
+     [ >inefficient_address_of_word_labels_Some_hit 
+       [ >IH1 >lookup_def_add_hit %
+       | <(eq_identifier_eq … Heq) in Hocc; //
+       ]
+     | >lookup_def_add_hit >IH1 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
+     ]
+    |*: #Hneq #Hocc
+     cut (occurs_exactly_once … lbl prefix)
+     [1,3: >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym >Hneq // ]
+     #Hocc' lapply (IH2 lbl ?) try assumption
+     [ <inefficient_address_of_word_labels_Some_miss //
+       >lookup_def_add_miss // % @neq_identifier_neq @Hneq
+     | >lookup_def_add_miss /2/
+     ]
+   ]
+ ]
+| @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try %
+  #l #abs cases (abs)
+| cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta *
+  #_ #H @H
+]
+qed.
+
+(* The function that creates the label-to-address map *)
+definition create_label_cost_map: ∀program:list labelled_instruction.
+  label_map × (BitVectorTrie costlabel 16) ≝
+    λprogram.
+      pi1 … (create_label_cost_map0 program).
+
+theorem create_label_cost_map_ok:
+ ∀instr_list.
+   let labels ≝ \fst (create_label_cost_map instr_list) in
+    ((∀id. occurs_exactly_once ??  id instr_list →
+     (bitvector_of_nat ? (lookup_def ?? labels id 0) = inefficient_address_of_word_labels_code_mem instr_list id))
+    ∧
+     (∀id. occurs_exactly_once ?? id instr_list → lookup_def ?? labels id 0 < |instr_list|)).
+ #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?);
+ @pi2
+qed.
+
+definition address_of_word_labels :
+ list labelled_instruction → Identifier → Word
+≝
+  λcode_mem : list labelled_instruction.
+  λid: Identifier.
+   let labels ≝ \fst (create_label_cost_map code_mem) in
+    bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O).
+
+lemma address_of_word_labels_None: ∀i,id,instr_list.
+ occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
+  address_of_word_labels instr_list id =
+  address_of_word_labels (instr_list@[〈None …,i〉]) id.
+ #i #id #instr_list #H
+ whd in match address_of_word_labels; normalize nodelta
+ lapply (create_label_cost_map_ok (instr_list@[〈None …,i〉])) * #K' #_
+ lapply (create_label_cost_map_ok instr_list) * #K #_
+ >K' // >K // <inefficient_address_of_word_labels_None //
+qed.
+
+lemma address_of_word_labels_Some_miss: ∀i,id,id',instr_list.
+ eq_identifier ? id' id = false →
+  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
+   address_of_word_labels instr_list id =
+   address_of_word_labels (instr_list@[〈Some … id',i〉]) id.
+ #i #id #id' #instr_list #H1 #H2
+ whd in match address_of_word_labels; normalize nodelta
+ lapply (create_label_cost_map_ok (instr_list@[〈Some … id',i〉])) * #K' #_
+ lapply (create_label_cost_map_ok instr_list) * #K #_
+ >K' // >K
+ [2: lapply (occurs_exactly_once_Some ?????? H2) >H1 #H @H ]
+ @inefficient_address_of_word_labels_Some_miss //
+qed.
+
+lemma address_of_word_labels_Some_hit: ∀i,id,instr_list.
+  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
+   address_of_word_labels (instr_list@[〈Some … id,i〉]) id
+   = bitvector_of_nat … (|instr_list|).
+ #i #id #instr_list #H
+ whd in match address_of_word_labels; normalize nodelta
+ lapply (create_label_cost_map_ok (instr_list@[〈Some … id,i〉])) * #K #_
+ >K // @inefficient_address_of_word_labels_Some_hit //
+qed.
+
+(***** Object-code *******)
 
 definition bitvector_max_nat ≝

src/ASM/Interpret.ma

@@ -1190 +1190 @@
   let s ≝
     match instr with
-    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels cm x) instr s
+    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels (\snd cm) x) instr s
     | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
     | Cost cst ⇒ s
     | Jmp jmp ⇒
        let s ≝ set_clock … s (\fst ticks + clock … s) in
-        set_program_counter … s (address_of_word_labels cm jmp)
+        set_program_counter … s (address_of_word_labels (\snd cm) jmp)
     | Call call ⇒
       let s ≝ set_clock ?? s (\fst ticks + clock … s) in
-      let a ≝ address_of_word_labels cm call in
+      let a ≝ address_of_word_labels (\snd cm) call in
       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
       let s ≝ set_8051_sfr … s SFR_SP new_sp in

src/ASM/Policy.ma

@@ -30 +30 @@
           ] (refl … z)
   ] (refl … n).
-[5: cases labels #label_map #spec #id #id_ok cases (spec … id_ok) // 
+[5: #l #_ %
 | normalize nodelta cases (jump_expansion_start program (create_label_map program))
   #x cases x -x
@@ -262 +262 @@
   | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc
   ].
-[2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) // ]
+[2: #l #_ %]
 #program #policy #l elim l -l;
 [ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ]
@@ -332 +332 @@
   [ None ⇒ True
   | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → sigma_jump_equal program policy p ].
-[2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) //]
+[2: #l #_ %]
 #program #policy inversion (jump_expansion_step ???)
 #p cases p -p #ch #pol normalize nodelta cases pol

src/ASM/PolicyFront.ma

@@ -315 +315 @@
   (Σlabels:label_map.
     ∀l.occurs_exactly_once ?? l program →
-    And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
-     address_of_word_labels_code_mem program l)
-    (lookup_def ?? labels l 0 < |program|)
+    (*And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
+     address_of_word_labels program l)
+    ( *)lookup_def ?? labels l 0 < |program|(*)*)
   ) ≝
  λprogram.
    \fst (create_label_cost_map program).
- #l #Hl lapply (pi2 ?? (create_label_cost_map0 program)) @pair_elim
- #labels #costs #EQ normalize nodelta #H whd in match create_label_cost_map;
- normalize nodelta >EQ @(H l Hl)
+ #l #Hl cases (create_label_cost_map_ok program) #_ #X @(X … Hl)
 qed.
 
@@ -667 +665 @@
               cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
               [1,3: cases (create_label_map program) #clm #Hclm
-                @le_S_to_le @(proj2 ?? (Hclm x ?))
+                @le_S_to_le @(Hclm x ?)
                 [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
                 |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
@@ -696 +694 @@
               cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
               [1,3,5,7: cases (create_label_map program) #clm #Hclm
-                @le_S_to_le @(proj2 ?? (Hclm x ?))
+                @le_S_to_le @(Hclm x ?)
                 [1,2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
                 |3,4: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
@@ -728 +726 @@
                lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
               [#x #Heq cases (create_label_map program) #clm #Hclm
-               @le_S_to_le @(proj2 ?? (Hclm x ?))
+               @le_S_to_le @(Hclm x ?)
                @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
                [ >nat_of_bitvector_bitvector_of_nat_inverse

src/ASM/PolicyStep.ma

@@ -1067 +1067 @@
     occurs_exactly_once ?? l program →
     bitvector_of_nat ? (lookup_def … lm l 0) =
-    address_of_word_labels_code_mem program l).
+    address_of_word_labels program l).
   ∀old_policy:(Σpolicy:ppc_pc_map.
     (* out_of_program_none program policy *)

src/ASM/Status.ma

@@ -1101 +1101 @@
         occurs_exactly_once ASMTag pseudo_instruction id instr_list.
 
-definition address_of_word_labels_code_mem ≝
-  λcode_mem : list labelled_instruction.
-  λid: Identifier.
-    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).
-
-lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
- occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
-  address_of_word_labels_code_mem instr_list id =
-  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
- #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
- >(index_of_internal_None ?????? H) %
-qed.
-
-lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
- eq_identifier ? id' id = false →
-  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
-   address_of_word_labels_code_mem instr_list id =
-   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
- #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
- >(index_of_internal_Some_miss ???????? H) [ @refl | // ]
-qed.
-
-lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
-  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
-   address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
-   = bitvector_of_nat … (|instr_list|).
- #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
- >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl
-qed.
-
-definition address_of_word_labels ≝
-  λpr: pseudo_assembly_program.
-  λid: Identifier.
-    address_of_word_labels_code_mem (\snd pr) id.
-
 definition construct_datalabels: preamble → ? ≝
   λthe_preamble: preamble.