Ignore:
Timestamp:
Jun 21, 2011, 4:27:06 AM (8 years ago)
Author:
sacerdot
Message:

One intermediate version of main_thm0 close to be repaired.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1014 r1015  
    19791979          SFR_SP sp2)
    19801980        pbu)).
     1981
     1982lemma main_thm0:
     1983 ∀M,M',ps,preamble,instr_list,pol.
     1984 ∀EQ0 : (code_memory pseudo_assembly_program ps=〈preamble,instr_list〉).
     1985 ∀assembled.
     1986  ∀H:
     1987   (∀ppc.
     1988     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc in
     1989     let instructions ≝
     1990     expand_pseudo_instruction
     1991                〈preamble,instr_list〉 pol ppc
     1992                (λx:Identifier
     1993                 .sigma 〈preamble,instr_list〉 pol
     1994                  (address_of_word_labels_code_mem instr_list x))
     1995                (λx:BitVector 16
     1996                 .lookup Identifier 16 x (construct_datalabels preamble) (zero 16))
     1997                (sigma 〈preamble,instr_list〉 pol ppc)
     1998                (refl …) (refl …) (refl …)
     1999     in
     2000     fetch_many (load_code_memory assembled)
     2001                (sigma 〈preamble,instr_list〉 pol newppc) (sigma 〈preamble,instr_list〉 pol ppc)
     2002                instructions).
     2003 ∀MAP:(next_internal_pseudo_address_map0 pseudo_assembly_program
     2004                    (\fst  (fetch_pseudo_instruction instr_list
     2005                                 (program_counter pseudo_assembly_program ps))) M ps
     2006                    =Some internal_pseudo_address_map M').
     2007 ∀ps'.
     2008  (ps'=execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉 pol) ps
     2009  →∃n:ℕ
     2010   .execute n
     2011    (set_low_internal_ram (BitVectorTrie Byte 16)
     2012     (set_high_internal_ram (BitVectorTrie Byte 16)
     2013      (set_program_counter (BitVectorTrie Byte 16)
     2014       (set_code_memory pseudo_assembly_program (BitVectorTrie Byte 16) ps
     2015        (load_code_memory assembled))
     2016       (sigma 〈preamble,instr_list〉 pol (program_counter pseudo_assembly_program ps)))
     2017      (high_internal_ram_of_pseudo_high_internal_ram M
     2018       (high_internal_ram pseudo_assembly_program ps)))
     2019     (low_internal_ram_of_pseudo_low_internal_ram M
     2020      (low_internal_ram pseudo_assembly_program ps)))
     2021    =set_low_internal_ram (BitVectorTrie Byte 16)
     2022     (set_high_internal_ram (BitVectorTrie Byte 16)
     2023      (set_program_counter (BitVectorTrie Byte 16)
     2024       (set_code_memory pseudo_assembly_program (BitVectorTrie Byte 16) ps'
     2025        (load_code_memory assembled))
     2026       (sigma 〈preamble,instr_list〉 pol
     2027        (program_counter pseudo_assembly_program ps')))
     2028      (high_internal_ram_of_pseudo_high_internal_ram M'
     2029       (high_internal_ram pseudo_assembly_program ps')))
     2030     (low_internal_ram_of_pseudo_low_internal_ram M'
     2031      (low_internal_ram pseudo_assembly_program ps'))).
     2032 #M #M' #ps #preamble #instr_list #pol #EQ0 #assembled #H #MAP #ps'
     2033 whd in ⊢ (???(?%?) → ?) normalize nodelta
     2034 generalize in match (H (program_counter … ps)) -H; >EQ0 normalize nodelta;
     2035 
     2036 whd in match expand_pseudo_instruction  normalize nodelta;
     2037 whd in match execute_1_pseudo_instruction (*!!! USARE 0 !!!*) normalize nodelta; >EQ0
     2038 normalize in match (\snd 〈preamble,instr_list〉);
     2039 cases (fetch_pseudo_instruction instr_list (program_counter pseudo_assembly_program ps)) in MAP ⊢ %
     2040 #pi #newppc normalize nodelta; #MAP
     2041 cases pi in MAP; normalize nodelta;
     2042  [2,3: (* Comment, Cost *) #ARG #MAP whd in ⊢ (% → ?) #H2 #EQ %[1,3:@0]
     2043    generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M';
     2044    (*
     2045    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 i
     2046n H2; whd in ⊢ (% → ?)
     2047    #H2*) >(eq_bv_eq … H2) >EQ %
     2048
     2049
    19812050
    19822051lemma main_thm0:
Note: See TracChangeset for help on using the changeset viewer.