Changeset 1909

Timestamp:

04/27/12 10:59:03 (13 months ago)

Author:

mulligan

Message:

Ported new statements to remainder of Interpret.ma file.

Location:

src/ASM

Files:

• ASMCosts.ma (modified) (5 diffs)
• Interpret.ma (modified) (8 diffs)

src/ASM/ASMCosts.ma

@@ -110 +110 @@
   cases other
 qed.
-        
-lemma is_a_decidable:
-  ∀hd.
-  ∀element.
-    is_a hd element = true ∨ is_a hd element = false.
-  #hd #element //
-qed.
-
-lemma mem_decidable:
-  ∀n: nat.
-  ∀v: Vector addressing_mode_tag n.
-  ∀element: addressing_mode_tag.
-    mem … eq_a n v element = true ∨
-      mem … eq_a … v element = false.
-  #n #v #element //
-qed.
-
-lemma eq_a_elim:
-  ∀tag.
-  ∀hd.
-  ∀P: bool → Prop.
-    (tag = hd → P (true)) →
-      (tag ≠ hd → P (false)) →
-        P (eq_a tag hd).
-  #tag #hd #P
-  cases tag
-  cases hd
-  #true_hyp #false_hyp
-  try @false_hyp
-  try @true_hyp
-  try %
-  #absurd destruct(absurd)
-qed.
-  
-lemma is_a_true_to_is_in:
-  ∀n: nat.
-  ∀x: addressing_mode.
-  ∀tag: addressing_mode_tag.
-  ∀supervector: Vector addressing_mode_tag n.
-  mem addressing_mode_tag eq_a n supervector tag →
-    is_a tag x = true →
-      is_in … supervector x.
-  #n #x #tag #supervector
-  elim supervector
-  [1:
-    #absurd cases absurd
-  |2:
-    #n' #hd #tl #inductive_hypothesis
-    whd in match (mem … eq_a (S n') (hd:::tl) tag);
-    @eq_a_elim normalize nodelta
-    [1:
-      #tag_hd_eq #irrelevant
-      whd in match (is_in (S n') (hd:::tl) x);
-      <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
-      @I
-    |2:
-      #tag_hd_neq
-      whd in match (is_in (S n') (hd:::tl) x);
-      change with (
-        mem … eq_a n' tl tag)
-          in match (fold_right … n' ? false tl);
-      #mem_hyp #is_a_hyp
-      cases(is_a hd x)
-      [1:
-        normalize nodelta //
-      |2:
-        normalize nodelta
-        @inductive_hypothesis assumption
-      ]
-    ]
-  ]
-qed.
-
-lemma is_in_subvector_is_in_supervector:
-  ∀m, n: nat.
-  ∀subvector: Vector addressing_mode_tag m.
-  ∀supervector: Vector addressing_mode_tag n.
-  ∀element: addressing_mode.
-    subvector_with … eq_a subvector supervector →
-      is_in m subvector element → is_in n supervector element.
-  #m #n #subvector #supervector #element
-  elim subvector
-  [1:
-    #subvector_with_proof #is_in_proof
-    cases is_in_proof
-  |2:
-    #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
-    whd in match (is_in … (hd':::tl') element);
-    cases (is_a_decidable hd' element)
-    [1:
-      #is_a_true >is_a_true
-      #irrelevant
-      whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
-      @(is_a_true_to_is_in … is_a_true)
-      lapply(subvector_with_proof)
-      cases(mem … eq_a n supervector hd') //
-    |2:
-      #is_a_false >is_a_false normalize nodelta
-      #assm
-      @inductive_hypothesis
-      [1:
-        generalize in match subvector_with_proof;
-        whd in match (subvector_with … eq_a (hd':::tl') supervector);
-        cases(mem_decidable n supervector hd')
-        [1:
-          #mem_true >mem_true normalize nodelta
-          #assm assumption
-        |2:
-          #mem_false >mem_false #absurd
-          cases absurd
-        ]
-      |2:
-        assumption
-      ]
-    ]
-  ]
-qed.
-
-let rec member_addressing_mode_tag
-  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
-    on v: Prop ≝
-  match v with
-  [ VEmpty ⇒ False
-  | VCons n' hd tl ⇒
-      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
-  ].
-  
-let rec subaddressing_mode_elim_type
-  (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
-    (Q: addressing_mode → T → Prop)
-      (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
-      (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
-      (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
-      (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
-      (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
-      (p_acc_a:                              is_in m fixed_v ACC_A             → T)
-      (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
-      (p_acc_b:                              is_in m fixed_v ACC_B             → T)
-      (p_dptr:                               is_in m fixed_v DPTR              → T)
-      (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
-      (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
-      (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
-      (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
-      (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
-      (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
-      (p_carry:                              is_in m fixed_v CARRY             → T)
-      (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
-      (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
-      (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
-        (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
-      on v: Prop ≝
-  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
-  [ VEmpty         ⇒ λm_refl. λv_refl.
-      ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
-        Q addr (
-        match addr return λx: addressing_mode. is_in … fixed_v x → T with 
-        [ ADDR11 x          ⇒ p_addr11 x
-        | ADDR16 x          ⇒ p_addr16 x
-        | DIRECT x          ⇒ p_direct x
-        | INDIRECT x        ⇒ p_indirect x
-        | EXT_INDIRECT x    ⇒ p_ext_indirect x
-        | ACC_A             ⇒ p_acc_a
-        | REGISTER x        ⇒ p_register x
-        | ACC_B             ⇒ p_acc_b
-        | DPTR              ⇒ p_dptr
-        | DATA x            ⇒ p_data x
-        | DATA16 x          ⇒ p_data16 x
-        | ACC_DPTR          ⇒ p_acc_dptr
-        | ACC_PC            ⇒ p_acc_pc
-        | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
-        | INDIRECT_DPTR     ⇒ p_indirect_dptr
-        | CARRY             ⇒ p_carry
-        | BIT_ADDR x        ⇒ p_bit_addr x
-        | N_BIT_ADDR x      ⇒ p_n_bit_addr x
-        | RELATIVE x        ⇒ p_relative x
-        ] p)
-  | VCons n' hd tl ⇒ λm_refl. λv_refl.
-    let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
-      p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
-        p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
-          p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
-            p_bit_addr p_n_bit_addr p_relative n' tl ?
-    in
-    match hd return λa: addressing_mode_tag. a = hd → ? with
-    [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
-    | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
-    | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
-    | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
-    | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
-    | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
-    | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
-    | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
-    | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
-    | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
-    | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
-    | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
-    | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
-    | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
-    | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
-    | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
-    | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
-    | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
-    | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
-    ] (refl … hd)
-  ] (refl … n) (refl_jmeq … v).
-  [20:
-    generalize in match proof; destruct
-    whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
-    cases (mem … eq_a m fixed_v hd) normalize nodelta
-    [1:
-      whd in match (subvector_with … eq_a tl fixed_v);
-      #assm assumption
-    |2:
-      normalize in ⊢ (% → ?);
-      #absurd cases absurd
-    ]
-  ]
-  @(is_in_subvector_is_in_supervector … proof)
-  destruct @I
-qed.
-
-(* XXX: todo *)
-lemma subaddressing_mode_elim':
-  ∀T: Type[2].
-  ∀n: nat.
-  ∀o: nat.
-  ∀v1: Vector addressing_mode_tag n.
-  ∀v2: Vector addressing_mode_tag o.
-  ∀Q: addressing_mode → T → Prop.
-  ∀fixed_v: Vector addressing_mode_tag (n + o).
-  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
-  ∀fixed_v_proof: fixed_v = v1 @@ v2.
-  ∀subaddressing_mode_proof.
-    subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
-      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
-  #T #n #o #v1 #v2
-  elim v1 cases v2
-  [1:
-    #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
-    #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
-    #subaddressing_mode_proof destruct normalize
-    #addr #absurd cases absurd
-  |2:
-    #n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
-    #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
-    destruct normalize in match ([[]]@@hd:::tl);
-  ]
-  cases daemon
-qed.
-
-(* XXX: todo *)
-lemma subaddressing_mode_elim:
-  ∀T: Type[2].
-  ∀m: nat.
-  ∀n: nat.
-  ∀Q: addressing_mode → T → Prop.
-  ∀fixed_v: Vector addressing_mode_tag m.
-  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
-  ∀v: Vector addressing_mode_tag n.
-  ∀proof.
-    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
-      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
-  #T #m #n #Q #fixed_v
-  elim fixed_v
-  [1:
-    #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
-    #P14 #P15 #P16 #P17 #P18 #P19 #v #proof
-    normalize
-  |2:
-  ]
-  cases daemon
-qed.
 
 definition current_instruction_is_labelled ≝
@@ -496 +224 @@
 qed.
 
+(*
 (* XXX: indexing bug *)
 lemma fetch_twice_fetch_execute_1:
@@ -508 +237 @@
   * #_ #classify_assm' @classify_assm' assumption
 qed-.
+*)
 
 lemma reachable_program_counter_to_0_lt_total_program_size:
@@ -685 +415 @@
   whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
   <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
-qed.
+qed. *)
 
 lemma trace_compute_paid_trace_cl_jump:
@@ -998 +728 @@
         | ACALL addr     ⇒ λinstr.
             ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
-        | AJMP  addr     ⇒ λinstr. ticks
+        | AJMP  addr     ⇒ λinstr.
+            ticks + block_cost' code_memory' ? program_size' total_program_size cost_labels ? good_program_witness false ?
         | LCALL addr     ⇒ λinstr.
             ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?

src/ASM/Interpret.ma

@@ -144 +144 @@
    | LCALL _ ⇒ cl_call
    | JMP _ ⇒ cl_call
-   | AJMP _ ⇒ cl_jump
-   | LJMP _ ⇒ cl_jump
-   | SJMP _ ⇒ cl_jump
+   | AJMP _ ⇒ cl_other
+   | LJMP _ ⇒ cl_other
+   | SJMP _ ⇒ cl_other
    | _ ⇒ cl_other
    ].
@@ -609 +609 @@
 discriminator Prod.
 
+definition compute_target_of_unconditional_jump:
+    ∀program_counter: Word.
+    ∀i: instruction.
+      Word ≝
+  λprogram_counter.
+  λi.
+    match i with
+    [ LJMP addr ⇒
+        match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with
+        [ ADDR16 a ⇒ λaddr16: True. a
+        | _ ⇒ λother: False. ⊥
+        ] (subaddressing_modein … addr)
+    | SJMP addr ⇒
+        match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with
+        [ RELATIVE r ⇒ λrelative: True.
+          let 〈carry, new_pc〉 ≝ half_add ? program_counter (sign_extension r) in
+            new_pc
+        | _ ⇒ λother: False. ⊥
+        ] (subaddressing_modein … addr)
+    | AJMP addr ⇒
+        match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
+        [ ADDR11 a ⇒ λaddr11: True.
+          let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 program_counter in
+          let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
+          let bit ≝ get_index' ? O ? nl in
+          let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
+          let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
+          let 〈carry, new_pc〉 ≝ half_add ? program_counter new_addr in
+            new_pc
+        | _ ⇒ λother: False. ⊥
+        ] (subaddressing_modein … addr)
+    | _ ⇒ zero ?
+    ].
+  //
+qed.
+
+definition is_unconditional_jump:
+    instruction → bool ≝
+  λi: instruction.
+    match i with
+    [ LJMP _ ⇒ true
+    | SJMP _ ⇒ true
+    | AJMP _ ⇒ true
+    | _ ⇒ false
+    ].
+
+let rec member_addressing_mode_tag
+  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
+    on v: Prop ≝
+  match v with
+  [ VEmpty ⇒ False
+  | VCons n' hd tl ⇒
+      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
+  ].
+
+lemma is_a_decidable:
+  ∀hd.
+  ∀element.
+    is_a hd element = true ∨ is_a hd element = false.
+  #hd #element //
+qed.
+
+lemma mem_decidable:
+  ∀n: nat.
+  ∀v: Vector addressing_mode_tag n.
+  ∀element: addressing_mode_tag.
+    mem … eq_a n v element = true ∨
+      mem … eq_a … v element = false.
+  #n #v #element //
+qed.
+
+lemma eq_a_elim:
+  ∀tag.
+  ∀hd.
+  ∀P: bool → Prop.
+    (tag = hd → P (true)) →
+      (tag ≠ hd → P (false)) →
+        P (eq_a tag hd).
+  #tag #hd #P
+  cases tag
+  cases hd
+  #true_hyp #false_hyp
+  try @false_hyp
+  try @true_hyp
+  try %
+  #absurd destruct(absurd)
+qed.
+  
+lemma is_a_true_to_is_in:
+  ∀n: nat.
+  ∀x: addressing_mode.
+  ∀tag: addressing_mode_tag.
+  ∀supervector: Vector addressing_mode_tag n.
+  mem addressing_mode_tag eq_a n supervector tag →
+    is_a tag x = true →
+      is_in … supervector x.
+  #n #x #tag #supervector
+  elim supervector
+  [1:
+    #absurd cases absurd
+  |2:
+    #n' #hd #tl #inductive_hypothesis
+    whd in match (mem … eq_a (S n') (hd:::tl) tag);
+    @eq_a_elim normalize nodelta
+    [1:
+      #tag_hd_eq #irrelevant
+      whd in match (is_in (S n') (hd:::tl) x);
+      <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
+      @I
+    |2:
+      #tag_hd_neq
+      whd in match (is_in (S n') (hd:::tl) x);
+      change with (
+        mem … eq_a n' tl tag)
+          in match (fold_right … n' ? false tl);
+      #mem_hyp #is_a_hyp
+      cases(is_a hd x)
+      [1:
+        normalize nodelta //
+      |2:
+        normalize nodelta
+        @inductive_hypothesis assumption
+      ]
+    ]
+  ]
+qed.
+
+lemma is_in_subvector_is_in_supervector:
+  ∀m, n: nat.
+  ∀subvector: Vector addressing_mode_tag m.
+  ∀supervector: Vector addressing_mode_tag n.
+  ∀element: addressing_mode.
+    subvector_with … eq_a subvector supervector →
+      is_in m subvector element → is_in n supervector element.
+  #m #n #subvector #supervector #element
+  elim subvector
+  [1:
+    #subvector_with_proof #is_in_proof
+    cases is_in_proof
+  |2:
+    #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
+    whd in match (is_in … (hd':::tl') element);
+    cases (is_a_decidable hd' element)
+    [1:
+      #is_a_true >is_a_true
+      #irrelevant
+      whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
+      @(is_a_true_to_is_in … is_a_true)
+      lapply(subvector_with_proof)
+      cases(mem … eq_a n supervector hd') //
+    |2:
+      #is_a_false >is_a_false normalize nodelta
+      #assm
+      @inductive_hypothesis
+      [1:
+        generalize in match subvector_with_proof;
+        whd in match (subvector_with … eq_a (hd':::tl') supervector);
+        cases(mem_decidable n supervector hd')
+        [1:
+          #mem_true >mem_true normalize nodelta
+          #assm assumption
+        |2:
+          #mem_false >mem_false #absurd
+          cases absurd
+        ]
+      |2:
+        assumption
+      ]
+    ]
+  ]
+qed.
+  
+let rec subaddressing_mode_elim_type
+  (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
+    (Q: addressing_mode → T → Prop)
+      (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
+      (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
+      (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
+      (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
+      (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
+      (p_acc_a:                              is_in m fixed_v ACC_A             → T)
+      (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
+      (p_acc_b:                              is_in m fixed_v ACC_B             → T)
+      (p_dptr:                               is_in m fixed_v DPTR              → T)
+      (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
+      (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
+      (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
+      (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
+      (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
+      (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
+      (p_carry:                              is_in m fixed_v CARRY             → T)
+      (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
+      (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
+      (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
+        (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
+      on v: Prop ≝
+  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
+  [ VEmpty         ⇒ λm_refl. λv_refl.
+      ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
+        Q addr (
+        match addr return λx: addressing_mode. is_in … fixed_v x → T with 
+        [ ADDR11 x          ⇒ p_addr11 x
+        | ADDR16 x          ⇒ p_addr16 x
+        | DIRECT x          ⇒ p_direct x
+        | INDIRECT x        ⇒ p_indirect x
+        | EXT_INDIRECT x    ⇒ p_ext_indirect x
+        | ACC_A             ⇒ p_acc_a
+        | REGISTER x        ⇒ p_register x
+        | ACC_B             ⇒ p_acc_b
+        | DPTR              ⇒ p_dptr
+        | DATA x            ⇒ p_data x
+        | DATA16 x          ⇒ p_data16 x
+        | ACC_DPTR          ⇒ p_acc_dptr
+        | ACC_PC            ⇒ p_acc_pc
+        | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
+        | INDIRECT_DPTR     ⇒ p_indirect_dptr
+        | CARRY             ⇒ p_carry
+        | BIT_ADDR x        ⇒ p_bit_addr x
+        | N_BIT_ADDR x      ⇒ p_n_bit_addr x
+        | RELATIVE x        ⇒ p_relative x
+        ] p)
+  | VCons n' hd tl ⇒ λm_refl. λv_refl.
+    let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
+      p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
+        p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
+          p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
+            p_bit_addr p_n_bit_addr p_relative n' tl ?
+    in
+    match hd return λa: addressing_mode_tag. a = hd → ? with
+    [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
+    | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
+    | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
+    | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
+    | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
+    | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
+    | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
+    | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
+    | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
+    | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
+    | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
+    | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
+    | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
+    | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
+    | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
+    | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
+    | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
+    | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
+    | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
+    ] (refl … hd)
+  ] (refl … n) (refl_jmeq … v).
+  [20:
+    generalize in match proof; destruct
+    whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
+    cases (mem … eq_a m fixed_v hd) normalize nodelta
+    [1:
+      whd in match (subvector_with … eq_a tl fixed_v);
+      #assm assumption
+    |2:
+      normalize in ⊢ (% → ?);
+      #absurd cases absurd
+    ]
+  ]
+  @(is_in_subvector_is_in_supervector … proof)
+  destruct @I
+qed.
+
+(* XXX: todo *)
+lemma subaddressing_mode_elim':
+  ∀T: Type[2].
+  ∀n: nat.
+  ∀o: nat.
+  ∀v1: Vector addressing_mode_tag n.
+  ∀v2: Vector addressing_mode_tag o.
+  ∀Q: addressing_mode → T → Prop.
+  ∀fixed_v: Vector addressing_mode_tag (n + o).
+  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
+  ∀fixed_v_proof: fixed_v = v1 @@ v2.
+  ∀subaddressing_mode_proof.
+    subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
+      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
+  #T #n #o #v1 #v2
+  elim v1 cases v2
+  [1:
+    #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
+    #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
+    #subaddressing_mode_proof destruct normalize
+    #addr #absurd cases absurd
+  |2:
+    #n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
+    #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
+    destruct normalize in match ([[]]@@hd:::tl);
+  ]
+  cases daemon
+qed.
+
+(* XXX: todo *)
+lemma subaddressing_mode_elim:
+  ∀T: Type[2].
+  ∀m: nat.
+  ∀n: nat.
+  ∀Q: addressing_mode → T → Prop.
+  ∀fixed_v: Vector addressing_mode_tag m.
+  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
+  ∀v: Vector addressing_mode_tag n.
+  ∀proof.
+    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
+      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
+  #T #m #n #Q #fixed_v
+  elim fixed_v
+  [1:
+    #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
+    #P14 #P15 #P16 #P17 #P18 #P19 #v #proof
+    normalize
+  |2:
+  ]
+  cases daemon
+qed.
+
 definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
   Σs': Status cm.
     And (clock ?? s' = \snd current + clock … s)
-      (ASM_classify0 (\fst (\fst current)) = cl_other →
-        program_counter ? ? s' = \snd (\fst current)) ≝
+      (if is_unconditional_jump (\fst (\fst current)) then
+        program_counter ? ? s' =
+          compute_target_of_unconditional_jump (\snd (\fst current)) (\fst (\fst current))
+       else
+        (ASM_classify0 (\fst (\fst current)) = cl_other →
+          program_counter ? ? s' = \snd (\fst current))) ≝
   λcm,s0,instr_pc_ticks.
     let 〈instr_pc, ticks〉 as INSTR_PC_TICKS ≝ instr_pc_ticks in
@@ -651 +973 @@
             set_program_counter … s new_pc
       | LJMP addr ⇒ λinstr_refl.
+          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
           let s ≝ set_clock ?? s (ticks + clock … s) in
-          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with
-            [ ADDR16 a ⇒ λaddr16: True.
-                set_program_counter … s a
-            | _ ⇒ λother: False. ⊥
-            ] (subaddressing_modein … addr)
+            set_program_counter … s new_pc
       | SJMP addr ⇒ λinstr_refl.
+          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
           let s ≝ set_clock ?? s (ticks + clock … s) in
-          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with
-            [ RELATIVE r ⇒ λrelative: True.
-                let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) (sign_extension r) in
-                  set_program_counter … s new_pc
-            | _ ⇒ λother: False. ⊥
-            ] (subaddressing_modein … addr)
+            set_program_counter … s new_pc
       | AJMP addr ⇒ λinstr_refl.
+          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
           let s ≝ set_clock ?? s (ticks + clock … s) in
-          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
-            [ ADDR11 a ⇒ λaddr11: True.
-              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
-              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
-              let bit ≝ get_index' ? O ? nl in
-              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
-              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
-              let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) new_addr in
-                set_program_counter … s new_pc
-            | _ ⇒ λother: False. ⊥
-            ] (subaddressing_modein … addr)
+            set_program_counter … s new_pc
       | ACALL addr ⇒ λinstr_refl.
           let s ≝ set_clock ?? s (ticks + clock … s) in
@@ -714 +1020 @@
     normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS %
     try //
-    destruct(INSTR_PC) <instr_refl
-    #absurd normalize in absurd; try destruct(absurd) try %
+    destruct(INSTR_PC) <instr_refl whd
+    try (#absurd normalize in absurd; try destruct(absurd) try %) %
   |9:
     cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??
@@ -728 +1034 @@
       destruct(INSTR_PC_TICKS) %
     |2:
-      #classify_assm -clock_proof >classify_proof -classify_proof
+      -clock_proof <INSTR_PC_TICKS normalize nodelta
+      cut(\fst instr_pc = instr ∧ \snd instr_pc = pc)
       [1:
-        normalize nodelta normalize <INSTR_PC_TICKS
-        destruct(INSTR_PC) %
+        destruct(INSTR_PC) /2/
       |2:
-        <classify_assm <INSTR_PC_TICKS destruct <e0 %
-      ]
+        * #hyp1 #hyp2 >hyp1 normalize nodelta
+      <instr_refl normalize nodelta #hyp >classify_proof -classify_proof
+      try assumption >hyp2 %
     ]
   ]
@@ -745 +1052 @@
 definition execute_1': ∀cm.∀s:Status cm.
   Σs':Status cm.
-    And (clock ?? s' = current_instruction_cost cm s + clock … s)
-      (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … s') ≝
+    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
+      And (clock ?? s' = current_instruction_cost cm s + clock … s)
+        (if is_unconditional_jump (\fst (\fst instr_pc_ticks)) then
+          program_counter ? ? s' =
+            compute_target_of_unconditional_jump (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))
+         else
+          (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
+            program_counter ? ? s' = \snd (\fst instr_pc_ticks))) ≝
   λcm. λs: Status cm.
   let instr_pc_ticks ≝ fetch cm (program_counter … s) in
@@ -756 +1069 @@
   |2:
     cases(execute_1_0 cm s instr_pc_ticks)
-    #the_status * #_ #classify_assm #classify_assm'
-    lapply(classify_assm ?)
-    [1:
-      change with (
-        ASM_classify cm s = cl_other
-      )
-      assumption
-    |2:
-      #program_counter_refl >program_counter_refl %
-    ]
+    #the_status * #_ #classify_assm
+    assumption
   ]
 qed.
@@ -772 +1077 @@
 
 lemma execute_1_ok: ∀cm.∀s.
-  (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
-    (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)).
- #cm #s whd in match execute_1; normalize nodelta @pi2
+  let instr_pc_ticks ≝ fetch cm (program_counter … s) in
+    (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
+      (if is_unconditional_jump (\fst (\fst instr_pc_ticks)) then
+         program_counter ? cm (execute_1 cm s) =
+           compute_target_of_unconditional_jump (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))
+       else
+         (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
+           (program_counter ? cm (execute_1 cm s)) = \snd (\fst instr_pc_ticks)))
+(*    (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)) *).
+  #cm #s normalize nodelta
+  whd in match execute_1; normalize nodelta @pi2
 qed-. (*x Andrea: indexing takes ages here *)