Changeset 1562 for src/ASM

Timestamp:

Nov 25, 2011, 1:20:41 PM (9 years ago)

Author:

mulligan

Message:

new version of assembly, fixed conflict in positivemap.ma, changed erroneous axiom in identifiers.ma

File:

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

src/ASM/Assembly.ma

@@ -1615 +1615 @@
    tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
 
-lemma eq_identifier_eq:
+axiom eq_identifier_eq:
   ∀tag: String.
   ∀l.
   ∀r.
     eq_identifier tag l r = true → l = r.
-  #tag #l #r cases l cases r #posl #posr
-  cases daemon
-qed.
+
+axiom neq_identifier_neq:
+  ∀tag: String.
+  ∀l, r: identifier tag.
+    eq_identifier tag l r = false → (l = r → False).
 
 definition build_maps:
@@ -1675 +1677 @@
      | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
        generalize in match (refl … (eq_identifier ? l id)); cases (eq_identifier … l id) in ⊢ (???% → %);
-        [ #EQ #_ <(eq_identifier_eq … EQ) check lookup_add_hit. >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
-          <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]
-        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; (*Andrea:XXXX used to work /2/*)>eq_bv_sym >EQ // ]
-          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
- |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?); #abs @⊥ //
+        [ #EQ #_ <(eq_identifier_eq … EQ) >lookup_def_add_hit >address_of_word_labels_code_mem_Some_hit
+          <IH0 [@IHn1 | <(eq_identifier_eq … EQ) in H; #H @H]
+        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_def_add_miss [2: -IHn1;
+          (*Andrea:XXXX used to work /2/*)@nmk #IDL lapply (sym_eq ? ? ? IDL)
+          lapply (neq_identifier_neq ? ? ? EQ) #ASSM assumption ]
+          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 assumption ]]]
+ |3: whd % [% [%]] [>sigma_0 % | % | % | #id normalize in ⊢ (% → ?); #abs @⊥ // ] 
  | generalize in match (sig2 … result) in ⊢ ?;
    normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?);
@@ -1685 +1689 @@
 qed.
 
-definition build_maps:
- ∀pseudo_program.∀pol:policy pseudo_program.
-  Σres:((BitVectorTrie Identifier 16) × (BitVectorTrie costlabel 16)).
-   let 〈labels,costs〉 ≝ res in
-    ∀id. occurs_exactly_once id (\snd pseudo_program) →
-     lookup ? ? id labels (zero …) = ? (* sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) *)
-≝ ?.
-  λpseudo_program.λpol:policy pseudo_program.
-  let result ≝
-   foldl_strong
-    (option Identifier × pseudo_instruction)
-    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie costlabel 16)))).
-      let 〈labels,ppc_pc_costs〉 ≝ res in
-      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
-      let 〈pc',costs〉 ≝ pc_costs in
-       And ( And (
-       And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
-       (ppc' = length … pre)) (*∧ *)
-       (tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
-       (∀id. occurs_exactly_once id pre →
-        lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
-    (\snd pseudo_program)
-    (λprefix,i,tl,prf,t.
-      let 〈labels, ppc_pc_costs〉 ≝ t in
-      let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
-      let 〈pc,costs〉 ≝ pc_costs in
-       let 〈label, i'〉 ≝ i in
-       let labels ≝
-         match label with
-         [ None ⇒ labels
-         | Some label ⇒
-           let program_counter_bv ≝ bitvector_of_nat ? pc in
-             insert ? ? label program_counter_bv labels]
-       in
-         let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
-          〈labels, 〈S ppc,construct〉〉
-    ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
-  in
-   let 〈labels, ppc_pc_costs〉 ≝ result in
-   let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
-   let 〈pc, costs〉 ≝ pc_costs in
-    〈labels, costs〉.
- [2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
-   generalize in match (refl … construct); cases construct in ⊢ (???% → %) #PC #CODE #JMEQ % [% [%]]
-   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
-   | >append_length <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
-   | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
-   | #id normalize nodelta; -labels1; cases label; normalize nodelta
-     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
-     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
-       generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
-        [ #EQ #_ <(eq_bv_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
-          <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]
-        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; (*Andrea:XXXX used to work /2/*)>eq_bv_sym >EQ // ]
-          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
- |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
- | generalize in match (sig2 … result) in ⊢ ?;
-   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?)
-   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
-qed.
-
 definition assembly:
- ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie Identifier 16) ≝
+ ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie costlabel 16) ≝
   λp.let 〈preamble, instr_list〉 ≝ p in
    λpol.
     let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in
     let datalabels ≝ construct_datalabels preamble in
-    let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
-    let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
+    let lookup_labels ≝ λx. lookup_def … labels x (zero ?) in
+    let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
     let result ≝
      foldl_strong