Changeset 1622 for src/ASM


Ignore:
Timestamp:
Dec 16, 2011, 10:09:12 AM (8 years ago)
Author:
mulligan
Message:

to avoid conflicts, bug in typechecker?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1621 r1622  
    100100        program_counter = fetch_program_counter_n (S n) code_memory (zero 16) ∧
    101101          nat_of_bitvector 16 program_counter ≤ program_size ∧
    102             nat_of_bitvector 16 tail_program_counter nat_of_bitvector 16 program_counter.
     102            nat_of_bitvector 16 tail_program_counter < nat_of_bitvector 16 program_counter.
    103103
    104104definition good_program: BitVectorTrie Byte 16 → Word → nat → Prop ≝
     
    176176qed.
    177177
    178 axiom dubious:
    179   ∀m, n, o, p: nat.
    180     1 ≤ p → n ≤ m → m - n ≤ S o → m - (n + p) ≤ o.
    181 
    182 lemma subaddressing_mod_elim:
    183  ∀T:Type[2].
    184  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19,addr,p.
    185  ∀Q: addressing_mode → T → Prop.
    186  (∀w. Q (ADDR11 w) (P1 w)) →
    187   Q addr (match addr
    188      in addressing_mode
    189      return λx:addressing_mode.(is_in 1 [[addr11]] x→T)
    190      with 
    191     [ADDR11 (x:Word11) ⇒ λH:True. P1 x
    192     |ADDR16 _ ⇒ λH:False. P2 H
    193     |DIRECT _ ⇒ λH:False. P3 H
    194     |INDIRECT _ ⇒ λH:False. P4 H
    195     |EXT_INDIRECT _ ⇒ λH:False. P5 H
    196     |ACC_A ⇒ λH:False. P6 H
    197     |REGISTER _ ⇒ λH:False. P7 H
    198     |ACC_B ⇒ λH:False. P8 H
    199     |DPTR ⇒ λH:False. P9 H
    200     |DATA _ ⇒ λH:False. P10 H
    201     |DATA16 _ ⇒ λH:False. P11 H
    202     |ACC_DPTR ⇒ λH:False. P12 H
    203     |ACC_PC ⇒ λH:False. P13 H
    204     |EXT_INDIRECT_DPTR ⇒ λH:False. P14 H
    205     |INDIRECT_DPTR ⇒ λH:False. P15 H
    206     |CARRY ⇒ λH:False. P16 H
    207     |BIT_ADDR _ ⇒ λH:False. P17 H
    208     |N_BIT_ADDR _ ⇒ λH:False. P18 H   
    209     |RELATIVE _ ⇒ λH:False. P19 H
    210     ] p).
    211  #T #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
    212  #P14 #P15 #P16 #P17 #P18 #P19
    213  * try #x1 try #x2 try #x3 try #x4
    214  try (@⊥ assumption) normalize @x4
     178let rec member_addressing_mode_tag
     179  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
     180    on v: Prop ≝
     181  match v with
     182  [ VEmpty ⇒ False
     183  | VCons n' hd tl ⇒
     184    match eq_a hd a with
     185    [ true  ⇒ True
     186    | false ⇒ member_addressing_mode_tag n' tl a
     187    ]
     188  ].
     189 
     190let rec subaddressing_mode_elim_type
     191  (T: Type[2]) (n: nat) (v: Vector addressing_mode_tag n)
     192    (Q: addressing_mode → T → Prop)
     193      on v:
     194    (∀n. ∀v. Word11      → member_addressing_mode_tag n v addr11            → T) →
     195    (∀n. ∀v. Word        → member_addressing_mode_tag n v addr16            → T) →
     196    (∀n. ∀v. Byte        → member_addressing_mode_tag n v direct            → T) →
     197    (∀n. ∀v. Bit         → member_addressing_mode_tag n v indirect          → T) →
     198    (∀n. ∀v. Bit         → member_addressing_mode_tag n v ext_indirect      → T) →
     199    (∀n. ∀v.               member_addressing_mode_tag n v acc_a             → T) →
     200    (∀n. ∀v. BitVector 3 → member_addressing_mode_tag n v registr           → T) →
     201    (∀n. ∀v.               member_addressing_mode_tag n v acc_b             → T) →
     202    (∀n. ∀v.               member_addressing_mode_tag n v dptr              → T) →
     203    (∀n. ∀v. Byte        → member_addressing_mode_tag n v data              → T) →
     204    (∀n. ∀v. Word        → member_addressing_mode_tag n v data16            → T) →
     205    (∀n. ∀v.               member_addressing_mode_tag n v acc_dptr          → T) →
     206    (∀n. ∀v.               member_addressing_mode_tag n v acc_pc            → T) →
     207    (∀n. ∀v.               member_addressing_mode_tag n v ext_indirect_dptr → T) →
     208    (∀n. ∀v.               member_addressing_mode_tag n v indirect_dptr     → T) →
     209    (∀n. ∀v.               member_addressing_mode_tag n v carry             → T) →
     210    (∀n. ∀v. Byte        → member_addressing_mode_tag n v bit_addr          → T) →
     211    (∀n. ∀v. Byte        → member_addressing_mode_tag n v n_bit_addr        → T) →
     212    (∀n. ∀v. Byte        → member_addressing_mode_tag n v relative          → T) → Prop ≝
     213  match v return λm: nat. λv': Vector addressing_mode_tag m. v ≃ v' → ? with
     214  [ VEmpty         ⇒ λv_refl.
     215    λp_addr11. λp_addr16. λp_direct. λp_indirect. λp_ext_indirect. λp_acc_a.
     216    λp_register. λp_acc_b. λp_dptr. λp_data. λp_data16. λp_acc_dptr. λp_acc_pc.
     217    λp_ext_indirect_dptr. λp_indirect_dptr. λp_carry. λp_bit_addr.
     218    λp_n_bit_addr. λp_relative. False
     219      (* ∀addr:v. Q addr (match addr with *)
     220  | VCons n' hd tl ⇒ λv_refl.
     221    λp_addr11. λp_addr16: ∀n. ∀v. Word   → member_addressing_mode_tag n v addr16  → T.
     222    λp_direct. λp_indirect. λp_ext_indirect. λp_acc_a. λp_register. λp_acc_b.
     223    λp_dptr. λp_data. λp_data16. λp_acc_dptr. λp_acc_pc. λp_ext_indirect_dptr.
     224    λp_indirect_dptr. λp_carry. λp_bit_addr. λp_n_bit_addr. λp_relative.
     225    match hd return λa: addressing_mode_tag. a = hd → Prop with
     226    [ addr11 ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 n v w ?)) →
     227        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     228          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     229            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     230              p_relative)
     231    | addr16 ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 n v w ?)) →
     232        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     233          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     234            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     235              p_relative)
     236    | direct ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct n v w ?)) →
     237        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     238          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     239            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     240              p_relative)
     241    | indirect ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect n v w ?)) →
     242        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     243          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     244            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     245              p_relative)
     246    | ext_indirect ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect n v w ?)) →
     247        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     248          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     249            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     250              p_relative)
     251    | acc_a ⇒ λhd_refl. (Q ACC_A (p_acc_a n v ?)) →
     252        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     253          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     254            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     255              p_relative)
     256    | registr ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register n v w ?)) →
     257        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     258          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     259            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     260              p_relative)
     261    | acc_b ⇒ λhd_refl. (Q ACC_A (p_acc_b n v ?)) →
     262        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     263          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     264            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     265              p_relative)
     266    | dptr ⇒ λhd_refl. (Q DPTR (p_dptr n v ?)) →
     267        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     268          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     269            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     270              p_relative)
     271    | data ⇒ λhd_refl. (∀w. Q (DATA w) (p_data n v w ?)) →
     272        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     273          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     274            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     275              p_relative)
     276    | data16 ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 n v w ?)) →
     277        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     278          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     279            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     280              p_relative)
     281    | acc_dptr ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr n v ?)) →
     282        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     283          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     284            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     285              p_relative)
     286    | acc_pc ⇒ λhd_refl. (Q ACC_PC (p_acc_pc n v ?)) →
     287        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     288          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     289            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     290              p_relative)
     291    | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr n v ?)) →
     292        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     293          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     294            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     295              p_relative)
     296    | indirect_dptr ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr n v ?)) →
     297        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     298          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     299            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     300              p_relative)
     301    | carry ⇒ λhd_refl. (Q CARRY (p_carry n v ?)) →
     302        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     303          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     304            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     305              p_relative)
     306    | bit_addr ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr n v w ?)) →
     307        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     308          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     309            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     310              p_relative)
     311    | n_bit_addr ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr n v w ?)) →
     312        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     313          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     314            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     315              p_relative)
     316    | relative ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative n v w ?)) →
     317        (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect
     318          p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     319            p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr
     320              p_relative)
     321    ] (refl … hd)
     322  ] (refl_jmeq … v).
     323
     324lemma subaddressing_mode_elim:
     325  ∀T:Type[2].
     326  ∀P1: Word11 → T.
     327  ∀P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19: False → T.
     328  ∀addr: addressing_mode.
     329  ∀p: is_in 1 [[ addr11 ]] addr.
     330  ∀Q: addressing_mode → T → Prop.
     331    (∀w. Q (ADDR11 w) (P1 w)) →
     332      Q addr (
     333        match addr return λx:addressing_mode. (is_in 1 [[addr11]] x → T) with 
     334        [ ADDR11 (x:Word11) ⇒ λH:True. P1 x
     335        | ADDR16 _ ⇒ λH:False. P2 H
     336        | DIRECT _ ⇒ λH:False. P3 H
     337        | INDIRECT _ ⇒ λH:False. P4 H
     338        | EXT_INDIRECT _ ⇒ λH:False. P5 H
     339        | ACC_A ⇒ λH:False. P6 H
     340        | REGISTER _ ⇒ λH:False. P7 H
     341        | ACC_B ⇒ λH:False. P8 H
     342        | DPTR ⇒ λH:False. P9 H
     343        | DATA _ ⇒ λH:False. P10 H
     344        | DATA16 _ ⇒ λH:False. P11 H
     345        | ACC_DPTR ⇒ λH:False. P12 H
     346        | ACC_PC ⇒ λH:False. P13 H
     347        | EXT_INDIRECT_DPTR ⇒ λH:False. P14 H
     348        | INDIRECT_DPTR ⇒ λH:False. P15 H
     349        | CARRY ⇒ λH:False. P16 H
     350        | BIT_ADDR _ ⇒ λH:False. P17 H
     351        | N_BIT_ADDR _ ⇒ λH:False. P18 H   
     352        | RELATIVE _ ⇒ λH:False. P19 H
     353        ] p).
     354  #T #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
     355  #P14 #P15 #P16 #P17 #P18 #P19
     356  * try #x1 try #x2 try #x3 try #x4
     357  try (@⊥ assumption) normalize @x4
    215358qed.
    216359
     360include alias "arithmetics/nat.ma".
     361
     362lemma lt_n_o_to_plus_m_n_lt_plus_m_o:
     363  ∀m, n, o: nat.
     364    n < o → m + n < m + o.
     365  #m #n #o #assm /2 by monotonic_le_plus_r/
     366qed.
     367
     368axiom fetch_program_counter_n_technical:
     369  ∀code_memory: BitVectorTrie Byte 16.
     370  ∀program_counter, program_counter': Word.
     371  ∀instruction: instruction.
     372  ∀ticks, n: nat.
     373  program_counter' = \snd (\fst (fetch code_memory program_counter)) →
     374    program_counter' = fetch_program_counter_n (S n) code_memory (zero …) →
     375      program_counter = fetch_program_counter_n n code_memory (zero …).
     376   
    217377let rec block_cost
    218378  (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
    219379    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
    220380      (good_program_witness: good_program code_memory program_counter total_program_size)
    221         on program_size: total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat ≝
    222   match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat with
     381        on program_size: total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat ≝
     382  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat with
    223383  [ O ⇒ λbase_case. 0
    224384  | S program_size' ⇒ λrecursive_case.
     
    229389        [ RealInstruction instruction ⇒ λreal_instruction.
    230390          match instruction return λx. x = instruction → ? with
    231           [ RET                    ⇒ λret. ticks
    232           | JC   relative          ⇒ λjc.  ticks
    233           | JNC  relative          ⇒ λjnc. ticks
    234           | JB   bit_addr relative ⇒ λjb.  ticks
    235           | JNB  bit_addr relative ⇒ λjnb. ticks
    236           | JBC  bit_addr relative ⇒ λjbc. ticks
    237           | JZ   relative          ⇒ λjz.  ticks
    238           | JNZ  relative          ⇒ λjnz. ticks
    239           | CJNE src_trgt relative ⇒ λcjne. ticks
    240           | DJNZ src_trgt relative ⇒ λdjnz. ticks
    241           | _                      ⇒ λalt.
     391          [ RET                    ⇒ λinstr. ticks
     392          | JC   relative          ⇒ λinstr. ticks
     393          | JNC  relative          ⇒ λinstr. ticks
     394          | JB   bit_addr relative ⇒ λinstr. ticks
     395          | JNB  bit_addr relative ⇒ λinstr. ticks
     396          | JBC  bit_addr relative ⇒ λinstr. ticks
     397          | JZ   relative          ⇒ λinstr. ticks
     398          | JNZ  relative          ⇒ λinstr. ticks
     399          | CJNE src_trgt relative ⇒ λinstr. ticks
     400          | DJNZ src_trgt relative ⇒ λinstr. ticks
     401          | _                      ⇒ λinstr.
    242402              ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
    243403          ] (refl … instruction)
    244         | ACALL addr     ⇒ λacall.
     404        | ACALL addr     ⇒ λinstr.
    245405            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
    246         | AJMP  addr     ⇒ λajmp. ticks
    247         | LCALL addr     ⇒ λlcall.
     406        | AJMP  addr     ⇒ λinstr. ticks
     407        | LCALL addr     ⇒ λinstr.
    248408            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
    249         | LJMP  addr     ⇒ λljmp. ticks
    250         | SJMP  addr     ⇒ λsjmp. ticks
    251         | JMP   addr     ⇒ λjmp. (* XXX: actually a call due to use with fptrs *)
     409        | LJMP  addr     ⇒ λinstr. ticks
     410        | SJMP  addr     ⇒ λinstr. ticks
     411        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
    252412            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
    253         | MOVC  src trgt ⇒ λmovc.
     413        | MOVC  src trgt ⇒ λinstr.
    254414            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
    255415        ] (refl … instruction)
     
    257417      ]
    258418  ].
    259   [1: -block_cost -eta62747 -program_size
     419  [1:
    260420    generalize in match good_program_witness;
    261421    whd in match good_program; normalize nodelta
    262422    cases FETCH normalize nodelta
    263     cases acall normalize nodelta
    264     @(subaddressing_mod_elim Prop ??????????????????? addr
    265        (subaddressing_modein ? [[addr11]] addr)
    266        (λ_.λP. P → total_program_size-nat_of_bitvector 16 program_counter'≤program_size'))
    267        
    268     cases addr #subaddressing_mode cases subaddressing_mode
    269     try (#assm #absurd normalize in absurd; cases absurd)
    270     try (#absurd normalize in absurd; cases absurd)
    271     normalize nodelta
     423    cases instr normalize nodelta
     424    @subaddressing_mode_elim #new_addr
    272425    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
    273     cases (split … 3 8 assm) #thr #eig normalize nodelta
     426    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    274427    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
    275428    #assm cases assm #ignore
     
    277430    #program_counter_eq' #program_counter_lt_total_program_size
    278431    #fetch_n_leq_program_counter'
    279     lapply(dubious total_program_size (nat_of_bitvector … program_counter')
    280       program_size' ? ? ? ?)
    281     [2: assumption ]
     432    @(transitive_le
     433      total_program_size
     434      ((S program_size') + nat_of_bitvector … program_counter)
     435      (program_size' + nat_of_bitvector … program_counter') recursive_case)
     436    whd in ⊢ (?%?);
     437    change with (
     438      program_size' + (nat_of_bitvector … program_counter) <
     439        program_size' + (nat_of_bitvector … program_counter'))
     440    @lt_n_o_to_plus_m_n_lt_plus_m_o
     441    >(fetch_program_counter_n_technical code_memory program_counter
     442      program_counter' instruction ticks n)
     443    /2 by pair_destruct_2/
     444  |3,5,7,9,11:
     445    (* XXX etc. need the subaddressing_mode_elim generalizing *)
     446  |2:
     447    generalize in match good_program_witness;
     448    whd in match (good_program code_memory program_counter total_program_size);
     449    cases FETCH normalize nodelta
     450    cases instr normalize nodelta
     451    @subaddressing_mode_elim #new_addr
     452    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
     453    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
     454    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
     455    #assm cases assm #ignore #good_program_counter
     456    whd in match (good_program code_memory program_counter' total_program_size);
     457    cases(fetch code_memory program_counter') #instruction_program_counter'' #ticks''
     458    cases(instruction_program_counter'') #instruction'' #program_counter'' normalize nodelta
     459   
    282460  [2:
    283461    (* generalize in match good_program_witness; *)
Note: See TracChangeset for help on using the changeset viewer.