Ignore:
Timestamp:
May 15, 2012, 11:13:14 AM (8 years ago)
Author:
mulligan
Message:

Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so all lemmas and functions that accepted a sigma before now accept a weakened sigma coupled with a policy. ASM/AssemblyProof.ma compiles until main_thm.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1947 r1948  
    4343    (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.
    4444  #b #c
    45   cases b
    46   [1:
    47     normalize //
    48   |2:
    49     normalize
    50     cases c normalize //
    51   ]
     45  cases b cases c normalize nodelta
     46  try (#_ % @I)
     47  #assm destruct %
    5248qed.
    5349
     
    14161412lemma fetch_assembly_pseudo':
    14171413  ∀lookup_labels.
    1418   ∀sigma: Word → Word × bool.
     1414  ∀sigma: Word → Word.
     1415  ∀policy: Word → bool.
    14191416  ∀ppc.
    14201417  ∀lookup_datalabels.
     
    14241421  ∀assembled.
    14251422  ∀instructions.
    1426     let 〈pc, force_long_jump〉 ≝ sigma ppc in
    1427       instructions = expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels pi →
    1428         〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi →
     1423    let pc ≝ sigma ppc in
     1424      instructions = expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi →
     1425        〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi →
    14291426          let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
    14301427            encoding_check code_memory pc pc_plus_len assembled →
    14311428              fetch_many code_memory pc_plus_len pc instructions.
    1432   #lookup_labels #sigma #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
    1433   generalize in match (refl … (sigma ppc));
    1434   cases (sigma ?) in ⊢ (??%? → %); #pc #force_long_jump #sigma_refl normalize nodelta
    1435   #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
     1429  #lookup_labels #sigma #policy #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
     1430  normalize nodelta #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
    14361431  cases (pair_destruct ?????? assembled_refl) -assembled_refl #len_refl #assembled_refl
    14371432  >len_refl >assembled_refl -len_refl
    1438   generalize in match (add 16 pc
     1433  generalize in match (add 16 (sigma ppc)
    14391434    (bitvector_of_nat 16
    14401435     (|flatten (Vector bool 8)
    14411436       (map instruction (list (Vector bool 8)) assembly1 instructions)|)));
    14421437  #final_pc
    1443   generalize in match pc; elim instructions
     1438  generalize in match (sigma ppc); elim instructions
    14441439  [1:
    14451440    #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
     
    14641459lemma fetch_assembly_pseudo:
    14651460  ∀program: pseudo_assembly_program.
    1466   ∀sigma: Word → Word × bool.
    1467   let lookup_labels ≝ λx:Identifier.\fst (sigma (address_of_word_labels_code_mem (\snd  program) x)) in
    1468   ∀ppc.∀code_memory.
     1461  ∀sigma: Word → Word.
     1462  ∀policy: Word → bool.
     1463  let lookup_labels ≝ λx:Identifier. sigma (address_of_word_labels_code_mem (\snd  program) x) in
     1464  ∀ppc.
     1465  ∀code_memory.
    14691466  let lookup_datalabels ≝ λx:Identifier.lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
    14701467  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc) in
    1471   let pc ≝ \fst (sigma ppc) in
    1472   let instructions ≝ expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels pi in
    1473   let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi in
     1468  let pc ≝ sigma ppc in
     1469  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
     1470  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
    14741471  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
    14751472    encoding_check code_memory pc pc_plus_len assembled →
    14761473      fetch_many code_memory pc_plus_len pc instructions.
    1477  #program #sigma letin lookup_labels ≝ (λx.?) #ppc #code_memory
     1474 #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #code_memory
    14781475 letin lookup_datalabels ≝ (λx.?)
    14791476 letin pi ≝ (fst ???)
    1480  letin pc ≝ (fst ???)
    1481  letin instructions ≝ (expand_pseudo_instruction ?????)
     1477 letin pc ≝ (sigma ?)
     1478 letin instructions ≝ (expand_pseudo_instruction ??????)
    14821479 @pair_elim #len #assembled #assembled_refl normalize nodelta
    14831480 #H
    14841481 generalize in match
    1485   (fetch_assembly_pseudo' lookup_labels sigma ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
    1486  #X destruct
    1487  cases (sigma ppc) in H X; #pc #force_long_jump normalize nodelta
    1488  #H #X @X try % <assembled_refl try % assumption
     1482  (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
     1483 #X destruct normalize nodelta @X try % <assembled_refl try % assumption
    14891484qed.
    14901485
     
    14981493*)
    14991494axiom assembly_ok:
    1500  ∀program,sigma,assembled,costs'.
     1495  ∀program.
     1496  ∀sigma: Word → Word.
     1497  ∀policy: Word → bool.
     1498  ∀assembled.
     1499  ∀costs'.
    15011500  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
    1502   〈assembled,costs'〉 = assembly program sigma
     1501  〈assembled,costs'〉 = assembly program sigma policy
    15031502  costs = costs' ∧
    15041503  let code_memory ≝ load_code_memory assembled in
    15051504  let datalabels ≝ construct_datalabels (\fst program) in
    1506   let lookup_labels ≝ λx.\fst (sigma (address_of_word_labels_code_mem (\snd program) x)) in 
     1505  let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem (\snd program) x) in 
    15071506  let lookup_datalabels ≝ λx. lookup_def ?? datalabels x (zero ?) in
    15081507  ∀ppc.
    15091508  let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    1510   let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi in
    1511   let pc ≝ \fst (sigma ppc) in
     1509  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
     1510  let pc ≝ sigma ppc in
    15121511  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
    15131512   encoding_check code_memory pc pc_plus_len assembled ∧
    1514        \fst (sigma newppc) = add … pc (bitvector_of_nat … len).
     1513       sigma newppc = add … pc (bitvector_of_nat … len).
    15151514
    15161515(* XXX: should we add that costs = costs'? *)
    15171516lemma fetch_assembly_pseudo2:
    1518  ∀program,sigma,ppc.
     1517  ∀program.
     1518  ∀sigma.
     1519  ∀policy.
     1520  ∀ppc.
    15191521  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
    1520   let 〈assembled, costs'〉 ≝ assembly program sigma in
     1522  let 〈assembled, costs'〉 ≝ assembly program sigma policy in
    15211523  let code_memory ≝ load_code_memory assembled in
    15221524  let data_labels ≝ construct_datalabels (\fst program) in
    1523   let lookup_labels ≝ λx.\fst (sigma (address_of_word_labels_code_mem (\snd program) x)) in 
     1525  let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem (\snd program) x) in 
    15241526  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
    15251527  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    1526   let instructions ≝ expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels pi in
    1527     fetch_many code_memory (\fst (sigma newppc)) (\fst (sigma ppc)) instructions.
    1528   * #preamble #instr_list #sigma #ppc
     1528  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
     1529    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
     1530  * #preamble #instr_list #sigma #policy #ppc
    15291531  @pair_elim #labels #costs #create_label_map_refl
    15301532  @pair_elim #assembled #costs' #assembled_refl
     
    15341536  letin lookup_datalabels ≝ (λx. ?)
    15351537  @pair_elim #pi #newppc #fetch_pseudo_refl
    1536   lapply (assembly_ok 〈preamble, instr_list〉 sigma assembled costs')
     1538  lapply (assembly_ok 〈preamble, instr_list〉 sigma policy assembled costs')
    15371539  @pair_elim #labels' #costs' #create_label_map_refl' #H
    15381540  cases (H (sym_eq … assembled_refl))
    15391541  #_
    1540   lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi))
    1541   cases (assembly_1_pseudoinstruction ?????) in ⊢ (???% → ?);
     1542  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
     1543  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
    15421544  #len #assembledi #EQ4 #H
    15431545  lapply (H ppc) >fetch_pseudo_refl #H
    1544   lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma ppc (load_code_memory assembled))
     1546  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc (load_code_memory assembled))
    15451547  >EQ4 #H1 cases H #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
    15461548  >fetch_pseudo_refl in H1; #assm @assm assumption
     
    16951697
    16961698definition code_memory_of_pseudo_assembly_program:
    1697  ∀pap:pseudo_assembly_program. (Word → Word × bool) → BitVectorTrie Byte 16
    1698 ≝ λpap,sigma.
    1699    let p ≝ assembly pap sigma in
    1700     load_code_memory (\fst p).
     1699    ∀pap:pseudo_assembly_program.
     1700      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
     1701  λpap.
     1702  λsigma.
     1703  λpolicy.
     1704    let p ≝ assembly pap sigma policy in
     1705      load_code_memory (\fst p).
    17011706
    17021707definition status_of_pseudo_status:
    1703  internal_pseudo_address_map → ∀pap.∀ps:PseudoStatus pap. ∀sigma: Word → Word × bool.
    1704   Status (code_memory_of_pseudo_assembly_program pap sigma) ≝
    1705  λM,pap,ps,sigma.
    1706   let cm ≝ code_memory_of_pseudo_assembly_program … sigma in
    1707   let pc ≝ \fst (sigma (program_counter … ps)) in
     1708    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
     1709      ∀sigma: Word → Word. ∀policy: Word → bool.
     1710        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
     1711  λM.
     1712  λpap.
     1713  λps.
     1714  λsigma.
     1715  λpolicy.
     1716  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
     1717  let pc ≝ sigma (program_counter … ps) in
    17081718  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
    17091719  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
     
    18331843*)
    18341844
    1835 definition ticks_of0: ∀p:pseudo_assembly_program. (Word → Word × bool) → Word → pseudo_instruction → nat × nat ≝
    1836   λprogram: pseudo_assembly_program.λsigma.
     1845definition ticks_of0:
     1846    ∀p:pseudo_assembly_program.
     1847      (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
     1848  λprogram: pseudo_assembly_program.
     1849  λsigma.
     1850  λpolicy.
    18371851  λppc: Word.
    18381852  λfetched. ?.
     
    19892003*)qed.
    19902004
    1991 definition ticks_of: ∀p:pseudo_assembly_program. (Word → Word × bool) → Word → nat × nat ≝
    1992   λprogram: pseudo_assembly_program.λsigma.
     2005definition ticks_of:
     2006    ∀p:pseudo_assembly_program.
     2007      (Word → Word) → (Word → bool) → Word → nat × nat ≝
     2008  λprogram: pseudo_assembly_program.
     2009  λsigma.
     2010  λpolicy.
    19932011  λppc: Word.
    19942012    let 〈preamble, pseudo〉 ≝ program in
    19952013    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
    1996      ticks_of0 program sigma ppc fetched.
     2014     ticks_of0 program sigma policy ppc fetched.
    19972015
    19982016lemma eq_rect_Type1_r:
    19992017  ∀A: Type[1].
    2000   ∀a:A.
     2018  ∀a: A.
    20012019  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
    20022020  #A #a #P #H #x #p
    20032021  generalize in match H;
    20042022  generalize in match P;
    2005   cases p
    2006   //
     2023  cases p //
    20072024qed.
    20082025
     
    21622179(*CSC: ???*)
    21632180axiom snd_assembly_1_pseudoinstruction_ok:
    2164  ∀program:pseudo_assembly_program.∀sigma.
    2165  ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels.
    2166   lookup_labels = (λx. \fst (sigma (address_of_word_labels_code_mem (\snd program) x))) →
    2167   lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    2168   \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    2169    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma (\fst (sigma ppc)) lookup_datalabels  pi) in
    2170     \fst (sigma (add … ppc (bitvector_of_nat ? 1))) =
    2171      add … (\fst (sigma ppc)) (bitvector_of_nat ? len).
     2181  ∀program: pseudo_assembly_program.
     2182  ∀sigma: Word → Word.
     2183  ∀policy: Word → bool.
     2184  ∀ppc: Word.
     2185  ∀pi.
     2186  ∀lookup_labels.
     2187  ∀lookup_datalabels.
     2188    lookup_labels = (λx. sigma (address_of_word_labels_code_mem (\snd program) x)) →
     2189    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
     2190    \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
     2191    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (sigma ppc) lookup_datalabels  pi) in
     2192      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
    21722193
    21732194lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
    2174  /2/
     2195  /2/
    21752196qed.
    21762197
    21772198(* To be moved in ProofStatus *)
    21782199lemma program_counter_set_program_counter:
    2179  ∀T,cm,s,x. program_counter T cm (set_program_counter T cm s x) = x.
    2180  //
     2200  ∀T.
     2201  ∀cm.
     2202  ∀s.
     2203  ∀x.
     2204    program_counter T cm (set_program_counter T cm s x) = x.
     2205  //
    21812206qed.
    21822207
    21832208theorem main_thm:
    2184  ∀M,M',cm,ps,sigma.
    2185   next_internal_pseudo_address_map M cm ps = Some … M' →
    2186    ∃n.
    2187       execute n … (status_of_pseudo_status M … ps sigma)
    2188     = status_of_pseudo_status M' … (execute_1_pseudo_instruction (ticks_of cm sigma) cm ps) sigma.
    2189  #M #M' * #preamble #instr_list #ps #sigma
    2190  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
    2191  @(pose … (program_counter ?? ps)) #ppc #EQppc
    2192  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma ppc) in ⊢ ?;
    2193  @pair_elim #labels #costs #H0 normalize nodelta
    2194  @pair_elim #assembled #costs' #EQ1 normalize nodelta
    2195  @pair_elim #pi #newppc #EQ2 normalize nodelta
    2196  @(pose … (λx. \fst (sigma (address_of_word_labels_code_mem instr_list x)))) #lookup_labels #EQlookup_labels
    2197  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
    2198  whd in match execute_1_pseudo_instruction; normalize nodelta
    2199  whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta
    2200  lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc
    2201  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … ppc pi … EQlookup_labels EQlookup_datalabels ?)
    2202  [>EQ2 %]
    2203  inversion pi
    2204   [2,3: (* Comment, Cost *) #ARG #EQ
    2205    #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ?????) in H3;
    2206    whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
    2207    whd in match (execute_1_pseudo_instruction0 ?????);
    2208    %{0} @split_eq_status
     2209  ∀M.
     2210  ∀M'.
     2211  ∀cm.
     2212  ∀ps.
     2213  ∀sigma.
     2214  ∀policy.
     2215    next_internal_pseudo_address_map M cm ps = Some … M' →
     2216      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
     2217        status_of_pseudo_status M' …
     2218          (execute_1_pseudo_instruction (ticks_of cm sigma policy) cm ps) sigma policy.
     2219  #M #M' * #preamble #instr_list #ps #sigma #policy
     2220  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
     2221  @(pose … (program_counter ?? ps)) #ppc #EQppc
     2222  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy ppc) in ⊢ ?;
     2223  @pair_elim #labels #costs #H0 normalize nodelta
     2224  @pair_elim #assembled #costs' #EQ1 normalize nodelta
     2225  @pair_elim #pi #newppc #EQ2 normalize nodelta
     2226  @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
     2227  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
     2228  whd in match execute_1_pseudo_instruction; normalize nodelta
     2229  whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta
     2230  lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc
     2231  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … policy … ppc pi … EQlookup_labels EQlookup_datalabels ?)
     2232  [>EQ2 %]
     2233  inversion pi
     2234  [2,3: (* Comment, Cost *)
     2235    #ARG #EQ
     2236    #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3;
     2237    whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
     2238    whd in match (execute_1_pseudo_instruction0 ?????);
     2239    %{0} @split_eq_status
    22092240   CSC: STOP HERE, was // but requires -H0 -H3 because of \fst and \pi1
    22102241   ⇒ CHANGE TO AVOID \fst and \pi1! (*
Note: See TracChangeset for help on using the changeset viewer.