Changeset 938 for src

Timestamp:

Jun 10, 2011, 6:36:55 PM (10 years ago)

Author:

sacerdot

Message:

...

Location:

src/ASM

Files:

• Assembly.ma (modified) (5 diffs)
• AssemblyProof.ma (modified) (2 diffs)

src/ASM/Assembly.ma

@@ -202 +202 @@
                  match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
                   [ DATA16 w ⇒ λ_.
-                     let 〈b1,b2〉 ≝ split ? 8 8 w in
+                     let b1_b2 ≝ split ? 8 8 w in
+                     let b1 ≝ \fst b1_b2 in
+                     let b2 ≝ \fst b1_b2 in
                       [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
                   | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
@@ -352 +354 @@
      match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
       [ ADDR11 w ⇒ λ_.
-         let 〈v1,v2〉 ≝ split ? 3 8 w in
+         let v1_v2 ≝ split ? 3 8 w in
+         let v1 ≝ \fst v1_v2 in
+         let v2 ≝ \snd v1_v2 in
           [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
@@ -358 +362 @@
      match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
       [ ADDR11 w ⇒ λ_.
-         let 〈v1,v2〉 ≝ split ?  3 8 w in
+         let v1_v2 ≝ split ? 3 8 w in
+         let v1 ≝ \fst v1_v2 in
+         let v2 ≝ \snd v1_v2 in
           [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
@@ -366 +372 @@
      match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
       [ ADDR16 w ⇒ λ_.
-         let 〈b1,b2〉 ≝ split ? 8 8 w in
+         let b1_b2 ≝ split ? 8 8 w in
+         let b1 ≝ \fst b1_b2 in
+         let b2 ≝ \snd b1_b2 in
           [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
@@ -372 +380 @@
      match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
       [ ADDR16 w ⇒ λ_.
-         let 〈b1,b2〉 ≝ split ? 8 8 w in
+         let b1_b2 ≝ split ? 8 8 w in
+         let b1 ≝ \fst b1_b2 in
+         let b2 ≝ \snd b1_b2 in
           [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)

src/ASM/AssemblyProof.ma

@@ -1761 +1761 @@
     | Comment comment ⇒ 〈0, 0〉
     | Cost cost ⇒ 〈0, 0〉
-    | Jmp jmp ⇒ 〈0, 2〉
-    | Call call ⇒ 〈0, 2〉
-    | Mov dptr tgt ⇒ 〈0, 2〉
+    | Jmp jmp ⇒ 〈2, 2〉
+    | Call call ⇒ 〈2, 2〉
+    | Mov dptr tgt ⇒ 〈2, 2〉
     ].
   cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
@@ -1984 +1984 @@
     normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
     #H2 >(eq_bv_to_eq … H2) >EQ %
-  |4: (* Jmp *)
+  |4: (* Jmp *) #label
+      whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
+       [3: (* long *) #H1 #H2 #EQ %[@1]
+           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
+           change in ⊢ (? → ??%?) with (execute_1_0 ??)
+           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
+           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
+           >H2b >(eq_instruction_to_eq … H2a)
+           generalize in match EQ; -EQ;
+           (*whd in ⊢ (???% → ??%?);*)
+           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
+           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
+       | (* short *)
+       | (* medium *)
+       ] *)
   |5: (* Call *)
   |6: (* Mov *)