Changeset 1940 for src/ASM/Policy.ma
 Timestamp:
 May 14, 2012, 4:05:55 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r1937 r1940 6 6 include "ASM/Assembly.ma". 7 7 8 (*include alias "common/Identifiers.ma".9 include alias "ASM/BitVector.ma".*)10 8 include alias "basics/lists/list.ma". 11 9 include alias "arithmetics/nat.ma". … … 166 164 match jmp_len with 167 165 [ short_jump ⇒ [ RealInstruction (i (RELATIVE (zero 8))) ] 168  medium_jump ⇒ [ ] (* XXXthis should not happen *)166  medium_jump ⇒ [ ] (* this should not happen *) 169 167  long_jump ⇒ 170 168 [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2))); … … 228 226  Call call ⇒ 229 227 match jmp_len with 230 [ short_jump ⇒ [ ] (* XXXthis should not happen *)228 [ short_jump ⇒ [ ] (* this should not happen *) 231 229  medium_jump ⇒ [ ACALL (ADDR11 (zero 11)) ] 232 230  long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ] … … 406 404 qed. 407 405 406 lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a. 407 #a #b / by refl/ 408 qed. 409 408 410 (*lemma jump_not_in_policy: ∀prefix:list labelled_instruction. 409 411 ∀policy:(Σp:ppc_pc_map. … … 431 433 ∀program:(Σl:list labelled_instruction.l < 2^16). 432 434 ∀labels:label_map. 433 Σpolicy:ppc_pc_map. 434 And (out_of_program_none (pi1 ?? program) policy) 435 (policy_isize_sum (pi1 ?? program) labels policy) ≝ 435 Σpolicy:option ppc_pc_map. 436 match policy with 437 [ None ⇒ True 438  Some p ⇒ 439 And (And (out_of_program_none (pi1 ?? program) p) 440 (policy_isize_sum (pi1 ?? program) labels p)) 441 (\fst p < 2^16) 442 ] ≝ 436 443 λprogram.λlabels. 437 foldl_strong (option Identifier × pseudo_instruction)438 (λprefix.Σpolicy:ppc_pc_map. 444 let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction) 445 (λprefix.Σpolicy:ppc_pc_map. 439 446 And (out_of_program_none prefix policy) 440 447 (policy_isize_sum prefix labels policy)) … … 462 469  _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 463 470 ]〉 464 ) 〈0, Stub ? ?〉. 465 [ @conj 466 [ #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2 471 ) 〈0, Stub ? ?〉 in 472 if geb (\fst final_policy) 2^16 then 473 None ? 474 else 475 Some ? (pi1 ?? final_policy). 476 [ / by I/ 477  lapply p p generalize in match (foldl_strong ?????); * #p #Hp #hg 478 @conj [ @Hp  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ] 479  @conj 480 [ (* out_of_program_none *) 481 #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2 467 482 cases (le_to_or_lt_eq … Hi) Hi #Hi 468 483 cases p p #p cases p p #pc #p #Hp cases x x #l #pi cases pi … … 545 560 ] 546 561 ] 547 (*  cases (le_to_or_lt_eq … Hi) Hi #Hi548 [ >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) @conj549 [ #Hj cases p p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta550 [1: #pi cases pi normalize nodelta551 [1,2,3,6,7,33,34,35,36,37: [1,2,3,4,5,6,7: #x #y] >lookup_insert_miss552 [2,4,6,8,10,12,14,16,18,20: @bitvector_of_nat_abs553 [1,4,7,10,13,16,19,22,25,28: @(transitive_lt … (pi2 ?? program)) >prf554 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)555 @le_S_S_to_le @le_plus_n_r556 2,5,8,11,14,17,20,23,26,29: @(transitive_lt … (pi2 ?? program)) >prf557 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r558 3,6,9,12,15,18,21,24,27,30: @lt_to_not_eq @(le_S_S_to_le … Hi)559 ]560 ]561 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x >lookup_insert_miss562 [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36: @bitvector_of_nat_abs563 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52:564 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm565 @le_S_to_le @(transitive_le … Hi) @le_S_S_to_le @le_plus_n_r566 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53:567 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm568 @le_S_S_to_le @le_plus_n_r569 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54:570 @lt_to_not_eq @(le_S_S_to_le … Hi)571 ]572 ]573 9,10,11,12,13,14,15,16,17:574 [1,2,6,7: #x  3,4,5,8,9: #x #id] >lookup_insert_miss575 [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs576 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf577 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)578 @le_S_S_to_le @le_plus_n_r579 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf580 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r581 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi)582 ]583 ]584 ]585 2,3: #x >lookup_insert_miss586 [2,4: @bitvector_of_nat_abs587 [1,4: @(transitive_lt … (pi2 ?? program)) >prf588 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)589 @le_S_S_to_le @le_plus_n_r590 2,5: @(transitive_lt … (pi2 ?? program)) >prf591 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r592 3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)593 ]594 ]595 4,5: #id >lookup_insert_miss596 [2,4: @bitvector_of_nat_abs597 [1,4: @(transitive_lt … (pi2 ?? program)) >prf598 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)599 @le_S_S_to_le @le_plus_n_r600 2,5: @(transitive_lt … (pi2 ?? program)) >prf601 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r602 3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)603 ]604 ]605 6: #x #id >lookup_insert_miss606 [2: @bitvector_of_nat_abs607 [ @(transitive_lt … (pi2 ?? program)) >prf608 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)609 @le_S_S_to_le @le_plus_n_r610  @(transitive_lt … (pi2 ?? program)) >prf611 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r612  @lt_to_not_eq @(le_S_S_to_le … Hi)613 ]614 ]615 ]616 @(proj1 ?? (proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi)) Hj)617  #H @(proj2 ?? (proj2 ?? (proj1 ?? (pi2 ?? p)) i (le_S_S_to_le … Hi)))618 cases p in H; p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta619 [1: #id cases id620 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:621 [1,2,3,6,7,24,25: #x #y622 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]623 normalize nodelta >lookup_insert_miss624 [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:625 @bitvector_of_nat_abs626 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:627 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm628 @le_S_to_le @(transitive_le … Hi) @le_S_S_to_le @le_plus_n_r629 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:630 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm631 @le_S_S_to_le @le_plus_n_r632 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:633 @lt_to_not_eq @(le_S_S_to_le … Hi)634 ]635 ] / by /636 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x 3,4,5,8,9: #x #id]637 normalize nodelta >lookup_insert_miss638 [1,3,5,7,9,11,13,15,17: / by /639 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs640 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf641 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)642 @le_S_S_to_le @le_plus_n_r643 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf644 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r645 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi)646 ]647 ]648 ]649 2,3: #x >lookup_insert_miss650 [2,4: @bitvector_of_nat_abs651 [1,4: @(transitive_lt … (pi2 ?? program)) >prf652 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)653 @le_S_S_to_le @le_plus_n_r654 2,5: @(transitive_lt … (pi2 ?? program)) >prf655 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r656 3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)657 ]658 1,3: / by /659 ]660 4,5: #id >lookup_insert_miss661 [2,4: @bitvector_of_nat_abs662 [1,4: @(transitive_lt … (pi2 ?? program)) >prf663 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)664 @le_S_S_to_le @le_plus_n_r665 2,5: @(transitive_lt … (pi2 ?? program)) >prf666 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r667 3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)668 ]669 1,3: / by /670 ]671 6: #x #id >lookup_insert_miss672 [2: @bitvector_of_nat_abs673 [@(transitive_lt … (pi2 ?? program)) >prf674 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)675 @le_S_S_to_le @le_plus_n_r676 @(transitive_lt … (pi2 ?? program)) >prf677 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r678 @lt_to_not_eq @(le_S_S_to_le … Hi)679 ]680 ]681 / by /682 ]683 ]684  >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (prefix)))685 <minus_n_n whd in match (nth ????); cases x #l #ins cases ins686 [1: #pi cases pi687 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:688 [1,2,3,6,7,24,25: #x #y689 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]690 @conj691 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:692 #H cases H in ⊢ ?;693 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:694 cases p p #p cases p p #pc #pol #Hp #H elim H H #p695 normalize nodelta >lookup_insert_hit #H destruct (H)696 ]697 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x  3,4,5,8,9: #x #id]698 @conj normalize nodelta699 [(*1: #_ @(ex_intro ?? (zero ?) (ex_intro ?? (bitvector_of_nat ? (lookup_def … labels x 0)) ?))*)700 1,3,5,7,9,11,13,15,17: #_ @(ex_intro ?? short_jump ?)701 2,4,6,8,10,12,14,16,18: #_ / by I/702 ]703 cases p p #p cases p p #pc #pol #Hp >lookup_insert_hit @refl704 ]705 2,3,6: #x [3: #id] @conj706 [1,3,5: #H cases H707 2,4,6:708 cases p p #p cases p p #pc #pol #Hp #H elim H H #p709 normalize nodelta >lookup_insert_hit #H destruct (H)710 ]711 4,5: #x @conj712 [1,3: #_ @(ex_intro ?? (short_jump) ?)713 cases p p #p cases p p #pc #pol #Hp normalize nodelta >lookup_insert_hit @refl714 2,4: #_ / by I/715 ]716 ]717 ]718 ] *)719 562  cases daemon 720 563 ] … … 739 582 ¬(∀i.i < program → \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,0,short_jump〉) = long_jump). *) 740 583 741 lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a. 742 #a #b / by refl/ 743 qed. 744 745 include alias "common/Identifiers.ma". 584 (*include alias "common/Identifiers.ma".*) 746 585 include alias "ASM/BitVector.ma". 747 586 include alias "basics/lists/list.ma". … … 763 602 match y with 764 603 [ None ⇒ (* nec_plus_ultra program old_policy *) True 765  Some p ⇒ And (And (And (And (And (out_of_program_none (pi1 ?? program) p) (* labels_okay labels p ∧*)604  Some p ⇒ And (And (And (And (And (out_of_program_none (pi1 ?? program) p) 766 605 (policy_isize_sum program labels p)) 767 606 (policy_increase program old_policy p)) … … 828 667  lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma 829 668 cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉) 830 #old_pc #old_length normalize nodelta 831 (* XXX complicated proof *) cases daemon 669 #old_pc #old_length #Hpolicy @pair_elim #added #policy normalize nodelta 670 @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2 671 @conj [ @conj [ @conj [ @conj 672 [ (* out_of_program_none *) #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2 673 cases instr in Heq2; normalize nodelta 674 #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss 675 [1,3,5,7,9,11: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i ? Hi2) 676 @le_S_to_le @Hi 677 2,4,6,8,10,12: @bitvector_of_nat_abs 678 [1,4,7,10,13,16: @Hi2 679 2,5,8,11,14,17: @(transitive_lt … Hi2) @Hi 680 3,6,9,12,15,18: @sym_neq @lt_to_not_eq @Hi 681 ] 682 ] 683  cases daemon (* XXX *) 684 ] 685  (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi; 686 cases (le_to_or_lt_eq … Hi) Hi; #Hi 687 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi)) 688 <(proj2 ?? (pair_destruct ?????? Heq2)) 689 @pair_elim #opc #oj #EQ1 >lookup_insert_miss 690 [ @pair_elim #pc #j #EQ2 / by / 691  @bitvector_of_nat_abs 692 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus @le_plus_a 693 @(le_S_S_to_le … Hi) 694  @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 695  @lt_to_not_eq @(le_S_S_to_le … Hi) 696 ] 697 ] 698  <(proj2 ?? (pair_destruct ?????? Heq2)) >(injective_S … Hi) >lookup_insert_hit 699 cases instr in Heq1 Heq2; 700 [2,3,6: #x [3: #y] normalize nodelta #Heq1 #Heq2 <(proj1 ?? (pair_destruct ?????? Heq1)) 701 cases daemon 702 1,4,5: cases daemon 703 ] 704 ] 705 ] 706  (* policy_compact *) cases daemon 707 ] 708  (* added = 0 → policy_equal *) cases daemon 709 ] 832 710  normalize nodelta @conj [ @conj [ @conj [ @conj 833 711 [ #i #Hi / by refl/ … … 1263 1141 let labels ≝ create_label_map program in 1264 1142 match n with 1265 [ O ⇒ 〈true, Some ? (pi1 ?? (jump_expansion_start program labels))〉1143 [ O ⇒ 〈true,pi1 ?? (jump_expansion_start program labels)〉 1266 1144  S m ⇒ let 〈ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in 1267 1145 match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with … … 1272 1150 ] (refl … z) 1273 1151 ]. 1274 [ normalize nodelta @conj 1275 [ @(pi2 ?? (jump_expansion_start program (create_label_map program))) 1276  (* XXX *) cases daemon 1152 [ normalize nodelta cases (jump_expansion_start program (create_label_map program)) 1153 #p cases p 1154 [ / by I/ 1155  #pm / by I/ 1277 1156 ] 1278 1157  lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by / … … 1448 1327 qed. 1449 1328 1329 (* uses the second part of policy_increase *) 1450 1330 lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.l<2^16. 1451 1331 ∀policy:Σp:ppc_pc_map. … … 1529 1409 qed. 1530 1410 1411 (* uses second part of policy_increase *) 1531 1412 lemma measure_special: ∀program:(Σl:list labelled_instruction.l < 2^16). 1532 1413 ∀policy:Σp:ppc_pc_map. … … 1573 1454 whd in match (measure_int ? p ?) in Hm; 1574 1455 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))) (t) Hp) 1575 (* XXX *) cases daemon 1576 (* change proof for not_jump 1577 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉) in 1456 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉) in 1578 1457 Hm; 1579 #x cases x x #x1 #x2 #x3 1580 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉); 1581 #y cases y y #y1 #y2 #y3 1582 normalize nodelta cases x3 cases y3 normalize nodelta 1583 [1,5,9: #_ #_ // 1458 #x1 #x2 1459 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉); 1460 #y1 #y2 1461 normalize nodelta cases x2 cases y2 normalize nodelta 1462 cases daemon 1463 (* [1,5,9: #_ #_ // 1584 1464 4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 2,4,6: destruct (H2) ] 1585 1465 2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt … … 1611 1491 qed. 1612 1492 1493 (* probably needs some kind of not_jump → short *) 1613 1494 lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.l < 2^16. 1614 l ≤ program → measure_int l (jump_expansion_start program (create_label_map program)) 0 = 0. 1615 #l #program elim l 1616 [ // 1617  #h #t #Hind #Hp cases daemon 1618 1619 (* old proof whd in match (measure_int ???); 1620 cases daemo 1621 cases (dec_is_jump (nth (t) ? program 〈None ?, Comment []〉)) #Hj 1622 [ lapply 1623 (proj1 ?? (pi2 ?? 1624 (jump_expansion_start program (create_label_map program))))) 〈0,None ?〉) 1495 match jump_expansion_start program (create_label_map program) with 1496 [ None ⇒ True 1497  Some p ⇒ l ≤ program → measure_int l p 0 = 0 1498 ]. 1499 #l #program lapply (refl ? (jump_expansion_start program (create_label_map program))) 1500 cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %); #p #Hp #EQ 1501 cases p in Hp EQ; 1502 [ / by I/ 1503  #pl normalize nodelta #Hpl #EQ elim l 1504 [ / by refl/ 1505  #h #t #Hind #Hp 1506 cases daemon (* 1507 cases (dec_is_jump (nth (t) ? program 〈None ?, Comment []〉)) #Hj 1625 1508 [ normalize nodelta @Hind @le_S_to_le ] 1626 1509 @Hp … … 1786 1669 ∀program:preamble × (Σl:list labelled_instruction.l < 2^16). 1787 1670 option (Σsigma:Word → Word × bool. 1788 ∀ppc. 1671 ∀ppc:ℕ. 1672 And (ppc ≤ (\snd program) → 1789 1673 \snd 1790 1674 (half_add ? 1791 (\fst (sigma ppc))1675 (\fst (sigma (bitvector_of_nat 16 ppc))) 1792 1676 (bitvector_of_nat ? 1793 1677 (instruction_size 1794 1678 (λid. bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) id 0)) 1795 sigma ppc (\fst (fetch_pseudo_instruction (\snd program) ppc))))) 1796 = \fst (sigma (\snd (half_add ? ppc (bitvector_of_nat ? 1))))) 1797 ≝ λprogram. 1679 sigma (bitvector_of_nat ? ppc) 1680 (\fst (fetch_pseudo_instruction (\snd program) (bitvector_of_nat ? ppc)))))) 1681 = (* \fst (sigma (\snd (half_add ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? 1)))) *) 1682 \fst (sigma (bitvector_of_nat ? (S ppc)))) 1683 (ppc < (\snd program) → 1684 Or (lt_u ? (\fst (sigma (bitvector_of_nat ? ppc))) (\fst (sigma (bitvector_of_nat ? (S ppc)))) = true) 1685 (And (S ppc = (\snd program)) (\fst (sigma (bitvector_of_nat ? (S ppc))) = (zero 16)))) 1686 ) 1687 ≝ λprogram.? (* 1798 1688 let policy ≝ pi1 … (je_fixpoint (\snd program)) in 1799 1689 match policy with … … 1802 1692 «λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in 1803 1693 〈bitvector_of_nat 16 pc,jmpeqb jl long_jump〉,?» 1804 ] .1694 ]*). 1805 1695 cases daemon 1806 1696 qed.
Note: See TracChangeset
for help on using the changeset viewer.