Changeset 1577 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Nov 30, 2011, 5:32:52 PM (9 years ago)
Author:
mulligan
Message:

A lot more cases added to the proof at the bottom of execute_1_preinstruction, thought these make use of tacticals, with one in particular taking 1000+ seconds to complete. Changed all the Russell specifications in Interpret.ma to use the new, simplified specification.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1576 r1577  
    252252  ∀s: Status.
    253253    clock … (execute_1 s) = current_instruction_cost s + clock … s.
    254 
    255 axiom plus_minus_minus:
    256   ∀m, n, o: nat.
    257     m - (n + o) = (m - n) - o.
    258254
    259255axiom plus_le_le:
     
    353349          (current_instruction_cost status_pre_fun_call
    354350            + clock (BitVectorTrie Byte 16) status_pre_fun_call));
    355         >plus_minus_minus
     351        <minus_plus
    356352        <(plus_minus_m_m (clock (BitVectorTrie Byte 16) status_after_fun_call
    357353  -clock (BitVectorTrie Byte 16) status_pre_fun_call) (current_instruction_cost status_pre_fun_call))
     
    406402        >clock_execute_1
    407403        >commutative_plus in match ((current_instruction_cost status_pre+clock (BitVectorTrie Byte 16) status_pre));
    408         >plus_minus_minus
     404        <minus_plus
    409405        <plus_minus_m_m
    410406        [1: %
Note: See TracChangeset for help on using the changeset viewer.