Changeset 1602 for src/ASM/Fetch.ma

Timestamp:

Dec 13, 2011, 4:23:40 PM (9 years ago)

Author:

mulligan

Message:

giving up on fetch proofs for time being

File:

• src/ASM/Fetch.ma (modified) (15 diffs)

src/ASM/Fetch.ma

@@ -27 +27 @@
     nat_of_bitvector … v < nat_of_bitvector … (\snd (half_add … v (bitvector_of_nat … (S O)))).
 
+lemma minus_leq_minus:
+  ∀m, n, o: nat.
+    n ≤ m → o ≤ m → o ≤ n → m - n ≤ m - o.
+  #m #n #o #m_le_n #m_le_o #o_le_n
+  cases daemon (* XXX: todo *)
+qed.
+
 definition next: BitVectorTrie Byte 16 → ∀program_counter: Word.
-    nat_of_bitvector … program_counter < (code_memory_size - 1) →
-      Σret: Word × Byte. nat_of_bitvector … program_counter < nat_of_bitvector … (\fst ret) ≝
+    nat_of_bitvector … program_counter < (code_memory_size - 24) →
+      Σret: Word × Byte. nat_of_bitvector … program_counter < nat_of_bitvector … (\fst ret) ∧
+        (nat_of_bitvector … (\fst ret)) ≤ code_memory_size ≝
   λpmem: BitVectorTrie Byte 16.
   λpc: Word.
   λproof.
     〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup ? ? pc pmem (zero 8)〉.
-  @w_lt_half_add_increment @proof
+  @conj
+  [1:
+    @w_lt_half_add_increment
+    @(transitive_le
+      (S (nat_of_bitvector … pc))
+      (code_memory_size - 24)
+      (code_memory_size - 1) ? ?)
+    [1:
+      @proof
+    |2:
+      @(minus_leq_minus code_memory_size 24 1) //
+    ]
+  |2:
+    cases daemon (* XXX: todo *)
+  ]
 qed.
 
@@ -150 +172 @@
          else
           let 〈b,v〉≝  head … v in if b then
-           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
+           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
           else
            〈〈RealInstruction (DA … ACC_A), pc〉, 1〉
@@ -191 +213 @@
       let 〈b,v〉≝  head … v in if b then
        let 〈b,v〉≝  head … v in if b then
-        let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
-       else
-        let 〈b,v〉≝  head … v in if b then
-         let 〈b,v〉≝  head … v in if b then
-          let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
-         else
-          let 〈b,v〉≝  head … v in if b then
-           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
-          else
-           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
+        let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
+       else
+        let 〈b,v〉≝  head … v in if b then
+         let 〈b,v〉≝  head … v in if b then
+          let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
+         else
+          let 〈b,v〉≝  head … v in if b then
+           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
+          else
+           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
@@ -255 +277 @@
            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
           else
-           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
+           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
       else
        let 〈b,v〉≝  head … v in if b then
@@ -265 +287 @@
          else
           let 〈b,v〉≝  head … v in if b then
-           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
+           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
           else
            〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
@@ -291 +313 @@
          else
           let 〈b,v〉≝  head … v in if b then
-           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
+           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
           else
            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
@@ -320 +342 @@
          let 〈b,v〉≝  head … v in if b then
           let 〈b,v〉≝  head … v in if b then
-           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
+           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
           else
            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
@@ -344 +366 @@
          let 〈b,v〉≝  head … v in if b then
           let 〈b,v〉≝  head … v in if b then
-           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
+           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
           else
            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
@@ -367 +389 @@
          let 〈b,v〉≝  head … v in if b then
           let 〈b,v〉≝  head … v in if b then
-           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
+           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
           else
            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
@@ -399 +421 @@
            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
           else
-           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
+           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
       else
        let 〈b,v〉≝  head … v in if b then
@@ -422 +444 @@
            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
           else
-           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
+           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
@@ -441 +463 @@
            〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
           else
-           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
+           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
          else
           let 〈b,v〉≝  head … v in if b then
            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
           else
-           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
+           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
       else
        let 〈b,v〉≝  head … v in if b then
@@ -464 +486 @@
            〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
           else
-           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
+           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
          else
           let 〈b,v〉≝  head … v in if b then
@@ -471 +493 @@
            〈〈RealInstruction (NOP …), pc〉, 1〉.
   try %
+  cases daemon (*
   try (
     @(o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p
@@ -476 +499 @@
       (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof)
   )
-  [1,2,3,4,5,6,7,8:
+  [6,8,14,15,16,17,20,21,22,23,25,28,30,31,32,33,34,37,38,39,40,41,44,45,46,47,
+   50,51,52,53,56,57,58,59,65,69,71,73,75:
+    cases daemon (* XXX: segmentation fault *)
+  |1,2,3,4,5,7,8,9,10,11,12,13,18,19,24,26,27,29,35,36,42,43,48,49,54,55,60,61,
+   62,63,64,66,67,68,70,72,74,76:
     @breakup_pair' cases (next pmem pc ?)
     normalize * normalize #pc' #byte @lt_to_le
-  |3:
-    @breakup_pair' cases (next pmem pc ?)
-    normalize * normalize #pc' #byte @lt_to_le
-  |2:
-    @breakup_pair' cases(next pmem pc ?)
-    normalize * normalize #pc' #byte @lt_to_le
-  [ 
-  | 92:
-    cases (next ???) in EQ; * #pc' #content #H #EQ whd in EQ:(??%?); destruct
-    
-    
-    lapply(eq_pair_fst_snd ? ? (next pmem pc ?))
-    #assm >assm
-    cut(nat_of_bitvector … pc < nat_of_bitvector …
-      (\fst  (next pmem pc
-                (o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p (nat_of_bitvector 16 pc)
-                 code_memory_size 24 1 (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof))))
-    [ @sig2
-    | #assm @lt_to_le assumption
-    ]
-  |92:
-    check next.
-    lapply pc -pc
-    @sig2
-  cases daemon (* XXX: requires rewrite of the above to make it more russell friendly *)
+  [30:
+    generalize in match pc in EQ; #pc' #EQ' -pc
+    cut(nat_of_bitvector … pc < nat_of_bitvector … pc')
+    [1:
+      cut(pc' = \fst (next pmem pc (o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p (nat_of_bitvector 16 pc)
+         code_memory_size 24 1 (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof)))
+      [1:
+        //
+      |2:
+        #assm >assm @sig2
+      ]
+    | #lt_assm
+      lapply(transitive_le
+        (S (nat_of_bitvector … pc))
+        (nat_of_bitvector … pc')
+        (S (nat_of_bitvector … pc')) lt_assm ?)
+      [1:
+        //
+      |2:
+        #le_assm
+        lapply(transitive_le
+          (S (nat_of_bitvector … pc))
+          (S (nat_of_bitvector … pc'))
+          (code_memory_size - 1) le_assm ?)
+        [2:
+          //
+        |1:
+          @(o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p
+            (nat_of_bitvector … pc) code_memory_size 24 1 ? ?)
+          [1:
+            @le_S_S @le_S_S @le_O_n
+          |2:
+            assumption
+          ]
+        ]
+      ]
+    ] XXX: blah! *)
 qed.