Changeset 1597 for src/ASM


Ignore:
Timestamp:
Dec 12, 2011, 9:51:21 AM (8 years ago)
Author:
mulligan
Message:

fixed fetch for jaap

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1591 r1597  
    9090    (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
    9191  //
    92 qed.
     92qed. 
    9393 
    9494axiom minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o:
    9595  ∀m, n, o: nat.
    9696    m - n ≤ m - S o → S m - n ≤ m - o.
     97(* XXX: ^^^ false without some preconditions *)
     98
     99axiom m_leq_n_to_m_eq_n_or_m_lt_n:
     100  ∀n, m: nat.
     101    m ≤ n → m = n ∨ m < n.
    97102
    98103lemma strengthened_invariant:
     
    112117  >new_program_counter_from_fetch
    113118  lapply (sig2 ? ? (fetch code_memory program_counter)) #assm
     119  cases daemon
     120qed.
    114121   
    115        
    116122(* XXX: use memoisation here in the future *)
    117123let rec block_cost
     
    123129            let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in
    124130              Or (ASM_classify0 instr = cl_jump) (ASM_classify0 instr = cl_return))
    125                 on program_size: total_program_size - nat_of_bitvector … program_counter < program_size → nat ≝
    126   match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter < program_size → nat with
    127   [ O ⇒ λabsurd. ⊥
     131                on program_size: total_program_size - nat_of_bitvector … program_counter program_size → nat ≝
     132  match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter program_size → nat with
     133  [ O ⇒ λbase_case. 0 (* XXX: change from ⊥ before *)
    128134  | S program_size ⇒ λrecursive_case.
    129135    let ticks ≝ \snd (fetch … code_memory program_counter) in
     
    132138    match lookup_opt … newpc cost_labels return λx: option costlabel. nat with
    133139    [ None ⇒
    134         let classify ≝ ASM_classify0 instr in
    135         match classify return λx. ∀classify_refl: x = classify. nat with
    136         [ cl_jump ⇒ λclassify_refl. ticks
    137         | cl_call ⇒ λclassify_refl. ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
    138         | cl_return ⇒ λclassify_refl. ticks
    139         | cl_other ⇒ λclassify_refl. ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
    140         ] (refl … classify)
     140        match ASM_classify0 instr with
     141        [ cl_jump ⇒ ticks
     142        | cl_call ⇒ ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
     143        | cl_return ⇒ ticks
     144        | cl_other ⇒ ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
     145        ]
    141146    | Some _ ⇒ ticks
    142147    ]
    143148  ].
     149  [1,3:
     150    lapply(sig2 ? ? (fetch code_memory program_counter))
     151    change with (
     152      nat_of_bitvector … newpc
     153    ) in ⊢ (??% → ?);
     154 
     155 
     156 
    144157  [1:
    145158    cases(lt_to_not_zero … absurd)
     
    147160    cut(nat_of_bitvector … program_counter < nat_of_bitvector … newpc)
    148161    [1,3:
    149       @fetch_pc_lt_new_pc (* XXX: now @sig2 from fetch's russell type *)
    150       lapply(transitive_lt
    151         (nat_of_bitvector 16 pc)
    152         initial_program_size
    153         (size Byte 16 mem) ? ?)
    154       [1,2,4,5:
    155         assumption
    156       |3,6:
    157         #assm assumption
    158       ]
     162      normalize nodelta in match newpc;
     163      lapply(sig2 ? ? (fetch code_memory program_counter))
     164      [*: #assm assumption ]
    159165    |2,4:
    160       change with (
    161         S (nat_of_bitvector … 16 pc) ≤ nat_of_bitvector … newpc
    162       ) in ⊢ (% → ?);
    163       #first_le_assm
     166      #first_lt_assm
     167    ]
     168   
     169   
     170  |3,5:
     171    lapply(sig2
    164172      normalize in recursive_case;
    165173      change with (
    166         S (initial_program_size - nat_of_bitvector … newpc) ≤ program_size)
     174        S (total_program_size - nat_of_bitvector … newpc) ≤ program_size)
    167175      lapply (le_S_S_to_le … recursive_case)
    168176      change with (
  • src/ASM/Fetch.ma

    r1591 r1597  
    4242definition fetch0: BitVectorTrie Byte 16 → ∀program_counter: Word. Byte →
    4343  nat_of_bitvector … program_counter < code_memory_size - 24 (* 3 bytes *) →
    44   Σret: instruction × Word × nat. nat_of_bitvector … program_counter nat_of_bitvector … (\snd (\fst ret)) ≝
     44  Σret: instruction × Word × nat. nat_of_bitvector … program_counter < nat_of_bitvector … (\snd (\fst ret)) ≝
    4545  λpmem.
    4646  λpc.
     
    425425
    426426definition fetch: BitVectorTrie Byte 16 → ∀program_counter: Word.
    427     Σret: instruction × Word × nat. nat_of_bitvector … program_counter nat_of_bitvector … (\snd (\fst ret)) ≝
     427    Σret: instruction × Word × nat. nat_of_bitvector … program_counter < nat_of_bitvector … (\snd (\fst ret)) ≝
    428428  λpmem: BitVectorTrie Byte 16.
    429429  λpc: Word.
Note: See TracChangeset for help on using the changeset viewer.