Changeset 2221 for src/ASM

Timestamp:

Jul 20, 2012, 10:46:29 AM (7 years ago)

Author:

boender

Message:

• removed cases daemon from PolicyFront?

Location:

src/ASM

Files:

• Assembly.ma (modified) (4 diffs)
• PolicyFront.ma (modified) (9 diffs)

src/ASM/Assembly.ma

@@ -624 +624 @@
     let 〈labels,costs〉 ≝ labels_costs in
     ∀l.occurs_exactly_once ?? l program →
-    bitvector_of_nat ? (lookup_def ?? labels l 0) =
-     address_of_word_labels_code_mem program l
+    And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
+     address_of_word_labels_code_mem program l)
+     (lookup_def ?? labels l 0 < |program|)
   ) ≝
   λprogram.
@@ -633 +634 @@
     ppc = |prefix| ∧
     ∀l.occurs_exactly_once ?? l prefix →
-    bitvector_of_nat ? (lookup_def ?? labels l 0) =
+    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.
@@ -656 +658 @@
    >occurs_exactly_once_None in Hocc; @(IH2 lbl)
  | #lbl normalize nodelta inversion (eq_identifier ? lbl l) 
-   [ #Heq #Hocc >(eq_identifier_eq … Heq)
-     >address_of_word_labels_code_mem_Some_hit 
-     [ >IH1 >lookup_def_add_hit %
-     | <(eq_identifier_eq … Heq) in Hocc; //
+   [ #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
-     <address_of_word_labels_code_mem_Some_miss
-     [ >lookup_def_add_miss 
-       [ @IH2 >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym> Hneq //
-       | % @neq_identifier_neq @Hneq
+   | #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
+         ]
        ]
-     | @Hocc
-     | >eq_identifier_sym @Hneq
      ]
    ]
@@ -688 +700 @@
  ∀pseudo_program: pseudo_assembly_program.
    let 〈labels, costs〉 ≝ create_label_cost_map (\snd pseudo_program) in
-    ∀id. occurs_exactly_once ??  id (\snd pseudo_program) →
-     bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id.
+    ∀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/PolicyFront.ma

@@ -302 +302 @@
   (Σlabels:label_map.
     ∀l.occurs_exactly_once ?? l program →
-    bitvector_of_nat ? (lookup_def ?? labels l 0) =
-     address_of_word_labels_code_mem program l
+    And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
+     address_of_word_labels_code_mem program l)
+    (lookup_def ?? labels l 0 < |program|)
   ) ≝
  λprogram.
@@ -650 +651 @@
   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
+  #program cases program -program #program #Hprogram #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)))
@@ -669 +671 @@
           whd in match (expand_pseudo_instruction …);
           normalize nodelta whd in match (append …) in H;
-          cases (nth i ? program 〈None ?,Comment []〉) in H;
+          lapply (refl ? (nth i ? program 〈None ?, Comment []〉)) lapply H
+          cases (nth i ? program 〈None ?,Comment []〉) in ⊢ (% → ???% → %);
           #lbl #instr cases instr
-          [2,3,6: #x [3: #y] normalize nodelta #H @refl
-          |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj
+          [2,3,6: #x [3: #y] normalize nodelta #H #_ %
+          |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj #Heq
             lapply (Hj x (refl ? x)) -Hj normalize nodelta
             >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O
@@ -678 +681 @@
             [1,4: whd in match short_jump_cond; 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? *)
+              [1,3: cases (create_label_map program) #clm #Hclm
+                @le_S_to_le @(proj2 ?? (Hclm x ?))
+                [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
+                |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
+                [1,4: >nat_of_bitvector_bitvector_of_nat_inverse
+                  [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
+                |2,5: whd in match fetch_pseudo_instruction; normalize nodelta
+                  >nth_safe_nth
+                  [1,3: >nat_of_bitvector_bitvector_of_nat_inverse
+                    [1,3: >Heq / by refl/
+                    |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
+                    ]
+                  ]
+                |3,6: / by /
+                ]
               |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)
@@ -693 +710 @@
             |2,5: whd in match short_jump_cond; whd in match absolute_jump_cond;
               cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
-              [1,3: cases daemon (* XXX should this be a property of create_label_map? *)
+              [1,3: cases (create_label_map program) #clm #Hclm
+                @le_S_to_le @(proj2 ?? (Hclm x ?))
+                [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
+                |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
+                [1,4: >nat_of_bitvector_bitvector_of_nat_inverse
+                  [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
+                |2,5: whd in match fetch_pseudo_instruction; normalize nodelta
+                  >nth_safe_nth
+                  [1,3: >nat_of_bitvector_bitvector_of_nat_inverse
+                    [1,3: >Heq / by refl/
+                    |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
+                    ]
+                  ]
+                |3,6: / by /
+                ]
               |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
               normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
@@ -705 +736 @@
             |3,6: whd in match short_jump_cond; whd in match absolute_jump_cond;
               cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
-              [1,3: cases daemon (* XXX should this be a property of create_label_map? *)
+              [1,3: cases (create_label_map program) #clm #Hclm
+                @le_S_to_le @(proj2 ?? (Hclm x ?))
+                [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
+                |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
+                [1,4: >nat_of_bitvector_bitvector_of_nat_inverse
+                  [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
+                |2,5: whd in match fetch_pseudo_instruction; normalize nodelta
+                  >nth_safe_nth
+                  [1,3: >nat_of_bitvector_bitvector_of_nat_inverse
+                    [1,3: >Heq / by refl/
+                    |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
+                    ]
+                  ]
+                |3,6: / by /
+                ]
               |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
               cases (vsplit bool 5 11 ?) #addr1 #addr2
@@ -720 +765 @@
               [1,2,3,6,7,24,25: #x #y
               |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
-              normalize nodelta #H @refl
+              normalize nodelta #H #Heq @refl
             |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x]
               normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
-              #Hj lapply (Hj x (refl ? x)) -Hj
+              #Hj #Heq lapply (Hj x (refl ? x)) -Hj
               whd in match expand_relative_jump; normalize nodelta
               whd in match expand_relative_jump_internal; normalize nodelta
@@ -737 +782 @@
                 [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? *)
+                  [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm
+                    @le_S_to_le @(proj2 ?? (Hclm x ?))
+                    @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
+                    [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse
+                      [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
+                    |2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta
+                      >nth_safe_nth
+                      [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse
+                        [1,3,5,7,9,11,13,15,17: >Heq %]
+                        @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
+                      ]
+                    ]
+                    >Heq / by /
+                  ]
                   #X >(le_to_leb_true … X) @refl
                 ]
@@ -753 +811 @@
                 [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? *)
+                  [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm
+                    @le_S_to_le @(proj2 ?? (Hclm x ?))
+                    @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
+                    [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse
+                      [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
+                    |2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta
+                      >nth_safe_nth
+                      [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse
+                        [1,3,5,7,9,11,13,15,17: >Heq %]
+                        @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
+                      ]
+                    ]
+                    >Heq / by /
+                  ]
                   #X >(le_to_leb_true … X) @refl
                 ]