Changeset 1573 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Nov 28, 2011, 5:13:04 PM (8 years ago)
Author:
mulligan
Message:

more complicated than it appears :(

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1571 r1573  
     1
    12include "ASM/ASMCosts.ma".
    23include "ASM/WellLabeled.ma".
     
    250251lemma current_instruction_cost_non_zero:
    251252  ∀s: Status.
    252     0 ≤ current_instruction_cost s.
    253   //
    254 qed.
     253    current_instruction_cost s > 0.
     254  #s
     255  cases s
     256  #code_memory #hi_ram #lo_ram #x_ram #pc #sfr_8051 #sfr_8052 #p1_latch
     257  #p2_latch #clock
     258  change with (\snd  (fetch ? ?)) in ⊢ (?%?);
     259  change with (fetch0 ? ?) in match (fetch ? ?);
     260  change with (
     261     let 〈pc,v〉 ≝ next code_memory pc in 
     262     let 〈b,v0〉 ≝head bool 7 v in
     263       ?) in match (fetch0 ? ?);
     264  normalize nodelta;
     265
     266  cases(fetch (code_memory … s) (program_counter … s))
     267  #instruction_pc
     268  cases(instruction_pc)
     269  #instruction #pc
     270  cases(instruction)
     271  [ #addr11
    255272
    256273lemma le_monotonic_plus:
     
    276293qed.
    277294   
    278 lemma minus_m_n_le_n_m:
     295axiom minus_m_n_gt_o_O_le_n_m:
    279296  ∀m, n, o.
    280297    m - n = o → o > 0 → n ≤ m.
    281   #m #n #o #eq_hyp
    282   cases o
    283   [ #absrd normalize in absrd; @le
    284   normalize in ⊢ (% → ?);
    285   <eq_hyp in ⊢ (% → ?);
    286   #lt_hyp
    287   generalize in match (le_plus_to_minus_l 1 n m ? lt_hyp);
    288   [1: /2/ |
    289 qed.
    290  
    291298
    292299let rec compute_max_trace_label_label_cost_is_ok
     
    333340        #the_status #assm
    334341        whd in match eject; normalize nodelta
    335         @(minus_m_n_gt_o_0_le_n_m ? ? (current_instruction_cost start_status))
     342        @(minus_m_n_gt_o_O_le_n_m ? ? (current_instruction_cost start_status))
    336343        [1: assumption
    337         |2: @current_instruction_cost_non_zero
     344        |2: @(current_instruction_cost_non_zero start_status)
    338345        ]
    339346      ]
     
    352359        #the_status #assm
    353360        whd in match eject; normalize nodelta
    354         @(minus_m_n_gt_o_0_le_n_m ? ? (current_instruction_cost start_status))
     361        @(minus_m_n_gt_o_O_le_n_m ? ? (current_instruction_cost start_status))
    355362        [1: assumption
    356363        |2: @current_instruction_cost_non_zero
     
    375382        #trace_any_label_eq #trace_any_label_le
    376383        >trace_label_return_eq >trace_any_label_eq
    377         cases daemon (* XXX: complete me *)
     384        >commutative_plus
     385       
     386        cut ((clock (BitVectorTrie Byte 16) status_after_fun_call
     387  -clock (BitVectorTrie Byte 16) status_start_fun_call
     388  +current_instruction_cost status_pre_fun_call
     389  +(clock (BitVectorTrie Byte 16) status_final
     390    -clock (BitVectorTrie Byte 16) status_after_fun_call) =
     391          ((clock (BitVectorTrie Byte 16) status_after_fun_call
     392            - clock (BitVectorTrie Byte 16) status_start_fun_call)
     393          + (clock (BitVectorTrie Byte 16) status_final
     394          - clock (BitVectorTrie Byte 16) status_after_fun_call))
     395          + current_instruction_cost status_pre_fun_call))
     396        [ 1:
     397          cases daemon (* XXX: complete me *)
     398        | 2:
     399          #eq_hyp >eq_hyp
     400          >plus_minus_rearrangement_1
     401          [1:
     402          |2, 3:
     403            assumption
     404          ]
     405        ]
    378406      |2:
    379407        cases daemon (* XXX: complete me *)
Note: See TracChangeset for help on using the changeset viewer.