Changeset 1909


Ignore:
Timestamp:
Apr 27, 2012, 10:59:03 AM (7 years ago)
Author:
mulligan
Message:

Ported new statements to remainder of Interpret.ma file.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1907 r1909  
    110110  cases other
    111111qed.
    112        
    113 lemma is_a_decidable:
    114   ∀hd.
    115   ∀element.
    116     is_a hd element = true ∨ is_a hd element = false.
    117   #hd #element //
    118 qed.
    119 
    120 lemma mem_decidable:
    121   ∀n: nat.
    122   ∀v: Vector addressing_mode_tag n.
    123   ∀element: addressing_mode_tag.
    124     mem … eq_a n v element = true ∨
    125       mem … eq_a … v element = false.
    126   #n #v #element //
    127 qed.
    128 
    129 lemma eq_a_elim:
    130   ∀tag.
    131   ∀hd.
    132   ∀P: bool → Prop.
    133     (tag = hd → P (true)) →
    134       (tag ≠ hd → P (false)) →
    135         P (eq_a tag hd).
    136   #tag #hd #P
    137   cases tag
    138   cases hd
    139   #true_hyp #false_hyp
    140   try @false_hyp
    141   try @true_hyp
    142   try %
    143   #absurd destruct(absurd)
    144 qed.
    145  
    146 lemma is_a_true_to_is_in:
    147   ∀n: nat.
    148   ∀x: addressing_mode.
    149   ∀tag: addressing_mode_tag.
    150   ∀supervector: Vector addressing_mode_tag n.
    151   mem addressing_mode_tag eq_a n supervector tag →
    152     is_a tag x = true →
    153       is_in … supervector x.
    154   #n #x #tag #supervector
    155   elim supervector
    156   [1:
    157     #absurd cases absurd
    158   |2:
    159     #n' #hd #tl #inductive_hypothesis
    160     whd in match (mem … eq_a (S n') (hd:::tl) tag);
    161     @eq_a_elim normalize nodelta
    162     [1:
    163       #tag_hd_eq #irrelevant
    164       whd in match (is_in (S n') (hd:::tl) x);
    165       <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
    166       @I
    167     |2:
    168       #tag_hd_neq
    169       whd in match (is_in (S n') (hd:::tl) x);
    170       change with (
    171         mem … eq_a n' tl tag)
    172           in match (fold_right … n' ? false tl);
    173       #mem_hyp #is_a_hyp
    174       cases(is_a hd x)
    175       [1:
    176         normalize nodelta //
    177       |2:
    178         normalize nodelta
    179         @inductive_hypothesis assumption
    180       ]
    181     ]
    182   ]
    183 qed.
    184 
    185 lemma is_in_subvector_is_in_supervector:
    186   ∀m, n: nat.
    187   ∀subvector: Vector addressing_mode_tag m.
    188   ∀supervector: Vector addressing_mode_tag n.
    189   ∀element: addressing_mode.
    190     subvector_with … eq_a subvector supervector →
    191       is_in m subvector element → is_in n supervector element.
    192   #m #n #subvector #supervector #element
    193   elim subvector
    194   [1:
    195     #subvector_with_proof #is_in_proof
    196     cases is_in_proof
    197   |2:
    198     #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
    199     whd in match (is_in … (hd':::tl') element);
    200     cases (is_a_decidable hd' element)
    201     [1:
    202       #is_a_true >is_a_true
    203       #irrelevant
    204       whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
    205       @(is_a_true_to_is_in … is_a_true)
    206       lapply(subvector_with_proof)
    207       cases(mem … eq_a n supervector hd') //
    208     |2:
    209       #is_a_false >is_a_false normalize nodelta
    210       #assm
    211       @inductive_hypothesis
    212       [1:
    213         generalize in match subvector_with_proof;
    214         whd in match (subvector_with … eq_a (hd':::tl') supervector);
    215         cases(mem_decidable n supervector hd')
    216         [1:
    217           #mem_true >mem_true normalize nodelta
    218           #assm assumption
    219         |2:
    220           #mem_false >mem_false #absurd
    221           cases absurd
    222         ]
    223       |2:
    224         assumption
    225       ]
    226     ]
    227   ]
    228 qed.
    229 
    230 let rec member_addressing_mode_tag
    231   (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
    232     on v: Prop ≝
    233   match v with
    234   [ VEmpty ⇒ False
    235   | VCons n' hd tl ⇒
    236       bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
    237   ].
    238  
    239 let rec subaddressing_mode_elim_type
    240   (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
    241     (Q: addressing_mode → T → Prop)
    242       (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
    243       (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
    244       (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
    245       (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
    246       (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
    247       (p_acc_a:                              is_in m fixed_v ACC_A             → T)
    248       (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
    249       (p_acc_b:                              is_in m fixed_v ACC_B             → T)
    250       (p_dptr:                               is_in m fixed_v DPTR              → T)
    251       (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
    252       (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
    253       (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
    254       (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
    255       (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
    256       (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
    257       (p_carry:                              is_in m fixed_v CARRY             → T)
    258       (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
    259       (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
    260       (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
    261         (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
    262       on v: Prop ≝
    263   match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
    264   [ VEmpty         ⇒ λm_refl. λv_refl.
    265       ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
    266         Q addr (
    267         match addr return λx: addressing_mode. is_in … fixed_v x → T with 
    268         [ ADDR11 x          ⇒ p_addr11 x
    269         | ADDR16 x          ⇒ p_addr16 x
    270         | DIRECT x          ⇒ p_direct x
    271         | INDIRECT x        ⇒ p_indirect x
    272         | EXT_INDIRECT x    ⇒ p_ext_indirect x
    273         | ACC_A             ⇒ p_acc_a
    274         | REGISTER x        ⇒ p_register x
    275         | ACC_B             ⇒ p_acc_b
    276         | DPTR              ⇒ p_dptr
    277         | DATA x            ⇒ p_data x
    278         | DATA16 x          ⇒ p_data16 x
    279         | ACC_DPTR          ⇒ p_acc_dptr
    280         | ACC_PC            ⇒ p_acc_pc
    281         | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
    282         | INDIRECT_DPTR     ⇒ p_indirect_dptr
    283         | CARRY             ⇒ p_carry
    284         | BIT_ADDR x        ⇒ p_bit_addr x
    285         | N_BIT_ADDR x      ⇒ p_n_bit_addr x
    286         | RELATIVE x        ⇒ p_relative x
    287         ] p)
    288   | VCons n' hd tl ⇒ λm_refl. λv_refl.
    289     let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
    290       p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
    291         p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
    292           p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
    293             p_bit_addr p_n_bit_addr p_relative n' tl ?
    294     in
    295     match hd return λa: addressing_mode_tag. a = hd → ? with
    296     [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
    297     | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
    298     | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
    299     | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
    300     | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
    301     | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
    302     | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
    303     | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
    304     | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
    305     | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
    306     | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
    307     | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
    308     | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
    309     | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
    310     | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
    311     | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
    312     | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
    313     | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
    314     | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
    315     ] (refl … hd)
    316   ] (refl … n) (refl_jmeq … v).
    317   [20:
    318     generalize in match proof; destruct
    319     whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
    320     cases (mem … eq_a m fixed_v hd) normalize nodelta
    321     [1:
    322       whd in match (subvector_with … eq_a tl fixed_v);
    323       #assm assumption
    324     |2:
    325       normalize in ⊢ (% → ?);
    326       #absurd cases absurd
    327     ]
    328   ]
    329   @(is_in_subvector_is_in_supervector … proof)
    330   destruct @I
    331 qed.
    332 
    333 (* XXX: todo *)
    334 lemma subaddressing_mode_elim':
    335   ∀T: Type[2].
    336   ∀n: nat.
    337   ∀o: nat.
    338   ∀v1: Vector addressing_mode_tag n.
    339   ∀v2: Vector addressing_mode_tag o.
    340   ∀Q: addressing_mode → T → Prop.
    341   ∀fixed_v: Vector addressing_mode_tag (n + o).
    342   ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
    343   ∀fixed_v_proof: fixed_v = v1 @@ v2.
    344   ∀subaddressing_mode_proof.
    345     subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
    346       P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
    347   #T #n #o #v1 #v2
    348   elim v1 cases v2
    349   [1:
    350     #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
    351     #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
    352     #subaddressing_mode_proof destruct normalize
    353     #addr #absurd cases absurd
    354   |2:
    355     #n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
    356     #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
    357     destruct normalize in match ([[]]@@hd:::tl);
    358   ]
    359   cases daemon
    360 qed.
    361 
    362 (* XXX: todo *)
    363 lemma subaddressing_mode_elim:
    364   ∀T: Type[2].
    365   ∀m: nat.
    366   ∀n: nat.
    367   ∀Q: addressing_mode → T → Prop.
    368   ∀fixed_v: Vector addressing_mode_tag m.
    369   ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
    370   ∀v: Vector addressing_mode_tag n.
    371   ∀proof.
    372     subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
    373       P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
    374   #T #m #n #Q #fixed_v
    375   elim fixed_v
    376   [1:
    377     #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
    378     #P14 #P15 #P16 #P17 #P18 #P19 #v #proof
    379     normalize
    380   |2:
    381   ]
    382   cases daemon
    383 qed.
    384112
    385113definition current_instruction_is_labelled ≝
     
    496224qed.
    497225
     226(*
    498227(* XXX: indexing bug *)
    499228lemma fetch_twice_fetch_execute_1:
     
    508237  * #_ #classify_assm' @classify_assm' assumption
    509238qed-.
     239*)
    510240
    511241lemma reachable_program_counter_to_0_lt_total_program_size:
     
    685415  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    686416  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
    687 qed.
     417qed. *)
    688418
    689419lemma trace_compute_paid_trace_cl_jump:
     
    998728        | ACALL addr     ⇒ λinstr.
    999729            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
    1000         | AJMP  addr     ⇒ λinstr. ticks
     730        | AJMP  addr     ⇒ λinstr.
     731            ticks + block_cost' code_memory' ? program_size' total_program_size cost_labels ? good_program_witness false ?
    1001732        | LCALL addr     ⇒ λinstr.
    1002733            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
  • src/ASM/Interpret.ma

    r1710 r1909  
    144144   | LCALL _ ⇒ cl_call
    145145   | JMP _ ⇒ cl_call
    146    | AJMP _ ⇒ cl_jump
    147    | LJMP _ ⇒ cl_jump
    148    | SJMP _ ⇒ cl_jump
     146   | AJMP _ ⇒ cl_other
     147   | LJMP _ ⇒ cl_other
     148   | SJMP _ ⇒ cl_other
    149149   | _ ⇒ cl_other
    150150   ].
     
    609609discriminator Prod.
    610610
     611definition compute_target_of_unconditional_jump:
     612    ∀program_counter: Word.
     613    ∀i: instruction.
     614      Word ≝
     615  λprogram_counter.
     616  λi.
     617    match i with
     618    [ LJMP addr ⇒
     619        match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with
     620        [ ADDR16 a ⇒ λaddr16: True. a
     621        | _ ⇒ λother: False. ⊥
     622        ] (subaddressing_modein … addr)
     623    | SJMP addr ⇒
     624        match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with
     625        [ RELATIVE r ⇒ λrelative: True.
     626          let 〈carry, new_pc〉 ≝ half_add ? program_counter (sign_extension r) in
     627            new_pc
     628        | _ ⇒ λother: False. ⊥
     629        ] (subaddressing_modein … addr)
     630    | AJMP addr ⇒
     631        match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
     632        [ ADDR11 a ⇒ λaddr11: True.
     633          let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 program_counter in
     634          let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
     635          let bit ≝ get_index' ? O ? nl in
     636          let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
     637          let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
     638          let 〈carry, new_pc〉 ≝ half_add ? program_counter new_addr in
     639            new_pc
     640        | _ ⇒ λother: False. ⊥
     641        ] (subaddressing_modein … addr)
     642    | _ ⇒ zero ?
     643    ].
     644  //
     645qed.
     646
     647definition is_unconditional_jump:
     648    instruction → bool ≝
     649  λi: instruction.
     650    match i with
     651    [ LJMP _ ⇒ true
     652    | SJMP _ ⇒ true
     653    | AJMP _ ⇒ true
     654    | _ ⇒ false
     655    ].
     656
     657let rec member_addressing_mode_tag
     658  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
     659    on v: Prop ≝
     660  match v with
     661  [ VEmpty ⇒ False
     662  | VCons n' hd tl ⇒
     663      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
     664  ].
     665
     666lemma is_a_decidable:
     667  ∀hd.
     668  ∀element.
     669    is_a hd element = true ∨ is_a hd element = false.
     670  #hd #element //
     671qed.
     672
     673lemma mem_decidable:
     674  ∀n: nat.
     675  ∀v: Vector addressing_mode_tag n.
     676  ∀element: addressing_mode_tag.
     677    mem … eq_a n v element = true ∨
     678      mem … eq_a … v element = false.
     679  #n #v #element //
     680qed.
     681
     682lemma eq_a_elim:
     683  ∀tag.
     684  ∀hd.
     685  ∀P: bool → Prop.
     686    (tag = hd → P (true)) →
     687      (tag ≠ hd → P (false)) →
     688        P (eq_a tag hd).
     689  #tag #hd #P
     690  cases tag
     691  cases hd
     692  #true_hyp #false_hyp
     693  try @false_hyp
     694  try @true_hyp
     695  try %
     696  #absurd destruct(absurd)
     697qed.
     698 
     699lemma is_a_true_to_is_in:
     700  ∀n: nat.
     701  ∀x: addressing_mode.
     702  ∀tag: addressing_mode_tag.
     703  ∀supervector: Vector addressing_mode_tag n.
     704  mem addressing_mode_tag eq_a n supervector tag →
     705    is_a tag x = true →
     706      is_in … supervector x.
     707  #n #x #tag #supervector
     708  elim supervector
     709  [1:
     710    #absurd cases absurd
     711  |2:
     712    #n' #hd #tl #inductive_hypothesis
     713    whd in match (mem … eq_a (S n') (hd:::tl) tag);
     714    @eq_a_elim normalize nodelta
     715    [1:
     716      #tag_hd_eq #irrelevant
     717      whd in match (is_in (S n') (hd:::tl) x);
     718      <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
     719      @I
     720    |2:
     721      #tag_hd_neq
     722      whd in match (is_in (S n') (hd:::tl) x);
     723      change with (
     724        mem … eq_a n' tl tag)
     725          in match (fold_right … n' ? false tl);
     726      #mem_hyp #is_a_hyp
     727      cases(is_a hd x)
     728      [1:
     729        normalize nodelta //
     730      |2:
     731        normalize nodelta
     732        @inductive_hypothesis assumption
     733      ]
     734    ]
     735  ]
     736qed.
     737
     738lemma is_in_subvector_is_in_supervector:
     739  ∀m, n: nat.
     740  ∀subvector: Vector addressing_mode_tag m.
     741  ∀supervector: Vector addressing_mode_tag n.
     742  ∀element: addressing_mode.
     743    subvector_with … eq_a subvector supervector →
     744      is_in m subvector element → is_in n supervector element.
     745  #m #n #subvector #supervector #element
     746  elim subvector
     747  [1:
     748    #subvector_with_proof #is_in_proof
     749    cases is_in_proof
     750  |2:
     751    #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
     752    whd in match (is_in … (hd':::tl') element);
     753    cases (is_a_decidable hd' element)
     754    [1:
     755      #is_a_true >is_a_true
     756      #irrelevant
     757      whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
     758      @(is_a_true_to_is_in … is_a_true)
     759      lapply(subvector_with_proof)
     760      cases(mem … eq_a n supervector hd') //
     761    |2:
     762      #is_a_false >is_a_false normalize nodelta
     763      #assm
     764      @inductive_hypothesis
     765      [1:
     766        generalize in match subvector_with_proof;
     767        whd in match (subvector_with … eq_a (hd':::tl') supervector);
     768        cases(mem_decidable n supervector hd')
     769        [1:
     770          #mem_true >mem_true normalize nodelta
     771          #assm assumption
     772        |2:
     773          #mem_false >mem_false #absurd
     774          cases absurd
     775        ]
     776      |2:
     777        assumption
     778      ]
     779    ]
     780  ]
     781qed.
     782 
     783let rec subaddressing_mode_elim_type
     784  (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
     785    (Q: addressing_mode → T → Prop)
     786      (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
     787      (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
     788      (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
     789      (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
     790      (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
     791      (p_acc_a:                              is_in m fixed_v ACC_A             → T)
     792      (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
     793      (p_acc_b:                              is_in m fixed_v ACC_B             → T)
     794      (p_dptr:                               is_in m fixed_v DPTR              → T)
     795      (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
     796      (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
     797      (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
     798      (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
     799      (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
     800      (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
     801      (p_carry:                              is_in m fixed_v CARRY             → T)
     802      (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
     803      (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
     804      (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
     805        (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
     806      on v: Prop ≝
     807  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
     808  [ VEmpty         ⇒ λm_refl. λv_refl.
     809      ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
     810        Q addr (
     811        match addr return λx: addressing_mode. is_in … fixed_v x → T with 
     812        [ ADDR11 x          ⇒ p_addr11 x
     813        | ADDR16 x          ⇒ p_addr16 x
     814        | DIRECT x          ⇒ p_direct x
     815        | INDIRECT x        ⇒ p_indirect x
     816        | EXT_INDIRECT x    ⇒ p_ext_indirect x
     817        | ACC_A             ⇒ p_acc_a
     818        | REGISTER x        ⇒ p_register x
     819        | ACC_B             ⇒ p_acc_b
     820        | DPTR              ⇒ p_dptr
     821        | DATA x            ⇒ p_data x
     822        | DATA16 x          ⇒ p_data16 x
     823        | ACC_DPTR          ⇒ p_acc_dptr
     824        | ACC_PC            ⇒ p_acc_pc
     825        | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
     826        | INDIRECT_DPTR     ⇒ p_indirect_dptr
     827        | CARRY             ⇒ p_carry
     828        | BIT_ADDR x        ⇒ p_bit_addr x
     829        | N_BIT_ADDR x      ⇒ p_n_bit_addr x
     830        | RELATIVE x        ⇒ p_relative x
     831        ] p)
     832  | VCons n' hd tl ⇒ λm_refl. λv_refl.
     833    let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
     834      p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
     835        p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     836          p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
     837            p_bit_addr p_n_bit_addr p_relative n' tl ?
     838    in
     839    match hd return λa: addressing_mode_tag. a = hd → ? with
     840    [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
     841    | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
     842    | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
     843    | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
     844    | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
     845    | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
     846    | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
     847    | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
     848    | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
     849    | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
     850    | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
     851    | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
     852    | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
     853    | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
     854    | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
     855    | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
     856    | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
     857    | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
     858    | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
     859    ] (refl … hd)
     860  ] (refl … n) (refl_jmeq … v).
     861  [20:
     862    generalize in match proof; destruct
     863    whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
     864    cases (mem … eq_a m fixed_v hd) normalize nodelta
     865    [1:
     866      whd in match (subvector_with … eq_a tl fixed_v);
     867      #assm assumption
     868    |2:
     869      normalize in ⊢ (% → ?);
     870      #absurd cases absurd
     871    ]
     872  ]
     873  @(is_in_subvector_is_in_supervector … proof)
     874  destruct @I
     875qed.
     876
     877(* XXX: todo *)
     878lemma subaddressing_mode_elim':
     879  ∀T: Type[2].
     880  ∀n: nat.
     881  ∀o: nat.
     882  ∀v1: Vector addressing_mode_tag n.
     883  ∀v2: Vector addressing_mode_tag o.
     884  ∀Q: addressing_mode → T → Prop.
     885  ∀fixed_v: Vector addressing_mode_tag (n + o).
     886  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
     887  ∀fixed_v_proof: fixed_v = v1 @@ v2.
     888  ∀subaddressing_mode_proof.
     889    subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
     890      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
     891  #T #n #o #v1 #v2
     892  elim v1 cases v2
     893  [1:
     894    #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
     895    #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
     896    #subaddressing_mode_proof destruct normalize
     897    #addr #absurd cases absurd
     898  |2:
     899    #n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
     900    #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
     901    destruct normalize in match ([[]]@@hd:::tl);
     902  ]
     903  cases daemon
     904qed.
     905
     906(* XXX: todo *)
     907lemma subaddressing_mode_elim:
     908  ∀T: Type[2].
     909  ∀m: nat.
     910  ∀n: nat.
     911  ∀Q: addressing_mode → T → Prop.
     912  ∀fixed_v: Vector addressing_mode_tag m.
     913  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
     914  ∀v: Vector addressing_mode_tag n.
     915  ∀proof.
     916    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
     917      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
     918  #T #m #n #Q #fixed_v
     919  elim fixed_v
     920  [1:
     921    #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
     922    #P14 #P15 #P16 #P17 #P18 #P19 #v #proof
     923    normalize
     924  |2:
     925  ]
     926  cases daemon
     927qed.
     928
    611929definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
    612930  Σs': Status cm.
    613931    And (clock ?? s' = \snd current + clock … s)
    614       (ASM_classify0 (\fst (\fst current)) = cl_other →
    615         program_counter ? ? s' = \snd (\fst current)) ≝
     932      (if is_unconditional_jump (\fst (\fst current)) then
     933        program_counter ? ? s' =
     934          compute_target_of_unconditional_jump (\snd (\fst current)) (\fst (\fst current))
     935       else
     936        (ASM_classify0 (\fst (\fst current)) = cl_other →
     937          program_counter ? ? s' = \snd (\fst current))) ≝
    616938  λcm,s0,instr_pc_ticks.
    617939    let 〈instr_pc, ticks〉 as INSTR_PC_TICKS ≝ instr_pc_ticks in
     
    651973            set_program_counter … s new_pc
    652974      | LJMP addr ⇒ λinstr_refl.
     975          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
    653976          let s ≝ set_clock ?? s (ticks + clock … s) in
    654           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with
    655             [ ADDR16 a ⇒ λaddr16: True.
    656                 set_program_counter … s a
    657             | _ ⇒ λother: False. ⊥
    658             ] (subaddressing_modein … addr)
     977            set_program_counter … s new_pc
    659978      | SJMP addr ⇒ λinstr_refl.
     979          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
    660980          let s ≝ set_clock ?? s (ticks + clock … s) in
    661           match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with
    662             [ RELATIVE r ⇒ λrelative: True.
    663                 let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) (sign_extension r) in
    664                   set_program_counter … s new_pc
    665             | _ ⇒ λother: False. ⊥
    666             ] (subaddressing_modein … addr)
     981            set_program_counter … s new_pc
    667982      | AJMP addr ⇒ λinstr_refl.
     983          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
    668984          let s ≝ set_clock ?? s (ticks + clock … s) in
    669           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
    670             [ ADDR11 a ⇒ λaddr11: True.
    671               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
    672               let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
    673               let bit ≝ get_index' ? O ? nl in
    674               let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
    675               let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    676               let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) new_addr in
    677                 set_program_counter … s new_pc
    678             | _ ⇒ λother: False. ⊥
    679             ] (subaddressing_modein … addr)
     985            set_program_counter … s new_pc
    680986      | ACALL addr ⇒ λinstr_refl.
    681987          let s ≝ set_clock ?? s (ticks + clock … s) in
     
    7141020    normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS %
    7151021    try //
    716     destruct(INSTR_PC) <instr_refl
    717     #absurd normalize in absurd; try destruct(absurd) try %
     1022    destruct(INSTR_PC) <instr_refl whd
     1023    try (#absurd normalize in absurd; try destruct(absurd) try %) %
    7181024  |9:
    7191025    cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??
     
    7281034      destruct(INSTR_PC_TICKS) %
    7291035    |2:
    730       #classify_assm -clock_proof >classify_proof -classify_proof
     1036      -clock_proof <INSTR_PC_TICKS normalize nodelta
     1037      cut(\fst instr_pc = instr ∧ \snd instr_pc = pc)
    7311038      [1:
    732         normalize nodelta normalize <INSTR_PC_TICKS
    733         destruct(INSTR_PC) %
     1039        destruct(INSTR_PC) /2/
    7341040      |2:
    735         <classify_assm <INSTR_PC_TICKS destruct <e0 %
    736       ]
     1041        * #hyp1 #hyp2 >hyp1 normalize nodelta
     1042      <instr_refl normalize nodelta #hyp >classify_proof -classify_proof
     1043      try assumption >hyp2 %
    7371044    ]
    7381045  ]
     
    7451052definition execute_1': ∀cm.∀s:Status cm.
    7461053  Σs':Status cm.
    747     And (clock ?? s' = current_instruction_cost cm s + clock … s)
    748       (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … s') ≝
     1054    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
     1055      And (clock ?? s' = current_instruction_cost cm s + clock … s)
     1056        (if is_unconditional_jump (\fst (\fst instr_pc_ticks)) then
     1057          program_counter ? ? s' =
     1058            compute_target_of_unconditional_jump (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))
     1059         else
     1060          (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
     1061            program_counter ? ? s' = \snd (\fst instr_pc_ticks))) ≝
    7491062  λcm. λs: Status cm.
    7501063  let instr_pc_ticks ≝ fetch cm (program_counter … s) in
     
    7561069  |2:
    7571070    cases(execute_1_0 cm s instr_pc_ticks)
    758     #the_status * #_ #classify_assm #classify_assm'
    759     lapply(classify_assm ?)
    760     [1:
    761       change with (
    762         ASM_classify cm s = cl_other
    763       )
    764       assumption
    765     |2:
    766       #program_counter_refl >program_counter_refl %
    767     ]
     1071    #the_status * #_ #classify_assm
     1072    assumption
    7681073  ]
    7691074qed.
     
    7721077
    7731078lemma execute_1_ok: ∀cm.∀s.
    774   (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
    775     (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)).
    776  #cm #s whd in match execute_1; normalize nodelta @pi2
     1079  let instr_pc_ticks ≝ fetch cm (program_counter … s) in
     1080    (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
     1081      (if is_unconditional_jump (\fst (\fst instr_pc_ticks)) then
     1082         program_counter ? cm (execute_1 cm s) =
     1083           compute_target_of_unconditional_jump (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))
     1084       else
     1085         (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
     1086           (program_counter ? cm (execute_1 cm s)) = \snd (\fst instr_pc_ticks)))
     1087(*    (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)) *).
     1088  #cm #s normalize nodelta
     1089  whd in match execute_1; normalize nodelta @pi2
    7771090qed-. (*x Andrea: indexing takes ages here *)
    7781091
Note: See TracChangeset for help on using the changeset viewer.