Ignore:
Timestamp:
Jul 26, 2012, 12:38:42 AM (8 years ago)
Author:
sacerdot
Message:

1) Major change: we now always use the efficient way of resolving labels

for the interpretation of pseudo assembly code. The inefficient way is
only used locally in ASM/Interpret.ma to prove some properties more easily.

2) AssemblyProofSplitSplit?.ma partially repaired. In particular, the main

lemma is now called correctly thanks to the previous change.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2235 r2264  
    315315  (Σlabels:label_map.
    316316    ∀l.occurs_exactly_once ?? l program →
    317     And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
    318      address_of_word_labels_code_mem program l)
    319     (lookup_def ?? labels l 0 < |program|)
     317    (*And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
     318     address_of_word_labels program l)
     319    ( *)lookup_def ?? labels l 0 < |program|(*)*)
    320320  ) ≝
    321321 λprogram.
    322322   \fst (create_label_cost_map program).
    323  #l #Hl lapply (pi2 ?? (create_label_cost_map0 program)) @pair_elim
    324  #labels #costs #EQ normalize nodelta #H whd in match create_label_cost_map;
    325  normalize nodelta >EQ @(H l Hl)
     323 #l #Hl cases (create_label_cost_map_ok program) #_ #X @(X … Hl)
    326324qed.
    327325
     
    667665              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    668666              [1,3: cases (create_label_map program) #clm #Hclm
    669                 @le_S_to_le @(proj2 ?? (Hclm x ?))
     667                @le_S_to_le @(Hclm x ?)
    670668                [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
    671669                |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
     
    696694              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    697695              [1,3,5,7: cases (create_label_map program) #clm #Hclm
    698                 @le_S_to_le @(proj2 ?? (Hclm x ?))
     696                @le_S_to_le @(Hclm x ?)
    699697                [1,2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
    700698                |3,4: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
     
    728726               lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    729727              [#x #Heq cases (create_label_map program) #clm #Hclm
    730                @le_S_to_le @(proj2 ?? (Hclm x ?))
     728               @le_S_to_le @(Hclm x ?)
    731729               @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
    732730               [ >nat_of_bitvector_bitvector_of_nat_inverse
Note: See TracChangeset for help on using the changeset viewer.