Changeset 2213 for src

Timestamp:

Jul 18, 2012, 5:57:26 PM (9 years ago)

Author:

boender

Message:

• removed one cases daemon

File:

• src/ASM/PolicyFront.ma (modified) (5 diffs)

src/ASM/PolicyFront.ma

@@ -644 +644 @@
 qed.
 
-lemma label_in_program: ∀program:(Σl.S (|l|) < 2^16 ∧ is_well_labelled_p l).∀labels:(Σlm.
-   ∀l.occurs_exactly_once ?? l program →
-    bitvector_of_nat ? (lookup_def ?? lm l 0) =
-     address_of_word_labels_code_mem program l).∀x.
- occurs_exactly_once ?? x program →   
- lookup_def ASMTag ℕ labels x O≤|program|.
-#program cases program -program #program #Hprogram #labels #x cases labels
--labels #labels #H lapply (H x) -H 
-generalize in match (lookup_def … labels x 0);
-whd in match address_of_word_labels_code_mem;
-whd in match index_of; normalize nodelta elim program in Hprogram;
-[ #Hprogram #n cases not_implemented
-| #h #t #Hind #Hprogram #n #Hlm #Hocc lapply (Hlm Hocc) -Hlm #Hbv 
-  whd in match (occurs_exactly_once ????) in Hocc;
-  whd in match (index_of_internal ????) in Hbv;
-  lapply (refl ? (instruction_matches_identifier … x h))
-  lapply Hocc; lapply Hbv; -Hocc -Hbv
-  cases (instruction_matches_identifier … x h) in ⊢ (% → % → ???% → %);
-  normalize nodelta #Hbv #Hocc #EQ
-  [ >(bitvector_of_nat_ok 16 n 0)
-    [ @le_O_n
-    | >(eq_eq_bv … Hbv) @I
-    | / by /
-    | cases daemon
-    ]
-  | cases n in Hbv;
-    [ #_ @le_O_n
-    | -n #n #Hbv @le_S_S @(Hind … Hocc)
-      [ @conj
-        [ @(transitive_lt … (proj1 ?? Hprogram)) @le_n
-        | cases daemon (* axiomatize this *)
-        ]
-      | #_ lapply (bitvector_of_nat_ok 16 (S n) (index_of_internal ? (instruction_matches_identifier ?? x) t 1) ???)
-        [ >Hbv >eq_bv_refl @I
-        | @(transitive_lt … (proj1 ?? Hprogram)) cases daemon
-        | cases daemon
-        | #H >(index_of_label_from_internal … Hocc)
-          <plus_O_n >(index_of_label_from_internal … Hocc) in H;
-          #H >(injective_S … H) <plus_O_n @refl
-        ]
-      ]
-    ]
-  ]
-]
-qed.
-
 lemma equal_compact_unsafe_compact: ∀program:(Σl.(S (|l|)) < 2^16 ∧ is_well_labelled_p l).
-  ∀labels.∀old_sigma.∀sigma.
+  ∀old_sigma.∀sigma.
   sigma_pc_equal program old_sigma sigma → 
-  sigma_safe program labels 0 old_sigma sigma → 
-  sigma_compact_unsafe program labels sigma →
-  sigma_compact program labels sigma.
-  #program #labels #old_sigma #sigma #Hequal #Hsafe #Hcp_unsafe #i #Hi
+  sigma_safe program (create_label_map program) 0 old_sigma sigma → 
+  sigma_compact_unsafe program (create_label_map program) sigma →
+  sigma_compact program (create_label_map program) sigma.
+  #program #old_sigma #sigma #Hequal #Hsafe #Hcp_unsafe #i #Hi
   lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi)
   lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)))
@@ -723 +677 @@
             cases x2 normalize nodelta
             [1,4: whd in match short_jump_cond; normalize nodelta
-              lapply (refl ? (leb (lookup_def ?? labels x 0) (|[]@program|)))
-              cases (leb (lookup_def ?? labels x 0) (|[]@program|)) in ⊢ (???% → %); #Hlab
-              normalize nodelta
-              >(Hequal (lookup_def ?? labels x 0) ?)
-              [2,4,6,8: @(label_in_program program labels x)
-                cases daemon (* XXX this has to come from somewhere else *)
-              ]
-              <plus_n_O
+              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
+              [1,3: cases daemon (* XXX should this be a property of create_label_map? *)
+              |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
               cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
               #result #flags normalize nodelta
               cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
               cases (get_index' bool 2 0 flags) normalize nodelta
-              [5,6,7,8: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
-              |1,2,3,4: cases (eq_bv 9 upper ?)
-                [2,4,6,8: #H lapply (proj1 ?? H) #H3 destruct (H3)
-                |1,3,5,7: #_ normalize nodelta @refl
+              [3,4: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
+              |1,2: cases (eq_bv 9 upper ?)
+                [2,4: #H lapply (proj1 ?? H) #H3 destruct (H3)
+                |1,3: #_ normalize nodelta @refl
                 ]
               ]
+              ]
             |2,5: whd in match short_jump_cond; whd in match absolute_jump_cond;
-              lapply (refl ? (leb (lookup_def ?? labels x 0) (|[]@program|)))
-              cases (leb (lookup_def ?? labels x 0) (|[]@program|)) in ⊢ (???% → %); #Hlab
-              normalize nodelta
-              (* USE: added = 0 → policy_pc_equal (from fold) *)
-              >(Hequal (lookup_def ?? labels x 0) ?)
-              [2,4,6,8: @(label_in_program program labels x) 
-                cases daemon (* XXX this has to come from somewhere else *)]
-              <plus_n_O
+              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
+              [1,3: cases daemon (* XXX should this be a property of create_label_map? *)
+              |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
               normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
               cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
@@ -757 +702 @@
               cases (get_index' bool 2 0 flags) normalize nodelta
               #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl
+              ]
             |3,6: whd in match short_jump_cond; whd in match absolute_jump_cond;
-              lapply (refl ? (leb (lookup_def ?? labels x 0) (|[]@program|)))
-              cases (leb (lookup_def ?? labels x 0) (|[]@program|)) in ⊢ (???% → %); #Hlab
-              normalize nodelta
-              (* USE: added = 0 → policy_pc_equal (from fold) *)
-              >(Hequal (lookup_def ?? labels x 0) ?)
-              [2,4,6,8: @(label_in_program program labels x)
-                cases daemon (* XXX this has to come from somewhere else *)]
-              <plus_n_O normalize nodelta
+              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
+              [1,3: cases daemon (* XXX should this be a property of create_label_map? *)
+              |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
               cases (vsplit bool 5 11 ?) #addr1 #addr2
               cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
@@ -773 +714 @@
               cases (get_index' bool 2 0 flags) normalize nodelta
               #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl
+              ]
             ]
           |1: #pi cases pi
@@ -787 +729 @@
               whd in match expand_relative_jump_internal_unsafe;
               normalize nodelta >(add_bitvector_of_nat_plus ? i 1)
-              <(plus_n_Sm i 0) <plus_n_O
-              cases daemon (* XXX this needs subadressing mode magic, see above *)
+              <(plus_n_Sm i 0) <plus_n_O <plus_n_O cases x2 normalize nodelta
+              [1,4,7,10,13,16,19,22,25:
+                cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a))
+                [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ]
+                #fst_foo >fst_foo @pair_elim #sj_possible #disp #H #H2
+                @(pair_replace ?????????? (eq_to_jmeq … H))
+                [1,3,5,7,9,11,13,15,17:
+                  cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
+                  [1,3,5,7,9,11,13,15,17: cases daemon] (* XXX should this be a property of create_label_map? *)
+                  #X >(le_to_leb_true … X) @refl
+                ]
+                >(proj1 ?? H2) try (@refl) normalize nodelta
+                [1,2,3,5: @(subaddressing_mode_elim … y) #w %
+                | cases y * #sth #sth2 @(subaddressing_mode_elim … sth) 
+                  @(subaddressing_mode_elim … sth2) #x [3,4: #x2] %
+                ]
+              |2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs #abs2 @⊥ @abs2 / by I/
+              ]
+              cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a))
+              [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ] 
+              #fst_foo * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H 
+              @(pair_replace ?????????? (eq_to_jmeq … H))
+                [1,3,5,7,9,11,13,15,17:
+                  cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
+                  [1,3,5,7,9,11,13,15,17: cases daemon] (* XXX should this be a property of create_label_map? *)
+                  #X >(le_to_leb_true … X) @refl
+                ]
+                #H2 >H2 try (@refl) normalize nodelta
+                [1,2,3,5: @(subaddressing_mode_elim … y) #w %
+                | cases y * #sth #sth2 @(subaddressing_mode_elim … sth2) #w
+                  [1,2: %] whd in match (map ????); whd in match (flatten ??);
+                  whd in match (map ????) in ⊢ (???%); whd in match (flatten ??) in ⊢ (???%);
+                  >length_append >length_append @eq_f2 %
+                ]
+              ]
             ]
           ]
         ]
       ]
-    ]
 qed.