Changeset 916 for src

Timestamp:

Jun 9, 2011, 11:56:49 AM (10 years ago)

Author:

sacerdot

Message:

Fix for jump_expansion_policy.

File:

• src/ASM/AssemblyProof.ma (modified) (3 diffs)

src/ASM/AssemblyProof.ma

@@ -891 +891 @@
  ∀program,ppc,lookup_labels,lookup_datalabels.
   ∀pi,code_memory,len,assembled,instructions,pc.
-   let expansion ≝ jump_expansion_policy program ppc in
+   let expansion ≝ jump_expansion ppc program in
    Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →
     Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →
@@ -1380 +1380 @@
     let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
     let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
-    let expansion ≝ jump_expansion_policy program ppc in
+    let expansion ≝ jump_expansion ppc program in
     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →
@@ -1597 +1597 @@
  whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ λ_.match % with [ _ ⇒ ? | _ ⇒ ? ]])
  >execute_1_pseudo_instruction_preserves_code_memory
+ generalize in match (fetch_assembly_pseudo2 (code_memory … ps))
+ cases (build_maps (code_memory pseudo_assembly_program ps))
  cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
  change with (execute_1 (set_program_counter ? (set_code_memory ?? ps (load_code_memory (\fst 〈cm,costs〉))) ?) = ?)
  change with (? = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_of ps) (load_code_memory (\fst 〈cm,costs〉))) ?)
+ whd in ⊢ (??%?)