Changeset 1036 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 22, 2011, 11:38:55 PM (10 years ago)

Author:

sacerdot

Message:

...

File:

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

src/ASM/AssemblyProof.ma

@@ -1284 +1284 @@
 axiom fetch_assembly_pseudo2:
  ∀program,pol,ppc.
-  let 〈labels,costs〉 ≝ build_maps program pol in
+(*  let 〈labels,costs〉 ≝ build_maps program pol in *)
   let assembled ≝ \fst (assembly program pol) in
   let code_memory ≝ load_code_memory assembled in
@@ -2014 +2014 @@
  generalize in match EQ -EQ;
  generalize in match (refl … (code_memory pseudo_assembly_program ps))
- generalize in match pol generalize in ⊢ (∀_.??%? → ?)
+ generalize in match pol -pol; generalize in ⊢ (∀_.??%? → ?)
  * #preamble #instr_list #pol #EQ1 generalize in match pol -pol <EQ1 #pol #EQps' <EQps'
+ (* Dependent types madness ends here *)
+ letin ppc ≝ (program_counter … ps)
+ generalize in match (fetch_assembly_pseudo2 ? pol ppc)
+ letin assembled ≝ (\fst (assembly ? pol))
+ letin lookup_labels ≝ (λx. sigma ? pol (address_of_word_labels_code_mem instr_list x))
+ letin lookup_datalabels ≝ (λx. lookup … x (construct_datalabels preamble) (zero 16))
+ @pair_elim' #pi #newppc #EQ2
+ letin instructions ≝
+  (expand_pseudo_instruction ? pol ppc lookup_labels lookup_datalabels
+    (sigma ? pol ppc) (refl …) (refl …) (refl …))
+ change with (fetch_many ???? → ?) #H1
+ change in EQ2 with (fetch_pseudo_instruction instr_list ppc = ?)
+ change in SAFE with (next_internal_pseudo_address_map0 ???? = ?) <EQ1 in SAFE;
+ >EQ2 whd in ⊢ (??(??%??)? → ?) #SAFE
  
-
+ XX
+ 
+ whd in match execute_1_pseudo_instruction
+ 
+ whd in match expand_pseudo_instruction  normalize nodelta; 
+ whd in match execute_1_pseudo_instruction (*!!! USARE 0 !!!*) normalize nodelta; >EQ0
+ normalize in match (\snd 〈preamble,instr_list〉);
+ cases (fetch_pseudo_instruction instr_list (program_counter pseudo_assembly_program ps)) in MAP ⊢ %
+ #pi #newppc normalize nodelta; #MAP
+ cases pi in MAP; normalize nodelta;
+  [2,3: (* Comment, Cost *) #ARG #MAP whd in ⊢ (% → ?) #H2 #EQ %[1,3:@0]
+    generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M';
+    (*
+    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 i
+n H2; whd in ⊢ (% → ?)
+    #H2*) >(eq_bv_eq … H2) >EQ %
 
 lemma main_thm0: