Changeset 1900 for src/ASM/CostsProof.ma
- Timestamp:
- Apr 23, 2012, 6:22:28 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CostsProof.ma
r1898 r1900 601 601 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k)) 602 602 on trace: 603 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →603 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → 604 604 ∃reachable_witness: reachable_program_counter cm total_program_size pc. 605 605 pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres). … … 616 616 (trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final) 617 617 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k)) 618 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →618 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → 619 619 ∃reachable_witness: reachable_program_counter cm total_program_size pc. 620 620 pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres)) … … 632 632 (trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final) 633 633 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k)) 634 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →634 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → 635 635 ∃reachable_witness: reachable_program_counter cm total_program_size pc. 636 636 pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres)) … … 664 664 <(tech_cost_of_label_shift ??? [?] ? i) // 665 665 |2: 666 whd in ⊢ (???%); (* XXX: should be easy *) 667 cases daemon 666 change with (? = lookup_present ? ? ? ? ?) 667 generalize in match (tech_cost_of_label0 ? ? ? ? ? ?); 668 normalize in match (nth_safe ? ? ? ?); 669 whd in costed_assm; lapply costed_assm -costed_assm 670 inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels) 671 [1: 672 #_ #absurd cases absurd 673 |2: 674 normalize nodelta #cost_label #Some_assm #_ #p 675 cases (dom_codom ? p ? Some_assm) 676 #reachable_witness #block_cost_assm <block_cost_assm 677 cases (block_cost ? ? ? ? ? ?) 678 #cost -block_cost_assm #block_cost_assm 679 cases (block_cost_assm ? ? ? trace_any_label (refl …)) 680 #_ #assm >assm % 681 ] 668 682 ] 669 683 |3: … … 707 721 ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final. 708 722 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k). 709 ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →723 ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → 710 724 ∃reachable_witness: reachable_program_counter code_memory total_program_size pc. 711 725 pi1 … (block_cost code_memory pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres). … … 725 739 ∀good_program_witness: good_program code_memory total_program_size. 726 740 ∀cost_labels: BitVectorTrie costlabel 16. 741 ∀cost_labels_injective: 742 (∀pc,pc',l. 743 lookup_opt costlabel 16 pc cost_labels=Some costlabel l 744 →lookup_opt costlabel 16 pc' cost_labels=Some costlabel l→pc=pc'). 727 745 ∀reachable_program_counter_witness: 728 746 ∀lbl: costlabel. … … 733 751 ∀final: Status code_memory. 734 752 ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final. 735 let cost_map ≝ traverse_code code_memory cost_labels total_program_size total_program_size_invariant753 let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective total_program_size total_program_size_invariant 736 754 reachable_program_counter_witness good_program_witness in 737 755 let ctrace ≝ compute_cost_trace_label_return code_memory … trace in … … 739 757 [1: 740 758 #code_memory #total_program_size #total_program_size_invariant #good_program_witness 741 #cost_labels # reachable_program_counter_witness #initial #final #trace759 #cost_labels #cost_labels_injective #reachable_program_counter_witness #initial #final #trace 742 760 @compute_max_trace_label_return_cost_ok_with_trace_aux try assumption 743 761 |2: … … 745 763 ] 746 764 normalize nodelta 747 cases (traverse_code ? ? ? ? ? ? )765 cases (traverse_code ? ? ? ? ? ? ?) 748 766 #cost_map * #dom_codom #codom_dom try assumption 749 767 #pc #k #lookup_opt_assm @(dom_codom … lookup_opt_assm)
Note: See TracChangeset
for help on using the changeset viewer.