Changeset 1665


Ignore:
Timestamp:
Jan 27, 2012, 5:05:25 PM (6 years ago)
Author:
mulligan
Message:

progress on closing holes in block_cost' proof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1663 r1665  
    485485    m = n → m + o = n + o.
    486486  #m #n #o #refl >refl %
     487qed.
     488
     489axiom as_execute_preserves_code_memory:
     490  ∀cost_labels : BitVectorTrie costlabel 16.
     491  ∀start_status: ASM_abstract_status cost_labels.
     492  ∀final_status: ASM_abstract_status cost_labels.
     493    as_execute … start_status final_status →
     494      code_memory … start_status = code_memory … final_status.
     495
     496axiom trace_label_return_preserves_code_memory:
     497  ∀cost_labels : BitVectorTrie costlabel 16.
     498  ∀start_status: ASM_abstract_status cost_labels.
     499  ∀final_status: ASM_abstract_status cost_labels.
     500  ∀the_trace   : trace_label_return … start_status final_status.
     501    code_memory … start_status = code_memory … final_status.
     502
     503(* XXX: indexing bug re-emerges! *)
     504example fetch_half_add:
     505  ∀cost_labels: BitVectorTrie costlabel 16.
     506  ∀the_status : ASM_abstract_status cost_labels.
     507    \snd (\fst (fetch (code_memory … the_status) (program_counter … the_status))) =
     508      \snd (half_add 16 (program_counter (BitVectorTrie Byte 16) the_status)
     509        (bitvector_of_nat … (\snd (fetch (code_memory … the_status) (program_counter … the_status))))).
     510  cases daemon
     511qed.
     512
     513axiom half_add_minus_right:
     514  ∀size : nat.
     515  ∀left : BitVector size.
     516  ∀right: nat.
     517  nat_of_bitvector … (\snd (half_add … left (bitvector_of_nat … right))) -
     518    nat_of_bitvector … left = right.
     519
     520lemma minus_plus_cancel:
     521  ∀m, n : nat.
     522  ∀proof: n ≤ m.
     523    (m - n) + n = m.
     524  #m #n #proof /2 by plus_minus/
    487525qed.
    488526
     
    587625      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    588626      destruct
     627      whd in match (compute_paid_trace_any_label … (tal_base_call …));
     628      whd in match (trace_any_label_length … (tal_base_call …));
    589629      cases(recursive_assm status_pre_fun_call status_final doesnt_end_with_ret
    590630        (tal_base_call (ASM_abstract_status cost_labels) status_pre_fun_call
    591631          (execute_1 status_pre_fun_call) status_final
    592           (refl Status (execute_1 status_pre_fun_call)) classifier_assm
    593           after_return_assm trace_label_return costed_assm) ? ?)
    594       [2: %
    595       |3:
    596       |1:
     632            (refl Status (execute_1 status_pre_fun_call)) classifier_assm
     633              after_return_assm trace_label_return costed_assm) ? ?)
     634      [1:
     635        * #recursive_n #recursive_trace_total #recursive_block_cost_assm %
     636        [1:
     637          %{(pred total_program_size)}
     638          whd in ⊢ (??%?);
     639          >S_pred [1: % ]
     640          <recursive_trace_total
     641          @lt_O_S
     642        |2:
     643          >recursive_block_cost_assm
     644          whd in ⊢ (??(??%)?); <FETCH
     645          (* XXX: ??? *)
     646        ]
     647      |2:
     648        %
     649      |3:
     650        cut(program_counter'' = \snd (\fst (fetch (code_memory … status_pre_fun_call) (program_counter … status_pre_fun_call))))
     651        [1:
     652          cases FETCH %
     653        |2:
     654          #program_counter_hyp'' >program_counter_hyp''
     655          whd in after_return_assm; <after_return_assm
     656          whd in match (current_instruction_cost status_pre_fun_call);
     657          @fetch_half_add
     658        ]
    597659      ]
     660      [1:
    598661    |4:
    599662      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    600663      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
    601664      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    602       #final_status_refl #the_trace_refl destruct
     665      #final_status_refl #the_trace_refl
     666      generalize in match execute_assm; destruct #execute_assm
    603667      whd in match (compute_paid_trace_any_label … (tal_step_call …));
    604668      whd in match (trace_any_label_length … (tal_step_call …));
    605669      cases(recursive_assm status_after_fun_call status_final end_flag trace_any_label ? ?)
    606670      [1:
    607         * #recursive_n #recursive_trace_total #recursive_block_cost_assm
    608         >recursive_block_cost_assm <recursive_trace_total %
     671        * #recursive_n #recursive_trace_total #recursive_block_cost_assm %
    609672        [1:
    610           %
     673          <recursive_trace_total %
    611674          [1:
     675            @(recursive_n - (current_instruction_cost status_pre_fun_call))
    612676          |2:
     677            whd in after_return_assm; cases after_return_assm
     678            >half_add_minus_right in ⊢ (??%?);
     679            >commutative_plus in ⊢ (???%);
    613680            >commutative_plus in ⊢ (??%?);
    614             >commutative_plus in ⊢ (???%);
     681            <associative_plus in ⊢ (??%?);
     682            @plus_right_monotone
     683            cut(current_instruction_cost status_pre_fun_call ≤ recursive_n)
     684            [1:
     685              (* XXX: ??? *)
     686            |2:
     687              #current_instruction_cost_assm
     688              <minus_Sn_m in ⊢ (??%?); [2: assumption ]
     689              >minus_plus_cancel [1: % ]
     690              @le_S assumption
     691            ]
    615692          ]
    616693        |2:
     694          >recursive_block_cost_assm
    617695          @plus_right_monotone
    618696          whd in match (current_instruction_cost status_pre_fun_call);
     
    620698        ]
    621699      |2:
     700        lapply (trace_label_return_preserves_code_memory … (execute_1 status_pre_fun_call) status_after_fun_call)
     701        #hyp cases (hyp trace_label_return)
     702        @as_execute_preserves_code_memory whd %
    622703      |3:
     704        cut(program_counter'' = \snd (\fst (fetch (code_memory … status_pre_fun_call) (program_counter … status_pre_fun_call))))
     705        [1:
     706          cases FETCH %
     707        |2:
     708          #program_counter_hyp'' >program_counter_hyp''
     709          whd in after_return_assm; <after_return_assm
     710          whd in match (current_instruction_cost status_pre_fun_call);
     711          @fetch_half_add
     712        ]
    623713      ]
    624714    |5:
Note: See TracChangeset for help on using the changeset viewer.