Changeset 1904


Ignore:
Timestamp:
Apr 26, 2012, 5:03:23 PM (7 years ago)
Author:
mulligan
Message:

Problem with proof fixed by noting that problem is actually irrelevant

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1903 r1904  
    545545      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
    546546        program_counter'' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
    547         (∃n:ℕ.
     547        (* (∃n:ℕ.
    548548            trace_any_label_length code_memory' cost_labels
    549549              trace_ends_flag0 start_status0 final_status0 the_trace0
    550550                + S n
    551                   = total_program_size)
     551                  = total_program_size) *) True
    552552                  pi1
    553553                    =compute_paid_trace_any_label code_memory' cost_labels
    554554                     trace_ends_flag0 start_status0 final_status0 the_trace0
    555555    else (pi1=O) )
    556    →(∃n:ℕ.
     556   → (* (∃n:ℕ.
    557557     trace_any_label_length code_memory' cost_labels trace_ends_flag
    558558      start_status final_status the_trace
    559559      +S n
    560560      =total_program_size)
    561     ∧ticks+pi1
     561    *) True ∧ticks+pi1
    562562     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    563563      start_status final_status the_trace.
     
    600600          #exists_assm #recursive_block_cost_assm %
    601601          [1:
    602             cases exists_assm #exists_n #total_program_size_refl
     602            cases exists_assm (* #exists_n #total_program_size_refl
    603603            <total_program_size_refl
    604604            %{(exists_n - (nat_of_bitvector 16
     
    608608                  (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))}
    609609            <plus_n_Sm <plus_n_Sm @eq_f >commutative_plus
    610             cases daemon
     610            cases daemon *) @I
    611611          |2:
    612612            >recursive_block_cost_assm
     
    672672          normalize nodelta #new_recursive_assm >new_recursive_assm %
    673673          [1:
     674          (*
    674675            %{(pred total_program_size)} whd in ⊢ (??%?);
    675676            @S_pred
    676             @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
     677            @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) *) @I
    677678          |2:
    678679            cut(ticks = \snd (fetch code_memory'
     
    727728  ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
    728729  ∀classify_assm: ASM_classify0 instruction = cl_jump.
    729    (∃n:ℕ
     730   (* (∃n:ℕ
    730731     .trace_any_label_length code_memory' cost_labels trace_ends_flag
    731732      start_status final_status the_trace
    732733      +S n
    733734      =total_program_size)
    734     ticks
     735    *) True ∧ ticks
    735736     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    736737      start_status final_status the_trace.
     
    751752    whd in match (trace_any_label_length … (tal_base_not_return …));
    752753    whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); %
    753     [1:
     754    [1: (*
    754755      %{(pred total_program_size)} whd in ⊢ (??%?);
    755756      @S_pred
    756       @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
     757      @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) *)
     758      @I
    757759    |2:
    758760      <FETCH %
     
    808810                .program_counter''
    809811                 =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
    810                  →(∃n:ℕ
     812                 →True (*(∃n:ℕ
    811813                   .trace_any_label_length code_memory' cost_labels trace_ends_flag0
    812814                    start_status0 final_status0 the_trace0
    813815                    +S n
    814                     =total_program_size)
     816                    =total_program_size) *)
    815817                  ∧pi1
    816818                   =compute_paid_trace_any_label code_memory' cost_labels
    817819                    trace_ends_flag0 start_status0 final_status0 the_trace0) 
    818820   else (pi1=O) 
    819    →(∃n:ℕ
     821   →True (*(∃n:ℕ
    820822     .trace_any_label_length code_memory' cost_labels trace_ends_flag
    821823      start_status final_status the_trace
    822824      +S n
    823       =total_program_size)
     825      =total_program_size) *)
    824826    ∧ticks+pi1
    825827     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
     
    867869        #program_counter_assm >program_counter_assm <Some_lookup_opt
    868870        normalize nodelta #new_recursive_assm >new_recursive_assm %
    869         [1:
     871        [1: (*
    870872          %{(pred total_program_size)} whd in ⊢ (??%?);
    871873          @S_pred
    872           @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
     874          @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) *) @I
    873875        |2:
    874876          cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
     
    913915            @plus_right_monotone
    914916            whd in ⊢ (???%); <FETCH %
    915           |1:
     917          |1: (*
    916918            cases exists_assm #exists_n #trace_total_program_size_assm
    917919            generalize in match execute_assm; destruct #execute_assm
     
    922924            @plus_left_monotone @sym_eq <commutative_plus in ⊢ (???%);
    923925            @plus_minus_m_m
    924             cases daemon (* XXX: !!! *)
     926            cases daemon (* XXX: !!! *) *) @I
    925927          ]
    926928        |2,4:
     
    960962  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
    961963  ∀classify_assm: ASM_classify0 instruction = cl_return.
    962     (∃n:ℕ
     964    (* (∃n:ℕ
    963965     .trace_any_label_length code_memory' cost_labels trace_ends_flag
    964966      start_status final_status the_trace
    965967      +S n
    966       =total_program_size)
     968      =total_program_size) *) True
    967969    ∧ticks
    968970     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
     
    983985    whd in match (trace_any_label_length … (tal_base_return …));
    984986    whd in match (compute_paid_trace_any_label … (tal_base_return …)); %
    985     [1:
     987    [1: (*
    986988      %{(pred total_program_size)} whd in ⊢ (??%?);
    987989      @S_pred
    988       @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
     990      @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) *)
     991      @I
    989992    |2:
    990993      <FETCH %
     
    10301033            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    10311034              program_counter' = program_counter … start_status →
    1032                 (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size)
     1035                (* (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) *) True
    10331036                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
    10341037          else
     
    10541057            ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
    10551058              program_counter' = program_counter … start_status →
    1056                 (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size)
     1059                (* (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) *) True
    10571060                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
    10581061          [ RET                    ⇒ λinstr. ticks
     
    10931096            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    10941097              program_counter' = program_counter … start_status →
    1095                 (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size)
     1098                (* (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) *) True
    10961099                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
    10971100          | false ⇒
     
    12721275        ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    12731276          program_counter' = program_counter … start_status →
    1274             (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size)
     1277            (* (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) *) True
    12751278              cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
    12761279  λcode_memory: BitVectorTrie Byte 16.
Note: See TracChangeset for help on using the changeset viewer.