Changeset 1576 for src/ASM


Ignore:
Timestamp:
Nov 29, 2011, 5:22:37 PM (8 years ago)
Author:
mulligan
Message:

big changes to proofs, just two small cases remain and a few (dubious?) axioms

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1575 r1576  
    249249qed.
    250250
    251 axiom current_instruction_cost_non_zero:
     251axiom clock_execute_1:
    252252  ∀s: Status.
    253     current_instruction_cost s > 0.
    254 
    255 lemma le_monotonic_plus:
     253    clock … (execute_1 s) = current_instruction_cost s + clock … s.
     254
     255axiom plus_minus_minus:
    256256  ∀m, n, o: nat.
    257     m ≤ n → m + o ≤ n + o.
    258   #m #n #o #hyp /2/
    259 qed.
    260 
    261 lemma le_plus_to_minus_l:
     257    m - (n + o) = (m - n) - o.
     258
     259axiom plus_le_le:
    262260  ∀m, n, o: nat.
    263     n ≤ o → m ≤ o - n → m + n ≤ o.
    264   #m #n #o #le_hyp #hyp
    265   generalize in match (le_monotonic_plus m (o - n) n hyp);
    266   generalize in match (plus_minus_m_m o n le_hyp);
    267   #assm <assm in ⊢ (% → ?); #finished assumption
    268 qed.
     261    m + n ≤ o → n ≤ o.
    269262   
    270 axiom minus_m_n_gt_o_O_le_n_m:
    271   ∀m, n, o.
    272     m - n = o → o > 0 → n ≤ m.
    273 (*  #m #n #o #eq_hyp <eq_hyp in ⊢ (% → ?);
    274   normalize in ⊢ (% → ?);
    275   >le_monot *)
    276 
    277263let rec compute_max_trace_label_label_cost_is_ok
    278264  (cost_labels: BitVectorTrie costlabel 16)
     
    313299        #the_status #assm
    314300        whd in match eject; normalize nodelta
    315         >assm %
     301        cases(assm)
     302        #eq_hyp #le_hyp
     303        >eq_hyp %
    316304      |2:
    317305        cases(execute_1 start_status)
    318306        #the_status #assm
    319307        whd in match eject; normalize nodelta
    320         @(minus_m_n_gt_o_O_le_n_m ? ? (current_instruction_cost start_status))
    321         [1: assumption
    322         |2: @(current_instruction_cost_non_zero start_status)
    323         ]
     308        cases(assm)
     309        #eq_hyp #le_hyp
     310        assumption
    324311      ]
    325312    |2:
     
    332319        #the_status #assm
    333320        whd in match eject; normalize nodelta
    334         >assm %
     321        cases(assm)
     322        #eq_hyp #le_hyp
     323        >eq_hyp %
    335324      |2:
    336325        cases(execute_1 start_status)
    337326        #the_status #assm
    338327        whd in match eject; normalize nodelta
    339         @(minus_m_n_gt_o_O_le_n_m ? ? (current_instruction_cost start_status))
    340         [1: assumption
    341         |2: @current_instruction_cost_non_zero
    342         ]
     328        cases(assm)
     329        #eq_hyp #le_hyp
     330        assumption
    343331      ]
    344332    |3:
     
    360348        #trace_any_label_eq #trace_any_label_le
    361349        >trace_label_return_eq >trace_any_label_eq
    362         >commutative_plus
    363        
    364         cut ((clock (BitVectorTrie Byte 16) status_after_fun_call
    365   -clock (BitVectorTrie Byte 16) status_start_fun_call
    366   +current_instruction_cost status_pre_fun_call
    367   +(clock (BitVectorTrie Byte 16) status_final
    368     -clock (BitVectorTrie Byte 16) status_after_fun_call) =
    369           ((clock (BitVectorTrie Byte 16) status_after_fun_call
    370             - clock (BitVectorTrie Byte 16) status_start_fun_call)
    371           + (clock (BitVectorTrie Byte 16) status_final
    372           - clock (BitVectorTrie Byte 16) status_after_fun_call))
    373           + current_instruction_cost status_pre_fun_call))
    374         [ 1:
    375           cases daemon (* XXX: complete me *)
    376         | 2:
    377           #eq_hyp >eq_hyp
     350        cases(is_next)
     351        >(clock_execute_1 status_pre_fun_call) in match (clock … (execute_1 status_pre_fun_call));
     352        >commutative_plus in match (
     353          (current_instruction_cost status_pre_fun_call
     354            + clock (BitVectorTrie Byte 16) status_pre_fun_call));
     355        >plus_minus_minus
     356        <(plus_minus_m_m (clock (BitVectorTrie Byte 16) status_after_fun_call
     357  -clock (BitVectorTrie Byte 16) status_pre_fun_call) (current_instruction_cost status_pre_fun_call))
     358        [1:
    378359          >plus_minus_rearrangement_1
    379360          [1:
    380           |2, 3:
     361            %
     362          |2:
    381363            assumption
     364          |3:
     365            generalize in match trace_label_return_le;
     366            cases(is_next)
     367            >(clock_execute_1 status_pre_fun_call)
     368            @plus_le_le
    382369          ]
     370        |2:
     371          cases daemon (* XXX: todo *)
    383372        ]
    384373      |2:
    385         cases daemon (* XXX: complete me *)
     374        cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
     375          status_after_fun_call call_trace)
     376        #trace_label_return_eq cases(is_next)
     377        >clock_execute_1
     378        #trace_label_return_le
     379        lapply (plus_le_le … trace_label_return_le)
     380        #trace_label_return_le'
     381        cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
     382          status_final final_trace)
     383        #trace_any_label_eq #trace_any_label_le
     384        @(transitive_le (clock … status_pre_fun_call) (clock … status_after_fun_call) (clock … status_final))
     385        assumption
    386386      ]
    387387    |4:
    388388      #end_flag #status_pre #status_init #status_end #is_next
    389389      #trace_any_label #is_other #is_not_costed
    390       cases daemon (* XXX: complete me *)
     390      change with (
     391      let current_instruction_cost ≝ current_instruction_cost status_pre in
     392      let tail_trace_cost ≝
     393       compute_max_trace_any_label_cost cost_labels end_flag
     394        status_init status_end trace_any_label
     395      in
     396        current_instruction_cost + tail_trace_cost) in ⊢ (?(??%?)?);
     397      normalize nodelta;
     398      @conj
     399      [1:
     400        cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag
     401        status_init status_end trace_any_label)
     402        #trace_any_label_eq #trace_any_label_le
     403        >trace_any_label_eq
     404        cases(is_next)
     405        >commutative_plus
     406        >clock_execute_1
     407        >commutative_plus in match ((current_instruction_cost status_pre+clock (BitVectorTrie Byte 16) status_pre));
     408        >plus_minus_minus
     409        <plus_minus_m_m
     410        [1: %
     411        |2: cases daemon (* XXX: todo *)
     412        ]
     413      |2:
     414        cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag
     415        status_init status_end trace_any_label)
     416        #trace_any_label_eq
     417        cases(is_next)
     418        >clock_execute_1
     419        @plus_le_le
     420      ]
    391421    ]
    392422  |3:
Note: See TracChangeset for help on using the changeset viewer.