Changeset 949 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 13, 2011, 6:42:14 PM (10 years ago)

Author:

mulligan

Message:

resolved conflict, work from today

File:

• src/ASM/AssemblyProof.ma (modified) (4 diffs)

src/ASM/AssemblyProof.ma

@@ -1499 +1499 @@
     bu@@bl = sigma (code_memory … s) (pbu@@pbl).
 
+(* changed from add to sub *)
 axiom low_internal_ram_of_pseudo_internal_ram_miss:
  ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7.
   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 
-  let 〈carr,Saddr〉 ≝ half_add ? addr (bitvector_of_nat 7 1) in
+  let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in
+  let carr ≝ get_index_v ? ? flags 1 ? in
   carr = false →
-  member ? (eq_bv 8) (false:::addr) M = false →
-   member ? (eq_bv 8) (false:::Saddr) M = false →
-    lookup ? 7 Saddr ram = lookup ? 7 Saddr (low_internal_ram … s).
+  member ? (eq_bv 8) (false:::Saddr) M = false →
+   member ? (eq_bv 8) (false:::addr) M = false →
+    lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
+  //
+qed.
 
 definition addressing_mode_ok ≝
@@ -1991 +1995 @@
       #bit1' #ignore'
       normalize nodelta
-      cases (get_index_v bool 4 nu' 1 ?)
+      cases (get_index_v bool 4 nu' 0 ?)
       [1,2,3,4:
         normalize nodelta
@@ -2004 +2008 @@
     ]
  ]
+ 
+
 qed.
 
@@ -2142 +2148 @@
 qed.
 
-(*
+axiom split_elim':
+  ∀A: Type[0].
+  ∀B: Type[1].
+  ∀l, m, v.
+  ∀T: Vector A l → Vector A m → B.
+  ∀P: B → Prop.
+    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
+      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
+
+axiom split_elim'':
+  ∀A: Type[0].
+  ∀B,B': Type[1].
+  ∀l, m, v.
+  ∀T: Vector A l → Vector A m → B.
+  ∀T': Vector A l → Vector A m → B'.
+  ∀P: B → B' → Prop.
+    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
+      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
+        (let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
+
+axiom split_append:
+  ∀A: Type[0].
+  ∀m, n: nat.
+  ∀v, v': Vector A m.
+  ∀q, q': Vector A n.
+    let 〈v', q'〉 ≝ split A m n (v@@q) in
+      v = v' ∧ q = q'.
+
+axiom split_vector_singleton:
+  ∀A: Type[0].
+  ∀n: nat.
+  ∀v: Vector A (S n).
+  ∀rest: Vector A n.
+  ∀s: Vector A 1.
+  ∀prf.
+    v = s @@ rest →
+    ((get_index_v A ? v 0 prf) ::: rest) = v.
+
+axiom sub_minus_one_seven_eight:
+  ∀v: BitVector 7.
+  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
+  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
+
 lemma blah:
-  ∀p: pseudo_instruction.
-  ∀m: pseudo_internal_address_map.
+  ∀m: internal_pseudo_address_map.
   ∀s: PseudoStatus.
   ∀arg: Byte.
-    next_internal_pseudo_address_map0 p m s (DIRECT arg) = Some ? →
-      get_arg_8 (next_internal_pseudo_address_map0 p (internal_ram ? s) s (DIRECT arg)) =
-      get_arg_8 (internal_ram ? s) (DIRECT arg).
-
+  ∀b: bool.
+    addressing_mode_ok m s (DIRECT arg) = true →
+      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
+      get_arg_8 ? s b (DIRECT arg).
+  [2, 3: normalize % ]
+  #m #s #arg #b #hyp
+  whd in ⊢ (??%%)
+  @split_elim''
+  #nu' #nl' #arg_nu_nl_eq
+  normalize nodelta
+  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
+  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
+  #get_index_v_eq
+  normalize nodelta
+  [2:
+    normalize nodelta
+    @split_elim''
+    #bit_one' #three_bits' #bit_one_three_bit_eq
+    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
+    normalize nodelta
+    generalize in match (refl ? (sub_7_with_carry ? ? ?))
+    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
+    #Saddr #carr' #Saddr_carr_eq
+    normalize nodelta
+    #carr_hyp'
+    @carr_hyp'
+    [1:
+    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
+        generalize in match (refl ? (¬(member (BitVector 8) ? arg m))) 
+        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
+        #member_eq
+        normalize nodelta
+        [2: #destr destruct(destr)
+        |1: -carr_hyp';
+            >arg_nu_nl_eq
+            <(split_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
+            [1: >get_index_v_eq in ⊢ (??%? → ?)
+            |2: @le_S @le_S @le_S @le_n
+            ]
+            cases (member (BitVector 8) ? (\fst ?) ?)
+            [1: #destr normalize in destr; destruct(destr)
+            |2:
+            ]
+        ]
+    |3: >get_index_v_eq in ⊢ (??%?)
+        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
+        >(split_vector_singleton … bit_one_three_bit_eq)
+        <arg_nu_nl_eq
+        whd in hyp:(??%?)
+        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
+        normalize nodelta [*: #ignore @sym_eq ]
+    ]
+  |
+  ].
+  
+(*
 map_address0 ... (DIRECT arg) = Some .. →
   get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =