Ignore:
Timestamp:
May 30, 2011, 6:43:14 PM (8 years ago)
Author:
sacerdot
Message:

Progress in the proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r859 r860  
    395395qed.
    396396
     397axiom occurs_exactly_once: Identifier → list labelled_instruction → Prop.
     398
    397399definition build_maps' ≝
    398400  λpseudo_program.
     
    405407      let 〈labels,pc_costs〉 ≝ res in
    406408      let 〈ignore,costs〉 ≝ pc_costs in
    407        ∀pc. (nat_of_bitvector … pc) < length … pre
    408         lookup ?? pc labels (zero …) = sigma pre' (\snd (fetch_pseudo_instruction pre pc)))
     409       ∀id. occurs_exactly_once id instr_list
     410        lookup ?? id labels (zero …) = sigma pre' (\snd (fetch_pseudo_instruction pre id)))
    409411    instr_list
    410412    (λprefix,i,tl,prf,t.
     
    431433   let 〈pc, costs〉 ≝ pc_costs in
    432434    〈labels, costs〉.
    433  [ whd cases construct in p3 #PC #CODE #JMEQ whd #pc #Hpc
     435 [ whd cases construct in p3 #PC #CODE #JMEQ whd #id #Hid
    434436   generalize in match (sig2 … t) whd in ⊢ (% → ?)
    435437   >p whd in ⊢ (% → ?) >p1 whd in ⊢ (% → ?) #IH1
    436    >length_append in Hpc <plus_n_Sm in ⊢ (% → ?) <plus_n_O in ⊢ (% → ?) #Hpc
    437438   whd in ⊢ (??(????%?)?) -labels1;
    438439   cases label
    439440    [ whd in ⊢ (??(????%?)?)
    440       cases (le_to_or_lt_eq … Hpc)
    441       [ #H1 >(IH1 pc) [2: @(le_S_S_to_le … H1)]
    442         (* lemmas needed here *)
    443       | #H1 generalize in match (injective_S … H1) -H1 #H1
    444         (* ??? *)
    445       ]
     441      (* COMPLETARE *)
     442      >IH1
    446443    | -label #label whd in ⊢ (??(????%?)?)
    447444     
Note: See TracChangeset for help on using the changeset viewer.