Changeset 1363 for src/ASM/Assembly.ma

Timestamp:

Oct 12, 2011, 9:11:07 PM (9 years ago)

Author:

boender

Message:

• done stuff with create_label_trie

File:

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

src/ASM/Assembly.ma

@@ -556 +556 @@
   let 〈new_pc, carry〉 ≝ add_16_with_carry pc (bitvector_of_nat 16 (|bv|)) false in
   new_pc.
+
+definition is_label ≝ 
+  λx:labelled_instruction.λl:Identifier. 
+  let 〈lbl,instr〉 ≝ x in
+  match lbl with
+  [ Some l' ⇒ l' = l
+  | _       ⇒ False
+  ].
   
+lemma oeo_Some_Stronger:
+  ∀id,id',i,prefix.
+    occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → 
+    (eq_bv ? id' id ∧ does_not_occur id prefix) ∨
+    (¬eq_bv ? id' id ∧ occurs_exactly_once id prefix).
+ #id #id' #i #prefix elim prefix
+ [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?)
+  change with (? → eq_v ?? eq_b id' id∧?∨?) cases (eq_v ?????)
+  [ normalize //
+  | normalize #H @⊥ @H  
+  ]
+ | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
+   cases he; normalize nodelta
+   [ #H @ (IH H)
+   | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
+     generalize in match (refl ? (eq_bv 16 x id)) change in match (eq_v ???x id) with (eq_bv ? x id)
+     cases (eq_bv ???) in ⊢ (???% → %) #Heq
+     [ generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta
+       [ #H >(eq_bv_eq … (sym_eq … H)) >does_not_occur_absurd #Hf @⊥ @Hf
+       | #H >(does_not_occur_Some)
+         [ #H2 whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
+           change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
+           @orb_elim normalize nodelta whd in match (occurs_exactly_once ??) whd in match (instruction_matches_identifier ??)
+           change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta @H2  
+         | @(sym_eq … H)
+         ]
+       ]
+     | normalize nodelta #H lapply (IH H) -IH -H; #Hor @orb_elim
+       generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) 
+       #Heq2
+       [ normalize nodelta <Heq2 in Hor; #Hor normalize in Hor;
+         whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
+         change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
+         cases (does_not_occur id tl) in Hor; normalize nodelta //
+       | normalize nodelta whd in match (occurs_exactly_once ??)
+         whd in match (instruction_matches_identifier ??) change in match (eq_v ???x id) with (eq_bv ? x id)
+         >Heq normalize nodelta <Heq2 in Hor; normalize //
+       ] 
+     ]  
+   ]
+ ]
+qed.   
+
+lemma bla:
+  ∀i,p,l.
+  is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false.
+ #i #p #l generalize in match i; elim p
+ [ #i >nth_nil #H @⊥ @H
+ | #h #t #IH #i cases i -i 
+   [ cases h #hi #hp cases hi normalize
+     [ #H @⊥ @H
+     | #l' #Heq change in match (eq_v ??? l' l) with (eq_bv ? l' l)
+       >(eq_eq_bv … Heq) //
+     ]
+   | #i #H whd in match (does_not_occur ??)
+     whd in match (instruction_matches_identifier ??)
+     cases h #hi #hp cases hi normalize
+     [ @(IH i) @H
+     | #l' cases (eq_v ??? l' l)
+       [ normalize //
+       | normalize @(IH i) @H
+       ]
+     ]
+   ]
+ ]
+qed.  
+     
 definition create_label_trie: list labelled_instruction → jump_expansion_policy → 
   label_trie ≝
   λprogram.λpolicy.
-  let 〈final_n, final_pc, final_labels〉 ≝
+  let 〈final_pc, final_labels〉 ≝
     foldl_strong (option Identifier × pseudo_instruction)
-    (λprefix.Σres.True)
+    (λprefix.Σres.
+      let 〈pc,labels〉 ≝ res in
+      ∀i:ℕ.i < |prefix| →
+      ∀l.occurs_exactly_once l prefix ->
+      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
+      ∃a.lookup_opt … l labels = Some ? 〈i,a〉
+    )
     program
     (λprefix.λx.λtl.λprf.λacc.
-     let 〈n,pc,labels〉 ≝ acc in
+     let 〈pc,labels〉 ≝ acc in
      let 〈label,instr〉 ≝ x in
      let new_labels ≝ 
        match label with
        [ None   ⇒ labels
-       | Some l ⇒ insert … l 〈n, pc〉 labels
+       | Some l ⇒ insert … l 〈|prefix|, pc〉 labels
        ] in
-     let 〈ignore,jmp_len〉 ≝ lookup … (bitvector_of_nat 16 n) policy 〈pc, long_jump〉 in
+     let 〈ignore,jmp_len〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉 in
      let new_pc ≝ add_instruction_size pc jmp_len instr in
-     〈S n, new_pc, new_labels〉
-    ) 〈0, zero ?, Stub ? ?〉 in
+     〈new_pc, new_labels〉
+    ) 〈zero ?, Stub ? ?〉 in
     final_labels.
- @I
+[ lapply (sig2 … acc) >p >p1 normalize nodelta #Hacc #i >append_length
+  <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
+  [ #Hi #l cases label
+    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
+      lapply (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #Ha elim Ha; -Ha; #addr #Haddr
+      % [ @addr | @Haddr ]
+    | #l' #Hocc #Hl lapply (oeo_Some_Stronger … Hocc) -Hocc; #Hocc
+      lapply (refl ? (eq_bv 16 l' l)) cases (eq_bv ? l' l) in ⊢ (???% → %) #Heq
+      [ >Heq in Hocc; #Hocc normalize in Hocc;
+        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl  
+        @⊥ @(absurd … Hocc) 
+      | >Heq in Hocc; normalize nodelta #Hocc lapply (Hacc i (le_S_S_to_le … Hi) l ? ?)
+        [ >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
+        | @Hocc
+        | #H elim H #addr #Haddr % [ @addr | <Haddr @lookup_opt_insert_miss >eq_bv_sym >Heq // ]   
+        ]
+      ]
+      >(bla i … Hl) normalize nodelta @nmk //
+    ]
+  | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second 
+    [ <minus_n_n #Hl normalize in Hl; cases label in Hl;
+      [ normalize nodelta #H @⊥ @H
+      | #l' normalize nodelta #Heq % [ @pc | <Heq @lookup_opt_insert_hit ]
+      ]
+    | @le_n
+    ]
+  ]
+| #i #Hi #l #Hl @⊥ @Hl
+]
 qed.
 
@@ -1025 +1134 @@
    generalize in match (refl … construct); cases construct in ⊢ (???% → %) #PC #CODE #JMEQ % [% [%]]
    [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
-   | >length_append <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
+   | >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