Changeset 2264 for src/ASM/Assembly.ma

Timestamp:

Jul 26, 2012, 12:38:42 AM (8 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.

File:

• src/ASM/Assembly.ma (modified) (2 diffs)

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.