Changeset 2171 for src/ASM

Timestamp:

Jul 10, 2012, 11:54:54 AM (9 years ago)

Author:

mulligan

Message:

Finished the commutations

File:

• src/ASM/Test.ma (modified) (9 diffs)

src/ASM/Test.ma

@@ -151 +151 @@
       normalize @eq_f @inductive_hypothesis @nmk #relevant
       >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) %
+    ]
+  ]
+qed.
+
+(* XXX: move elsewhere *)
+lemma get_index_v_set_index_miss:
+  ∀a: Type[0].
+  ∀n: nat.
+  ∀v: Vector a n.
+  ∀i, j: nat.
+  ∀e: a.
+  ∀i_proof: i < n.
+  ∀j_proof: j < n.
+    i ≠ j →
+      get_index_v a n (set_index a n v i e i_proof) j j_proof =
+        get_index_v a n v j j_proof.
+  #a #n #v elim v
+  [1:
+    #i #j #e #i_proof
+    cases (lt_to_not_zero … i_proof)
+  |2:
+    #n' #hd #tl #inductive_hypothesis #i #j
+    cases i cases j
+    [1:
+      #e #i_proof #j_proof #neq_assm
+      cases (absurd ? (refl … 0) neq_assm)
+    |2,3:
+      #i' #e #i_proof #j_proof #_ %
+    |4:
+      #i' #j' #e #i_proof #j_proof #neq_assm
+      @inductive_hypothesis @nmk #eq_assm
+      >eq_assm in neq_assm; #neq_assm
+      cases (absurd ? (refl ??) neq_assm)
     ]
   ]
@@ -202 +235 @@
 qed.
 
+lemma get_index_v_status_of_pseudo_status:
+  ∀M, code_memory, sigma, policy, s, sfr.
+    (get_index_v Byte 19
+      (special_function_registers_8051 (BitVectorTrie Byte 16)
+      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
+      (status_of_pseudo_status M code_memory s sigma policy))
+      (sfr_8051_index sfr) (sfr8051_index_19 sfr) =
+    map_address_using_internal_pseudo_address_map M sigma sfr
+      (get_index_v Byte 19
+        (special_function_registers_8051 pseudo_assembly_program code_memory s)
+        (sfr_8051_index sfr) (sfr8051_index_19 sfr))).
+  #M #code_memory #sigma #policy #s #sfr
+  whd in match status_of_pseudo_status; normalize nodelta
+  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
+  inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta
+ [1:
+    cases sfr
+    [18:
+      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
+      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
+      >sndM_refl %
+    ]
+    %
+  |2:
+    @pair_elim #high #low #high_low_refl normalize nodelta
+    inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
+    cases sfr
+    [18,37:
+      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
+      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
+      >sndM_refl normalize nodelta >high_low_refl normalize nodelta 
+      >eq_upper_lower_refl normalize nodelta
+      whd in match (set_8051_sfr ?????); //
+    ]
+    @get_index_v_set_index_miss whd in ⊢ (?(??%%));
+    @nmk #absurd destruct(absurd)
+  ]
+qed.
+
 lemma set_8051_sfr_status_of_pseudo_status:
   ∀M, code_memory, sigma, policy, s, sfr, v,v'.
@@ -212 +284 @@
   #M #code_memory #sigma #policy #s #sfr #v #v' #v_ok
   whd in ⊢ (??%%); @split_eq_status try % /2/
+qed.
+
+lemma get_8051_sfr_status_of_pseudo_status:
+  ∀M, code_memory, sigma, policy, s, sfr.
+  (get_8051_sfr (BitVectorTrie Byte 16)
+    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
+    (status_of_pseudo_status M code_memory s sigma policy) sfr =
+  map_address_using_internal_pseudo_address_map M sigma sfr
+   (get_8051_sfr pseudo_assembly_program code_memory s sfr)).
+  #M #code_memory #sigma #policy #s #sfr
+  whd in match get_8051_sfr; normalize nodelta
+  @get_index_v_status_of_pseudo_status
+qed.
+
+lemma get_8052_sfr_status_of_pseudo_status:
+  ∀M, code_memory, sigma, policy, s, sfr.
+  (get_8052_sfr (BitVectorTrie Byte 16)
+    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
+    (status_of_pseudo_status M code_memory s sigma policy) sfr =
+   (get_8052_sfr pseudo_assembly_program code_memory s sfr)).
+  //
 qed.
 
@@ -394 +487 @@
 qed.
 
-(*CSC: Taken from AssemblyProofSplit *)
-lemma get_index_v_set_index_miss:
-  ∀T: Type[0].
-  ∀n, i, j: nat.
-  ∀v: Vector T n.
-  ∀b: T.
-  ∀i_proof: i < n.
-  ∀j_proof: j < n.
-  i ≠ j →
-    get_index_v T n (set_index T n v i b i_proof) j j_proof =
-      get_index_v T n v j j_proof.
-  #T #n #i #j #v lapply i lapply j elim v #i #j
-  [1:
-    #b #i_proof
-    cases (lt_to_not_zero … i_proof)
-  |2:
-    #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j
-    lapply i_proof lapply i_neq_j cases i'
-    [1:
-      -i_neq_j #i_neq_j -i_proof #i_proof
-      whd in match (set_index ??????);
-      lapply j_proof lapply i_neq_j cases j'
-      [1:
-        #relevant @⊥ cases relevant -relevant #absurd @absurd %
-      |2:
-        #j' #_ -j_proof #j_proof %
-      ]
-    |2:
-      #i' -i_neq_j #i_neq_j -i_proof #i_proof
-      lapply j_proof lapply i_neq_j cases j'
-      [1:
-        #_ #j_proof %
-      |2:
-        #j' #i_neq_j #j_proof
-        @inductive_hypothesis @nmk #relevant
-        cases i_neq_j #absurd @absurd >relevant %
-      ]
-    ]
-  ]
-qed.
-
-lemma get_8051_sfr_status_of_pseudo_status:
- ∀M,cm,s,sigma,policy,sfr.
-  get_8051_sfr …
-   (code_memory_of_pseudo_assembly_program cm sigma policy)
-   (status_of_pseudo_status M cm s sigma policy) sfr =
-  map_address_using_internal_pseudo_address_map M sigma sfr
-   (get_8051_sfr … cm s sfr).
- #M #cm #s #sigma #policy #sfr whd in ⊢ (??%%);
- whd in match status_of_pseudo_status; normalize nodelta
- whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
- whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
- cases (\snd M) normalize nodelta [cases sfr %]
- #map_mem #map_acc @pair_elim #high #low #_ normalize nodelta
- cases (eq_upper_lower ??) normalize nodelta cases sfr normalize nodelta
- [18,37: @get_index_v_set_index
- |*: >get_index_v_set_index_miss % normalize #abs destruct]
-qed.
-
 lemma bit_address_of_register_status_of_pseudo_status:
  ∀M,cm,s,sigma,policy,r.
@@ -476 +510 @@
   (lookup Byte 7 addr
    (low_internal_ram pseudo_assembly_program cm s) (zero 8)).
+
+(*CSC: provable using the axiom in AssemblyProof, but this one seems more
+  primitive *)
+axiom lookup_high_internal_ram_of_pseudo_high_internal_ram:
+ ∀M,sigma,cm,s,addr.
+  lookup Byte 7 addr
+  (high_internal_ram_of_pseudo_high_internal_ram M
+   (high_internal_ram pseudo_assembly_program cm s)) (zero 8)
+  =
+  map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr)
+  (lookup Byte 7 addr
+   (high_internal_ram pseudo_assembly_program cm s) (zero 8)).
 
 lemma get_register_status_of_pseudo_status:
@@ -526 +572 @@
 
 definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝
- λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λaddr.
+ λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λsigma. λaddr.
   match addr with
   [ INDIRECT i ⇒
@@ -534 +580 @@
      assoc_list_lookup ??
       (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None …
+  | ACC_DPTR ⇒
+    (* XXX: \snd M = None plus in the very rare case when we are trying to dereference a null (O) pointer
+            in the ACC_A *)
+      map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) =
+        get_8051_sfr … cm s SFR_ACC_A
+  | ACC_PC ⇒
+      (* XXX: as above *)
+      map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) =
+        get_8051_sfr … cm s SFR_ACC_A ∧ sigma (program_counter … s) = program_counter … s
   | _ ⇒ True ].
 
@@ -633 +688 @@
   ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
   ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'.
-   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps addr →
+   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
    map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
     set_arg_8 (BitVectorTrie Byte 16)
@@ -712 +767 @@
       >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ]
 qed.
+
+definition get_bit_addressable_sfr:
+    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → bool → Byte ≝
+  λM: Type[0].
+  λcode_memory:M.
+  λs: PreStatus M code_memory.
+  λb: Byte.
+  λl: bool.
+  match sfr_of_Byte b with
+  [ None ⇒ match not_implemented in False with [ ]
+  | Some sfr8051_8052 ⇒
+    match sfr8051_8052 with
+    [ inl sfr ⇒
+      match sfr with
+      [ SFR_P1 ⇒
+        if l then
+          p1_latch … s
+        else
+          get_8051_sfr … s SFR_P1
+      | SFR_P3 ⇒
+        if l then
+          p3_latch … s
+        else
+          get_8051_sfr … s SFR_P3
+      | _ ⇒ get_8051_sfr … s sfr
+      ]
+    | inr sfr ⇒ get_8052_sfr M code_memory s sfr
+    ]
+  ].
+
+definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ;
+                                          acc_a ; acc_b ; data ; acc_dptr ;
+                                          acc_pc ; ext_indirect ;
+                                          ext_indirect_dptr ]] → Byte ≝
+  λm, cm, s, l, a.
+    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
+                                                acc_a ; acc_b ; data ; acc_dptr ;
+                                                acc_pc ; ext_indirect ;
+                                                ext_indirect_dptr ]] x) → ? with
+      [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
+      | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
+      | DATA d ⇒ λdata: True. d
+      | REGISTER r ⇒ λregister: True. get_register ?? s r
+      | EXT_INDIRECT_DPTR ⇒
+        λext_indirect_dptr: True.
+          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
+            lookup ? 16 address (external_ram ?? s) (zero 8)
+      | EXT_INDIRECT e ⇒
+        λext_indirect: True.
+          let address ≝ get_register ?? s [[ false; false; e ]]  in
+          let padded_address ≝ pad 8 8 address in
+            lookup ? 16 padded_address (external_ram ?? s) (zero 8)
+      | ACC_DPTR ⇒
+        λacc_dptr: True.
+          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
+          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
+          let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
+            lookup ? 16 address (external_ram ?? s) (zero 8)
+      | ACC_PC ⇒
+        λacc_pc: True.
+          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
+          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
+            lookup ? 16 address (external_ram ?? s) (zero 8)
+      | DIRECT d ⇒
+        λdirect: True.
+          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
+            match head' … hd with
+            [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
+            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
+            ]
+      | INDIRECT i ⇒
+        λindirect: True.
+          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
+            match head' … hd with
+            [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)
+            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
+            ]
+      | _ ⇒ λother.
+        match other in False with [ ]
+      ] (subaddressing_modein … a).
+
+lemma p1_latch_status_of_pseudo_status:
+    ∀M.
+    ∀code_memory: pseudo_assembly_program.
+    ∀s: PreStatus … code_memory.
+    ∀sigma.
+    ∀policy.
+    (p1_latch (BitVectorTrie Byte 16)
+      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
+      (status_of_pseudo_status M code_memory s sigma policy) =
+    (p1_latch pseudo_assembly_program code_memory s)).
+  //
+qed.
+
+lemma p3_latch_status_of_pseudo_status:
+    ∀M.
+    ∀code_memory: pseudo_assembly_program.
+    ∀s: PreStatus … code_memory.
+    ∀sigma.
+    ∀policy.
+    (p3_latch (BitVectorTrie Byte 16)
+      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
+      (status_of_pseudo_status M code_memory s sigma policy) =
+    (p3_latch pseudo_assembly_program code_memory s)).
+  //
+qed.
+
+lemma get_bit_addressable_sfr_status_of_pseudo_status':
+  let M ≝ pseudo_assembly_program in
+    ∀code_memory: M.
+    ∀s: PreStatus M code_memory.
+    ∀d: Byte.
+    ∀l: bool.
+      Σp: Byte. ∀M. ∀sigma. ∀policy.
+        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
+          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
+          (status_of_pseudo_status M code_memory s sigma policy) d l =
+        map_address_Byte_using_internal_pseudo_address_map M sigma
+         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)).
+  whd in match get_bit_addressable_sfr;
+  whd in match map_address_Byte_using_internal_pseudo_address_map;
+  normalize nodelta
+  @(let M ≝ pseudo_assembly_program in
+    λcode_memory:M.
+    λs: PreStatus M code_memory.
+    λb: Byte.
+    λl: bool.
+    match sfr_of_Byte b with
+    [ None ⇒ match not_implemented in False with [ ]
+    | Some sfr8051_8052 ⇒
+    match sfr8051_8052 with
+    [ inl sfr ⇒
+      match sfr with
+      [ SFR_P1 ⇒
+        if l then
+          p1_latch … s
+        else
+          get_8051_sfr … s SFR_P1
+      | SFR_P3 ⇒
+        if l then
+          p3_latch … s
+        else
+          get_8051_sfr … s SFR_P3
+      | _ ⇒ get_8051_sfr … s sfr
+      ]
+    | inr sfr ⇒ get_8052_sfr M code_memory s sfr
+    ]
+    ])
+  #M #sigma #policy normalize nodelta
+  /by get_8051_sfr_status_of_pseudo_status, p1_latch_status_of_pseudo_status, p3_latch_status_of_pseudo_status/
+qed.
+
+lemma get_bit_addressable_sfr_status_of_pseudo_status:
+  let M ≝ pseudo_assembly_program in
+    ∀code_memory: M.
+    ∀s: PreStatus M code_memory.
+    ∀d: Byte.
+    ∀l: bool.
+    ∀M. ∀sigma. ∀policy.
+        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
+          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
+          (status_of_pseudo_status M code_memory s sigma policy) d l =
+        map_address_Byte_using_internal_pseudo_address_map M sigma
+         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)).
+ #code #s #d #v cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_
+ #H @H
+qed.
+
+lemma program_counter_status_of_pseudo_status:
+    ∀code_memory: pseudo_assembly_program.
+    ∀s: PreStatus ? code_memory.
+    ∀M. ∀sigma. ∀policy.
+      program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy)
+          (status_of_pseudo_status M code_memory s sigma policy) =
+        sigma (program_counter … s).
+  //
+qed.
+
+lemma get_cy_flag_status_of_pseudo_status:
+  ∀M, cm, sigma, policy, s.
+  (get_cy_flag (BitVectorTrie Byte 16)
+    (code_memory_of_pseudo_assembly_program cm sigma policy)
+    (status_of_pseudo_status M cm s sigma policy) =
+  get_cy_flag pseudo_assembly_program cm s).
+  #M #cm #sigma #policy #s
+  whd in match get_cy_flag; normalize nodelta
+  >get_index_v_status_of_pseudo_status %
+qed.
+
+lemma get_arg_8_status_of_pseudo_status:
+  ∀cm.
+  ∀ps.
+  ∀l.
+  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
+    Σp: Byte. ∀M. ∀sigma. ∀policy.
+      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
+      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
+      (status_of_pseudo_status M cm ps sigma policy) l addr =
+      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr).
+  whd in match get_arg_8; normalize nodelta
+  @(let m ≝ pseudo_assembly_program in
+    λcm: m. λs: PreStatus m cm. λl: bool. λa: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr]].
+    match a return λx. bool_to_Prop (is_in ? [[ direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr ]] x) → Σp. ? with
+      [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
+      | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
+      | DATA d ⇒ λdata: True. d
+      | REGISTER r ⇒ λregister: True. get_register ?? s r
+      | EXT_INDIRECT_DPTR ⇒
+        λext_indirect_dptr: True.
+          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
+            lookup ? 16 address (external_ram ?? s) (zero 8)
+      | EXT_INDIRECT e ⇒
+        λext_indirect: True.
+          let address ≝ get_register ?? s [[ false; false; e ]]  in
+          let padded_address ≝ pad 8 8 address in
+            lookup ? 16 padded_address (external_ram ?? s) (zero 8)
+      | ACC_DPTR ⇒
+        λacc_dptr: True.
+          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
+          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
+          let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
+            lookup ? 16 address (external_ram ?? s) (zero 8)
+      | ACC_PC ⇒
+        λacc_pc: True.
+          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
+          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
+            lookup ? 16 address (external_ram ?? s) (zero 8)
+      | DIRECT d ⇒
+        λdirect: True.
+          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
+            match head' … hd with
+            [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
+            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
+            ]
+      | INDIRECT i ⇒
+        λindirect: True.
+          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
+            match head' … hd with
+            [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)
+            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
+            ]
+      | _ ⇒ λother: False.
+        match other in False with [ ]
+      ] (subaddressing_modein … a)) normalize nodelta
+  #M #sigma #policy
+  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
+  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
+  [1:
+    #_ >p normalize nodelta >p1 normalize nodelta
+    @get_bit_addressable_sfr_status_of_pseudo_status
+  |2:
+    #_>p normalize nodelta >p1 normalize nodelta
+    @lookup_low_internal_ram_of_pseudo_low_internal_ram
+  |3,4:
+    #assoc_list_assm >get_register_status_of_pseudo_status
+    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
+    >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta
+    [1:
+      >(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma)
+    |2:
+      >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
+    ]
+    @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
+  |5:
+    #assoc_list_assm >get_register_status_of_pseudo_status
+    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
+    >assoc_list_assm normalize nodelta %
+  |6,7,8,9:
+    #_ /2/
+  |10:
+    #acc_a_assm >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
+    >get_8051_sfr_status_of_pseudo_status
+    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
+    >acc_a_assm >p normalize nodelta //
+  |11:
+    * #map_acc_a_assm #sigma_assm >get_8051_sfr_status_of_pseudo_status >program_counter_status_of_pseudo_status
+    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
+    >sigma_assm >map_acc_a_assm >p normalize nodelta //
+  |12:
+    #_ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
+    >external_ram_status_of_pseudo_status //
+  ]
+qed.
+
+lemma get_arg_16_status_of_pseudo_status:
+  ∀cm.
+  ∀ps.
+  ∀addr: [[data16]].
+  ∀M. ∀sigma. ∀policy.
+      get_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
+      (status_of_pseudo_status M cm ps sigma policy) addr =
+      (get_arg_16 … cm ps addr).
+  //
+qed.
+
+lemma set_arg_16_status_of_pseudo_status:
+  ∀cm.
+  ∀ps.
+  ∀addr: [[dptr]].
+  ∀v: Word.
+  ∀M. ∀sigma. ∀policy.
+      set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
+      (status_of_pseudo_status M cm ps sigma policy) v addr =
+      status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy.
+  #cm #ps #addr #v #M #sigma #policy
+  @(subaddressing_mode_elim … addr)
+  whd in match set_arg_16; normalize nodelta
+  whd in match set_arg_16'; normalize nodelta
+  @(vsplit_elim bool ???) #bu #bl #bu_bl_refl normalize nodelta
+  >(set_8051_sfr_status_of_pseudo_status … bu)
+  [1: >(set_8051_sfr_status_of_pseudo_status … bl) ]
+  //
+qed.
+
+definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] →
+                       bool → bool ≝
+  λm, cm, s, a, l.
+    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
+                                                 n_bit_addr ;
+                                                 carry ]] x) → ? with
+      [ BIT_ADDR b ⇒
+        λbit_addr: True.
+        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
+        match head' … bit_1 with
+        [ true ⇒
+          let address ≝ nat_of_bitvector … seven_bits in
+          let d ≝ address ÷ 8 in
+          let m ≝ address mod 8 in
+          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
+          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
+            get_index_v … sfr m ?
+        | false ⇒
+          let address ≝ nat_of_bitvector … seven_bits in
+          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
+          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
+            get_index_v … t (modulus address 8) ? 
+        ]
+      | N_BIT_ADDR n ⇒
+        λn_bit_addr: True.
+        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
+        match head' … bit_1 with
+        [ true ⇒
+          let address ≝ nat_of_bitvector … seven_bits in
+          let d ≝ address ÷ 8 in
+          let m ≝ address mod 8 in
+          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
+          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
+            ¬(get_index_v … sfr m ?)
+        | false ⇒
+          let address ≝ nat_of_bitvector … seven_bits in
+          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
+          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
+            ¬(get_index_v … t (modulus address 8) ?)
+        ]
+      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
+      | _ ⇒ λother.
+        match other in False with [ ]
+      ] (subaddressing_modein … a).
+      @modulus_less_than
+qed.
+
+definition map_bit_address_mode_using_internal_pseudo_address_map_get ≝
+ λM:internal_pseudo_address_map.λcm: pseudo_assembly_program.λs:PreStatus ? cm.λsigma: Word → Word. λaddr. λl.
+  match addr with
+  [ BIT_ADDR b ⇒
+    let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
+    match head' … bit_1 with
+    [ true ⇒
+      let address ≝ nat_of_bitvector … seven_bits in
+      let d ≝ address ÷ 8 in
+      let m ≝ address mod 8 in
+      let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
+        map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l
+    | false ⇒
+      let address ≝ nat_of_bitvector … seven_bits in
+      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
+      let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
+        map_internal_ram_address_using_pseudo_address_map M sigma
+          (false:::address') t = t
+    ]
+  | N_BIT_ADDR b ⇒
+    let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
+    match head' … bit_1 with
+    [ true ⇒
+      let address ≝ nat_of_bitvector … seven_bits in
+      let d ≝ address ÷ 8 in
+      let m ≝ address mod 8 in
+      let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
+        map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l
+    | false ⇒
+      let address ≝ nat_of_bitvector … seven_bits in
+      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
+      let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
+        map_internal_ram_address_using_pseudo_address_map M sigma
+          (false:::address') t = t
+    ]
+  | _ ⇒ True ].
+
+lemma get_arg_1_status_of_pseudo_status':
+  ∀cm.
+  ∀ps.
+  ∀addr: [[bit_addr; n_bit_addr; carry]].
+  ∀l.
+    Σb: bool. ∀M. ∀sigma. ∀policy.
+      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
+      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
+      (status_of_pseudo_status M cm ps sigma policy) addr l =
+      (get_arg_1 … cm ps addr l).
+  whd in match get_arg_1; normalize nodelta
+  @(let m ≝ pseudo_assembly_program in
+    λcm: m. λs: PseudoStatus cm. λa:[[bit_addr; n_bit_addr; carry]]. λl.
+    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
+                                                 n_bit_addr ;
+                                                 carry ]] x) → Σb: bool. ? with
+      [ BIT_ADDR b ⇒
+        λbit_addr: True.
+        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
+        match head' … bit_1 with
+        [ true ⇒
+          let address ≝ nat_of_bitvector … seven_bits in
+          let d ≝ address ÷ 8 in
+          let m ≝ address mod 8 in
+          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
+          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
+            get_index_v … sfr m ?
+        | false ⇒
+          let address ≝ nat_of_bitvector … seven_bits in
+          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
+          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
+            get_index_v … t (modulus address 8) ? 
+        ]
+      | N_BIT_ADDR n ⇒
+        λn_bit_addr: True.
+        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
+        match head' … bit_1 with
+        [ true ⇒
+          let address ≝ nat_of_bitvector … seven_bits in
+          let d ≝ address ÷ 8 in
+          let m ≝ address mod 8 in
+          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
+          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
+            ¬(get_index_v … sfr m ?)
+        | false ⇒
+          let address ≝ nat_of_bitvector … seven_bits in
+          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
+          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
+            ¬(get_index_v … t (modulus address 8) ?)
+        ]
+      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
+      | _ ⇒ λother.
+        match other in False with [ ]
+      ] (subaddressing_modein … a)) normalize nodelta
+  try @modulus_less_than
+  #M #sigma #policy
+  [1:
+    #_ @get_cy_flag_status_of_pseudo_status
+  |2,4:
+    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
+    >get_bit_addressable_sfr_status_of_pseudo_status #map_address_assm
+    >map_address_assm %
+  |3,5:
+    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
+    whd in match status_of_pseudo_status; normalize nodelta
+    >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
+    #map_address_assm >map_address_assm %
+  ]
+qed.
+
+lemma get_arg_1_status_of_pseudo_status:
+  ∀cm.
+  ∀ps.
+  ∀addr: [[bit_addr; n_bit_addr; carry]].
+  ∀l.
+  ∀M. ∀sigma. ∀policy.
+      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
+      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
+      (status_of_pseudo_status M cm ps sigma policy) addr l =
+      (get_arg_1 … cm ps addr l).
+  #cm #ps #addr #l
+  cases (get_arg_1_status_of_pseudo_status' cm ps addr l) #_ #assm
+  @assm
+qed.
+
+definition set_arg_1': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → Σs':PreStatus M code_memory. clock ? code_memory s = clock ? code_memory s' ≝
+  λm: Type[0].
+  λcm.
+  λs: PreStatus m cm.
+  λa: [[bit_addr; carry]].
+  λv: Bit.
+    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with
+      [ BIT_ADDR b ⇒ λbit_addr: True.
+        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
+        match head' … bit_1 with
+        [ true ⇒
+          let address ≝ nat_of_bitvector … seven_bits in
+          let d ≝ address ÷ 8 in
+          let m ≝ address mod 8 in
+          let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
+          let sfr ≝ get_bit_addressable_sfr … s t true in
+          let new_sfr ≝ set_index … sfr m v ? in
+            set_bit_addressable_sfr … s new_sfr t
+        | false ⇒
+          let address ≝ nat_of_bitvector … seven_bits in
+          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
+          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
+          let n_bit ≝ set_index … t (modulus address 8) v ? in
+          let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
+            set_low_internal_ram … s memory
+        ]
+      | CARRY ⇒
+        λcarry: True.
+        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
+        let new_psw ≝ v:::seven_bits in
+          set_8051_sfr ?? s SFR_PSW new_psw
+      | _ ⇒
+        λother: False.
+          match other in False with
+            [ ]
+      ] (subaddressing_modein … a).
+  try (repeat @le_S_S @le_O_n)
+  try @modulus_less_than
+  /by/
+  cases daemon (* XXX: russell type for preservation of clock on set_bit_addressable_sfr *)
+qed.
+
+definition set_arg_1:
+    ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] →
+      Bit → PreStatus M code_memory ≝ set_arg_1'.
+
+definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝
+  λM: internal_pseudo_address_map.
+  λcm: pseudo_assembly_program.
+  λs: PreStatus ? cm.
+  λsigma: Word → Word.
+  λaddr: [[bit_addr; carry]].
+  λv: Bit.
+  match addr with
+  [ BIT_ADDR b ⇒
+    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
+    match head' … bit_1 with
+    [ true ⇒
+      let address ≝ nat_of_bitvector … seven_bits in
+      let d ≝ address ÷ 8 in
+      let m ≝ address mod 8 in
+      let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
+      let sfr ≝ get_bit_addressable_sfr … s t true in
+        map_address_Byte_using_internal_pseudo_address_map M sigma t sfr = sfr
+    | false ⇒
+      let address ≝ nat_of_bitvector … seven_bits in
+      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
+      let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
+        map_internal_ram_address_using_pseudo_address_map M sigma
+          (false:::address') t = t
+    ]   
+  | CARRY ⇒ True
+  | _ ⇒ True
+  ].
+
+definition map_bit_address_mode_using_internal_pseudo_address_map_set_2 ≝
+  λM: internal_pseudo_address_map.
+  λcm: pseudo_assembly_program.
+  λs: PreStatus ? cm.
+  λsigma: Word → Word.
+  λaddr: [[bit_addr; carry]].
+  λv: Bit.
+  match addr with
+  [ BIT_ADDR b ⇒
+    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
+    match head' … bit_1 with
+    [ true ⇒
+      let address ≝ nat_of_bitvector … seven_bits in
+      let d ≝ address ÷ 8 in
+      let m ≝ address mod 8 in
+      let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
+      let sfr ≝ get_bit_addressable_sfr … s t true in
+      let new_sfr ≝ set_index … sfr m v ? in
+        map_address_Byte_using_internal_pseudo_address_map M sigma new_sfr t = t
+    | false ⇒
+      let address ≝ nat_of_bitvector … seven_bits in
+      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
+      let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
+      let n_bit ≝ set_index … t (modulus address 8) v ? in
+      let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
+        map_internal_ram_address_using_pseudo_address_map M sigma
+          (false:::address') n_bit = n_bit
+    ]   
+  | CARRY ⇒ True
+  | _ ⇒ True
+  ].
+  @modulus_less_than
+qed.
+
+lemma set_arg_1_status_of_pseudo_status:
+  ∀cm: pseudo_assembly_program.
+  ∀ps: PreStatus pseudo_assembly_program cm.
+  ∀addr: [[bit_addr; carry]].
+  ∀b: Bit.
+    Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy.
+      map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
+      map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b →
+        set_arg_1 (BitVectorTrie Byte 16)
+          (code_memory_of_pseudo_assembly_program cm sigma policy)
+          (status_of_pseudo_status M cm ps sigma policy) addr b =
+        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b) sigma policy.
+  whd in match set_arg_1; normalize nodelta
+  whd in match set_arg_1'; normalize nodelta
+  whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_1; normalize nodelta
+  whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_2; normalize nodelta
+  @(let m ≝ pseudo_assembly_program in
+    λcm.
+    λs: PreStatus m cm.
+    λa: [[bit_addr; carry]].
+    λv: Bit.
+    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σp. ? with
+      [ BIT_ADDR b ⇒ λbit_addr: True.
+        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
+        match head' … bit_1 with
+        [ true ⇒
+          let address ≝ nat_of_bitvector … seven_bits in
+          let d ≝ address ÷ 8 in
+          let m ≝ address mod 8 in
+          let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
+          let sfr ≝ get_bit_addressable_sfr … s t true in
+          let new_sfr ≝ set_index … sfr m v ? in
+            set_bit_addressable_sfr … s new_sfr t
+        | false ⇒
+          let address ≝ nat_of_bitvector … seven_bits in
+          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
+          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
+          let n_bit ≝ set_index … t (modulus address 8) v ? in
+          let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
+            set_low_internal_ram … s memory
+        ]
+      | CARRY ⇒
+        λcarry: True.
+        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
+        let new_psw ≝ v:::seven_bits in
+          set_8051_sfr ?? s SFR_PSW new_psw
+      | _ ⇒
+        λother: False.
+          match other in False with
+            [ ]
+      ] (subaddressing_modein … a)) normalize nodelta
+  try @modulus_less_than #M #sigma #policy
+  [1:
+    #_ #_ >get_8051_sfr_status_of_pseudo_status
+    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
+    >p normalize nodelta @set_8051_sfr_status_of_pseudo_status %
+  |2,3:
+    >get_8051_sfr_status_of_pseudo_status
+    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
+    >p normalize nodelta >p1 normalize nodelta
+    #map_bit_address_assm_1 #map_bit_address_assm_2
+    [1:
+      >get_bit_addressable_sfr_status_of_pseudo_status
+      >map_bit_address_assm_1
+      >(set_bit_addressable_sfr_status_of_pseudo_status cm s … map_bit_address_assm_2) %
+    |2:
+      whd in match status_of_pseudo_status in ⊢ (??(????%)?); normalize nodelta
+      >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
+      >map_bit_address_assm_1
+      >(insert_low_internal_ram_of_pseudo_low_internal_ram … map_bit_address_assm_2)
+      >set_low_internal_ram_status_of_pseudo_status in ⊢ (??%?); %
+    ]
+  ]
+qed.