Changeset 1642 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Jan 12, 2012, 6:16:50 PM (8 years ago)
Author:
mulligan
Message:

finished big proof in all but two cases

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1639 r1642  
    9090    (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
    9191  //
    92 qed.
    93    
    94 definition good_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝
     92qed.
     93
     94let rec fetch_program_counter_n
     95  (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
     96    on n: option Word ≝
     97  match n with
     98  [ O ⇒ Some … program_counter
     99  | S n ⇒
     100    match fetch_program_counter_n n code_memory program_counter with
     101    [ None ⇒ None …
     102    | Some tail_pc ⇒
     103      let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in
     104        if ltb (nat_of_bitvector … tail_pc) (nat_of_bitvector … program_counter) then
     105          Some … program_counter
     106        else
     107          None Word (* XXX: overflow! *)
     108    ]
     109  ].
     110   
     111definition reachable_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝
    95112  λcode_memory: BitVectorTrie Byte 16.
    96113  λprogram_size: nat.
    97114  λprogram_counter: Word.
    98     ∃n: nat.
    99       let tail_program_counter ≝ fetch_program_counter_n n code_memory (zero 16) in
    100         program_counter = fetch_program_counter_n (S n) code_memory (zero 16) ∧
    101           nat_of_bitvector 16 program_counter ≤ program_size ∧
    102             nat_of_bitvector 16 tail_program_counter < nat_of_bitvector 16 program_counter.
    103 
    104 axiom half_add_zero:
     115    (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧
     116        nat_of_bitvector 16 program_counter < program_size.
     117
     118axiom full_add_zero:
     119  ∀n: nat.
     120  ∀b: BitVector n.
     121    \snd (full_add n (zero …) b false) = b.
     122
     123lemma half_add_zero:
    105124  ∀n: nat.
    106125  ∀b: BitVector n.
    107126    \snd (half_add n (zero …) b) = b.
    108 
    109 lemma fetch_program_counter_n_half_add:
    110   ∀n: nat.
    111   ∀code_memory: BitVectorTrie Byte 16.
    112     fetch_program_counter_n (S n) code_memory (zero …) =
    113       let program_counter ≝ fetch_program_counter_n n code_memory (zero …) in
    114       let 〈instr, new_program_counter, cost〉 ≝ fetch code_memory program_counter in
    115         \snd (half_add … program_counter new_program_counter).
    116   #n #code_memory elim n
     127  #n #b
     128  cases b
    117129  [1:
    118     whd in match (fetch_program_counter_n 1 code_memory (zero …));
    119     normalize in match (fetch_program_counter_n 0 code_memory (zero …));
    120     change with (
    121       let 〈instr, program_counter, ticks〉 ≝ fetch code_memory (zero …) in
    122         program_counter
    123     ) in ⊢ (??%?);
    124     cases (fetch code_memory (zero …)) #instr #program_counter normalize nodelta
    125     generalize in match instr; #instr
    126     cases instr #instr #program_counter normalize nodelta
    127     >half_add_zero %
     130    %
    128131  |2:
    129     #n' #ind_hyp
    130     whd in match (fetch_program_counter_n (S (S n')) code_memory (zero …));
    131     >ind_hyp (* XXX: things start going wrong here!
    132     generalize in match (let (program_counter:Word) ≝
    133                   fetch_program_counter_n n' code_memory (zero 16) in 
    134            let 〈eta40050,cost〉 ≝fetch code_memory program_counter in 
    135            let 〈instr,new_program_counter〉 ≝eta40050 in 
    136            \snd  (half_add 16 program_counter new_program_counter));
    137     #B normalize nodelta
    138     cases (fetch code_memory B) #instr_program_counter #cost normalize nodelta
    139     cases instr_program_counter #instr #program_counter normalize nodelta *)
    140     cases daemon
     132    #n' #hd #tl
     133    cases hd
     134    whd in match half_add; normalize nodelta
     135    >full_add_zero %
    141136  ]
    142137qed.
    143138   
    144 definition good_program: BitVectorTrie Byte 16 → Word → nat → Prop ≝
     139definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝
    145140  λcode_memory: BitVectorTrie Byte 16.
    146   λprogram_counter: Word.
    147141  λtotal_program_size: nat.
    148   let 〈instruction, program_counter, ticks〉 ≝ fetch code_memory program_counter in
     142  ∀program_counter: Word.
     143  ∀good_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
     144  let 〈instruction, program_counter', ticks〉 ≝ fetch code_memory program_counter in
    149145    match instruction with
    150146    [ RealInstruction instr ⇒
     
    161157      | DJNZ src_trgt relative ⇒ True
    162158      | _                      ⇒
    163           good_program_counter code_memory total_program_size program_counter
     159        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
     160          nat_of_bitvector … program_counter' < total_program_size
    164161      ]
    165162    | LCALL addr         ⇒
    166163      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
    167164      [ ADDR16 addr ⇒ λaddr16: True.
    168           good_program_counter code_memory total_program_size addr ∧
    169             good_program_counter code_memory total_program_size program_counter
     165          reachable_program_counter code_memory total_program_size addr ∧
     166            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
     167              nat_of_bitvector … program_counter' < total_program_size
    170168      | _ ⇒ λother: False. ⊥
    171169      ] (subaddressing_modein … addr)
     
    173171      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
    174172      [ ADDR11 addr ⇒ λaddr11: True.
    175         let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter in
     173        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
    176174        let 〈thr, eig〉 ≝ split … 3 8 addr in
    177175        let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
    178176        let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in
    179           good_program_counter code_memory total_program_size new_program_counter ∧
    180             good_program_counter code_memory total_program_size program_counter
     177          reachable_program_counter code_memory total_program_size new_program_counter ∧
     178            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
     179              nat_of_bitvector … program_counter' < total_program_size
    181180      | _ ⇒ λother: False. ⊥
    182181      ] (subaddressing_modein … addr)
     
    184183      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
    185184      [ ADDR11 addr ⇒ λaddr11: True.
    186         let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter in
     185        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
    187186        let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
    188187        let bit ≝ get_index' … O ? nl in
     
    190189        let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    191190        let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in
    192           (good_program_counter code_memory total_program_size new_program_counter) ∧
    193             (good_program_counter code_memory total_program_size program_counter)
     191          reachable_program_counter code_memory total_program_size new_program_counter
    194192      | _ ⇒ λother: False. ⊥
    195193      ] (subaddressing_modein … addr)
     
    197195      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
    198196      [ ADDR16 addr ⇒ λaddr16: True.
    199           good_program_counter code_memory total_program_size addr ∧
    200             good_program_counter code_memory total_program_size program_counter
     197          reachable_program_counter code_memory total_program_size addr
    201198      | _ ⇒ λother: False. ⊥
    202199      ] (subaddressing_modein … addr)
     
    204201      match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with
    205202      [ RELATIVE addr ⇒ λrelative: True.
    206         let 〈carry, new_program_counter〉 ≝ half_add … program_counter (sign_extension addr) in
    207           good_program_counter code_memory total_program_size new_program_counter ∧
    208             good_program_counter code_memory total_program_size program_counter
     203        let 〈carry, new_program_counter〉 ≝ half_add … program_counter' (sign_extension addr) in
     204          reachable_program_counter code_memory total_program_size new_program_counter
    209205      | _ ⇒ λother: False. ⊥
    210206      ] (subaddressing_modein … addr)
    211     | JMP   addr     ⇒ True (* XXX: should recurse here, but dptr in JMP ... *)
     207    | JMP   addr     ⇒ True (* XXX: JMP is used for fptrs and unconstrained *)
    212208    | MOVC  src trgt ⇒
    213         good_program_counter code_memory total_program_size program_counter
     209        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
     210          nat_of_bitvector … program_counter' < total_program_size
    214211    ].
    215212  cases other
     
    227224qed.
    228225
    229 axiom is_in_subvector_is_in_supervector:
     226lemma is_in_subvector_is_in_supervector:
    230227  ∀m, n: nat.
    231228  ∀subvector: Vector addressing_mode_tag m.
     
    234231    subvector_with … eq_a subvector supervector →
    235232      is_in m subvector element → is_in n supervector element.
     233  #m #n #subvector #supervector #element
     234  elim subvector
     235  [1:
     236    #subvector_proof #is_in_proof
     237    normalize in is_in_proof; cases is_in_proof
     238  |2:
     239    #n' #addressing_mode_tag #tail #ind_hyp #subvector_proof #is_in_proof
     240    @ind_hyp
     241    cases daemon (* XXX *)
     242  ]
     243qed.
    236244
    237245let rec member_addressing_mode_tag
     
    400408qed.
    401409
    402 axiom fetch_program_counter_n_technical:
    403   ∀n: nat.
     410(*
     411axiom blah:
     412  ∀instruction: instruction.
     413  ∀program_counter': Word.
     414  ∀ticks, n: nat.
    404415  ∀code_memory: BitVectorTrie Byte 16.
    405   ∀program_counter, program_counter': Word.
    406   program_counter' = fetch_program_counter_n (S n) code_memory (zero …) →
    407     program_counter' = \snd (\fst (fetch code_memory program_counter)) →
    408       program_counter = fetch_program_counter_n n code_memory (zero …).
    409    
     416    〈instruction,program_counter',ticks〉 = fetch code_memory (fetch_program_counter_n n code_memory (zero 16)) →
     417       program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
     418*)   
     419
    410420let rec block_cost
    411421  (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
    412422    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
    413       (good_program_witness: good_program code_memory program_counter total_program_size)
    414         on program_size: total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat ≝
     423      (reachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter)
     424        (good_program_witness: good_program code_memory total_program_size)
     425          on program_size: total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat ≝
    415426  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat with
    416   [ O ⇒ λbase_case. 0
     427  [ O ⇒ λbase_case.
    417428  | S program_size' ⇒ λrecursive_case.
    418429    let 〈instruction, program_counter', ticks〉 as FETCH ≝ fetch code_memory program_counter in
     
    433444          | DJNZ src_trgt relative ⇒ λinstr. ticks
    434445          | _                      ⇒ λinstr.
    435               ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
     446              ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
    436447          ] (refl … real_instruction)
    437448        | ACALL addr     ⇒ λinstr.
    438             ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
     449            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
    439450        | AJMP  addr     ⇒ λinstr. ticks
    440451        | LCALL addr     ⇒ λinstr.
    441             ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
     452            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
    442453        | LJMP  addr     ⇒ λinstr. ticks
    443454        | SJMP  addr     ⇒ λinstr. ticks
    444455        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
    445             ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
     456            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
    446457        | MOVC  src trgt ⇒ λinstr.
    447             ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
     458            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
    448459        ] (refl … instruction)
    449460      | Some _ ⇒ ticks
    450461      ]
    451462  ].
     463  [1:
     464    cases reachable_program_counter_witness #_ #hyp
     465    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
     466    @(le_to_lt_to_lt … base_case hyp)
     467  |2:
     468    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     469    lapply(good_program_witness program_counter reachable_program_counter_witness)
     470      <FETCH normalize nodelta <instr normalize nodelta
     471    @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
     472    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
     473    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
     474    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
     475    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
     476    @(transitive_le
     477      total_program_size
     478      ((S program_size') + nat_of_bitvector … program_counter)
     479      (program_size' + nat_of_bitvector … program_counter') recursive_case)
     480    normalize in match (S program_size' + nat_of_bitvector … program_counter);
     481    >plus_n_Sm
     482    @monotonic_le_plus_r
     483    change with (
     484      nat_of_bitvector … program_counter <
     485        nat_of_bitvector … program_counter')
     486    assumption
     487  |3:
     488    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     489    lapply(good_program_witness program_counter reachable_program_counter_witness)
     490      <FETCH normalize nodelta <instr normalize nodelta
     491    @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
     492    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
     493    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
     494    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
     495    #_ #_ #program_counter_lt' #program_counter_lt_tps'
     496    %
     497    [1:
     498      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     499      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     500      >(le_to_leb_true … program_counter_lt') %
     501    |2:
     502      assumption
     503    ]
     504  |4:
     505    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     506    lapply(good_program_witness program_counter reachable_program_counter_witness)
     507      <FETCH normalize nodelta <instr normalize nodelta
     508    @(subaddressing_mode_elim' … [[addr16]] … [[addr16]]) [1: // ] #new_addr
     509    * * * * #n'
     510    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
     511    @(transitive_le
     512      total_program_size
     513      ((S program_size') + nat_of_bitvector … program_counter)
     514      (program_size' + nat_of_bitvector … program_counter') recursive_case)
     515    normalize in match (S program_size' + nat_of_bitvector … program_counter);
     516    >plus_n_Sm
     517    @monotonic_le_plus_r
     518    change with (
     519      nat_of_bitvector … program_counter <
     520        nat_of_bitvector … program_counter')
     521    assumption
     522  |5:
     523    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     524    lapply(good_program_witness program_counter reachable_program_counter_witness)
     525      <FETCH normalize nodelta <instr normalize nodelta
     526    @(subaddressing_mode_elim' … [[addr16]] … [[addr16]]) [1: // ] #new_addr
     527    * * * * #n'
     528    #_ #_ #program_counter_lt' #program_counter_lt_tps'
     529    %
     530    [1:
     531      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     532      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     533      >(le_to_leb_true … program_counter_lt') %
     534    |2:
     535      assumption
     536    ]
     537  |6:
     538    cases daemon (* XXX *)
     539  |7:
     540    cases daemon (* XXX *)
     541  |8:
     542    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     543    lapply(good_program_witness program_counter reachable_program_counter_witness)
     544    <FETCH normalize nodelta <instr normalize nodelta
     545    try(<real_instruction_refl <instr normalize nodelta) *
     546    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
     547    @(transitive_le
     548      total_program_size
     549      ((S program_size') + nat_of_bitvector … program_counter)
     550      (program_size' + nat_of_bitvector … program_counter') recursive_case)
     551    normalize in match (S program_size' + nat_of_bitvector … program_counter);
     552    >plus_n_Sm
     553    @monotonic_le_plus_r
     554    change with (
     555      nat_of_bitvector … program_counter <
     556        nat_of_bitvector … program_counter')
     557    assumption
     558  |9:
     559    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     560    lapply(good_program_witness program_counter reachable_program_counter_witness)
     561      <FETCH normalize nodelta <instr normalize nodelta *
     562    #program_counter_lt' #program_counter_lt_tps' %
     563    [1:
     564      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     565      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     566      >(le_to_leb_true … program_counter_lt') %
     567    |2:
     568      assumption
     569    ]
     570  |11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,
     571    55,57,59,61,63:
     572    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     573    lapply(good_program_witness program_counter reachable_program_counter_witness)
     574      <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
     575    #program_counter_lt' #program_counter_lt_tps' %
     576    [1:
     577      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     578      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     579      >(le_to_leb_true … program_counter_lt') %
     580    |2:
     581      assumption
     582    ]
     583  |10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,
     584    54,56,58,60,62:
     585    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     586    lapply(good_program_witness program_counter reachable_program_counter_witness)
     587    <FETCH normalize nodelta
     588    <real_instruction_refl <instr normalize nodelta *
     589    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
     590    @(transitive_le
     591      total_program_size
     592      ((S program_size') + nat_of_bitvector … program_counter)
     593      (program_size' + nat_of_bitvector … program_counter') recursive_case)
     594    normalize in match (S program_size' + nat_of_bitvector … program_counter);
     595    >plus_n_Sm
     596    @monotonic_le_plus_r
     597    change with (
     598      nat_of_bitvector … program_counter <
     599        nat_of_bitvector … program_counter')
     600    assumption
     601  ]
     602qed.
     603   
     604   
     605   
     606   
     607   
     608   
     609   
    452610  [1: (* ACALL *)
    453611    generalize in match good_program_witness;
     
    456614    cases instr normalize nodelta
    457615    @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    458     cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
     616    cases (split … 8 8 program_counter) #pc_bu #pc_bl normalize nodelta
    459617    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    460618    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
    461619    #assm cases assm #ignore
    462620    whd in match good_program_counter; normalize nodelta * #n * *
    463     #program_counter_eq' #program_counter_lt_total_program_size
    464     #fetch_n_leq_program_counter'
     621    #program_counter_eq #program_counter_lt_total_program_size
     622    #fetch_n_leq_program_counter
    465623    @(transitive_le
    466624      total_program_size
    467625      ((S program_size') + nat_of_bitvector … program_counter)
    468626      (program_size' + nat_of_bitvector … program_counter') recursive_case)
    469     whd in ⊢ (?%?);
     627    normalize in match (S program_size' + nat_of_bitvector … program_counter);
     628    >plus_n_Sm
     629    @monotonic_le_plus_r
    470630    change with (
    471       program_size' + (nat_of_bitvector … program_counter) <
    472         program_size' + (nat_of_bitvector … program_counter'))
    473     @lt_n_o_to_plus_m_n_lt_plus_m_o
    474     >(fetch_program_counter_n_technical n code_memory program_counter program_counter')
    475     /2 by pair_destruct_2/
     631      nat_of_bitvector … program_counter <
     632        nat_of_bitvector … program_counter')
     633    >program_counter_eq in FETCH; #hyp
     634    >(blah … hyp)
     635    <program_counter_eq assumption
    476636  |2:
    477637    generalize in match good_program_witness;
    478     whd in match good_program in ⊢ (? → %); normalize nodelta
     638    whd in match good_program; normalize nodelta
    479639    cases FETCH normalize nodelta
    480640    cases instr normalize nodelta
    481641    @(subaddressing_mode_elim' … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    482     cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
     642    cases (split … 8 8 program_counter) #pc_bu #pc_bl normalize nodelta
    483643    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    484644    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
    485     * #ignore #good_program_counter_assm
    486     cases (fetch code_memory program_counter') #instruction_program_counter #cost normalize nodelta
    487     cases instruction_program_counter #instruction #program_counter normalize nodelta
    488     cases instruction
    489     [1:
    490       #addr11 normalize nodelta
    491       cases addr11 #addressing_mode
    492       cases addressing_mode
    493       try (#assm #proof normalize in proof; cases proof)
    494       try (#proof normalize in proof; cases proof)
    495       normalize nodelta
     645    #assm cases assm #ignore
     646    whd in match good_program_counter; normalize nodelta * #n * *
     647    #program_counter_eq #program_counter_lt_total_program_size
     648    #fetch_n_leq_program_counter
     649
     650    whd in match good_program; normalize nodelta
     651    @pair_elim #lft #rgt normalize nodelta #fetch_hyp
     652    @pair_elim #instruction #program
     653  |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,
     654   54,56,58,60,62:
    496655  |3: (* LCALL *)
    497656    generalize in match good_program_witness;
     
    500659    cases instr normalize nodelta
    501660    @(subaddressing_mode_elim' … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    502     #assm cases assm #ignore
     661    * #irrelevant
    503662    whd in match good_program_counter; normalize nodelta * #n * *
    504     #program_counter_eq' #program_counter_lt_total_program_size
    505     #fetch_n_leq_program_counter'
     663    #program_counter_eq #program_counter_lt_total_program_size
     664    #fetch_n_leq_program_counter
    506665    @(transitive_le
    507666      total_program_size
    508667      ((S program_size') + nat_of_bitvector … program_counter)
    509668      (program_size' + nat_of_bitvector … program_counter') recursive_case)
    510     whd in ⊢ (?%?);
     669    normalize in match (S program_size' + nat_of_bitvector … program_counter);
     670    >plus_n_Sm
     671    @monotonic_le_plus_r
    511672    change with (
    512       program_size' + (nat_of_bitvector … program_counter) <
    513         program_size' + (nat_of_bitvector … program_counter'))
    514     @lt_n_o_to_plus_m_n_lt_plus_m_o
    515     >(fetch_program_counter_n_technical n code_memory program_counter program_counter')
    516     /2 by pair_destruct_2/
    517   |5: (* JMP *)
     673      nat_of_bitvector … program_counter <
     674        nat_of_bitvector … program_counter')
     675    >program_counter_eq in FETCH; #hyp
     676    >(blah … hyp)
     677    <program_counter_eq assumption
     678  |5,7: (* JMP and MOVC *)
    518679    generalize in match good_program_witness;
    519680    whd in match good_program; normalize nodelta
    520681    cases FETCH normalize nodelta
    521682    cases instr normalize nodelta
    522     cases daemon (* XXX ??? *)
    523   |7: (* MOVC *)
    524     generalize in match good_program_witness;
    525     whd in match good_program; normalize nodelta
    526     cases FETCH normalize nodelta
    527     cases instr normalize nodelta
    528     cases daemon (* XXX ??? *)
    529683  |9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,
    530684   49,51,53,55,57,59,61,63: (* ADD and similar non-branching instructions *)
     
    532686    whd in match good_program; normalize nodelta
    533687    cases FETCH normalize nodelta
    534     cases real_instruction_refl
    535     cases instr normalize nodelta
    536     whd in match good_program_counter; normalize nodelta
    537     * #the_n * *
    538     #program_counter_fetch_program_counter_n' #program_counter_lt_total_program_size'
    539     #fetch_program_n_lt_program_counter'
     688    <real_instruction_refl <instr normalize nodelta
     689  ]
     690    whd in match good_program_counter; normalize nodelta * #n * *
     691    #program_counter_eq #program_counter_lt_total_program_size
     692    #fetch_n_leq_program_counter
    540693    @(transitive_le
    541694      total_program_size
     
    549702      nat_of_bitvector … program_counter <
    550703        nat_of_bitvector … program_counter')
    551     generalize in match (
    552       fetch_program_counter_n_technical the_n code_memory
    553         program_counter program_counter' program_counter_fetch_program_counter_n');
    554     #hyp >hyp
    555     >program_counter_fetch_program_counter_n'
    556   ]
    557 qed.
    558      
    559      
    560      
    561      
    562      
    563      
    564      
    565      
    566      
     704    >program_counter_eq in FETCH; #hyp
     705    >(blah … hyp)
     706    <program_counter_eq assumption
     707qed.
     708       
    567709(* XXX: use memoisation here in the future *)
    568710let rec block_cost
Note: See TracChangeset for help on using the changeset viewer.