Changeset 2062 for src

Timestamp:

Jun 13, 2012, 5:00:35 PM (9 years ago)

Author:

sacerdot

Message:

Everything repaired (broken because of new proof obligation for fetch).

Location:

src/ASM

Files:

• AssemblyProofSplitSplit.ma (modified) (8 diffs)
• Interpret.ma (modified) (1 diff)

src/ASM/AssemblyProofSplitSplit.ma

@@ -27 +27 @@
   λinstr_list.
   ∀id: Identifier.
-  ∀ppc.
+  ∀ppc. ∀ppc_ok.
   ∀i.
-    fetch_pseudo_instruction instr_list ppc = i →
+    fetch_pseudo_instruction instr_list ppc ppc_ok = i →
       instruction_has_label id (\fst i) →
         occurs_exactly_once ASMTag pseudo_instruction id instr_list.
@@ -105 +105 @@
   ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
   ∀ps: PseudoStatus program.
-  ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) ≤ |\snd program|.
-    next_internal_pseudo_address_map M program ps = Some … M' →
+  ∀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' →
       ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
         status_of_pseudo_status M' … 
-          (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy.
-  #M #M' * #preamble #instr_list #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps #program_counter_in_bounds
+          (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 ????? = ? → ?)
-  @(pose … (program_counter ?? ps)) #ppc #EQppc
-  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?;
+  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
@@ -121 +121 @@
   @(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 <EQppc >fetch_pseudo_refl normalize nodelta
-  lapply (snd_fetch_pseudo_instruction instr_list ppc) >fetch_pseudo_refl #EQnewppc >EQnewppc
+  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: >EQppc assumption ]
+  [1: >fetch_pseudo_refl % |2: skip ]
   #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
   generalize in match assm1; -assm1 -assm2 -assm3
@@ -144 +144 @@
     whd in ⊢ (??%?);
     @split_eq_status try %
-    /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *)
+    /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *)
   |6: (* Mov *)
     #arg1 #arg2 #_
@@ -158 +158 @@
     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
+    whd in ⊢ (??%?); whd in match (program_counter ???);
     (* XXX: execute fetches some more *)
     whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
@@ -189 +189 @@
     #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 EQppc labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
+      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 >assembly_refl <EQppc assumption
-  |4:
+    try assumption try % >assembly_refl assumption
+  |4: (* Jmp *)
     #arg1 #pi_refl
     (* XXX: we first work on sigma_increment_commutation *)
@@ -214 +214 @@
     %{1}
     (* XXX: work on the left hand side of the equality *)
-    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
+    whd in ⊢ (??%?); whd in match (program_counter ???);
     (* XXX: execute fetches some more *)
     whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
@@ -272 +272 @@
     ]
   |5: (* Call *)
-    #arg1
+    #arg1 #_
     (* XXX: we first work on sigma_increment_commutation *)
     #sigma_increment_commutation

src/ASM/Interpret.ma

@@ -1222 +1222 @@
 
 definition execute_1_pseudo_instruction:
- (Word → nat × nat) → ∀cm. ∀s:PseudoStatus cm.
+ ∀cm. (∀ppc:Word. nat_of_bitvector … ppc < |\snd cm| → nat × nat) → ∀s:PseudoStatus cm.
    nat_of_bitvector 16 (program_counter pseudo_assembly_program cm s) <|\snd  cm| →
     PseudoStatus cm
 ≝
-  λticks_of,cm,s,pc_ok.
+  λcm,ticks_of,s,pc_ok.
   let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) pc_ok in
-  let ticks ≝ ticks_of (program_counter … s) in
+  let ticks ≝ ticks_of (program_counter … s) pc_ok in
    execute_1_pseudo_instruction0 ticks cm s instr pc.