Changeset 941 for src

Timestamp:

Jun 11, 2011, 11:37:20 PM (10 years ago)

Author:

sacerdot

Message:

Jmp case finished up to arithmetical properties.

File:

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

src/ASM/AssemblyProof.ma

@@ -1962 +1962 @@
 qed.
 
+lemma split_eq_status:
+ ∀T.
+ ∀A1,A2,A3,A4,A5,A6,A7,A8,A9,A10.
+ ∀B1,B2,B3,B4,B5,B6,B7,B8,B9,B10.
+  A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → A10=B10 →
+   mk_PreStatus T A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 =
+   mk_PreStatus T B1 B2 B3 B4 B5 B6 B7 B8 B9 B10.
+ //
+qed.
+
 lemma main_thm:
  ∀ps,s,s''.
@@ -2017 +2027 @@
            #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 *)
-       ]
+       | (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
+           generalize in match
+            (refl ?
+             (sub_16_with_carry
+              (sigma 〈preamble,instr_list〉 (program_counter … ps))
+              (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))
+              false))
+           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
+           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
+           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
+           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (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)
+           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ??) ? in ?) = ?)
+           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 newppc) (sign_extension lower)))
+           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
+           @split_eq_status try % change with (newpc = sigma ? (address_of_word_labels ps label))
+           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
+       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
+         generalize in match
+          (refl …
+            (split … 5 11 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))))
+         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
+         generalize in match
+          (refl …
+            (split … 5 11 (sigma 〈preamble,instr_list〉 (program_counter … ps))))
+         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
+         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
+         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
+         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #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) whd in ⊢ (??%?)
+           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
+           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
+           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
+           generalize in match (refl … (split bool 4 4 pc_bu))
+           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
+           generalize in match (refl … (split bool 3 8 rest_addr))
+           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
+           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
+           generalize in match
+            (refl …
+             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
+             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
+           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
+           @split_eq_status try %
+            [ change with (? = sigma ? (address_of_word_labels ps label))
+              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
+            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 
+              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
   |5: (* Call *)
   |6: (* Mov *)