Changeset 2221 for src/ASM/Assembly.ma

Timestamp:

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

Author:

boender

Message:

• removed cases daemon from PolicyFront?

File:

• src/ASM/Assembly.ma (modified) (4 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.