Changeset 2110 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 26, 2012, 4:05:15 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2108 r2110 1511 1511 lemma assembly_ok: 1512 1512 ∀program. 1513 ∀length_proof: \snd program <2^16.1513 ∀length_proof: \snd program ≤ 2^16. 1514 1514 ∀sigma: Word → Word. 1515 1515 ∀policy: Word → bool. … … 1533 1533 sigma newppc = add … pc (bitvector_of_nat … len). 1534 1534 #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs' 1535 @pair_elim #preamble #instr_list #EQprogram1536 1535 cases (assembly program sigma policy) * #assembled' #costs'' 1537 >EQprogram normalize nodelta1538 @pair_elim #labels #costs #EQcreate_label_cost_refl normalize nodelta1539 # assembly_ok #Pair_eq destruct(Pair_eq) whd1540 #ppc #ppc_ok1541 @pair_elim #pi #newppc #EQfetch_pseudo_instruction1542 >EQprogram in sigma_policy_witness; #sigma_policy_witness1543 lapply (assembly_ok sigma_policy_witness ? ppc ?)1544 [2: >EQprogram in length_proof; #length_proof; assumption ] try assumption1545 > EQfetch_pseudo_instruction normalize nodelta1536 @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %); 1537 cut (instr_list ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok 1538 #H lapply (H sigma_policy_witness instr_list_ok) H whd in ⊢ (% → ?); 1539 @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %); 1540 * #assembly_ok1 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd 1541 #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction 1542 @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd 1543 lapply (assembly_ok2 ppc ?) try // assembly_ok2 1544 >eq_fetch_pseudo_instruction 1546 1545 change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<assembledi.?) → ?) 1547 @pair_elim #len #assembledi #EQassembly_1_pseudo_instruction 1548 letin lookup_labels ≝ (λx.sigma (bitvector_of_nat 16 (lookup_def ASMTag ℕ labels x O))) 1549 letin lookup_datalabels ≝ (λx. lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)) 1550 >(? : assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi = 〈len,assembledi〉) 1551 [2: <EQassembly_1_pseudo_instruction % ] 1552 whd in ⊢ (% → ?); #assembly_ok % 1553 [2: (*CSC: Use Jaap's invariant here *) cases daemon 1554 1: 1555 lapply (load_code_memory_ok assembledi ?) 1556 [1: 1557 lapply sigma_policy_witness whd in match sigma_policy_specification; 1558 normalize nodelta * #_ #relevant 1559 (* XXX: wait for Jaap to propagate the property that program 1560 is less than 2^16. 1561 *) 1546 > (?:((λx.bitvector_of_nat ? (lookup_def … labels x 0)) = 1547 (λx.address_of_word_labels_code_mem instr_list x))) 1548 [2: lapply (create_label_cost_map_ok 〈preamble,instr_list〉) >create_label_cost_refl 1549 #H (*CSC: REQUIRES FUNCTIONAL EXTENSIONALITY; REPHRASE THE LEMMA *) cases daemon ] 1550 >eq_assembly_1_pseudoinstruction 1551 whd in ⊢ (% → ?); #assembly_ok 1552 % 1553 [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction)) 1554 >snd_fetch_pseudo_instruction 1555 cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) H 1556 #spw1 #_ >spw1 spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f 1557 >eq_fetch_pseudo_instruction whd in match instruction_size; 1558 normalize nodelta (*CSC: TRUE, NEEDS LEMMA AND FUNCTIONAL EXTENSIONALITY *) 1562 1559 cases daemon 1563 1560  lapply (load_code_memory_ok assembled' ?) [ assumption ] 1564 1561 #load_code_memory_ok 1565 cut (len=assembled i)1562 cut (len=assembled) 1566 1563 [1: (*CSC: provable before cleaning *) 1567 1564 cases daemon … … 1569 1566 #EQlen 1570 1567 (* Nice statement here *) 1571 cut (∀j. ∀H: j < assembled i.1572 nth_safe Byte j assembled iH =1568 cut (∀j. ∀H: j < assembled. 1569 nth_safe Byte j assembled H = 1573 1570 \snd (next (load_code_memory assembled') 1574 1571 (bitvector_of_nat 16 … … 1579 1576 2: 1580 1577 assembly_ok load_code_memory_ok generalize in match (sigma ppc); >EQlen len 1581 elim assembled i1578 elim assembled 1582 1579 [1: 1583 #pc #_ whd (*<add_zero %1584 1580 #pc #_ whd <add_zero % 1581  #hd #tl #IH #pc #H % 1585 1582 [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); H #H 1586 1583 >H H whd in ⊢ (??%?); <add_zero // 1587 1584  >(?: add … pc (bitvector_of_nat … (S (tl))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (tl))) 1588 [2: (*CSC: TRUE, ARITHMETIC*) cases daemon]1585 [2: <add_bitvector_of_nat_Sm @add_associative ] 1589 1586 @IH IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ] 1590 <(nth_safe_prepend … [hd] … LTj) #IH >IH 1591 (*CSC: TRUE, ARITHMETICS*) 1592 cases daemon 1593 ] 1594 ] *) cases daemon 1595 ] 1596 cases daemon 1587 <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm 1588 >add_associative % ]] 1589 ]] 1597 1590 qed. 1598 1591 … … 1600 1593 lemma fetch_assembly_pseudo2: 1601 1594 ∀program. 1602 ∀length_proof: \snd program <2^16.1595 ∀length_proof: \snd program ≤ 2^16. 1603 1596 ∀sigma. 1604 1597 ∀policy. … … 1973 1966 match pol lookup_labels ppc with 1974 1967 [ short_jump ⇒ 〈2, 2〉 1975  medium_jump ⇒ ?1968  absolute_jump ⇒ ? 1976 1969  long_jump ⇒ 〈4, 4〉 1977 1970 ] *) … … 1979 1972 match pol lookup_labels ppc with 1980 1973 [ short_jump ⇒ 〈2, 2〉 1981  medium_jump ⇒ ?1974  absolute_jump ⇒ ? 1982 1975  long_jump ⇒ 〈4, 4〉 1983 1976 ] *) … … 1985 1978 match pol lookup_labels ppc with 1986 1979 [ short_jump ⇒ 〈2, 2〉 1987  medium_jump ⇒ ?1980  absolute_jump ⇒ ? 1988 1981  long_jump ⇒ 〈4, 4〉 1989 1982 ] *) … … 1991 1984 match pol lookup_labels ppc with 1992 1985 [ short_jump ⇒ 〈2, 2〉 1993  medium_jump ⇒ ?1986  absolute_jump ⇒ ? 1994 1987  long_jump ⇒ 〈4, 4〉 1995 1988 ] *) … … 1997 1990 match pol lookup_labels ppc with 1998 1991 [ short_jump ⇒ 〈2, 2〉 1999  medium_jump ⇒ ?1992  absolute_jump ⇒ ? 2000 1993  long_jump ⇒ 〈4, 4〉 2001 1994 ] *) … … 2003 1996 match pol lookup_labels ppc with 2004 1997 [ short_jump ⇒ 〈2, 2〉 2005  medium_jump ⇒ ?1998  absolute_jump ⇒ ? 2006 1999  long_jump ⇒ 〈4, 4〉 2007 2000 ] *) … … 2009 2002 match pol lookup_labels ppc with 2010 2003 [ short_jump ⇒ 〈2, 2〉 2011  medium_jump ⇒ ?2004  absolute_jump ⇒ ? 2012 2005  long_jump ⇒ 〈4, 4〉 2013 2006 ] *) … … 2015 2008 match pol lookup_labels ppc with 2016 2009 [ short_jump ⇒ 〈2, 2〉 2017  medium_jump ⇒ ?2010  absolute_jump ⇒ ? 2018 2011  long_jump ⇒ 〈4, 4〉 2019 2012 ] *) … … 2021 2014 match pol lookup_labels ppc with 2022 2015 [ short_jump ⇒ 〈2, 2〉 2023  medium_jump ⇒ ?2016  absolute_jump ⇒ ? 2024 2017  long_jump ⇒ 〈4, 4〉 2025 2018 ] *) … … 2320 2313 lemma snd_assembly_1_pseudoinstruction_ok: 2321 2314 ∀program: pseudo_assembly_program. 2322 ∀program_length_proof: \snd program <2^16.2315 ∀program_length_proof: \snd program ≤ 2^16. 2323 2316 ∀sigma: Word → Word. 2324 2317 ∀policy: Word → bool.
Note: See TracChangeset
for help on using the changeset viewer.