Changeset 1514 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Nov 17, 2011, 5:41:08 PM (8 years ago)
Author:
mulligan
Message:

changes from today. matita keeps dieing

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1511 r1514  
    257257qed.
    258258
    259 lemma plus_minus_rearrangement:
     259lemma plus_minus_rearrangement_1:
    260260  ∀m, n, o: nat.
    261261  ∀proof_n_m: n < m.
     
    300300qed.
    301301
     302axiom plus_minus_rearrangement_2:
     303  ∀m, n, o: nat.
     304    (m - n) + (n - o) = m - o.
     305
    302306example set_program_counter_ignores_clock:
    303307  ∀s: Status.
     
    461465      normalize nodelta; cases addressing_mode
    462466      normalize nodelta;
    463      
     467      [1,2,3,4,8,9,15,16,17,18,19:
     468        #assm whd in ⊢ (% → ?)
     469        #absurd cases(absurd)
     470      |5,6,7,10,11,12,14:
     471        whd in ⊢ (% → ?)
     472        #absurd cases(absurd)
     473      |13:
     474        #irrelevant
     475        normalize nodelta;
     476        >set_program_counter_ignores_clock
     477        >set_program_counter_ignores_clock
     478        >clock_set_clock //
     479      ]
     480  |8: cases daemon (* XXX: my god *)
     481  |7: #acc_a cases acc_a #addressing_mode
     482      normalize nodelta; cases addressing_mode
     483      normalize nodelta;
     484      [1,2,3,4,8,9,15,16,17,18,19:
     485        #assm whd in ⊢ (% → ?)
     486        #absurd cases(absurd)
     487      |6,7,10,11,12,13,14:
     488        whd in ⊢ (% → ?)
     489        #absurd cases(absurd)
     490      |5:
     491        #irrelevant #acc_dptr_acc_pc
     492        normalize nodelta;
     493        cases daemon (* XXX: my god *)
     494      ]
     495  ]
     496qed.
    464497
    465498lemma current_instruction_cost_is_ok:
     
    476509    \snd (fetch (code_memory … s) (program_counter … s)));
    477510  normalize nodelta;
     511  whd in match (
     512    execute_1_0 s (fetch (code_memory (BitVectorTrie Byte 16) s)
     513     (program_counter (BitVectorTrie Byte 16) s)));
     514  normalize nodelta;
     515  cases (fetch (code_memory (BitVectorTrie Byte 16) s)
     516           (program_counter (BitVectorTrie Byte 16) s));
     517  #instr_pc #ticks normalize nodelta;
     518  cases (\fst instr_pc)
     519  [1:
     520    #addr11 normalize nodelta;
     521    cases addr11 #addressing_mode
     522    cases addressing_mode
     523    [1,2,3,4,8,9,15,16,17,19:
     524      #assm whd in ⊢ (% → ?)
     525      #absurd cases(absurd)
     526    |5,6,7,10,11,12,13,14:
     527      whd in ⊢ (% → ?)
     528      #absurd cases(absurd)
     529    |18:
     530      #word11 #irrelevant normalize nodelta;
     531      >set_program_counter_ignores_clock
     532      >write_at_stack_pointer_ignores_clock
     533      >set_8051_sfr_ignores_clock
     534      >write_at_stack_pointer_ignores_clock
     535      >set_8051_sfr_ignores_clock
     536      >clock_set_clock
     537      >set_program_counter_ignores_clock
     538      >commutative_plus
     539      <plus_minus
     540      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
     541      %
     542    ]
     543  |2:
     544    #addr16 cases addr16 #addressing_mode
     545    normalize nodelta; cases addressing_mode
     546    normalize nodelta;
     547    [1,2,3,4,8,9,15,16,17,18:
     548      #assm whd in ⊢ (% → ?)
     549      #absurd cases(absurd)
     550    |5,6,7,10,11,12,13,14:
     551      whd in ⊢ (% → ?)
     552      #absurd cases(absurd)
     553    |19:
     554      #addr16 #irrelevant
     555      normalize nodelta;
     556      >set_program_counter_ignores_clock
     557      >write_at_stack_pointer_ignores_clock
     558      >set_8051_sfr_ignores_clock
     559      >write_at_stack_pointer_ignores_clock
     560      >set_8051_sfr_ignores_clock
     561      >clock_set_clock
     562      >set_program_counter_ignores_clock
     563      >commutative_plus
     564      <plus_minus
     565      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
     566      %
     567    ]
     568  |3:
     569    #addr11 cases addr11 #addressing_mode
     570    normalize nodelta; cases addressing_mode
     571    normalize nodelta;
     572    [1,2,3,4,8,9,15,16,17,19:
     573      #assm whd in ⊢ (% → ?)
     574      #absurd cases(absurd)
     575    |5,6,7,10,11,12,13,14:
     576      whd in ⊢ (% → ?)
     577      #absurd cases(absurd)
     578    |18:
     579      #word11 #irrelevant
     580      normalize nodelta;
     581      >set_program_counter_ignores_clock
     582      >clock_set_clock
     583      >set_program_counter_ignores_clock
     584      >commutative_plus
     585      <plus_minus
     586      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
     587      %
     588    ]
     589  |4:
     590    #addr16 cases addr16 #addressing_mode
     591    normalize nodelta; cases addressing_mode
     592    normalize nodelta;
     593    [1,2,3,4,8,9,15,16,17,18:
     594      #assm whd in ⊢ (% → ?)
     595      #absurd cases(absurd)
     596    |5,6,7,10,11,12,13,14:
     597      whd in ⊢ (% → ?)
     598      #absurd cases(absurd)
     599    |19:
     600      #word #irrelevant
     601      normalize nodelta;
     602      >set_program_counter_ignores_clock
     603      >clock_set_clock
     604      >set_program_counter_ignores_clock
     605      >commutative_plus
     606      <plus_minus
     607      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
     608      %
     609    ]
     610  |5:
     611    #relative cases relative #addressing_mode
     612    normalize nodelta; cases addressing_mode
     613    normalize nodelta;
     614    [1,2,3,4,8,9,15,16,18,19:
     615      #assm whd in ⊢ (% → ?)
     616      #absurd cases(absurd)
     617    |5,6,7,10,11,12,13,14:
     618      whd in ⊢ (% → ?)
     619      #absurd cases(absurd)
     620    |17:
     621      #byte #irrelevant
     622      normalize nodelta;
     623      >set_program_counter_ignores_clock
     624      >set_program_counter_ignores_clock
     625      >clock_set_clock
     626      >commutative_plus
     627      <plus_minus
     628      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
     629      %
     630    ]
     631  |6:
     632    #indirect_dptr cases indirect_dptr #addressing_mode
     633    normalize nodelta; cases addressing_mode
     634    normalize nodelta;
     635    [1,2,3,4,8,9,15,16,17,18,19:
     636      #assm whd in ⊢ (% → ?)
     637      #absurd cases(absurd)
     638    |5,6,7,10,11,12,14:
     639      whd in ⊢ (% → ?)
     640      #absurd cases(absurd)
     641    |13:
     642      #irrelevant
     643      normalize nodelta;
     644      >set_program_counter_ignores_clock
     645      >set_program_counter_ignores_clock
     646      >clock_set_clock
     647      >commutative_plus
     648      <plus_minus
     649      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
     650      %
     651    ]
     652  |7:
     653    #acc_a cases acc_a #addressing_mode
     654    normalize nodelta; cases addressing_mode
     655    normalize nodelta;
     656    [1,2,3,4,8,9,15,16,17,18,19:
     657      #assm whd in ⊢ (% → ?)
     658      #absurd cases(absurd)
     659    |6,7,10,11,12,13,14:
     660      whd in ⊢ (% → ?)
     661      #absurd cases(absurd)
     662    |5:
     663      #irrelevant #acc_dptr_acc_pc
     664      normalize nodelta;
     665      cases daemon (* XXX: todo *)
     666    ]
     667  |8: cases daemon (* XXX: todo *)
     668  ]
     669qed.
    478670
    479671let rec compute_max_trace_label_label_cost_is_ok
     
    540732          let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
    541733            sum = pc_after)
    542         normalize nodelta;
     734        normalize nodelta; #relation_pre_after_fun_call
     735        >plus_minus_rearrangement_2 in match (
     736          (clock (BitVectorTrie Byte 16) after_fun_call
     737            -clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)
     738          +(clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)
     739            -clock (BitVectorTrie Byte 16) pre_fun_call)));
    543740        >(plus_minus_rearrangement
    544741          (clock (BitVectorTrie Byte 16) after_fun_call)
Note: See TracChangeset for help on using the changeset viewer.