Changeset 979 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 16, 2011, 2:26:47 PM (9 years ago)

Author:

sacerdot

Message:

...

File:

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

src/ASM/AssemblyProof.ma

@@ -1130 +1130 @@
 qed.
 
+example sigma_0: ∀p. sigma p (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
+ cases daemon.
+qed.
+
+axiom construct_costs_sigma:
+ ∀p,ppc,pc,pc',costs,costs',i.
+  bitvector_of_nat ? pc = sigma p (bitvector_of_nat ? ppc) →
+   Some … 〈pc',costs'〉 = construct_costs p ppc pc (λx.zero 16) (λx.zero 16) costs i →
+    bitvector_of_nat ? pc' = sigma p (bitvector_of_nat 16 (S ppc)).
+
 definition build_maps' ≝
   λpseudo_program.
@@ -1139 +1149 @@
       let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
       let 〈pc',costs〉 ≝ pc_costs in
+       bitvector_of_nat ? pc' = sigma pseudo_program (bitvector_of_nat ? ppc') ∧
        ppc' = length … pre ∧
        tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
@@ -1169 +1180 @@
    let 〈pc, costs〉 ≝ pc_costs in
     〈labels, costs〉.
- [3: whd % [%] // #id normalize in ⊢ (% → ?) #abs @⊥ //
- | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * #IH0 #IH1 #IH2
-   cases construct in p4 #PC #CODE #JMEQ % [%]
-   [ >length_append <IH0 normalize; //
+ [3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
+ | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
+   cases construct in p4 #PC #CODE #JMEQ % [% [%]]
+   [ @(construct_costs_sigma … IHn1) [4: <JMEQ % |*: skip]
+   | >length_append <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
    | @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
    | #id normalize nodelta; -labels1; cases label; normalize nodelta
-     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 //
+     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
      | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
        generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
         [ #EQ #_ <(eq_bv_to_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit 
-          <IH0 
-        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: /2/]
-          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 //]]]
+          <IH0 [@IHn1 | <(eq_bv_to_eq … EQ) in H #H @H] 
+        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
+          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
  | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2 
    @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]