Changeset 2129 for src/ASM

Timestamp:

Jun 27, 2012, 7:14:32 PM (7 years ago)

Author:

mulligan

Message:

Large changes from today trying to complete the main theorem. Again :(

Location:

src/ASM

Files:

• AssemblyProof.ma (modified) (4 diffs)
• AssemblyProofSplit.ma (modified) (2 diffs)
• AssemblyProofSplitSplit.ma (modified) (2 diffs)
• Interpret.ma (modified) (3 diffs)

src/ASM/AssemblyProof.ma

@@ -64 +64 @@
           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: *]]]]]
@@ -83 +85 @@
  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
+ try <H2 whd >eq_instruction_refl >H4 @eq_bv_refl *)
 qed.
 
@@ -936 +938 @@
   ∀i: instruction.
     |(assembly1 i)| < 128.
+  cases daemon
+(* XXX: commented out as takes ages to type check 
   #i cases i
   try (#assm1 #assm2) try #assm1
@@ -1004 +1008 @@
     @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n
   ]
-qed.
+  *)
+qed.

src/ASM/AssemblyProofSplit.ma

@@ -400 +400 @@
                       status_of_pseudo_status M' cm s sigma policy).
     P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
+  cases daemon (* XXX: commented out as it takes 45 minutes to typecheck *)
+  (*
   #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels
   #costs #create_label_cost_refl #newppc
@@ -1371 +1373 @@
   (* XXX: finally, prove the equality using sigma commutation *)
   cases daemon
-  ]
-qed.
+  ] *)
+qed.

src/ASM/AssemblyProofSplitSplit.ma

@@ -38 +38 @@
   >(eq_bv_eq … relevant) %
 qed.
-        
+  
 theorem main_thm:
   ∀M, M': internal_pseudo_address_map.
   ∀program: pseudo_assembly_program.
+  ∀program_in_bounds: |\snd program| ≤ 2^16.
+  ∀addr_of: Identifier → PreStatus pseudo_assembly_program program → BitVector 16.
   ∀is_well_labelled: is_well_labelled_p (\snd program).
   ∀sigma: Word → Word.
@@ -48 +50 @@
   ∀ps: PseudoStatus program.
   ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) < |\snd program|.
-    next_internal_pseudo_address_map M program ps program_counter_in_bounds = Some … M' →
+    next_internal_pseudo_address_map M program addr_of ps program_counter_in_bounds = Some … M' →
       ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
         status_of_pseudo_status M' … 
           (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy.
-  #M #M' * #preamble #instr_list #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps
-  letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds
-  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
-  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?;
-  @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
-  @pair_elim #assembled #costs' #assembly_refl normalize nodelta
-  lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
-  @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
-  @(pose … (λx. address_of_word_labels_code_mem instr_list x)) #lookup_labels #EQlookup_labels
-  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
-  whd in match execute_1_pseudo_instruction; normalize nodelta
-  whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta
-  lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc
-  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?)
-  [1: >fetch_pseudo_refl % |2: skip ]
-  #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
-  generalize in match assm1; -assm1 -assm2 -assm3
-  normalize nodelta
-  inversion pi
-  [2,3:
-    #arg #_
-    (* XXX: we first work on sigma_increment_commutation *)
-    #sigma_increment_commutation
-    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
-    (* XXX: we work on the maps *)
-    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
-    (* XXX: we assume the fetch_many hypothesis *)
-    #fetch_many_assm
-    (* XXX: we give the existential *)
-    %{0}
-    whd in match (execute_1_pseudo_instruction0 ?????);
-    (* XXX: work on the left hand side of the equality *)
-    whd in ⊢ (??%?);
-    @split_eq_status try %
-    /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *)
-  |6: (* Mov *)
-    #arg1 #arg2 #_
-    (* XXX: we first work on sigma_increment_commutation *)
-    #sigma_increment_commutation
-    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
-    (* XXX: we work on the maps *)
-    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
-    (* XXX: we assume the fetch_many hypothesis *)
-    #fetch_many_assm
-    (* XXX: we give the existential *)
-    %{1}
-    whd in match (execute_1_pseudo_instruction0 ?????);
-    (* XXX: work on the left hand side of the equality *)
-    whd in ⊢ (??%?); whd in match (program_counter ???);
-    (* XXX: execute fetches some more *)
-    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
-    whd in fetch_many_assm;
-    >EQassembled in fetch_many_assm;
-    cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
-    #eq_instr
-    #fetch_many_assm whd in fetch_many_assm;
-    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
-    destruct whd in ⊢ (??%?);
-    (* XXX: now we start to work on the mk_PreStatus equality *)
-    (* XXX: lhs *)
-    change with (set_arg_16 ????? = ?)
-    >set_program_counter_mk_Status_commutation
-    >set_clock_mk_Status_commutation
-    >set_arg_16_mk_Status_commutation
-    (* XXX: rhs *)
-    change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
-    >set_program_counter_mk_Status_commutation
-    >set_clock_mk_Status_commutation
-    >set_arg_16_mk_Status_commutation in ⊢ (???%);
-    (* here we are *)
-    @split_eq_status try %
-    [1:
-      assumption
-    |2:
-      @special_function_registers_8051_set_arg_16 %
-    ]
-  |1: (* Instruction *)
-    #instr #_ #EQP #EQnext #fetch_many_assm
-    @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness
-      ps ppc ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
-      EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
-      (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
-      (refl …) ? (refl …))
-    try assumption try % >assembly_refl assumption
-  |4: (* Jmp *)
-    #arg1 #pi_refl
-    (* XXX: we first work on sigma_increment_commutation *)
-    whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
-    whd in match (expand_pseudo_instruction ??????);
-    inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
-    inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
-    [2:
-      inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
-      inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
-    ]
-    #sigma_increment_commutation
-    normalize in sigma_increment_commutation:(???(???(??%)));
-    (* XXX: we work on the maps *)
-    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
-    (* XXX: we assume the fetch_many hypothesis *)
-    * #fetch_refl #fetch_many_assm
-    (* XXX: we give the existential *)
-    %{1}
-    (* XXX: work on the left hand side of the equality *)
-    whd in ⊢ (??%?); whd in match (program_counter ???);
-    (* XXX: execute fetches some more *)
-    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
-    whd in fetch_many_assm;
-    >EQassembled in fetch_refl; #fetch_refl <fetch_refl
-    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
-    whd in ⊢ (??%%);
-    (* XXX: now we start to work on the mk_PreStatus equality *)
-    (* XXX: lhs *)
-    (* XXX: rhs *)
-    (* here we are *)
-    @split_eq_status try % /demod nohyps/
-    [1,3,4:
-      change with (add ???) in match (\snd (half_add ???));
-      whd in match execute_1_pseudo_instruction0; normalize nodelta
-      /demod nohyps/ >set_clock_set_program_counter
-      >program_counter_set_program_counter
-      whd in ⊢ (??%?); normalize nodelta whd in match address_of_word_labels; normalize nodelta
-      lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl
-      normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm
+    #M #M' * #preamble #instr_list #program_in_bounds #addr_of
+    #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps
+    letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds
+    change with (next_internal_pseudo_address_map0 ?????? = ? → ?)
+    generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 program_in_bounds sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?;
+    @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
+    @pair_elim #assembled #costs' #assembly_refl normalize nodelta
+    lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
+    @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
+    @(pose … (λx. address_of_word_labels_code_mem instr_list x)) #lookup_labels #EQlookup_labels
+    @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
+    whd in match execute_1_pseudo_instruction; normalize nodelta
+    whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta
+    lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc
+    lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?)
+    [1: >fetch_pseudo_refl % |2: skip |3: assumption ]
+    #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
+    generalize in match assm1; -assm1 -assm2 -assm3
+    normalize nodelta
+    inversion pi
+    [(*2,3:
+      #arg #_
+      (* XXX: we first work on sigma_increment_commutation *)
+      #sigma_increment_commutation
+      normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
+      (* XXX: we work on the maps *)
+      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
+      (* XXX: we assume the fetch_many hypothesis *)
+      #fetch_many_assm
+      (* XXX: we give the existential *)
+      %{0}
+      whd in match (execute_1_pseudo_instruction0 ?????);
+      (* XXX: work on the left hand side of the equality *)
+      whd in ⊢ (??%?);
+      @split_eq_status try %
+      /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *)
+    |6: (* Mov *)
+      #arg1 #arg2 #_
+      (* XXX: we first work on sigma_increment_commutation *)
+      #sigma_increment_commutation
+      normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
+      (* XXX: we work on the maps *)
+      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
+      (* XXX: we assume the fetch_many hypothesis *)
+      #fetch_many_assm
+      (* XXX: we give the existential *)
+      %{1}
+      whd in match (execute_1_pseudo_instruction0 ?????);
+      (* XXX: work on the left hand side of the equality *)
+      whd in ⊢ (??%?); whd in match (program_counter ???);
+      (* XXX: execute fetches some more *)
+      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
+      whd in fetch_many_assm;
+      >EQassembled in fetch_many_assm;
+      cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
+      #eq_instr
+      #fetch_many_assm whd in fetch_many_assm;
+      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
+      destruct whd in ⊢ (??%?);
+      (* XXX: now we start to work on the mk_PreStatus equality *)
+      (* XXX: lhs *)
+      change with (set_arg_16 ????? = ?)
+      >set_program_counter_mk_Status_commutation
+      >set_clock_mk_Status_commutation
+      >set_arg_16_mk_Status_commutation
+      (* XXX: rhs *)
+      change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
+      >set_program_counter_mk_Status_commutation
+      >set_clock_mk_Status_commutation
+      >set_arg_16_mk_Status_commutation in ⊢ (???%);
+      (* here we are *)
+      @split_eq_status try %
       [1:
-        >EQnewpc
-        inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
-        @sym_eq >address_of_word_labels_assm
+        assumption
+      |2:
+        @special_function_registers_8051_set_arg_16 %
+      ]
+    |1: (* Instruction *)
+      #instr #_ #EQP #EQnext #fetch_many_assm
+      @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness
+        ps ppc ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
+        EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
+        (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
+        (refl …) ? (refl …))
+      try assumption try % >assembly_refl assumption
+    |4: (* Jmp *)
+      #arg1 #pi_refl
+      (* XXX: we first work on sigma_increment_commutation *)
+      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
+      whd in match (expand_pseudo_instruction ??????);
+      inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
+      inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
+      [2:
+        inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
+        inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
+      ]
+      #sigma_increment_commutation
+      normalize in sigma_increment_commutation:(???(???(??%)));
+      (* XXX: we work on the maps *)
+      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
+      (* XXX: we assume the fetch_many hypothesis *)
+      * #fetch_refl #fetch_many_assm
+      (* XXX: we give the existential *)
+      %{1}
+      (* XXX: work on the left hand side of the equality *)
+      whd in ⊢ (??%?); whd in match (program_counter ???);
+      (* XXX: execute fetches some more *)
+      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
+      whd in fetch_many_assm;
+      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
+      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
+      whd in ⊢ (??%%);
+      (* XXX: now we start to work on the mk_PreStatus equality *)
+      (* XXX: lhs *)
+      (* XXX: rhs *)
+      (* here we are *)
+      @split_eq_status try % /demod nohyps/
+      [1,3,4:
+        change with (add ???) in match (\snd (half_add ???));
+        whd in match execute_1_pseudo_instruction0; normalize nodelta
+        /demod nohyps/ >set_clock_set_program_counter
+        >program_counter_set_program_counter
+        whd in ⊢ (??%?); normalize nodelta whd in match address_of_word_labels; normalize nodelta
+        lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl
+        normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm
         [1:
-          >EQlookup_labels in mjc_refl; #mjc_refl
-          @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
-          >(andb_true_l … mj_possible_refl) @I
+          >EQnewpc
+          inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
+          @sym_eq >address_of_word_labels_assm
+          [1:
+            >EQlookup_labels in mjc_refl; #mjc_refl
+            @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
+            >(andb_true_l … mj_possible_refl) @I
+          ]
+        |3:
+          >EQlookup_labels normalize nodelta
+          >address_of_word_labels_assm try %
+        |5:
+          >EQnewpc
+          inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
+          @sym_eq >address_of_word_labels_assm
+          [1:
+            >EQlookup_labels in sjc_refl; #sjc_refl
+            >(pair_destruct_2 ????? (sym_eq … half_add_refl))
+            @(short_jump_cond_ok ???? (sym_eq … sjc_refl))
+            >(andb_true_l … sj_possible_refl) @I
+          ]
         ]
-      |3:
-        >EQlookup_labels normalize nodelta
-        >address_of_word_labels_assm try %
-      |5:
-        >EQnewpc
-        inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
-        @sym_eq >address_of_word_labels_assm
-        [1:
-          >EQlookup_labels in sjc_refl; #sjc_refl
-          >(pair_destruct_2 ????? (sym_eq … half_add_refl))
-          @(short_jump_cond_ok ???? (sym_eq … sjc_refl))
-          >(andb_true_l … sj_possible_refl) @I
+        @(is_well_labelled_witness … fetch_pseudo_refl)
+        >pi_refl %
+      |2:
+        whd in ⊢ (??(?%%)%);
+        cases (bitvector_11_cases address)
+        * * * * * * #b4 * #b5
+        * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl
+        normalize in match (fetch ??); <plus_n_Sm @eq_f
+        @commutative_plus
+      ]
+    |*)5: (* Call *)
+      #arg1 #pi_refl
+      (* XXX: we first work on sigma_increment_commutation *)
+      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
+      whd in match (expand_pseudo_instruction ??????);
+      whd in match (execute_1_pseudo_instruction0 ?????);
+      inversion (absolute_jump_cond ??) #aj_possible #offset #ajc_refl normalize nodelta
+      inversion (aj_possible ∧ ¬ policy ?) #aj_possible_refl normalize nodelta
+      @pair_elim #carry #new_sp #carry_new_sp_refl lapply (refl_to_jmrefl ??? carry_new_sp_refl) -carry_new_sp_refl #carry_new_sp_refl
+      @pair_elim #pc_bu #pc_bl #pc_bu_bl_refl lapply (refl_to_jmrefl ??? pc_bu_bl_refl) -pc_bu_bl_refl #pc_bu_bl_refl
+      @pair_elim #carry' #new_sp' #carry_new_sp_refl' lapply (refl_to_jmrefl ??? carry_new_sp_refl') -carry_new_sp_refl' #carry_new_sp_refl'
+      #sigma_increment_commutation
+      normalize in sigma_increment_commutation:(???(???(??%)));
+      (* XXX: we work on the maps *)
+      whd in ⊢ (??%? → ?);
+      @pair_elim #callM #accM #Mrefl
+      @Some_Some_elim #map_refl_assm <map_refl_assm
+      (* XXX: we assume the fetch_many hypothesis *)
+      * #fetch_refl #fetch_many_assm
+      (* XXX: we give the existential *)
+      %{1}
+      (* XXX: work on the left hand side of the equality *)
+      whd in ⊢ (??%?); whd in match (program_counter ???);
+      (* XXX: execute fetches some more *)
+      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
+      whd in fetch_many_assm;
+      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
+      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
+      whd in ⊢ (??(???%)?); normalize in match (length ? (assembly1 …));
+      normalize in match (length ? (assembly1 …)) in EQnewpc;
+      normalize nodelta
+      [1:
+        @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
+        try /demod nohyps/ [1: %]
+        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
+        @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
+        try /demod nohyps/ [1: %]
+        @pair_elim #thr #eig #thr_eig_refl
+        @pair_elim #fiv #thr' #fiv_thr_refl' whd in ⊢ (??%%);
+        @split_eq_status try /demod nohyps/ try %
+        [1,2:
+          (* XXX: need the commented out axioms from AssemblyProof.ma *)
+          cases daemon
+        |3:
+          >program_counter_set_program_counter
+          whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
+          >EQlookup_labels normalize nodelta
+          @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl normalize nodelta
+          <EQnewpc @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
+          #relevant >fst_5_rest_refl
+          check absolute_jump_cond
+          <(vsplit_ok ?????? (sym_eq … thr_eig_refl))
+          lapply pc_bu_bl_refl' -pc_bu_bl_refl'
+          >program_counter_set_8051_sfr >set_clock_set_program_counter
+          >program_counter_set_program_counter >fst_5_rest_pc_refl
+          cut(fst_5_addr = fst_5_pc)
+          [1:
+            cases daemon (* XXX: !! *)
+          |2:
+            #relevant2 >relevant2
+            <(vsplit_ok ?????? (sym_eq … fiv_thr_refl'))
+            #relevant3
+            lapply(vsplit_ok ?????? (sym_eq … relevant3))
+            >(vector_associative_append bool 5 3 8) #relevant4
+            cut(fiv = fst_5_pc ∧ thr'@@pc_bl' = rest_pc)
+            [1:
+              cases daemon (* XXX: !! *)
+            |2:
+              * #relevant5 #relevant6 >relevant5
+              >(vector_associative_append bool 5 3 8) @eq_f
+              destruct(relevant)
+              <(vsplit_ok ?????? (sym_eq … thr_eig_refl)) @eq_f
+            ]
+          ]
+        |4:
+          >set_program_counter_mk_Status_commutation in ⊢ (???%);
+          >special_function_registers_8051_write_at_stack_pointer in ⊢ (???%);
+          (* XXX: require set_8051_sfr_write_at_stack_pointer and
+                          special_function_registers_8051_set_8051_sfr
+          *)
+          cases daemon
+        |5,6,7:
+          >set_program_counter_mk_Status_commutation in ⊢ (???%);
+          (* XXX: similar to above but for 8052
+          *)
+          cases daemon
+        |8:
+          whd in match (ticks_of_instruction ?);
+          cut(\snd  (fetch (load_code_memory (assembly1 (ACALL (ADDR11 offset)))) (zero 16)) = 2)
+          [1: //
+          |2:
+            normalize in match (assembly1 ?); >thr_eig_refl
+            @(bitvector_3_elim_prop … thr) %
+          |3:
+            #fetch_2_refl >fetch_2_refl >commutative_plus %
+          ]
+        |2:
         ]
-      ]
-      @(is_well_labelled_witness … fetch_pseudo_refl)
-      >pi_refl %
-    |2:
-      whd in ⊢ (??(?%%)%);
-      cases (bitvector_11_cases address)
-      * * * * * * #b4 * #b5
-      * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl
-      normalize in match (fetch ??); <plus_n_Sm @eq_f
-      @commutative_plus
-    ]
-  |5: (* Call *)
-    #arg1 #_
-    (* XXX: we first work on sigma_increment_commutation *)
-    #sigma_increment_commutation
-    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
-    (* XXX: we work on the maps *)
-    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
-    (* XXX: we assume the fetch_many hypothesis *)
-    #fetch_many_assm
-    (* XXX: we give the existential *)
-    %{1}
-    whd in match (execute_1_pseudo_instruction0 ?????);
-    (* XXX: work on the left hand side of the equality *)
-    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
-    (* XXX: execute fetches some more *)
-    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
-    whd in fetch_many_assm;
-    >EQassembled in fetch_many_assm;
-    cases (fetch ??) * #instr #newpc #?ticks normalize nodelta *
-    #eq_instr
-    #fetch_many_assm whd in fetch_many_assm;
-    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
-    destruct whd in ⊢ (??%?);
-    (* XXX: now we start to work on the mk_PreStatus equality *)
-    (* XXX: lhs *)
-    change with (set_arg_16 ????? = ?)
-    >set_program_counter_mk_Status_commutation
-    >set_clock_mk_Status_commutation
-    >set_arg_16_mk_Status_commutation
-    (* XXX: rhs *)
-    change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
-    >set_program_counter_mk_Status_commutation
-    >set_clock_mk_Status_commutation
-    >set_arg_16_mk_Status_commutation in ⊢ (???%);
-    (* here we are *)
-    @split_eq_status //
-    [1:
-      assumption
-    |2:
-      @special_function_registers_8051_set_arg_16
-      [2: %
-      |1: //
       ]
     ]

src/ASM/Interpret.ma

@@ -1072 +1072 @@
           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
             [ ADDR11 a ⇒ λaddr11: True.
+              «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
+              let 〈fiv, thr'〉 ≝ vsplit ? 5 3 pc_bu in
+              let new_addr ≝ fiv @@ a in
+                set_program_counter … s new_addr, ?»
+            | _ ⇒ λother: False. ⊥
+            ] (subaddressing_modein … addr)
+      | RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … (addr_of_relative … cm) instr' s
+      | LCALL addr ⇒ λinstr_refl.
+          let s ≝ set_clock ?? s (ticks + clock … s) in
+          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with
+            [ ADDR16 a ⇒ λaddr16: True.
+              «
               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
@@ -1079 +1097 @@
               let s ≝ set_8051_sfr … s SFR_SP new_sp in
               let s ≝ write_at_stack_pointer … s pc_bu in
-              let 〈thr, eig〉 ≝ vsplit ? 3 8 a in
-              let 〈fiv, thr'〉 ≝ vsplit ? 5 3 pc_bu in
-              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
-                set_program_counter … s new_addr
-            | _ ⇒ λother: False. ⊥
-            ] (subaddressing_modein … addr)
-      | RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … (addr_of_relative … cm) instr' s
-      | LCALL addr ⇒ λinstr_refl.
-          let s ≝ set_clock ?? s (ticks + clock … s) in
-          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with
-            [ ADDR16 a ⇒ λaddr16: True.
-              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
+                set_program_counter … s a, ?»
             | _ ⇒ λother: False. ⊥
             ] (subaddressing_modein … addr)
@@ -1106 +1106 @@
     try //
     -s destruct(INSTR_PC) <instr_refl whd
-    try (#absurd normalize in absurd; try destruct(absurd) try %) %
+    try (#absurd normalize in absurd; try destruct(absurd) try %)
+    @pair_elim #carry #new_sp #carry_new_sp_refl
+    @pair_elim #pc_bu #pc_bl #pc_bu_bl_refl
+    @pair_elim #carry' #new_sp' #carry_new_sp_refl'
+    [2:
+      /demod nohyps/ %
+    |1:
+      cases (vsplit ????) #thr #eig normalize nodelta
+      cases (vsplit ????) #fiv #thr' normalize nodelta
+      /demod by clock_set_program_counter/ /demod nohyps/ %
+    ]
   |9:
     cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??