Ignore:
Timestamp:
May 17, 2012, 5:45:21 PM (8 years ago)
Author:
mulligan
Message:

Progress made on main_thm proof: trying to find a pattern to use across all ~150 goals

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1957 r1966  
    13121312
    13131313lemma destruct_bug_fix:
    1314   3 = 0 → False.
    1315   #absurd destruct(absurd)
     1314  ∀n: nat.
     1315    S n = 0 → False.
     1316  #n #absurd destruct(absurd)
    13161317qed.
    13171318
     
    13191320  ∀b: BitVector 3.
    13201321    ∃l, c, r: bool.
    1321       b ≃ [[l; c; r]] ≝ ?.
     1322      b ≃ [[l; c; r]].
    13221323  #b
    13231324  @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]]))
    13241325  [1:
    1325     #absurd @⊥ @destruct_bug_fix
     1326    #absurd @⊥ -b @(destruct_bug_fix 2)
    13261327    >absurd %
    13271328  |2:
    1328     #n #hd #tl #_ #_ #_ %{hd}
     1329    #n #hd #tl #_ #size_refl #hd_tl_refl %{hd}
     1330    cut (n = 2)
     1331    [1:
     1332    |2:
     1333      #n_refl >n_refl in tl;
    13291334    cases daemon
    13301335  ]
     1336  cases daemon
    13311337qed.
    13321338
     
    14771483    encoding_check code_memory pc pc_plus_len assembled →
    14781484      fetch_many code_memory pc_plus_len pc instructions.
    1479  #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #code_memory
    1480  letin lookup_datalabels ≝ (λx.?)
    1481  letin pi ≝ (fst ???)
    1482  letin pc ≝ (sigma ?)
    1483  letin instructions ≝ (expand_pseudo_instruction ??????)
    1484  @pair_elim #len #assembled #assembled_refl normalize nodelta
    1485  #H
    1486  generalize in match
    1487   (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
    1488  #X destruct normalize nodelta @X try % <assembled_refl try % assumption
    1489 qed.
     1485  #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #code_memory
     1486  letin lookup_datalabels ≝ (λx.?)
     1487  letin pi ≝ (fst ???)
     1488  letin pc ≝ (sigma ?)
     1489  letin instructions ≝ (expand_pseudo_instruction ??????)
     1490  @pair_elim #len #assembled #assembled_refl normalize nodelta
     1491  #H
     1492  generalize in match
     1493   (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
     1494  #X destruct normalize nodelta @X try % <assembled_refl try % assumption
     1495qed.
     1496
     1497definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
     1498  λpseudo_instruction.
     1499    match pseudo_instruction with
     1500    [ Comment c ⇒ False
     1501    | Cost c ⇒ False
     1502    | _ ⇒ True
     1503    ].
     1504
     1505definition sigma_policy_specification ≝
     1506  λprogram: pseudo_assembly_program.
     1507  λsigma: Word → Word.
     1508  λpolicy: Word → bool.
     1509  ∀ppc: Word.
     1510    let 〈preamble, instr_list〉 ≝ program in
     1511    let pc ≝ sigma ppc in
     1512    let labels ≝ \fst (create_label_cost_map instr_list) in
     1513    let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
     1514    let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc) in
     1515    let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
     1516      And (nat_of_bitvector … ppc ≤ |instr_list| →
     1517        next_pc = add 16 pc (bitvector_of_nat …
     1518          (instruction_size lookup_labels sigma policy ppc instruction)))
     1519       (Or (nat_of_bitvector … ppc < |instr_list| →
     1520         nat_of_bitvector … pc < nat_of_bitvector … next_pc)
     1521        (nat_of_bitvector … ppc = |instr_list| → next_pc = (zero …))).
    14901522
    14911523(* This is a trivial consequence of fetch_assembly_pseudo + the proof that the
     
    15011533  ∀sigma: Word → Word.
    15021534  ∀policy: Word → bool.
     1535  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
    15031536  ∀assembled.
    15041537  ∀costs'.
    15051538  let 〈preamble, instr_list〉 ≝ program in
    15061539  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
    1507   〈assembled,costs'〉 = assembly program sigma policy →
    1508   costs = costs' ∧
    1509   let code_memory ≝ load_code_memory assembled in
    1510   let datalabels ≝ construct_datalabels (\fst program) in
    1511   let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem (\snd program) x) in 
    1512   let lookup_datalabels ≝ λx. lookup_def ?? datalabels x (zero ?) in
    1513   ∀ppc.
    1514   let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    1515   let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
    1516   let pc ≝ sigma ppc in
    1517   let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
    1518    encoding_check code_memory pc pc_plus_len assembled ∧
    1519        sigma newppc = add … pc (bitvector_of_nat … len).
    1520   #program #sigma #policy #assembled #costs'
     1540  let datalabels ≝ construct_datalabels preamble in
     1541  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
     1542    〈assembled,costs'〉 = assembly program sigma policy →
     1543      costs = costs' ∧
     1544        let code_memory ≝ load_code_memory assembled in
     1545        let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in 
     1546          ∀ppc.
     1547            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in     
     1548            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
     1549            let pc ≝ sigma ppc in
     1550            let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
     1551              encoding_check code_memory pc pc_plus_len assembled ∧
     1552                  sigma newppc = add … pc (bitvector_of_nat … len).
     1553  #program #sigma #policy #sigma_policy_witness #assembled #costs'
    15211554  @pair_elim #preamble #instr_list #program_refl
    15221555  @pair_elim #labels #costs #create_label_cost_refl
    1523   #assembly_refl %
     1556  #assembly_refl % cases daemon (*
    15241557  [1:
    1525     >(?: costs = \snd (create_label_cost_map instr_list))
    1526     [1:
    1527       >(?: costs' = \snd (assembly program sigma policy))
     1558    (* XXX: lemma on BitVectorTries *)
     1559    cases daemon
     1560  |2:
     1561    #ppc #sigma_policy_specification_witness
     1562    @pair_elim #pi #newppc #fetch_pseudo_refl
     1563    cases pi
     1564    [2,3: (* Cost and Comment cases *)
     1565      #comment_or_cost normalize in ⊢ (% → ?); #absurd cases absurd
     1566    |1: (* PreInstruction cases *)
     1567      #preinstruction #_
     1568      @pair_elim #len #assembled' #assembly_1_pseudo_refl
     1569      normalize nodelta %
    15281570      [1:
    1529         whd in match assembly; normalize nodelta
    1530         >program_refl normalize nodelta
    1531         >create_label_cost_refl in ⊢ (???%); normalize nodelta
    1532         whd in match create_label_cost_map; normalize nodelta
    1533         whd in match create_label_cost_map0; normalize nodelta
     1571        cases assembled' normalize
    15341572      |2:
    1535         <assembly_refl %
    15361573      ]
    1537     |2:
    1538       >create_label_cost_refl %
    1539     ]
    1540   |2:
     1574    ]
    15411575  ]
    1542   cases daemon (* XXX: !!! *)
     1576  cases daemon (* XXX: !!! *) *)
    15431577qed.
    15441578
     
    15481582  ∀sigma.
    15491583  ∀policy.
     1584  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
    15501585  ∀ppc.
    15511586  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
     
    15581593  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
    15591594    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
    1560   * #preamble #instr_list #sigma #policy #ppc
     1595  * #preamble #instr_list #sigma #policy #sigma_policy_specification_witness #ppc
    15611596  @pair_elim #labels #costs #create_label_map_refl
    15621597  @pair_elim #assembled #costs' #assembled_refl
     
    15661601  letin lookup_datalabels ≝ (λx. ?)
    15671602  @pair_elim #pi #newppc #fetch_pseudo_refl
    1568   lapply (assembly_ok 〈preamble, instr_list〉 sigma policy assembled costs')
     1603  lapply (assembly_ok 〈preamble, instr_list〉 sigma policy sigma_policy_specification_witness assembled costs')
    15691604  normalize nodelta
    15701605  @pair_elim #labels' #costs' #create_label_map_refl' #H
     
    15761611  lapply (H ppc) >fetch_pseudo_refl #H
    15771612  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc (load_code_memory assembled))
    1578   >EQ4 #H1 cases H #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
     1613  >EQ4 #H1 cases H
     1614  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
    15791615  >fetch_pseudo_refl in H1; #assm @assm assumption
    15801616qed.
     
    22182254qed.
    22192255
    2220 definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
    2221   λpseudo_instruction.
    2222     match pseudo_instruction with
    2223     [ Comment c ⇒ False
    2224     | Cost c ⇒ False
    2225     | _ ⇒ True
    2226     ].
    2227 
    22282256lemma pair_destruct_right:
    22292257  ∀A: Type[0].
     
    22402268  ∀sigma: Word → Word.
    22412269  ∀policy: Word → bool.
     2270  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
    22422271  ∀ppc: Word.
    22432272  ∀pi.
    2244   ∀present_in_machine_code_image_witness: is_present_in_machine_code_image_p pi.
    22452273  ∀lookup_labels.
    22462274  ∀lookup_datalabels.
     
    22502278    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels  pi) in
    22512279      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
    2252   #program #sigma #policy #ppc #pi #is_present_in_machine_code_image_witness
    2253   #lookup_labels #lookup_datalabels #lookup_labels_refl #lookup_datalabels_refl
    2254   #fetch_pseudo_refl
     2280  #program #sigma #policy #sigma_policy_specification_witness #ppc #pi
     2281  #lookup_labels #lookup_datalabels
     2282  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
    22552283  normalize nodelta
    22562284  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
    2257   generalize in match is_present_in_machine_code_image_witness; -is_present_in_machine_code_image_witness
    2258   cases pi
    2259   [1:
    2260     #preinstruction #_
    2261   |2,3:
    2262     (* XXX: bug in original statement here, to prove: sigma (ppc + 1) = sigma ppc *)
    2263     #cost_or_comment normalize in ⊢ (% → ?); #absurd cases absurd
    2264   |4,5:
    2265     #identifier #_
    2266   |6:
    2267     #dptr #identifier #_
    2268   ]
    22692285  #fetch_pseudo_refl
    22702286  letin assembled ≝ (\fst (assembly program sigma policy))
    22712287  letin costs ≝ (\snd (assembly program sigma policy))
    2272   lapply (assembly_ok program sigma policy assembled costs)
     2288  lapply (assembly_ok program sigma policy sigma_policy_specification_witness assembled costs)
    22732289  @pair_elim #preamble #instr_list #program_refl
    22742290  @pair_elim #labels #costs' #create_label_cost_map_refl
     
    22762292  lapply (H ppc) -H
    22772293  @pair_elim #pi' #newppc #fetch_pseudo_refl'
    2278   @pair_elim #len #assembled #assembly1_refl #H cases H
     2294  @pair_elim #len #assembled #assembly1_refl #H
     2295  cases H
    22792296  #encoding_check_assm #sigma_newppc_refl
    22802297  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
    22812298  >pi_refl' in assembly1_refl; #assembly1_refl
    2282   >lookup_labels_refl >lookup_datalabels_refl >assembly1_refl
     2299  >lookup_labels_refl >lookup_datalabels_refl
     2300  >program_refl normalize nodelta
     2301  >assembly1_refl
    22832302  <sigma_newppc_refl
    22842303  generalize in match fetch_pseudo_refl';
Note: See TracChangeset for help on using the changeset viewer.