Ignore:
Timestamp:
Jun 21, 2011, 2:02:37 AM (10 years ago)
Author:
sacerdot
Message:

The main theorem is completely broken (again).

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProof.ma

    r998 r1014  
    11include "ASM/Assembly.ma".
    22include "ASM/Interpret.ma".
     3include "ASM/StatusProofs.ma".
    34
    45definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
    … …  
    12271228   let pc ≝ ? in
    12281229   let pi ≝  \fst  (fetch_pseudo_instruction (\snd  program) ppc) in
    1229    let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc pi (refl …) (refl …) (refl …) (refl …) in
     1230   let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc (refl …) (refl …) (refl …) in
    12301231   let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi (refl …) (refl …) (refl …) in
    12311232     encoding_check code_memory pc (bitvector_of_nat … (nat_of_bitvector ? pc + len)) assembled →
    … …  
    12391240 letin pc ≝ (sigma program pol ppc)
    12401241 letin pi ≝ (\fst  (fetch_pseudo_instruction (\snd  program) ppc))
    1241  letin instructions ≝ (expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc pi (refl …) (refl …) (refl …) (refl …))
     1242 letin instructions ≝ (expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc (refl …) (refl …) (refl …))
    12421243 @pair_elim' #len #assembled #EQ1 #H
    12431244 generalize in match
    … …  
    12591260  let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
    12601261  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
    1261    ∀ppc,pi,newppc.
    1262    ∀prf:〈pi,newppc〉 = fetch_pseudo_instruction (\snd program) ppc.
     1262  ∀ppc.
     1263  let pi_newppc ≝ fetch_pseudo_instruction (\snd program) ppc in
    12631264   ∀len,assembledi.
    1264      〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi (refl …) (refl …) ? →
     1265     〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels (\fst pi_newppc) (refl …) (refl …) (refl …) →
    12651266      encoding_check code_memory (sigma program pol ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)) assembledi ∧
    1266        sigma program pol newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
    1267  <(pair_destruct_1 ????? prf) %
    1268 qed.
    1269 
    1270 (*
     1267       sigma program pol (\snd pi_newppc) = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
     1268
    12711269axiom assembly_ok_to_expand_pseudo_instruction_ok:
    12721270 ∀program,pol,assembled,costs.
    … …  
    12811279    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    12821280     ∃instructions.
    1283       Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi.
    1284 *)
    1285 
    1286 lemma fetch_assembly_pseudo2:
    1287  ∀program,pol,assembled.
     1281      Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi.
     1282
     1283(*CSC: repair me!*)
     1284axiom fetch_assembly_pseudo2:
     1285 ∀program,pol,ppc.
    12881286  let 〈labels,costs〉 ≝ build_maps program pol in
    1289   〈assembled,costs〉 = assembly program pol →
    1290    ∀ppc,pi,newppc.
    1291     let code_memory ≝ load_code_memory assembled in
    1292     let preamble ≝ \fst program in
    1293     let data_labels ≝ construct_datalabels preamble in
    1294     let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
    1295     let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
    1296     ∀prf:〈pi,newppc〉 = fetch_pseudo_instruction (\snd program) ppc.
    1297     let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels (sigma program pol ppc) pi (refl …) (refl …) ? (refl …) in
    1298      fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
    1299  [2: <(pair_destruct_1 ????? prf) %]
     1287  let assembled ≝ \fst (assembly program pol) in
     1288  let code_memory ≝ load_code_memory assembled in
     1289  let data_labels ≝ construct_datalabels (\fst program) in
     1290  let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
     1291  let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
     1292  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
     1293  let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels (sigma program pol ppc) (refl …) (refl …) (refl …) in
     1294   fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
     1295(*
    13001296 #program #pol #assembled generalize in match (assembly_ok program pol assembled)
    13011297 @pair_elim' #labels #costs #BUILD_MAPS
    … …  
    13061302 letin lookup_labels ≝ (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x))
    13071303 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
    1308  normalize nodelta #EQ generalize in match (H ASSEMBLY ppc … EQ) -H;
     1304 normalize nodelta #EQ generalize in match (H ASSEMBLY ppc) -H;
    13091305 generalize in match (fetch_assembly_pseudo program pol ppc code_memory) in ⊢ ? normalize nodelta
    1310  @pair_elim' #len #assembledi #ASSEMBLE1
     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 
    13111311 
    13121312 cases
    … …  
    13331333  [ #K3 % [2: % [% | @K3]] | @K1 ]
    13341334qed.
    1335 
    1336 
     1335*)
     1336
     1337(*
    13371338lemma fetch_assembly_pseudo2:
    13381339 ∀program,pol,assembled.
    13391340  let 〈labels,costs〉 ≝ build_maps program pol in
    1340   Some … 〈assembled,costs〉 = assembly program pol →
     1341  〈assembled,costs〉 = assembly program pol →
    13411342   ∀ppc.
    13421343    let code_memory ≝ load_code_memory assembled in
    … …  
    13481349    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    13491350     ∃instructions.
    1350       Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi ∧
     1351      Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi ∧
    13511352       fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
    13521353 #program #pol #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc
    … …  
    13601361 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
    13611362 generalize in match (fetch_assembly_pseudo program pol ppc
    1362   (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
     1363  (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?))
    13631364  (load_code_memory assembled));
    13641365 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
    … …  
    13731374  [ #K3 % [2: % [% | @K3]] | @K1 ]
    13741375qed.
     1376*)
    13751377
    13761378(* OLD?
    … …  
    15201522   
    15211523definition status_of_pseudo_status:
    1522  internal_pseudo_address_map → ∀ps:PseudoStatus. policy (code_memory … ps) → option Status ≝
     1524 internal_pseudo_address_map → ∀ps:PseudoStatus. policy (code_memory … ps) → Status ≝
    15231525 λM,ps,pol.
    15241526  let pap ≝ code_memory … ps in
    1525    match assembly pap pol with
    1526     [ None ⇒ None …
    1527     | Some p ⇒
    1528        let cm ≝ load_code_memory (\fst p) in
    1529        let pc ≝ sigma pap pol (program_counter ? ps) in
    1530        let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
    1531        let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
    1532         Some …
    1533          (mk_PreStatus (BitVectorTrie Byte 16)
    1534            cm
    1535            lir
    1536            hir
    1537            (external_ram … ps)
    1538            pc
    1539            (special_function_registers_8051 … ps)
    1540            (special_function_registers_8052 … ps)
    1541            (p1_latch … ps)
    1542            (p3_latch … ps)
    1543            (clock … ps)) ].
     1527  let p ≝ assembly pap pol in
     1528  let cm ≝ load_code_memory (\fst p) in
     1529  let pc ≝ sigma pap pol (program_counter ? ps) in
     1530  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
     1531  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
     1532     mk_PreStatus (BitVectorTrie Byte 16)
     1533      cm
     1534      lir
     1535      hir
     1536      (external_ram … ps)
     1537      pc
     1538      (special_function_registers_8051 … ps)
     1539      (special_function_registers_8052 … ps)
     1540      (p1_latch … ps)
     1541      (p3_latch … ps)
     1542      (clock … ps).
    15441543
    15451544(*
    … …  
    16401639*)
    16411640
     1641(* DEAD CODE?
    16421642lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
    16431643 ∀M:internal_pseudo_address_map.
    … …  
    16571657  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
    16581658qed.
     1659*)
    16591660
    16601661definition ticks_of0: ∀p:pseudo_assembly_program. policy p → Word → ? → nat × nat ≝
    … …  
    18201821     ticks_of0 program pol ppc fetched.
    18211822
    1822 lemma get_register_set_program_counter:
    1823  ∀T,s,pc. get_register T (set_program_counter … s pc) = get_register … s.
    1824  #T #s #pc %
    1825 qed.
    1826 
    1827 lemma get_8051_sfr_set_program_counter:
    1828  ∀T,s,pc. get_8051_sfr T (set_program_counter … s pc) = get_8051_sfr … s.
    1829  #T #s #pc %
    1830 qed.
    1831 
    1832 lemma get_bit_addressable_sfr_set_program_counter:
    1833  ∀T,s,pc. get_bit_addressable_sfr T (set_program_counter … s pc) = get_bit_addressable_sfr … s.
    1834  #T #s #pc %
    1835 qed.
    1836 
    1837 lemma low_internal_ram_set_program_counter:
    1838  ∀T,s,pc. low_internal_ram T (set_program_counter … s pc) = low_internal_ram … s.
    1839  #T #s #pc %
    1840 qed.
    1841 
    1842 lemma get_arg_8_set_program_counter:
    1843  ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) →
    1844   ∀T,s,pc,b.∀arg:l.
    1845    get_arg_8 T (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
    1846  [2,3: cases arg; *; normalize //]
    1847  #n #l #H #T #s #pc #b * *; [11: #NH @⊥ //] #X try #Y %
    1848 qed.
    1849 
    1850 lemma set_bit_addressable_sfr_set_code_memory:
    1851   ∀T, U: Type[0].
    1852   ∀ps: PreStatus ?.
    1853   ∀code_mem.
    1854   ∀x.
    1855   ∀val.
    1856   set_bit_addressable_sfr ? (set_code_memory T U ps code_mem) x val =
    1857   set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem.
    1858   #T #U #ps #code_mem #x #val
    1859   whd in ⊢ (??%?)
    1860   whd in ⊢ (???(???%?))
    1861   cases (eqb ? 128) [ normalize nodelta cases not_implemented
    1862   | normalize nodelta
    1863   cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
    1864   | normalize nodelta
    1865   cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
    1866   | normalize nodelta
    1867   cases (eqb ? 176) [ normalize nodelta %
    1868   | normalize nodelta
    1869   cases (eqb ? 153) [ normalize nodelta %
    1870   | normalize nodelta
    1871   cases (eqb ? 138) [ normalize nodelta %
    1872   | normalize nodelta
    1873   cases (eqb ? 139) [ normalize nodelta %
    1874   | normalize nodelta
    1875   cases (eqb ? 140) [ normalize nodelta %
    1876   | normalize nodelta
    1877   cases (eqb ? 141) [ normalize nodelta %
    1878   | normalize nodelta
    1879   cases (eqb ? 200) [ normalize nodelta %
    1880   | normalize nodelta
    1881   cases (eqb ? 202) [ normalize nodelta %
    1882   | normalize nodelta
    1883   cases (eqb ? 203) [ normalize nodelta %
    1884   | normalize nodelta
    1885   cases (eqb ? 204) [ normalize nodelta %
    1886   | normalize nodelta
    1887   cases (eqb ? 205) [ normalize nodelta %
    1888   | normalize nodelta
    1889   cases (eqb ? 135) [ normalize nodelta %
    1890   | normalize nodelta
    1891   cases (eqb ? 136) [ normalize nodelta %
    1892   | normalize nodelta
    1893   cases (eqb ? 137) [ normalize nodelta %
    1894   | normalize nodelta
    1895   cases (eqb ? 152) [ normalize nodelta %
    1896   | normalize nodelta
    1897   cases (eqb ? 168) [ normalize nodelta %
    1898   | normalize nodelta
    1899   cases (eqb ? 184) [ normalize nodelta %
    1900   | normalize nodelta
    1901   cases (eqb ? 129) [ normalize nodelta %
    1902   | normalize nodelta
    1903   cases (eqb ? 130) [ normalize nodelta %
    1904   | normalize nodelta
    1905   cases (eqb ? 131) [ normalize nodelta %
    1906   | normalize nodelta
    1907   cases (eqb ? 208) [ normalize nodelta %
    1908   | normalize nodelta
    1909   cases (eqb ? 224) [ normalize nodelta %
    1910   | normalize nodelta
    1911   cases (eqb ? 240) [ normalize nodelta %
    1912   | normalize nodelta
    1913     cases not_implemented
    1914   ]]]]]]]]]]]]]]]]]]]]]]]]]]
    1915 qed.
    1916 
    1917 lemma set_arg_8_set_code_memory:
    1918   ∀n:nat.
    1919   ∀l:Vector addressing_mode_tag (S n).
    1920     ¬(is_in ? l ACC_PC) →
    1921     ∀T: Type[0].
    1922     ∀U: Type[0].
    1923     ∀ps: PreStatus ?.
    1924     ∀code_mem.
    1925     ∀val.
    1926     ∀b: l.
    1927   set_arg_8 ? (set_code_memory T U ps code_mem) b val =
    1928   set_code_memory T U (set_arg_8 ? ps b val) code_mem.
    1929   [2,3: cases b; *; normalize //]
    1930   #n #l #prf #T #U #ps #code_mem #val * *;
    1931   [*:
    1932     [1,2,3,4,8,9,15,16,17,18,19: #x]
    1933     try #y whd in ⊢ (??(%)?)
    1934     whd in ⊢ (???(???(%)?))
    1935     [1,2:
    1936       cases (split bool 4 4 ?)
    1937       #nu' #nl'
    1938       normalize nodelta
    1939       cases (split bool 1 3 nu')
    1940       #bit1' #ignore'
    1941       normalize nodelta
    1942       cases (get_index_v bool 4 nu' 0 ?)
    1943       [1,2,3,4:
    1944         normalize nodelta
    1945         try %
    1946         try (@(set_bit_addressable_sfr_set_code_memory T U ps code_mem x val))
    1947         try (normalize in ⊢ (???(???%?)))
    1948       ]
    1949     |3,4: %
    1950     |*:
    1951        try normalize nodelta
    1952        normalize cases (not_implemented)
    1953     ]
    1954  ]
    1955  
    1956 
    1957 qed.
    1958 
    1959 axiom set_arg_8_set_program_counter:
    1960   ∀n:nat.
    1961   ∀l:Vector addressing_mode_tag (S n).
    1962     ¬(is_in ? l ACC_PC) →
    1963     ∀T: Type[0].
    1964     ∀ps: PreStatus ?.
    1965     ∀pc.
    1966     ∀val.
    1967     ∀b: l.
    1968   set_arg_8 ? (set_program_counter T ps pc) b val =
    1969   set_program_counter T (set_arg_8 ? ps b val) pc.
    1970   [1,2: cases b; *; normalize //]
    1971 qed.
    1972  
    1973 
    1974 lemma get_arg_8_set_code_memory:
    1975  ∀T1,T2,s,code_mem,b,arg.
    1976    get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.
    1977  #T1 #T2 #s #code_mem #b #arg %
    1978 qed.
    1979 
    1980 lemma set_code_memory_set_flags:
    1981  ∀T1,T2,s,f1,f2,f3,code_mem.
    1982   set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =
    1983    set_flags … (set_code_memory … s code_mem) f1 f2 f3.
    1984  #T1 #T2 #s #f1 #f2 #f3 #code_mem %
    1985 qed.
    1986 
    1987 lemma set_program_counter_set_flags:
    1988  ∀T1,s,f1,f2,f3,pc.
    1989   set_program_counter T1 (set_flags T1 s f1 f2 f3) pc =
    1990    set_flags … (set_program_counter … s pc) f1 f2 f3.
    1991  #T1 #s #f1 #f2 #f3 #pc  %
    1992 qed.
    1993 
    1994 lemma program_counter_set_flags:
    1995  ∀T1,s,f1,f2,f3.
    1996   program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s.
    1997  #T1 #s #f1 #f2 #f3 %
    1998 qed.
    1999 
    2000 lemma special_function_registers_8051_write_at_stack_pointer:
    2001  ∀T,s,x.
    2002     special_function_registers_8051 T (write_at_stack_pointer T s x)
    2003   = special_function_registers_8051 T s.
    2004  #T #s #x whd in ⊢ (??(??%)?)
    2005  cases (split ????) #nu #nl normalize nodelta;
    2006  cases (get_index_v bool ????) %
    2007 qed.
    2008 
    2009 lemma get_8051_sfr_write_at_stack_pointer:
    2010  ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
    2011  #T #s #x #y whd in ⊢ (??%%) //
    2012 qed.
    2013 
    2014 lemma code_memory_write_at_stack_pointer:
    2015  ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
    2016  #T #s #x whd in ⊢ (??(??%)?)
    2017  cases (split ????) #nu #nl normalize nodelta;
    2018  cases (get_index_v bool ????) %
    2019 qed.
    2020 
    2021 axiom low_internal_ram_write_at_stack_pointer:
    2022  ∀T1,T2,M,s1,s2,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
    2023   get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
    2024   low_internal_ram ? s2 = low_internal_ram T2 s3 →
    2025   sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
    2026   sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
    2027   bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
    2028    low_internal_ram T1
    2029      (write_at_stack_pointer ?
    2030        (set_8051_sfr ?
    2031          (write_at_stack_pointer ?
    2032            (set_8051_sfr ?
    2033              (set_low_internal_ram ? s1
    2034                (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? s2)))
    2035              SFR_SP sp1)
    2036           bl)
    2037         SFR_SP sp2)
    2038       bu)
    2039    = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
    2040       (low_internal_ram ?
    2041        (write_at_stack_pointer ?
    2042          (set_8051_sfr ?
    2043            (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
    2044           SFR_SP sp2)
    2045         pbu)).
    2046        
    2047 axiom high_internal_ram_write_at_stack_pointer:
    2048  ∀T1,T2,M,s1,s2,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
    2049   get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
    2050   high_internal_ram ? s2 = high_internal_ram T2 s3 →
    2051   sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
    2052   sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
    2053   bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
    2054    high_internal_ram T1
    2055      (write_at_stack_pointer ?
    2056        (set_8051_sfr ?
    2057          (write_at_stack_pointer ?
    2058            (set_8051_sfr ?
    2059              (set_high_internal_ram ? s1
    2060                (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram ? s2)))
    2061              SFR_SP sp1)
    2062           bl)
    2063         SFR_SP sp2)
    2064       bu)
    2065    = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
    2066       (high_internal_ram ?
    2067        (write_at_stack_pointer ?
    2068          (set_8051_sfr ?
    2069            (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
    2070           SFR_SP sp2)
    2071         pbu)).
    2072 
    2073 lemma set_program_counter_set_low_internal_ram:
    2074  ∀T,s,x,y.
    2075   set_program_counter T (set_low_internal_ram … s x) y =
    2076    set_low_internal_ram … (set_program_counter … s y) x.
    2077  //
    2078 qed.
    2079 
    2080 lemma set_clock_set_low_internal_ram:
    2081  ∀T,s,x,y.
    2082   set_clock T (set_low_internal_ram … s x) y =
    2083    set_low_internal_ram … (set_clock … s y) x.
    2084  //
    2085 qed.
    2086 
    2087 lemma set_program_counter_set_high_internal_ram:
    2088  ∀T,s,x,y.
    2089   set_program_counter T (set_high_internal_ram … s x) y =
    2090    set_high_internal_ram … (set_program_counter … s y) x.
    2091  //
    2092 qed.
    2093 
    2094 lemma set_clock_set_high_internal_ram:
    2095  ∀T,s,x,y.
    2096   set_clock T (set_high_internal_ram … s x) y =
    2097    set_high_internal_ram … (set_clock … s y) x.
    2098  //
    2099 qed.
    2100 
    2101 lemma set_low_internal_ram_set_high_internal_ram:
    2102  ∀T,s,x,y.
    2103   set_low_internal_ram T (set_high_internal_ram … s x) y =
    2104    set_high_internal_ram … (set_low_internal_ram … s y) x.
    2105  //
    2106 qed.
    2107 
    2108 lemma external_ram_write_at_stack_pointer:
    2109  ∀T,s,x. external_ram T (write_at_stack_pointer T s x) = external_ram T s.
    2110  #T #s #x whd in ⊢ (??(??%)?)
    2111  cases (split ????) #nu #nl normalize nodelta;
    2112  cases (get_index_v bool ????) %
    2113 qed.
    2114 
    2115 lemma special_function_registers_8052_write_at_stack_pointer:
    2116  ∀T,s,x.
    2117     special_function_registers_8052 T (write_at_stack_pointer T s x)
    2118   = special_function_registers_8052 T s.
    2119  #T #s #x whd in ⊢ (??(??%)?)
    2120  cases (split ????) #nu #nl normalize nodelta;
    2121  cases (get_index_v bool ????) %
    2122 qed.
    2123 
    2124 lemma p1_latch_write_at_stack_pointer:
    2125  ∀T,s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch T s.
    2126  #T #s #x whd in ⊢ (??(??%)?)
    2127  cases (split ????) #nu #nl normalize nodelta;
    2128  cases (get_index_v bool ????) %
    2129 qed.
    2130 
    2131 lemma p3_latch_write_at_stack_pointer:
    2132  ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s.
    2133  #T #s #x whd in ⊢ (??(??%)?)
    2134  cases (split ????) #nu #nl normalize nodelta;
    2135  cases (get_index_v bool ????) %
    2136 qed.
    2137 
    2138 lemma clock_write_at_stack_pointer:
    2139  ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s.
    2140  #T #s #x whd in ⊢ (??(??%)?)
    2141  cases (split ????) #nu #nl normalize nodelta;
    2142  cases (get_index_v bool ????) %
    2143 qed.
    2144 
    2145 axiom get_index_v_set_index:
    2146  ∀T,n,x,m,p,y. get_index_v T n (set_index T n x m y p) m p = y.
    2147 
    2148 lemma get_8051_sfr_set_8051_sfr:
    2149  ∀T,s,x,y. get_8051_sfr T (set_8051_sfr ? s x y) x = y.
    2150  #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?)
    2151  whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
    2152 qed.
    2153 
    2154 lemma program_counter_set_8051_sfr:
    2155  ∀T,s,x,y. program_counter T (set_8051_sfr ? s x y) = program_counter ? s.
    2156  //
    2157 qed.
    2158 
    2159 axiom get_arg_8_set_low_internal_ram:
    2160  ∀M,s,x,b,z. get_arg_8 M (set_low_internal_ram ? s x) b z = get_arg_8 ? s b z.
    2161 
    21621823lemma eq_rect_Type1_r:
    21631824  ∀A: Type[1].
    … …  
    21691830  cases p
    21701831  //
    2171 qed.
    2172 
    2173 lemma split_eq_status:
    2174  ∀T.
    2175  ∀A1,A2,A3,A4,A5,A6,A7,A8,A9,A10.
    2176  ∀B1,B2,B3,B4,B5,B6,B7,B8,B9,B10.
    2177   A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → A10=B10 →
    2178    mk_PreStatus T A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 =
    2179    mk_PreStatus T B1 B2 B3 B4 B5 B6 B7 B8 B9 B10.
    2180  //
    21811832qed.
    21821833
    … …  
    22771928*)
    22781929
    2279 lemma main_thm:
     1930axiom low_internal_ram_write_at_stack_pointer:
     1931 ∀T1,T2,M,s1,s2,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
     1932  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
     1933  low_internal_ram ? s2 = low_internal_ram T2 s3 →
     1934  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
     1935  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
     1936  bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
     1937   low_internal_ram T1
     1938     (write_at_stack_pointer ?
     1939       (set_8051_sfr ?
     1940         (write_at_stack_pointer ?
     1941           (set_8051_sfr ?
     1942             (set_low_internal_ram ? s1
     1943               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? s2)))
     1944             SFR_SP sp1)
     1945          bl)
     1946        SFR_SP sp2)
     1947      bu)
     1948   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
     1949      (low_internal_ram ?
     1950       (write_at_stack_pointer ?
     1951         (set_8051_sfr ?
     1952           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
     1953          SFR_SP sp2)
     1954        pbu)).
     1955
     1956axiom high_internal_ram_write_at_stack_pointer:
     1957 ∀T1,T2,M,s1,s2,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
     1958  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
     1959  high_internal_ram ? s2 = high_internal_ram T2 s3 →
     1960  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
     1961  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
     1962  bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
     1963   high_internal_ram T1
     1964     (write_at_stack_pointer ?
     1965       (set_8051_sfr ?
     1966         (write_at_stack_pointer ?
     1967           (set_8051_sfr ?
     1968             (set_high_internal_ram ? s1
     1969               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram ? s2)))
     1970             SFR_SP sp1)
     1971          bl)
     1972        SFR_SP sp2)
     1973      bu)
     1974   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
     1975      (high_internal_ram ?
     1976       (write_at_stack_pointer ?
     1977         (set_8051_sfr ?
     1978           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
     1979          SFR_SP sp2)
     1980        pbu)).
     1981
     1982lemma main_thm0:
    22801983 ∀M,M',ps,s,s'',pol.
    22811984  next_internal_pseudo_address_map M ps = Some … M' →
    2282   status_of_pseudo_status M ps pol = Some … s →
    2283   status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ? = Some … s'' →
     1985  status_of_pseudo_status M ps pol = s →
     1986  status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ? = s'' →
    22841987   ∃n. execute n s = s''.
    22851988 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
    22861989 #M #M' #ps #s #s'' #pol
    22871990 generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol)
     1991 >execute_1_pseudo_instruction_preserves_code_memory
     1992 generalize in match (refl … (assembly (code_memory … ps) pol))
     1993 generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → ?) #ASS #K <K generalize in match K; -K;
     1994 
     1995 
    22881996 whd in ⊢ (? → ? → ??%? → ??%? → ?)
    22891997 >execute_1_pseudo_instruction_preserves_code_memory
    22901998 generalize in match (refl … (assembly (code_memory … ps) pol))
     1999 generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → ?) #ASS #K <K generalize in match K; -K;
     2000 whd in ⊢ (???% → ?)
     2001 cases (build_maps (code_memory … ps) pol)
     2002 #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
     2003 cases (code_memory … ps) in pol ⊢ %;
     2004 generalize in match pol; -pol;
     2005 @(match code_memory … ps return λx. ∀e:code_memory … ps = x.? with [pair preamble instr_list ⇒ ?]) [%]
     2006 #EQ0 #pol normalize nodelta;
     2007
     2008
     2009
     2010lemma main_thm0:
     2011 ∀M,M',ps,ps',pol.
     2012  next_internal_pseudo_address_map M ps = Some … M' →
     2013  ∀H:ps' = execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps.
     2014   ∃n.
     2015      execute n (status_of_pseudo_status M ps pol)
     2016    = status_of_pseudo_status M' ps' ?.
     2017 [2: >H >execute_1_pseudo_instruction_preserves_code_memory @pol]
     2018 #M #M' #ps #ps' #pol
     2019 change with (next_internal_pseudo_address_map0 ???? = ? → ?)
     2020 generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol (program_counter … ps))
     2021 @pair_elim' #labels #costs #EQ1 normalize nodelta
     2022 whd in match execute_1_pseudo_instruction
     2023 @pair_elim' #pi #newppc #EQ2 normalize nodelta
     2024 cases pi in EQ2; normalize nodelta
     2025  [2: #ARG #MAP #H1 #H2 #EQ >MAP in EQ;
     2026 
     2027 
     2028 cases (execute_1_pseudo_instruction_preserves_code_memory ??) XX
     2029 cases (assembly ??) #assembled #costs normalize nodelta
     2030 cases (build_maps (code_memory … ps) pol) * #labels #costs whd in match eject; normalize nodelta;
     2031 cases ps in pol ⊢ %; #code_mem #lir #hir #er #pc #sfr1 #sfr2 #p1l #p3l #clock #pol
     2032 #MAP
     2033 cases (fetch_pseudo_instruction (\snd code_mem) ppc)
     2034
     2035 change with
     2036  (? → ∃n.
     2037    execute n
     2038     (set_low_internal_ram ?
     2039       (set_high_internal_ram ?
     2040         (set_program_counter ?
     2041           (set_code_memory ?? ps (load_code_memory ?))
     2042          (sigma ? pol (program_counter ? ps)))
     2043        (high_internal_ram_of_pseudo_high_internal_ram M ?))
     2044      (low_internal_ram_of_pseudo_low_internal_ram M ?))
     2045   = set_low_internal_ram ?
     2046      (set_high_internal_ram ?
     2047        (set_program_counter ?
     2048          (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory ?))
     2049         (sigma ???))
     2050       ?)
     2051     ?)
     2052 change with (next_internal_pseudo_address_map0 ???? = ? → ?)
     2053 generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol (program_counter … ps))
     2054 @pair_elim' #labels #costs #EQ1 normalize nodelta
     2055 @pair_elim' #pi #newppc #EQ2
     2056 >execute_1_pseudo_instruction_preserves_code_memory
     2057 cases (assembly ??) #assembled #costs normalize nodelta
     2058 cases (build_maps (code_memory … ps) pol) * #labels #costs whd in match eject; normalize nodelta;
     2059 cases ps in pol ⊢ %; #code_mem #lir #hir #er #pc #sfr1 #sfr2 #p1l #p3l #clock #pol
     2060 #MAP
     2061 cases (fetch_pseudo_instruction (\snd code_mem) ppc)
     2062 
     2063 
     2064 (code_memory pseudo_assembly_program ps)
     2065 #MAP
     2066
     2067 
     2068 
     2069 whd in ⊢ (? → ? → ??%? → ??%? → ?)
    22912070 generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?)
    22922071 cases (build_maps (code_memory … ps) pol)
    … …  
    26142393            |
    26152394            ] *)
     2395
     2396lemma main_thm:
     2397 ∀M,M',ps,pol.
     2398  next_internal_pseudo_address_map M ps = Some … M' →
     2399   ∃n.
     2400      execute n (status_of_pseudo_status M ps pol)
     2401    = status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ?.
     2402 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
Note: See TracChangeset for help on using the changeset viewer.