Changeset 1039


Ignore:
Timestamp:
Jun 24, 2011, 2:11:08 PM (8 years ago)
Author:
sacerdot
Message:

fetch_assembly_pseudo2 repaired from dependent type madness

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1037 r1039  
    12521252
    12531253axiom assembly_ok:
    1254  ∀program,pol,assembled.
     1254 ∀program,pol,assembled,costs'.
    12551255  let 〈labels,costs〉 ≝ build_maps program pol in
    1256   〈assembled,costs〉 = assembly program pol →
     1256  〈assembled,costs'〉 = assembly program pol →
     1257  costs = costs' ∧
    12571258  let code_memory ≝ load_code_memory assembled in
    12581259  let preamble ≝ \fst program in
     
    12811282      Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi.
    12821283
    1283 (*CSC: repair me!*)
    1284 axiom fetch_assembly_pseudo2:
     1284lemma fetch_assembly_pseudo2:
    12851285 ∀program,pol,ppc.
    12861286(*  let 〈labels,costs〉 ≝ build_maps program pol in *)
     
    12931293  let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels (sigma program pol ppc) (refl …) (refl …) (refl …) in
    12941294   fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
    1295 (*
    1296  #program #pol #assembled generalize in match (assembly_ok program pol assembled)
    1297  @pair_elim' #labels #costs #BUILD_MAPS
    1298  #H #ASSEMBLY #ppc #pi #newppc
     1295 * #preamble #instr_list #pol #ppc
     1296 letin assembled ≝ (\fst (assembly 〈preamble,instr_list〉 pol))
    12991297 letin code_memory ≝ (load_code_memory assembled)
    1300  letin preamble ≝ (\fst program)
    13011298 letin data_labels ≝ (construct_datalabels preamble)
    1302  letin lookup_labels ≝ (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x))
     1299 letin lookup_labels ≝ (λx. sigma … pol (address_of_word_labels_code_mem instr_list x))
    13031300 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
    1304  normalize nodelta #EQ generalize in match (H ASSEMBLY ppc) -H;
    1305  generalize in match (fetch_assembly_pseudo program pol ppc code_memory) in ⊢ ? normalize nodelta
    1306  @pair_elim' #len #assembledi #ASSEMBLE1 #H1 #H2
    1307  generalize in match (H1 ?) [2: cases (H2 len assembledi (refl …)) #H1 #_ @H1]
    1308  >bitvector_of_nat_nat_of_bitvector
    1309   #K
    1310  
    1311  
    1312  cases
    1313   (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels ????)
    1314  @split_elim' #len #assembledi #ASSEMBLY1
    1315  
    1316   @pair_elim'
    1317  
    1318  normalize nodelta;
    1319  whd in ⊢ (% → %) generalize in match (assembly_ok program pol assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;
    1320  cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
    1321  generalize in match (fetch_assembly_pseudo program pol ppc
    1322   (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
    1323   (load_code_memory assembled));
    1324  whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
    1325  whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
    1326  normalize nodelta in EXPAND; (* HERE *)
    1327  generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program pol ppc))) -H1; #H1
    1328  >bitvector_of_nat_nat_of_bitvector in H1; #H1
    1329  <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
    1330  #H1 #H2
    1331  cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2
    1332  generalize in match (H1 ?? (refl …) (refl …) ?) -H1;
    1333   [ #K3 % [2: % [% | @K3]] | @K1 ]
    1334 qed.
    1335 *)
    1336 
    1337 (*
    1338 lemma fetch_assembly_pseudo2:
    1339  ∀program,pol,assembled.
    1340   let 〈labels,costs〉 ≝ build_maps program pol in
    1341   〈assembled,costs〉 = assembly program pol →
    1342    ∀ppc.
    1343     let code_memory ≝ load_code_memory assembled in
    1344     let preamble ≝ \fst program in
    1345     let data_labels ≝ construct_datalabels preamble in
    1346     let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
    1347     let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
    1348     let expansion ≝ pol ppc in
    1349     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    1350      ∃instructions.
    1351       Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi ∧
    1352        fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
    1353  #program #pol #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc
    1354  generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program pol assembled costs ASSEMBLY ppc)
    1355  letin code_memory ≝ (load_code_memory assembled)
    1356  letin preamble ≝ (\fst program)
    1357  letin data_labels ≝ (construct_datalabels preamble)
    1358  letin lookup_labels ≝ (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x))
    1359  letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
    1360  whd in ⊢ (% → %) generalize in match (assembly_ok program pol assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;
    1361  cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
    1362  generalize in match (fetch_assembly_pseudo program pol ppc
    1363   (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?))
    1364   (load_code_memory assembled));
    1365  whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
    1366  whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
    1367  normalize nodelta in EXPAND; (* HERE *)
    1368  generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program pol ppc))) -H1; #H1
    1369  >bitvector_of_nat_nat_of_bitvector in H1; #H1
    1370  <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
    1371  #H1 #H2
    1372  cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2
    1373  generalize in match (H1 ?? (refl …) (refl …) ?) -H1;
    1374   [ #K3 % [2: % [% | @K3]] | @K1 ]
    1375 qed.
    1376 *)
     1301 @pair_elim' #pi #newppc #EQ1 change in EQ1 with (fetch_pseudo_instruction instr_list ? = ?)
     1302 generalize in match (assembly_ok ? pol assembled (\snd (assembly 〈preamble,instr_list〉 pol)))
     1303 @pair_elim' #labels #costs #EQ2 <eq_pair_fst_snd
     1304 #H cases (H (refl \ldots)) -H; #EQ3
     1305 generalize in match (refl … (assembly_1_pseudoinstruction … pol ppc lookup_labels lookup_datalabels ? (refl …) (refl …) (refl …)))
     1306 cases (assembly_1_pseudoinstruction ?????????) in ⊢ (???% → ?) #len #assembledi #EQ4
     1307 #H cases (H ppc len assembledi ?) [2: <EQ4 %] -H; #H1 #H2
     1308 generalize in match (fetch_assembly_pseudo … pol ppc (load_code_memory assembled)) in ⊢ ?
     1309 >EQ4 #H generalize in match (H H1) in ⊢ ? -H; >(pair_destruct_2 ????? (sym_eq … EQ1))
     1310 >H2 #K @K
     1311qed.
    13771312
    13781313(* OLD?
     
    20231958 (* Dependent types madness ends here *)
    20241959 letin ppc ≝ (program_counter … ps)
    2025  generalize in match (fetch_assembly_pseudo2 ? pol ppc)
     1960 generalize in match (fetch_assembly_pseudo2 ? pol ppc) in ⊢ ?
    20261961 letin assembled ≝ (\fst (assembly ? pol))
    20271962 letin lookup_labels ≝ (λx. sigma ? pol (address_of_word_labels_code_mem instr_list x))
     
    20451980   #H2 #EQ %[1,3:@0]
    20461981   <MAP >(eq_bv_eq … H2) >EQ %
    2047 
    2048 lemma main_thm0:
    2049  ∀M,M',ps,preamble,instr_list,pol.
    2050  ∀EQ0 : (code_memory pseudo_assembly_program ps=〈preamble,instr_list〉).
    2051  ∀assembled.
    2052   ∀H:
    2053    (∀ppc.
    2054      let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc in
    2055      let instructions ≝
    2056      expand_pseudo_instruction
    2057                 〈preamble,instr_list〉 pol ppc
    2058                 (λx:Identifier
    2059                  .sigma 〈preamble,instr_list〉 pol
    2060                   (address_of_word_labels_code_mem instr_list x))
    2061                 (λx:BitVector 16
    2062                  .lookup Identifier 16 x (construct_datalabels preamble) (zero 16))
    2063                 (sigma 〈preamble,instr_list〉 pol ppc)
    2064                 (refl …) (refl …) (refl …)
    2065      in
    2066      fetch_many (load_code_memory assembled)
    2067                 (sigma 〈preamble,instr_list〉 pol newppc) (sigma 〈preamble,instr_list〉 pol ppc)
    2068                 instructions).
    2069  ∀MAP:(next_internal_pseudo_address_map0 pseudo_assembly_program
    2070                     (\fst  (fetch_pseudo_instruction instr_list
    2071                                  (program_counter pseudo_assembly_program ps))) M ps
    2072                     =Some internal_pseudo_address_map M').
    2073  ∀ps'.
    2074   (ps'=execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉 pol) ps
    2075   →∃n:ℕ
    2076    .execute n
    2077     (set_low_internal_ram (BitVectorTrie Byte 16)
    2078      (set_high_internal_ram (BitVectorTrie Byte 16)
    2079       (set_program_counter (BitVectorTrie Byte 16)
    2080        (set_code_memory pseudo_assembly_program (BitVectorTrie Byte 16) ps
    2081         (load_code_memory assembled))
    2082        (sigma 〈preamble,instr_list〉 pol (program_counter pseudo_assembly_program ps)))
    2083       (high_internal_ram_of_pseudo_high_internal_ram M
    2084        (high_internal_ram pseudo_assembly_program ps)))
    2085      (low_internal_ram_of_pseudo_low_internal_ram M
    2086       (low_internal_ram pseudo_assembly_program ps)))
    2087     =set_low_internal_ram (BitVectorTrie Byte 16)
    2088      (set_high_internal_ram (BitVectorTrie Byte 16)
    2089       (set_program_counter (BitVectorTrie Byte 16)
    2090        (set_code_memory pseudo_assembly_program (BitVectorTrie Byte 16) ps'
    2091         (load_code_memory assembled))
    2092        (sigma 〈preamble,instr_list〉 pol
    2093         (program_counter pseudo_assembly_program ps')))
    2094       (high_internal_ram_of_pseudo_high_internal_ram M'
    2095        (high_internal_ram pseudo_assembly_program ps')))
    2096      (low_internal_ram_of_pseudo_low_internal_ram M'
    2097       (low_internal_ram pseudo_assembly_program ps'))).
    2098  #M #M' #ps #preamble #instr_list #pol #EQ0 #assembled #H #MAP #ps'
    2099  whd in ⊢ (???(?%?) → ?) normalize nodelta
    2100  generalize in match (H (program_counter … ps)) -H; >EQ0 normalize nodelta;
    2101  
    2102  whd in match expand_pseudo_instruction  normalize nodelta;
    2103  whd in match execute_1_pseudo_instruction (*!!! USARE 0 !!!*) normalize nodelta; >EQ0
    2104  normalize in match (\snd 〈preamble,instr_list〉);
    2105  cases (fetch_pseudo_instruction instr_list (program_counter pseudo_assembly_program ps)) in MAP ⊢ %
    2106  #pi #newppc normalize nodelta; #MAP
    2107  cases pi in MAP; normalize nodelta;
    2108   [2,3: (* Comment, Cost *) #ARG #MAP whd in ⊢ (% → ?) #H2 #EQ %[1,3:@0]
    2109     generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M';
    2110     (*
    2111     normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 i
    2112 n H2; whd in ⊢ (% → ?)
    2113     #H2*) >(eq_bv_eq … H2) >EQ %
    2114 
    2115 
    2116 
    2117 lemma main_thm0:
    2118  ∀M,M',ps,s,s'',pol.
    2119   next_internal_pseudo_address_map M ps = Some … M' →
    2120   status_of_pseudo_status M ps pol = s →
    2121   status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ? = s'' →
    2122    ∃n. execute n s = s''.
    2123  [2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
    2124  #M #M' #ps #s #s'' #pol
    2125  generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol)
    2126  >execute_1_pseudo_instruction_preserves_code_memory
    2127  generalize in match (refl … (assembly (code_memory … ps) pol))
    2128  generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → ?) #ASS #K <K generalize in match K; -K;
    2129  
    2130  
    2131  whd in ⊢ (? → ? → ??%? → ??%? → ?)
    2132  >execute_1_pseudo_instruction_preserves_code_memory
    2133  generalize in match (refl … (assembly (code_memory … ps) pol))
    2134  generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → ?) #ASS #K <K generalize in match K; -K;
    2135  whd in ⊢ (???% → ?)
    2136  cases (build_maps (code_memory … ps) pol)
    2137  #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
    2138  cases (code_memory … ps) in pol ⊢ %;
    2139  generalize in match pol; -pol;
    2140  @(match code_memory … ps return λx. ∀e:code_memory … ps = x.? with [pair preamble instr_list ⇒ ?]) [%]
    2141  #EQ0 #pol normalize nodelta;
     1982  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?)
     1983   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
     1984       [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
     1985         whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
     1986         @pair_elim' * #instr #newppc' #ticks #EQ4       
     1987         * * #H2a #H2b whd in ⊢ (% → ?) #H2
     1988         >H2b >(eq_instruction_to_eq … H2a)
     1989         #EQ %[@1]
     1990         <MAP >(eq_bv_eq … H2) >EQ
     1991         whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)
     1992         cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %
     1993         whd in ⊢ (??%?)
     1994         whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
     1995         cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
    21421996
    21431997
Note: See TracChangeset for help on using the changeset viewer.