include "ASM/Assembly.ma".
include "ASM/Interpret.ma".
include "ASM/StatusProofs.ma".
include alias "arithmetics/nat.ma".

let rec encoding_check
  (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
    (encoding: list Byte)
      on encoding: Prop ≝
  match encoding with
  [ nil ⇒ final_pc = pc
  | cons hd tl ⇒
    let 〈new_pc, byte〉 ≝ next code_memory pc in
      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
  ].

lemma encoding_check_append:
  ∀code_memory: BitVectorTrie Byte 16.
  ∀final_pc: Word.
  ∀l1: list Byte.
  ∀pc: Word.
  ∀l2: list Byte.
    encoding_check code_memory pc final_pc (l1@l2) →
      let pc_plus_len ≝ add … pc (bitvector_of_nat … (length … l1)) in
        encoding_check code_memory pc pc_plus_len l1 ∧
          encoding_check code_memory pc_plus_len final_pc l2.
  #code_memory #final_pc #l1 elim l1
  [1:
    #pc #l2
    whd in ⊢ (????% → ?); #H
    <add_zero
    whd whd in ⊢ (?%?); /2/
  |2:
    #hd #tl #IH #pc #l2 * #H1 #H2
(*    >add_SO in H2; #H2 *)
    cases (IH … H2) #E1 #E2 %
    [1:
      % try @H1
      <(add_bitvector_of_nat_Sm 16 (|tl|)) in E1;
      <add_associative #assm assumption
    |2:
      <add_associative in E2;
      <(add_bitvector_of_nat_Sm 16 (|tl|)) #assm
      assumption
    ]
  ]
qed.

definition ticks_of_instruction ≝
  λi.
    let trivial_code_memory ≝ assembly1 i in
    let trivial_status ≝ load_code_memory trivial_code_memory in
      \snd (fetch trivial_status (zero ?)).

lemma fetch_assembly:
  ∀pc: Word.
  ∀i: instruction.
  ∀code_memory: BitVectorTrie Byte 16.
  ∀assembled: list Byte.
    assembled = assembly1 i →
      let len ≝ length … assembled in
      let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
        encoding_check code_memory pc pc_plus_len assembled →
          let 〈instr, pc', ticks〉 ≝ fetch code_memory pc in
           (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' pc_plus_len) = true.
  cases daemon
(* XXX: commented out as takes ages to typecheck
  #pc #i #code_memory #assembled cases i [8: *]
 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
 [47,48,49:
 |*: #arg @(subaddressing_mode_elim … arg)
  [2,3,5,7,10,12,16,17,18,21,26,27,28,31,32,33,37,38,39,40,41,42,43,44,45,48,51,58,
   59,60,63,64,65,66,67: #ARG]]
 [4,5,6,7,8,9,10,11,12,13,22,23,24,27,28,39,40,41,42,43,44,45,46,47,48,49,50,51,52,
  56,57,69,70,72: #arg2 @(subaddressing_mode_elim … arg2)
  [1,2,4,7,9,11,12,14,15,17,18,19,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38,
   39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,
   68,69,70,71: #ARG2]]
 [1,2,19,20: #arg3 @(subaddressing_mode_elim … arg3) #ARG3]
 normalize in ⊢ (???% → ?);
 [92,94,42,93,95: @vsplit_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
  normalize in ⊢ (???% → ?);]
 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
 whd in match fetch; normalize nodelta <H1 whd in ⊢ (match % with [ _ ⇒ ? ]);
 [17,18,19,20,21,22,23,24,25,26,32,34,35,36,37,39: <H3]
 try <H2 whd >eq_instruction_refl >H4 @eq_bv_refl *)
qed.

let rec fetch_many
  (code_memory: BitVectorTrie Byte 16) (final_pc: Word) (pc: Word)
    (expected: list instruction)
      on expected: Prop ≝
  match expected with
  [ nil ⇒ eq_bv … pc final_pc = true
  | cons i tl ⇒
    let pc' ≝ add 16 pc (bitvector_of_nat 16 (|assembly1 … i|)) in
      (〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧
        fetch_many code_memory final_pc pc' tl)
  ].
          
lemma fetch_assembly_pseudo':
  ∀lookup_labels.
  ∀sigma: Word → Word.
  ∀policy: Word → bool.
  ∀ppc.
  ∀lookup_datalabels.
  ∀pi.
  ∀code_memory.
  ∀len.
  ∀assembled.
  ∀instructions.
    let pc ≝ sigma ppc in
      instructions = expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi →
        〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi →
          let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
            encoding_check code_memory pc pc_plus_len assembled →
              fetch_many code_memory pc_plus_len pc instructions.
  #lookup_labels #sigma #policy #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
  normalize nodelta #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
  cases (pair_destruct ?????? assembled_refl) -assembled_refl #len_refl #assembled_refl
  >len_refl >assembled_refl -len_refl
  generalize in match (add 16 (sigma ppc)
    (bitvector_of_nat 16
     (|flatten (Vector bool 8)
       (map instruction (list (Vector bool 8)) assembly1 instructions)|)));
  #final_pc
  generalize in match (sigma ppc); elim instructions
  [1:
    #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
  |2:
    #i #tl #IH #pc #H whd
    cases (encoding_check_append ????? H) -H #H1 #H2
    lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);    
    cases (fetch ??) * #instr #pc' #ticks
    #H3 lapply (H3 H1) -H3 normalize nodelta #H3
    lapply (conjunction_true ?? H3) * #H4 #H5
    lapply (conjunction_true … H4) * #B1 #B2
    >(eq_instruction_to_eq … B1) >(eq_bv_eq … H5) %
    >(eqb_true_to_refl … B2) >(eq_instruction_to_eq … B1) try % @IH @H2
  ]
qed.

lemma fetch_assembly_pseudo:
  ∀program: pseudo_assembly_program.
  ∀sigma: Word → Word.
  ∀policy: Word → bool.
  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
  ∀ppc.∀ppc_ok.
  ∀code_memory.
  let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
  let pc ≝ sigma ppc in
  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
    encoding_check code_memory pc pc_plus_len assembled →
      fetch_many code_memory pc_plus_len pc instructions.
  #program #sigma #policy
  @pair_elim #labels #costs #create_label_cost_map_refl
  letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory
  letin lookup_datalabels ≝ (λx.?) 
  letin pi ≝ (fst ???)
  letin pc ≝ (sigma ?)
  letin instructions ≝ (expand_pseudo_instruction ??????)
  @pair_elim #len #assembled #assembled_refl normalize nodelta
  #H
  generalize in match
   (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
  #X destruct normalize nodelta @X try % <assembled_refl try % assumption
qed.

definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
  λpseudo_instruction.
    match pseudo_instruction with
    [ Comment c ⇒ False
    | Cost c ⇒ False
    | _ ⇒ True
    ].

(* This is a non trivial consequence of fetch_assembly_pseudo +
   load_code_memory_ok because of the finite amount of memory. In
   particular the case when the compiled program exhausts the
   code memory is very tricky. It also requires monotonicity of
   sigma in the out-of-bounds region too. *)      
lemma assembly_ok:
  ∀program.
  ∀length_proof: |\snd program| ≤ 2^16.
  ∀sigma: Word → Word.
  ∀policy: Word → bool.
  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
  ∀assembled.
  ∀costs': BitVectorTrie costlabel 16.
  let 〈preamble, instr_list〉 ≝ program in
  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
  let datalabels ≝ construct_datalabels preamble in
  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
    〈assembled,costs'〉 = assembly program sigma policy →
      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
        let code_memory ≝ load_code_memory assembled in
        let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
          ∀ppc.∀ppc_ok.
            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in     
            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
            let pc ≝ sigma ppc in
            let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
              encoding_check code_memory pc pc_plus_len assembled ∧
                  sigma newppc = add … pc (bitvector_of_nat … len).
  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
  cases (assembly program sigma policy) * #assembled' #costs''
  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
  cut (|instr_list| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
  * * #assembly_ok1 #assembly_ok3 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
  lapply (assembly_ok2 ppc ?) try // -assembly_ok2
  >eq_fetch_pseudo_instruction
  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ? ∧ ∀j.∀H:j<|assembledi|.?) → ?)
  >eq_assembly_1_pseudoinstruction
  whd in ⊢ (% → ?); * #assembly_ok4 #assembly_ok
  %
  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
      >snd_fetch_pseudo_instruction
      cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
      #spw1 #_ >spw1 -spw1 @eq_f @eq_f
      >eq_fetch_pseudo_instruction whd in match instruction_size;
      normalize nodelta >create_label_cost_refl
      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
      [>eq_assembly_1_pseudoinstruction % | skip]
  | lapply (load_code_memory_ok assembled' ?) [ assumption ]
    #load_code_memory_ok
    lapply (fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) #EQlen
    (* Nice statement here *)
    cut (∀j. ∀H: j < |assembled|.
          nth_safe Byte j assembled H =
          \snd (next (load_code_memory assembled')
          (bitvector_of_nat 16
           (nat_of_bitvector …
            (add … (sigma ppc) (bitvector_of_nat … j))))))
    [1: #j #H cases (assembly_ok … H) #K -assembly_ok #assembly_ok <load_code_memory_ok
        [ @assembly_ok | skip ]
    |2:
      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
      elim assembled
      [1:
        #pc #_ whd <add_zero %
      | #hd #tl #IH #pc #H %
         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
           >H -H whd in ⊢ (??%?); <add_zero //
         | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
           [2: <add_bitvector_of_nat_Sm @add_associative ]
           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
           <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
           >add_associative % ]]]]
qed.

(* XXX: should we add that costs = costs'? *)
lemma fetch_assembly_pseudo2:
  ∀program.
  ∀length_proof: |\snd program| ≤ 2^16.
  ∀sigma.
  ∀policy.
  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
  ∀ppc.∀ppc_ok.
  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
  let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
  let code_memory ≝ load_code_memory assembled in
  let data_labels ≝ construct_datalabels (\fst program) in
  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
  * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok 
  @pair_elim #labels #costs #create_label_map_refl
  @pair_elim #assembled #costs' #assembled_refl
  letin code_memory ≝ (load_code_memory ?)
  letin data_labels ≝ (construct_datalabels ?)
  letin lookup_labels ≝ (λx. ?)
  letin lookup_datalabels ≝ (λx. ?)
  @pair_elim #pi #newppc #fetch_pseudo_refl
  lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
  normalize nodelta try assumption
  >create_label_map_refl in ⊢ (match % with [_ ⇒ ?] → ?); #H
  lapply (H (sym_eq … assembled_refl)) -H
  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
  #len #assembledi #EQ4 #H
  lapply (H ppc) >fetch_pseudo_refl #H
  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy)
  >create_label_map_refl #X lapply (X ppc ppc_ok (load_code_memory assembled)) -X
  >EQ4 #H1 cases (H ppc_ok)
  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
  >fetch_pseudo_refl in H1; #assm @assm assumption
qed.

inductive upper_lower: Type[0] ≝
  | upper: upper_lower
  | lower: upper_lower.

definition eq_upper_lower:
    upper_lower → upper_lower → bool ≝
  λleft: upper_lower.
  λright: upper_lower.
  match left with
  [ upper ⇒
    match right with
    [ upper ⇒ true
    | _     ⇒ false
    ]
  | lower ⇒
    match right with
    [ lower ⇒ true
    | _     ⇒ false
    ]
  ].

lemma eq_upper_lower_true_to_eq:
  ∀left: upper_lower.
  ∀right: upper_lower.
    eq_upper_lower left right = true → left = right.
  * * normalize try (#_ %)
  #absurd destruct(absurd)
qed.

lemma eq_upper_lower_false_to_neq:
  ∀left: upper_lower.
  ∀right: upper_lower.
    eq_upper_lower left right = false → left ≠ right.
  * * normalize try (#absurd destruct(absurd))
  @nmk #absurd destruct(absurd)
qed.

(* XXX: if upper then the byte in the entry is the least significant byte of the address and
        the byte in the status is the most significant, otherwise if lower then the
        other way around
*)
definition address_entry ≝ upper_lower × Byte.

definition eq_accumulator_address_map_entry:
    option address_entry → option address_entry → bool ≝
  λleft.
  λright.
    match left with
    [ None                   ⇒
      match right with
      [ None ⇒ true
      | _    ⇒ false
      ]
    | Some upper_lower_addr ⇒
      let 〈upper_lower, addr〉 ≝ upper_lower_addr in
      match right with
      [ Some upper_lower_addr' ⇒
        let 〈upper_lower', addr'〉 ≝ upper_lower_addr' in
          eq_upper_lower upper_lower upper_lower' ∧ eq_bv … addr addr'
      | _                          ⇒ false
      ]
    ].

lemma eq_accumulator_address_map_entry_true_to_eq:
  ∀left: option address_entry.
  ∀right: option address_entry.
    eq_accumulator_address_map_entry left right = true → left = right.
  #left #right cases left cases right
  [1:
    #_ %
  |2,3:
    * * #word normalize #absurd destruct(absurd)
  |4:
    * * #word * * #word'
    [2,3:
      #absurd normalize in absurd; destruct(absurd)
    ]
    normalize change with (eq_bv 8 ?? = true → ?)
    #relevant >(eq_bv_eq … relevant) %
  ]
qed.

lemma eq_bv_false_to_neq:
  ∀n: nat.
  ∀left, right: BitVector n.
    eq_bv n left right = false → left ≠ right.
  #n #left elim left
  [1:
    #right >(BitVector_O … right) normalize #absurd destruct(absurd)
  |2:
    #n' #hd #tl #inductive_hypothesis #right
    cases (BitVector_Sn … right) #hd' * #tl' #right_refl
    >right_refl normalize
    cases hd normalize nodelta
    cases hd' normalize nodelta
    [2,3:
      #_ @nmk #absurd destruct(absurd)
    ]
    change with (eq_bv ??? = false → ?)
    #relevant lapply (inductive_hypothesis … relevant)
    #tl_neq_assm @nmk #tl_eq_assm cases tl_neq_assm
    #tl_eq_assm' @tl_eq_assm' destruct(tl_eq_assm) %
  ]
qed.
    
lemma eq_accumulator_address_map_entry_false_to_neq:
  ∀left: option address_entry.
  ∀right: option address_entry.
    eq_accumulator_address_map_entry left right = false → left ≠ right.
  #left #right cases left cases right
  [1:
    normalize #absurd destruct(absurd)
  |2,3:
    * * #word normalize #_ % #absurd destruct(absurd)
  |4:
    * * #word * * #word' normalize
    [2,3:
      #_ % #absurd destruct(absurd)
    ]
    change with (eq_bv ??? = false → ?)
    #eq_bv_false_assm lapply (eq_bv_false_to_neq … eq_bv_false_assm)
    #word_neq_assm % @Some_Some_elim #address_eq_assm cases word_neq_assm
    #word_eq_assm @word_eq_assm destruct(address_eq_assm) %
  ]
qed.

(* XXX: changed this type.  Bool specifies whether byte is first or second
        component of an address, and the Word is the pseudoaddress that it
        corresponds to.  Second component is the same principle for the accumulator
        A.
*)
definition internal_pseudo_address_map ≝
  (* low, high, acc *)
  (BitVectorTrie address_entry 7) × (BitVectorTrie address_entry 7) × (option address_entry).

include alias "ASM/BitVectorTrie.ma".
  
include "common/AssocList.ma".

axiom bvt_map2:
  ∀A, B, C: Type[0].
  ∀n: nat.
  ∀bvt_1: BitVectorTrie A n.
  ∀bvt_2: BitVectorTrie B n.
  ∀f: ∀a: option A. ∀b: option B. option C.
    BitVectorTrie C n.

(*
axiom is_in_domain:
  ∀A: Type[0].
  ∀n: nat.
  ∀bvt: BitVectorTrie A n.
  ∀b: BitVector n.
    Prop.

axiom bvt_map2_function_extensionality:
  ∀A, B, C: Type[0].
  ∀n: nat.
  ∀bvt_1: BitVectorTrie A n.
  ∀bvt_2, bvt_2': BitVectorTrie B n.
  ∀f: ∀a: option A. ∀b: option B. option C.
    (∀addr.
      is_in_domain … bvt_1 addr ∨ is_in_domain … bvt_2 addr ∨ is_in_domain … bvt_2' addr →
        f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2) = f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2')) →
          bvt_map2 … bvt_1 bvt_2 f = bvt_map2 … bvt_1 bvt_2' f.
*)

axiom lookup_opt_bvt_map2:
 ∀A,B,C,n,map1,map2,f,addr.
lookup_opt … addr (bvt_map2 A B C n map1 map2 f) =
 f (lookup_opt … addr map1) (lookup_opt … addr map2).

definition lookup_from_internal_ram:
    ∀addr: Byte.
    ∀M: internal_pseudo_address_map.
      option address_entry ≝
  λaddr, M.
    let 〈low, high, accA〉 ≝ M in
    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
      if head' … bit_one then
        lookup_opt … seven_bits high
      else
        lookup_opt … seven_bits low.

definition map_value_using_opt_address_entry:
  (Word → Word) → Byte → option address_entry → Byte ≝
  λsigma: Word → Word.
  λvalue: Byte.
  λul_addr: option address_entry.
  match ul_addr with
  [ None ⇒ value
  | Some upper_lower_word ⇒
    let 〈upper_lower, word〉 ≝ upper_lower_word in
      if eq_upper_lower upper_lower upper then
        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (value@@word)) in
          high
      else
        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (word@@value)) in
          low
  ].

definition map_acc_a_using_internal_pseudo_address_map:
 ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝
   λM, sigma, v. map_value_using_opt_address_entry sigma v (\snd M).

definition map_internal_ram_address_using_pseudo_address_map:
  ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
  λM: internal_pseudo_address_map.
  λsigma: Word → Word.
  λaddress: Byte.
  λvalue: Byte.
   map_value_using_opt_address_entry sigma value
    (lookup_from_internal_ram … address M ).

definition map_opt_value_using_opt_address_entry:
 (Word → Word) → option Byte → option address_entry → option Byte ≝
 λsigma,v,ul_addr.
  let v ≝ match v with [ None ⇒ zero … | Some v ⇒ v ] in
  let v' ≝ map_value_using_opt_address_entry sigma v ul_addr in
    if eq_bv … v' (zero …) then
      None …
    else
      Some … v'.

definition internal_ram_of_pseudo_internal_ram:
    ∀sigma: Word → Word.
    ∀ram: BitVectorTrie Byte 7.
    ∀map: BitVectorTrie address_entry 7.
      BitVectorTrie Byte 7 ≝
  λsigma, ram, map.
      bvt_map2 ??? ? ram map (map_opt_value_using_opt_address_entry sigma).

definition internal_half_pseudo_address_map_equal_up_to_address:
 BitVectorTrie address_entry 7 → BitVectorTrie address_entry 7 → (Word → Word) →
  BitVector 7 → Byte → Byte → Prop
 ≝
 λM,M',sigma,addr,v,v'.
  v' = map_value_using_opt_address_entry sigma v (lookup_opt … addr M') ∧
   ∀addr'. addr' ≠ addr → lookup_opt … addr' M = lookup_opt … addr' M'.  

axiom insert_internal_ram_of_pseudo_internal_ram:
 ∀M,M',sigma,addr,v,v',ram.
  internal_half_pseudo_address_map_equal_up_to_address M M' sigma addr v v' →
  insert Byte … addr v' (internal_ram_of_pseudo_internal_ram sigma ram M)
  = internal_ram_of_pseudo_internal_ram sigma (insert ?? addr v ram) M'.

definition low_internal_ram_of_pseudo_low_internal_ram:
    ∀M: internal_pseudo_address_map.
    ∀sigma: Word → Word.
    ∀ram: BitVectorTrie Byte 7.
      BitVectorTrie Byte 7 ≝
  λM, sigma, ram.
    let 〈low, high, accA〉 ≝ M in
      internal_ram_of_pseudo_internal_ram sigma ram low.

definition high_internal_ram_of_pseudo_high_internal_ram:
    ∀M: internal_pseudo_address_map.
    ∀sigma: Word → Word.
    ∀ram: BitVectorTrie Byte 7.
      BitVectorTrie Byte 7 ≝
  λM, sigma, ram.
    let 〈low, high, accA〉 ≝ M in
      internal_ram_of_pseudo_internal_ram sigma ram high.

(*
axiom low_internal_ram_of_pseudo_internal_ram_hit:
 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7.
  lookup_opt ?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉  →
   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in 
   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
   let bl ≝ lookup ? 7 addr ram (zero 8) in
   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (sigma points_to) in
     if eq_upper_lower upper_lower upper then
       (pbl = higher) ∧ (bl = phigher)
     else
       (pbl = lower) ∧ (bl = plower).
*)

(* changed from add to sub *)
axiom low_internal_ram_of_pseudo_internal_ram_miss:
 ∀T.∀M:internal_pseudo_address_map.∀sigma. ∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in
    lookup_opt … addr (\fst (\fst M)) = None … →
      lookup … addr ram (zero …) = lookup … addr (low_internal_ram … s) (zero ?).

definition exists:
    ∀A: Type[0].
    ∀n: nat.
    ∀v: BitVector n.
    ∀bvt: BitVectorTrie A n.
      bool ≝
  λA, n, v, bvt.
    match lookup_opt … v bvt with
    [ None ⇒ false
    | _    ⇒ true
    ].

definition data_or_address ≝
  λT.
  λM: internal_pseudo_address_map.
  λcm.
  λs: PreStatus T cm.
  λaddr: addressing_mode.
  let 〈low, high, accA〉 ≝ M in
  match addr return λx. option (option address_entry) with
    [ DIRECT d ⇒
       let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
         match head' … hd with
         [ true ⇒
             if eq_bv … d (bitvector_of_nat … 224) then
               Some … accA
             else
               Some … (None …)
         | false ⇒ Some … (lookup_opt … seven_bits low)
         ]
    | INDIRECT i ⇒
        let d ≝ get_register … s [[false;false;i]] in
        let address ≝ bit_address_of_register … s [[false;false;i]] in
          if ¬exists … address low then
            let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
              if head' … 0 bit_one then
                Some … (lookup_opt … seven_bits high)
              else
                Some … (lookup_opt … seven_bits low)
          else
            None ?
    | EXT_INDIRECT e ⇒
        let address ≝ bit_address_of_register … s [[false;false;e]] in
          if ¬exists … address low then
            Some … (None …)
          else
            None ?
    | REGISTER r ⇒
        let address ≝ bit_address_of_register … s r in
          Some … (lookup_opt … address low)
    | ACC_A ⇒ Some … accA
    | ACC_B ⇒ Some … (None …)
    | DPTR ⇒ Some … (None …)
    | DATA _ ⇒ Some … (None …)
    | DATA16 _ ⇒ Some … (None …)
    | ACC_DPTR ⇒ Some … (None …)
    | ACC_PC ⇒ Some … (None …)
    | EXT_INDIRECT_DPTR ⇒ Some … (None …)
    | INDIRECT_DPTR ⇒ Some … (None …)
    | CARRY ⇒ Some … (None …)
    | BIT_ADDR b ⇒
      let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in
      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
        if head' bool 0 bit_one then
            if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *)
              Some … accA
            else
              Some … (None …)
        else
          let address' ≝ [[true; false; false]]@@four_bits in
            Some … (lookup_opt … address' low)
    | N_BIT_ADDR b ⇒
      let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in
      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
        if head' bool 0 bit_one then
            if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *)
              Some … accA
            else
              Some … (None …)
        else
          let address' ≝ [[true; false; false]]@@four_bits in
            Some … (lookup_opt … address' low)
    | RELATIVE _ ⇒ Some … (None …)
    | ADDR11 _ ⇒ Some … (None …)
    | ADDR16 _ ⇒ Some … (None …)
    ].

definition assert_data ≝
  λT.
  λM: internal_pseudo_address_map.
  λcm.
  λs: PreStatus T cm.
  λaddr: addressing_mode.
    match data_or_address T M cm s addr with
    [ None   ⇒ false
    | Some s ⇒
      match s with
      [ None ⇒ true
      | _    ⇒ false
      ]
    ].
    
definition insert_into_internal_ram:
  ∀addr: Byte.
  ∀v: address_entry.
  ∀M: internal_pseudo_address_map.
    internal_pseudo_address_map ≝
  λaddr, v, M.
    let 〈low, high, accA〉 ≝ M in
    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
      if head' … bit_one then
        〈low, insert … seven_bits v high, accA〉
      else
        〈insert … seven_bits v low, high, accA〉.
    
axiom delete:
  ∀A: Type[0].
  ∀n: nat.
  ∀b: BitVector n.
    BitVectorTrie A n → BitVectorTrie A n.

definition delete_from_internal_ram:
    ∀addr: Byte.
    ∀M: internal_pseudo_address_map.
      internal_pseudo_address_map ≝
  λaddr, M.
    let 〈low, high, accA〉 ≝ M in
    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
      if head' … bit_one then
        〈low,delete … seven_bits high, accA〉
      else
        〈delete … seven_bits low, high, accA〉.

definition overwrite_or_delete_from_internal_ram:
    ∀addr: Byte.
    ∀v: option address_entry.
    ∀M: internal_pseudo_address_map.
      internal_pseudo_address_map ≝
  λaddr, v, M.
    match v with
    [ None ⇒ delete_from_internal_ram addr M
    | Some v' ⇒ insert_into_internal_ram addr v' M
    ].
    
definition next_internal_pseudo_address_map0 ≝
  λT.
  λcm:T.
  λaddr_of: Identifier → PreStatus T cm → Word.
  λfetched.
  λM: internal_pseudo_address_map.
  λs: PreStatus T cm.
  let 〈low, high, accA〉 ≝ M in
   match fetched with
    [ Comment _ ⇒ Some ? M
    | Cost _ ⇒ Some … M
    | Jmp _ ⇒ Some … M
    | Call a ⇒
      let a' ≝ addr_of a s in
      let 〈upA, lowA〉 ≝ vsplit bool 8 8 a' in
        Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) 〈lower, upA〉
                (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) 〈upper, lowA〉 M))
    | Mov _ _ ⇒ Some … M
    | Instruction instr ⇒
      match instr return λx. option internal_pseudo_address_map with
       [ ADD addr1 addr2 ⇒
         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
           Some ? M
         else
           None ?
       | ADDC addr1 addr2 ⇒ 
         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
           Some ? M
         else
           None ?
       | SUBB addr1 addr2 ⇒
         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
           Some ? M
         else
           None ?
       | INC addr1 ⇒
         if assert_data T M ? s addr1 then
           Some ? M
         else
           None ?
       | DEC addr1 ⇒
         if assert_data T M … s addr1 then
           Some ? M
         else
           None ?
       | MUL addr1 addr2 ⇒
         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
           Some ? M
         else
           None ?
       | DIV addr1 addr2 ⇒
         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
           Some ? M
         else
           None ?
       | DA addr1 ⇒
         if assert_data T M … s addr1 then
           Some ? M
         else
           None ?
       | JC addr1 ⇒ Some ? M
       | JNC addr1 ⇒ Some ? M
       | JB addr1 addr2 ⇒ Some ? M
       | JNB addr1 addr2 ⇒ Some ? M
       | JBC addr1 addr2 ⇒ Some ? M
       | JZ addr1 ⇒ Some ? M
       | JNZ addr1 ⇒ Some ? M
       | CJNE addr1 addr2 ⇒
         match addr1 with
         [ inl l ⇒
           let 〈left, right〉 ≝ l in
             if assert_data T M … s left ∧ assert_data T M … s right then
               Some ? M
             else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then
               Some ? M
             else
               None ?
         | inr r ⇒
           let 〈left, right〉 ≝ r in
             if assert_data T M … s left ∧ assert_data T M … s right then
               Some ? M
             else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then
               Some ? M
             else
               None ?
         ]
       | DJNZ addr1 addr2 ⇒
         if assert_data T M … s addr1 then
           Some ? M
         else
           None ?
       | CLR addr1 ⇒
         if assert_data T M … s addr1 then
           Some ? M
         else
           None ?
       | CPL addr1 ⇒
         if assert_data T M … s addr1 then
           Some ? M
         else
           None ?
       | RL addr1 ⇒
         if assert_data T M … s addr1 then
           Some ? M
         else
           None ?
       | RLC addr1 ⇒
         if assert_data T M … s addr1 then
           Some ? M
         else
           None ?
       | RR addr1 ⇒
         if assert_data T M … s addr1 then
           Some ? M
         else
           None ?
       | RRC addr1 ⇒
         if assert_data T M … s addr1 then
           Some ? M
         else
           None ?
       | SWAP addr1 ⇒
         if assert_data T M … s addr1 then
           Some ? M
         else
           None ?
       | SETB addr1 ⇒
         if assert_data T M … s addr1 then
           Some ? M
         else
           None ?
       (* XXX: need to track addresses pushed and popped off the stack? *)
       | PUSH addr1 ⇒
         match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
         [ DIRECT d ⇒ λproof.
           let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
             if head' … bit_one then
               if eq_bv … seven_bits (bitvector_of_nat … 224) then
                 Some … (overwrite_or_delete_from_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) accA M)
               else
                 Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M)
             else
               Some … (overwrite_or_delete_from_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (lookup_from_internal_ram … d M) M)
         | _ ⇒ λother: False. ⊥
         ] (subaddressing_modein … addr1)
       | POP addr1 ⇒
         let sp ≝ get_8051_sfr ?? s SFR_SP in
         match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
         [ DIRECT d ⇒ λproof.
           let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
             if head' … bit_one then
               if eq_bv … d (bitvector_of_nat … 224) then
                 Some … 〈low, high, lookup_from_internal_ram … sp M〉
               else
                 match lookup_from_internal_ram sp M with
                 [ None ⇒ Some ? M
                 | _    ⇒ None ?
                 ]
             else
               Some … (overwrite_or_delete_from_internal_ram d (lookup_from_internal_ram … sp M) M)
         | _ ⇒ λother: False. ⊥
         ] (subaddressing_modein … addr1)
       | XCH addr1 addr2 ⇒
         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
           Some ? M
         else
           None ?
       | XCHD addr1 addr2 ⇒
         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
           Some ? M
         else
           None ?
      | RET ⇒
        let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in
        let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in
        match lookup_from_internal_ram sp_minus_1 M with
        [ None ⇒ None …
        | Some low_addr_high ⇒
            match lookup_from_internal_ram sp_minus_2 M with
            [ None ⇒ None …
            | Some high_addr_low ⇒
              let 〈low, addr_high〉 ≝ low_addr_high in
              let 〈high, addr_low〉 ≝ high_addr_low in
              let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in
              let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in
                if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then
                  Some ? M
                else
                  None ?
            ]
        ]
      | RETI ⇒
        let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in
        let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in
        match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M with
        [ None ⇒ None …
        | Some low_addr_high ⇒
            match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) M with
            [ None ⇒ None …
            | Some high_addr_low ⇒
              let 〈low, addr_high〉 ≝ low_addr_high in
              let 〈high, addr_low〉 ≝ high_addr_low in
              let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in
              let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in
                if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then
                  Some ? M
                else
                  None ?
            ]
        ]
      | NOP ⇒ Some … M
      | MOVX addr1 ⇒
        match addr1 with
        [ inl l ⇒
            Some ? 〈low, high, None …〉
        | inr r ⇒
          let 〈others, acc_a〉 ≝ r in
            if assert_data T M … s acc_a then
              Some ? M
            else
              None ?
        ]
      | XRL addr1 ⇒
        match addr1 with
        [ inl l ⇒
          let 〈acc_a, others〉 ≝ l in
          let acc_a_ok ≝ assert_data T M … s acc_a in
          let others_ok ≝ assert_data T M … s others in
          if acc_a_ok ∧ others_ok then
            Some ? M
          else
            None ?
        | inr r ⇒
          let 〈direct, others〉 ≝ r in
          let direct_ok ≝ assert_data T M … s direct in
          let others_ok ≝ assert_data T M … s others in
          if direct_ok ∧ others_ok then
            Some ? M
          else
            None ?
        ]
      | ORL addr1 ⇒
        match addr1 with
        [ inl l ⇒
          match l with
          [ inl l ⇒
            let 〈acc_a, others〉 ≝ l in
            let acc_a_ok ≝ assert_data T M … s acc_a in
            let others_ok ≝ assert_data T M … s others in
            if acc_a_ok ∧ others_ok then
              Some ? M
            else
              None ?
          | inr r ⇒
            let 〈direct, others〉 ≝ r in
            let direct_ok ≝ assert_data T M … s direct in
            let others_ok ≝ assert_data T M … s others in
            if direct_ok ∧ others_ok then
              Some ? M
            else
              None ?
          ]
        | inr r ⇒
          let 〈carry, others〉 ≝ r in
          let carry_ok ≝ assert_data T M … s carry in
          let others_ok ≝ assert_data T M … s others in
          if carry_ok ∧ others_ok then
            Some ? M
          else
            None ?
        ]
      | ANL addr1 ⇒
        match addr1 with
        [ inl l ⇒
          match l with
          [ inl l ⇒
            let 〈acc_a, others〉 ≝ l in
            let acc_a_ok ≝ assert_data T M … s acc_a in
            let others_ok ≝ assert_data T M … s others in
            if acc_a_ok ∧ others_ok then
              Some ? M
            else
              None ?
          | inr r ⇒
            let 〈direct, others〉 ≝ r in
            let direct_ok ≝ assert_data T M … s direct in
            let others_ok ≝ assert_data T M … s others in
            if direct_ok ∧ others_ok then
              Some ? M
            else
              None ?
          ]
        | inr r ⇒
          let 〈carry, others〉 ≝ r in
          let carry_ok ≝ assert_data T M … s carry in
          let others_ok ≝ assert_data T M … s others in
          if carry_ok ∧ others_ok then
            Some ? M
          else
            None ?
        ]
      | MOV addr1 ⇒
        (* XXX: wrong *)
        match addr1 with
        [ inl l ⇒
          match l with
          [ inl l' ⇒
            match l' with
            [ inl l'' ⇒
              match l'' with
              [ inl l''' ⇒
                match l''' with
                [ inl l'''' ⇒
                  let 〈acc_a, others〉 ≝ l'''' in
                    match data_or_address T M … s others with
                    [ None ⇒ None ?
                    | Some s ⇒
                        Some … 〈low, high, s〉
                    ]
                | inr r ⇒
                  let 〈others, others'〉 ≝ r in
                  let address ≝
                    match others return λx. bool_to_Prop (is_in … [[ registr; indirect ]] x) → ? with
                    [ REGISTER r ⇒ λproof. false:::bit_address_of_register … s r
                    | INDIRECT i ⇒ λproof. get_register … s [[false; false; i]]
                    | _ ⇒ λother: False. ⊥
                    ] (subaddressing_modein … others)
                  in
                    match data_or_address T M … s others' with
                    [ None ⇒ None ?
                    | Some s ⇒
                        Some … (overwrite_or_delete_from_internal_ram address s M)
                    ]
                ]
              | inr r ⇒
                let 〈direct', others〉 ≝ r in
                  match direct' return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
                  [ DIRECT d ⇒ λproof.
                    match data_or_address T M … s others with
                    [ None ⇒ None ?
                    | Some s' ⇒
                        let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
                          if head' … bit_one then
                            if eq_bv … d (bitvector_of_nat … 224) then
                              Some … 〈low, high, s'〉
                            else
                              match s' with
                              [ None ⇒ Some ? M
                              | Some s'' ⇒ None ?
                              ]
                          else
                            Some … (overwrite_or_delete_from_internal_ram d s' M)
                    ]
                  | _ ⇒ λother: False. ⊥
                  ] (subaddressing_modein … direct')
              ]
            | inr r ⇒ Some … M
            ]
          | inr r ⇒
            let 〈carry, bit_addr〉 ≝ r in
            if assert_data T M … s bit_addr then
              Some ? M
            else
              None ?
          ]
        | inr r ⇒
          let 〈bit_addr, carry〉 ≝ r in
          if assert_data T M … s bit_addr then
            Some ? M
          else
            None ?
        ]
      ]
    ].
    cases other
qed.

definition next_internal_pseudo_address_map ≝
 λM:internal_pseudo_address_map.
 λcm.
 λaddr_of.
 λs:PseudoStatus cm.
 λppc_ok.
    next_internal_pseudo_address_map0 ? cm addr_of
     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.

definition code_memory_of_pseudo_assembly_program:
    ∀pap:pseudo_assembly_program.
      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
  λpap.
  λsigma.
  λpolicy.
    let p ≝ pi1 … (assembly pap sigma policy) in
      load_code_memory (\fst p).

definition sfr_8051_of_pseudo_sfr_8051 ≝
  λM: internal_pseudo_address_map.
  λsfrs: Vector Byte 19.
  λsigma: Word → Word.
    match \snd M with
    [ None ⇒ sfrs
    | Some upper_lower_address ⇒
      let index ≝ sfr_8051_index SFR_ACC_A in
      let acc_a ≝ get_index_v … sfrs index ? in
      let 〈upper_lower, address〉 ≝ upper_lower_address in
        if eq_upper_lower upper_lower upper then
          let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (acc_a@@address)) in
            set_index Byte 19 sfrs index high ?
        else
          let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (address@@acc_a)) in
            set_index Byte 19 sfrs index low ?
    ].
  //
qed.

definition status_of_pseudo_status:
    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
      ∀sigma: Word → Word. ∀policy: Word → bool.
        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
  λM.
  λpap.
  λps.
  λsigma.
  λpolicy.
  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
  let pc ≝ sigma (program_counter … ps) in
  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … ps) in
  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M sigma (high_internal_ram … ps) in
     mk_PreStatus (BitVectorTrie Byte 16)
      cm
      lir
      hir
      (external_ram … ps)
      pc
      (sfr_8051_of_pseudo_sfr_8051 M (special_function_registers_8051 … ps) sigma)
      (special_function_registers_8052 … ps)
      (p1_latch … ps)
      (p3_latch … ps)
      (clock … ps).

(*
definition write_at_stack_pointer':
 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
  λM: Type[0].
  λs: PreStatus M.
  λv: Byte.
    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
    let bit_zero ≝ get_index_v… nu O ? in
    let bit_1 ≝ get_index_v… nu 1 ? in
    let bit_2 ≝ get_index_v… nu 2 ? in
    let bit_3 ≝ get_index_v… nu 3 ? in
      if bit_zero then
        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
                              v (low_internal_ram ? s) in
          set_low_internal_ram ? s memory
      else
        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
                              v (high_internal_ram ? s) in
          set_high_internal_ram ? s memory.
  [ cases l0 %
  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
qed.

definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
≝
  λticks_of.
  λs.
  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
  let ticks ≝ ticks_of (program_counter ? s) in
  let s ≝ set_clock ? s (clock ? s + ticks) in
  let s ≝ set_program_counter ? s pc in
    match instr with
    [ Instruction instr ⇒
       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
    | Comment cmt ⇒ s
    | Cost cst ⇒ s
    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
    | Call call ⇒
      let a ≝ address_of_word_labels s call in
      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
      let s ≝ write_at_stack_pointer' ? s pc_bl in
      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
      let s ≝ write_at_stack_pointer' ? s pc_bu in
        set_program_counter ? s a
    | Mov dptr ident ⇒
       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
    ].
 [
 |2,3,4: %
 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
 |
 | %
 ]
 cases not_implemented
qed.
*)

(*
lemma execute_code_memory_unchanged:
 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
 #ticks #ps whd in ⊢ (??? (??%))
 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
  (program_counter pseudo_assembly_program ps)) #instr #pc
 whd in ⊢ (??? (??%)) cases instr
  [ #pre cases pre
     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
       cases (vsplit ????) #z1 #z2 %
     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
       cases (vsplit ????) #z1 #z2 %
     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
       cases (vsplit ????) #z1 #z2 %
     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
       [ #x1 whd in ⊢ (??? (??%)) 
     | *: cases not_implemented
     ]
  | #comment %
  | #cost %
  | #label %
  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
    (* CSC: ??? *)
  | #dptr #label (* CSC: ??? *)
  ]
  cases not_implemented
qed.
*)

(* XXX: check values returned for conditional jumps below! They are wrong,
        find correct values *)
definition ticks_of0:
    ∀p:pseudo_assembly_program.
      (Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
  λprogram: pseudo_assembly_program.
  λlookup_labels: Identifier → Word.
  λsigma.
  λpolicy.
  λppc: Word.
  λfetched.
    match fetched with
    [ Instruction instr ⇒
      match instr with
      [ JC lbl ⇒
        let lookup_address ≝ sigma (lookup_labels lbl) in
        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
          if sj_possible then
            〈2, 2〉
          else
            〈4, 4〉
      | JNC lbl ⇒
        let lookup_address ≝ sigma (lookup_labels lbl) in
        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
          if sj_possible then
            〈2, 2〉
          else
            〈4, 4〉
      | JB bit lbl ⇒
        let lookup_address ≝ sigma (lookup_labels lbl) in
        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
          if sj_possible then
            〈2, 2〉
          else
            〈4, 4〉
      | JNB bit lbl ⇒
        let lookup_address ≝ sigma (lookup_labels lbl) in
        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
          if sj_possible then
            〈2, 2〉
          else
            〈4, 4〉
      | JBC bit lbl ⇒
        let lookup_address ≝ sigma (lookup_labels lbl) in
        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
          if sj_possible then
            〈2, 2〉
          else
            〈4, 4〉
      | JZ lbl ⇒
        let lookup_address ≝ sigma (lookup_labels lbl) in
        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
          if sj_possible then
            〈2, 2〉
          else
            〈4, 4〉
      | JNZ lbl ⇒
        let lookup_address ≝ sigma (lookup_labels lbl) in
        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
          if sj_possible then
            〈2, 2〉
          else
            〈4, 4〉
      | CJNE arg lbl ⇒
        let lookup_address ≝ sigma (lookup_labels lbl) in
        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
          if sj_possible then
            〈2, 2〉
          else
            〈4, 4〉
      | DJNZ arg lbl ⇒
        let lookup_address ≝ sigma (lookup_labels lbl) in
        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
          if sj_possible then
            〈2, 2〉
          else
            〈4, 4〉
      | ADD arg1 arg2 ⇒
        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
         〈ticks, ticks〉
      | ADDC arg1 arg2 ⇒ 
        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
         〈ticks, ticks〉
      | SUBB arg1 arg2 ⇒ 
        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
         〈ticks, ticks〉
      | INC arg ⇒ 
        let ticks ≝ ticks_of_instruction (INC ? arg) in
         〈ticks, ticks〉
      | DEC arg ⇒ 
        let ticks ≝ ticks_of_instruction (DEC ? arg) in
         〈ticks, ticks〉
      | MUL arg1 arg2 ⇒ 
        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
         〈ticks, ticks〉
      | DIV arg1 arg2 ⇒ 
        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
         〈ticks, ticks〉
      | DA arg ⇒ 
        let ticks ≝ ticks_of_instruction (DA ? arg) in
         〈ticks, ticks〉
      | ANL arg ⇒
        let ticks ≝ ticks_of_instruction (ANL ? arg) in
         〈ticks, ticks〉
      | ORL arg ⇒
        let ticks ≝ ticks_of_instruction (ORL ? arg) in
         〈ticks, ticks〉
      | XRL arg ⇒
        let ticks ≝ ticks_of_instruction (XRL ? arg) in
         〈ticks, ticks〉
      | CLR arg ⇒
        let ticks ≝ ticks_of_instruction (CLR ? arg) in
         〈ticks, ticks〉
      | CPL arg ⇒
        let ticks ≝ ticks_of_instruction (CPL ? arg) in
         〈ticks, ticks〉
      | RL arg ⇒
        let ticks ≝ ticks_of_instruction (RL ? arg) in
         〈ticks, ticks〉
      | RLC arg ⇒
        let ticks ≝ ticks_of_instruction (RLC ? arg) in
         〈ticks, ticks〉
      | RR arg ⇒
        let ticks ≝ ticks_of_instruction (RR ? arg) in
         〈ticks, ticks〉
      | RRC arg ⇒
        let ticks ≝ ticks_of_instruction (RRC ? arg) in
         〈ticks, ticks〉
      | SWAP arg ⇒
        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
         〈ticks, ticks〉
      | MOV arg ⇒
        let ticks ≝ ticks_of_instruction (MOV ? arg) in
         〈ticks, ticks〉
      | MOVX arg ⇒
        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
         〈ticks, ticks〉
      | SETB arg ⇒
        let ticks ≝ ticks_of_instruction (SETB ? arg) in
         〈ticks, ticks〉
      | PUSH arg ⇒
        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
         〈ticks, ticks〉
      | POP arg ⇒
        let ticks ≝ ticks_of_instruction (POP ? arg) in
         〈ticks, ticks〉
      | XCH arg1 arg2 ⇒
        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
         〈ticks, ticks〉
      | XCHD arg1 arg2 ⇒
        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
         〈ticks, ticks〉
      | RET ⇒
        let ticks ≝ ticks_of_instruction (RET ?) in
         〈ticks, ticks〉
      | RETI ⇒
        let ticks ≝ ticks_of_instruction (RETI ?) in
         〈ticks, ticks〉
      | NOP ⇒
        let ticks ≝ ticks_of_instruction (NOP ?) in
         〈ticks, ticks〉
      ]
    | Comment comment ⇒ 〈0, 0〉
    | Cost cost ⇒ 〈0, 0〉
    | Jmp jmp ⇒
      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
      let do_a_long ≝ policy ppc in
      let lookup_address ≝ sigma (lookup_labels jmp) in
      let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
        if sj_possible ∧ ¬ do_a_long then
          〈2, 2〉 (* XXX: SJMP *)
        else
        let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
          if mj_possible ∧ ¬ do_a_long then
            〈2, 2〉 (* XXX: AJMP *)
          else
            〈2, 2〉 (* XXX: LJMP *)
    | Call call ⇒
      (* XXX: collapse the branches as they are identical? *)
      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
      let lookup_address ≝ sigma (lookup_labels call) in
      let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
      let do_a_long ≝ policy ppc in
      if mj_possible ∧ ¬ do_a_long then
        〈2, 2〉 (* ACALL *)
      else
        〈2, 2〉 (* LCALL *)
    | Mov dptr tgt ⇒ 〈2, 2〉
    ].

definition ticks_of:
    ∀p:pseudo_assembly_program.
      (Identifier → Word) → (Word → Word) → (Word → bool) → ∀ppc:Word.
       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
  λprogram: pseudo_assembly_program.
  λlookup_labels.
  λsigma.
  λpolicy.
  λppc: Word. λppc_ok.
    let pseudo ≝ \snd program in
    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
     ticks_of0 program lookup_labels sigma policy ppc fetched.

(*
lemma blah:
  ∀m: internal_pseudo_address_map.
  ∀s: PseudoStatus.
  ∀arg: Byte.
  ∀b: bool.
    assert_data m s (DIRECT arg) = true →
      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
      get_arg_8 ? s b (DIRECT arg).
  [2, 3: normalize % ]
  #m #s #arg #b #hyp
  whd in ⊢ (??%%)
  @vsplit_elim''
  #nu' #nl' #arg_nu_nl_eq
  normalize nodelta
  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
  #get_index_v_eq
  normalize nodelta
  [2:
    normalize nodelta
    @vsplit_elim''
    #bit_one' #three_bits' #bit_one_three_bit_eq
    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
    normalize nodelta
    generalize in match (refl ? (sub_7_with_carry ? ? ?))
    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
    #Saddr #carr' #Saddr_carr_eq
    normalize nodelta
    #carr_hyp'
    @carr_hyp'
    [1:
    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
        generalize in match (refl ? (¬(member (BitVector 8) ? arg m))) 
        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
        #member_eq
        normalize nodelta
        [2: #destr destruct(destr)
        |1: -carr_hyp';
            >arg_nu_nl_eq
            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
            [1: >get_index_v_eq in ⊢ (??%? → ?)
            |2: @le_S @le_S @le_S @le_n
            ]
            cases (member (BitVector 8) ? (\fst ?) ?)
            [1: #destr normalize in destr; destruct(destr)
            |2:
            ]
        ]
    |3: >get_index_v_eq in ⊢ (??%?)
        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
        >(vsplit_vector_singleton … bit_one_three_bit_eq)
        <arg_nu_nl_eq
        whd in hyp:(??%?)
        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
        normalize nodelta [*: #ignore @sym_eq ]
    ]
  |
  ].
*)
(*
map_address0 ... (DIRECT arg) = Some .. →
  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
  get_arg_8 (internal_ram ...) (DIRECT arg)

((if assert_data M ps ACC_A∧assert_data M ps (DIRECT ARG2) 
                     then Some internal_pseudo_address_map M 
                     else None internal_pseudo_address_map )
                    =Some internal_pseudo_address_map M')

axiom low_internal_ram_write_at_stack_pointer:
 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
  bu@@bl = sigma (pbu@@pbl) →
   low_internal_ram T1 cm1
     (write_at_stack_pointer …
       (set_8051_sfr …
         (write_at_stack_pointer …
           (set_8051_sfr …
             (set_low_internal_ram … s1
               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
             SFR_SP sp1)
          bl)
        SFR_SP sp2)
      bu)
   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
      (low_internal_ram …
       (write_at_stack_pointer …
         (set_8051_sfr …
           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
          SFR_SP sp2)
        pbu)).

lemma high_internal_ram_write_at_stack_pointer:
 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
  bu@@bl = sigma (pbu@@pbl) →
   high_internal_ram T1 cm1
     (write_at_stack_pointer …
       (set_8051_sfr …
         (write_at_stack_pointer …
           (set_8051_sfr …
             (set_high_internal_ram … s1
               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
             SFR_SP sp1)
          bl)
        SFR_SP sp2)
      bu)
   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
      (high_internal_ram …
       (write_at_stack_pointer …
         (set_8051_sfr …
           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
          SFR_SP sp2)
        pbu)).
  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
  cases daemon (* XXX: !!! *)
qed.
*)

lemma snd_assembly_1_pseudoinstruction_ok:
  ∀program: pseudo_assembly_program.
  ∀program_length_proof: |\snd program| ≤ 2^16.
  ∀sigma: Word → Word.
  ∀policy: Word → bool.
  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
  ∀ppc: Word.
  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
  ∀pi.
  ∀lookup_labels.
  ∀lookup_datalabels.
    let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
    lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) →
    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
  #lookup_labels #lookup_datalabels
  @pair_elim #labels #costs #create_label_cost_map_refl
  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
  normalize nodelta
  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
  #fetch_pseudo_refl
  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
  @pair_elim #preamble #instr_list #program_refl
  lapply create_label_cost_map_refl; -create_label_cost_map_refl
  >program_refl in ⊢ (% → ?); #create_label_cost_map_refl
  >create_label_cost_map_refl
  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
  lapply (H ppc ppc_in_bounds) -H
  @pair_elim #pi' #newppc #fetch_pseudo_refl'
  @pair_elim #len #assembled #assembly1_refl #H
  cases H
  #encoding_check_assm #sigma_newppc_refl
  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
  >pi_refl' in assembly1_refl; #assembly1_refl
  >lookup_labels_refl >lookup_datalabels_refl
  >program_refl normalize nodelta
  >assembly1_refl
  <sigma_newppc_refl
  generalize in match fetch_pseudo_refl';
  whd in match (fetch_pseudo_instruction ???);
  @pair_elim #lbl #instr #nth_refl normalize nodelta
  #G cases (pair_destruct_right ?????? G) %
qed.

(* To be moved in ProofStatus *)
lemma program_counter_set_program_counter:
  ∀T.
  ∀cm.
  ∀s.
  ∀x.
    program_counter T cm (set_program_counter T cm s x) = x.
  //
qed.