Changeset 1039 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 24, 2011, 2:11:08 PM (9 years ago)

Author:

sacerdot

Message:

fetch_assembly_pseudo2 repaired from dependent type madness

File:

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

src/ASM/AssemblyProof.ma

@@ -1252 +1252 @@
 
 axiom assembly_ok:
- ∀program,pol,assembled.
+ ∀program,pol,assembled,costs'.
   let 〈labels,costs〉 ≝ build_maps program pol in
-  〈assembled,costs〉 = assembly program pol →
+  〈assembled,costs'〉 = assembly program pol →
+  costs = costs' ∧
   let code_memory ≝ load_code_memory assembled in
   let preamble ≝ \fst program in
@@ -1281 +1282 @@
       Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi.
 
-(*CSC: repair me!*)
-axiom fetch_assembly_pseudo2:
+lemma fetch_assembly_pseudo2:
  ∀program,pol,ppc.
 (*  let 〈labels,costs〉 ≝ build_maps program pol in *)
@@ -1293 +1293 @@
   let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels (sigma program pol ppc) (refl …) (refl …) (refl …) in
    fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
-(*
- #program #pol #assembled generalize in match (assembly_ok program pol assembled)
- @pair_elim' #labels #costs #BUILD_MAPS
- #H #ASSEMBLY #ppc #pi #newppc
+ * #preamble #instr_list #pol #ppc
+ letin assembled ≝ (\fst (assembly 〈preamble,instr_list〉 pol))
  letin code_memory ≝ (load_code_memory assembled)
- letin preamble ≝ (\fst program)
  letin data_labels ≝ (construct_datalabels preamble)
- letin lookup_labels ≝ (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x))
+ letin lookup_labels ≝ (λx. sigma … pol (address_of_word_labels_code_mem instr_list x))
  letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
- normalize nodelta #EQ generalize in match (H ASSEMBLY ppc) -H;
- generalize in match (fetch_assembly_pseudo program pol ppc code_memory) in ⊢ ? normalize nodelta
- @pair_elim' #len #assembledi #ASSEMBLE1 #H1 #H2
- generalize in match (H1 ?) [2: cases (H2 len assembledi (refl …)) #H1 #_ @H1]
- >bitvector_of_nat_nat_of_bitvector
-  #K
- 
- 
- cases
-  (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels ????)
- @split_elim' #len #assembledi #ASSEMBLY1
- 
-  @pair_elim'
- 
- normalize nodelta;
- whd in ⊢ (% → %) generalize in match (assembly_ok program pol assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;
- cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
- generalize in match (fetch_assembly_pseudo program pol ppc
-  (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
-  (load_code_memory assembled));
- whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
- whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
- normalize nodelta in EXPAND; (* HERE *)
- generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program pol ppc))) -H1; #H1
- >bitvector_of_nat_nat_of_bitvector in H1; #H1
- <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
- #H1 #H2
- cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2
- generalize in match (H1 ?? (refl …) (refl …) ?) -H1;
-  [ #K3 % [2: % [% | @K3]] | @K1 ]
-qed.
-*)
-
-(*
-lemma fetch_assembly_pseudo2:
- ∀program,pol,assembled.
-  let 〈labels,costs〉 ≝ build_maps program pol in
-  〈assembled,costs〉 = assembly program pol →
-   ∀ppc.
-    let code_memory ≝ load_code_memory assembled in
-    let preamble ≝ \fst program in
-    let data_labels ≝ construct_datalabels preamble in
-    let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
-    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
-    let expansion ≝ pol ppc in
-    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
-     ∃instructions.
-      Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi ∧
-       fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
- #program #pol #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc
- generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program pol assembled costs ASSEMBLY ppc)
- letin code_memory ≝ (load_code_memory assembled)
- letin preamble ≝ (\fst program)
- letin data_labels ≝ (construct_datalabels preamble)
- letin lookup_labels ≝ (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x))
- letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
- whd in ⊢ (% → %) generalize in match (assembly_ok program pol assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;
- cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
- generalize in match (fetch_assembly_pseudo program pol ppc
-  (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?))
-  (load_code_memory assembled));
- whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
- whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
- normalize nodelta in EXPAND; (* HERE *)
- generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program pol ppc))) -H1; #H1
- >bitvector_of_nat_nat_of_bitvector in H1; #H1
- <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
- #H1 #H2
- cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2
- generalize in match (H1 ?? (refl …) (refl …) ?) -H1;
-  [ #K3 % [2: % [% | @K3]] | @K1 ]
-qed.
-*)
+ @pair_elim' #pi #newppc #EQ1 change in EQ1 with (fetch_pseudo_instruction instr_list ? = ?)
+ generalize in match (assembly_ok ? pol assembled (\snd (assembly 〈preamble,instr_list〉 pol)))
+ @pair_elim' #labels #costs #EQ2 <eq_pair_fst_snd
+ #H cases (H (refl \ldots)) -H; #EQ3
+ generalize in match (refl … (assembly_1_pseudoinstruction … pol ppc lookup_labels lookup_datalabels ? (refl …) (refl …) (refl …)))
+ cases (assembly_1_pseudoinstruction ?????????) in ⊢ (???% → ?) #len #assembledi #EQ4
+ #H cases (H ppc len assembledi ?) [2: <EQ4 %] -H; #H1 #H2
+ generalize in match (fetch_assembly_pseudo … pol ppc (load_code_memory assembled)) in ⊢ ?
+ >EQ4 #H generalize in match (H H1) in ⊢ ? -H; >(pair_destruct_2 ????? (sym_eq … EQ1))
+ >H2 #K @K
+qed.
 
 (* OLD?
@@ -2023 +1958 @@
  (* Dependent types madness ends here *)
  letin ppc ≝ (program_counter … ps)
- generalize in match (fetch_assembly_pseudo2 ? pol ppc)
+ generalize in match (fetch_assembly_pseudo2 ? pol ppc) in ⊢ ?
  letin assembled ≝ (\fst (assembly ? pol))
  letin lookup_labels ≝ (λx. sigma ? pol (address_of_word_labels_code_mem instr_list x))
@@ -2045 +1980 @@
    #H2 #EQ %[1,3:@0]
    <MAP >(eq_bv_eq … H2) >EQ %
-
-lemma main_thm0:
- ∀M,M',ps,preamble,instr_list,pol.
- ∀EQ0 : (code_memory pseudo_assembly_program ps=〈preamble,instr_list〉).
- ∀assembled.
-  ∀H:
-   (∀ppc.
-     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc in
-     let instructions ≝
-     expand_pseudo_instruction
-                〈preamble,instr_list〉 pol ppc
-                (λx:Identifier
-                 .sigma 〈preamble,instr_list〉 pol
-                  (address_of_word_labels_code_mem instr_list x))
-                (λx:BitVector 16
-                 .lookup Identifier 16 x (construct_datalabels preamble) (zero 16))
-                (sigma 〈preamble,instr_list〉 pol ppc)
-                (refl …) (refl …) (refl …)
-     in
-     fetch_many (load_code_memory assembled)
-                (sigma 〈preamble,instr_list〉 pol newppc) (sigma 〈preamble,instr_list〉 pol ppc)
-                instructions).
- ∀MAP:(next_internal_pseudo_address_map0 pseudo_assembly_program
-                    (\fst  (fetch_pseudo_instruction instr_list
-                                 (program_counter pseudo_assembly_program ps))) M ps
-                    =Some internal_pseudo_address_map M').
- ∀ps'.
-  (ps'=execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉 pol) ps
-  →∃n:ℕ
-   .execute n
-    (set_low_internal_ram (BitVectorTrie Byte 16)
-     (set_high_internal_ram (BitVectorTrie Byte 16)
-      (set_program_counter (BitVectorTrie Byte 16)
-       (set_code_memory pseudo_assembly_program (BitVectorTrie Byte 16) ps
-        (load_code_memory assembled))
-       (sigma 〈preamble,instr_list〉 pol (program_counter pseudo_assembly_program ps)))
-      (high_internal_ram_of_pseudo_high_internal_ram M
-       (high_internal_ram pseudo_assembly_program ps)))
-     (low_internal_ram_of_pseudo_low_internal_ram M
-      (low_internal_ram pseudo_assembly_program ps)))
-    =set_low_internal_ram (BitVectorTrie Byte 16)
-     (set_high_internal_ram (BitVectorTrie Byte 16)
-      (set_program_counter (BitVectorTrie Byte 16)
-       (set_code_memory pseudo_assembly_program (BitVectorTrie Byte 16) ps'
-        (load_code_memory assembled))
-       (sigma 〈preamble,instr_list〉 pol
-        (program_counter pseudo_assembly_program ps')))
-      (high_internal_ram_of_pseudo_high_internal_ram M'
-       (high_internal_ram pseudo_assembly_program ps')))
-     (low_internal_ram_of_pseudo_low_internal_ram M'
-      (low_internal_ram pseudo_assembly_program ps'))).
- #M #M' #ps #preamble #instr_list #pol #EQ0 #assembled #H #MAP #ps'
- whd in ⊢ (???(?%?) → ?) normalize nodelta
- generalize in match (H (program_counter … ps)) -H; >EQ0 normalize nodelta;
- 
- 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:
- ∀M,M',ps,s,s'',pol.
-  next_internal_pseudo_address_map M ps = Some … M' →
-  status_of_pseudo_status M ps pol = s →
-  status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ? = s'' →
-   ∃n. execute n s = s''.
- [2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
- #M #M' #ps #s #s'' #pol
- generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol)
- >execute_1_pseudo_instruction_preserves_code_memory
- generalize in match (refl … (assembly (code_memory … ps) pol))
- generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → ?) #ASS #K <K generalize in match K; -K;
- 
- 
- whd in ⊢ (? → ? → ??%? → ??%? → ?)
- >execute_1_pseudo_instruction_preserves_code_memory
- generalize in match (refl … (assembly (code_memory … ps) pol))
- generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → ?) #ASS #K <K generalize in match K; -K;
- whd in ⊢ (???% → ?)
- cases (build_maps (code_memory … ps) pol)
- #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
- cases (code_memory … ps) in pol ⊢ %;
- generalize in match pol; -pol;
- @(match code_memory … ps return λx. ∀e:code_memory … ps = x.? with [pair preamble instr_list ⇒ ?]) [%]
- #EQ0 #pol normalize nodelta;
+  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?)
+   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
+       [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
+         whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
+         @pair_elim' * #instr #newppc' #ticks #EQ4       
+         * * #H2a #H2b whd in ⊢ (% → ?) #H2
+         >H2b >(eq_instruction_to_eq … H2a)
+         #EQ %[@1]
+         <MAP >(eq_bv_eq … H2) >EQ
+         whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)
+         cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %
+         whd in ⊢ (??%?)
+         whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
+         cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %