Changeset 860 for src

Timestamp:

May 30, 2011, 6:43:14 PM (10 years ago)

Author:

sacerdot

Message:

Progress in the proof.

File:

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

src/ASM/AssemblyProof.ma

@@ -395 +395 @@
 qed.
 
+axiom occurs_exactly_once: Identifier → list labelled_instruction → Prop.
+
 definition build_maps' ≝
   λpseudo_program.
@@ -405 +407 @@
       let 〈labels,pc_costs〉 ≝ res in
       let 〈ignore,costs〉 ≝ pc_costs in
-       ∀pc. (nat_of_bitvector … pc) < length … pre →
-        lookup ?? pc labels (zero …) = sigma pre' (\snd (fetch_pseudo_instruction pre pc)))
+       ∀id. occurs_exactly_once id instr_list →
+        lookup ?? id labels (zero …) = sigma pre' (\snd (fetch_pseudo_instruction pre id)))
     instr_list
     (λprefix,i,tl,prf,t.
@@ -431 +433 @@
    let 〈pc, costs〉 ≝ pc_costs in
     〈labels, costs〉.
- [ whd cases construct in p3 #PC #CODE #JMEQ whd #pc #Hpc
+ [ whd cases construct in p3 #PC #CODE #JMEQ whd #id #Hid
    generalize in match (sig2 … t) whd in ⊢ (% → ?)
    >p whd in ⊢ (% → ?) >p1 whd in ⊢ (% → ?) #IH1
-   >length_append in Hpc <plus_n_Sm in ⊢ (% → ?) <plus_n_O in ⊢ (% → ?) #Hpc
    whd in ⊢ (??(????%?)?) -labels1;
    cases label
     [ whd in ⊢ (??(????%?)?)
-      cases (le_to_or_lt_eq … Hpc)
-      [ #H1 >(IH1 pc) [2: @(le_S_S_to_le … H1)]
-        (* lemmas needed here *)
-      | #H1 generalize in match (injective_S … H1) -H1 #H1
-        (* ??? *)
-      ]
+      (* COMPLETARE *)
+      >IH1
     | -label #label whd in ⊢ (??(????%?)?)