Changeset 1956 for src/ASM/Policy.ma


Ignore:
Timestamp:
May 16, 2012, 3:10:58 PM (8 years ago)
Author:
boender
Message:
  • finished proof of lemma (where auto does strange things again)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1950 r1956  
    256256    | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
    257257       pc1 = instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
    258          (λppc.let 〈x,y〉 ≝ bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉 in
    259            〈bitvector_of_nat ? x, jmpeqb y long_jump〉)
     258         (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
     259         (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    260260         (bitvector_of_nat ? pc) (\snd (nth n ? program 〈None ?, Comment []〉))
    261261    ]
     
    301301  (λhd.λx.λtl.λp.λacc.
    302302    acc + (instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
    303     (λppc.let 〈x,y〉 ≝ bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉 in
    304            〈bitvector_of_nat ? x, jmpeqb y long_jump〉)
     303    (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
     304    (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    305305    (bitvector_of_nat 16 (\fst sigma)) (\snd x)))
    306306  0.
     
    315315 λprogram.
    316316   \fst (create_label_cost_map program).
    317  #l #Hl lapply (pi2 ?? (create_label_cost_map program)) @pair_elim
    318  #labels #costs #EQ normalize nodelta #H @(H l Hl)
     317 #l #Hl lapply (pi2 ?? (create_label_cost_map0 program)) @pair_elim
     318 #labels #costs #EQ normalize nodelta #H whd in match create_label_cost_map;
     319 normalize nodelta >EQ @(H l Hl)
    319320qed.
    320321
     
    768769     |19,22,23,24,25,26,27: / by le_n/
    769770     |29,30: cases x #ad cases ad #a1 #a2
    770        [ cases a2 #ad2 cases ad2
     771       [1,3: cases a2 #ad2 cases ad2
     772         [1,8,20,27: #b #Hb normalize @le_S @le_S @le_S @le_S @le_S @le_n (* auto inexplicably takes a long time here *)
     773         |2,3,4,9,15,16,17,18,19,21,22,23,28,34,35,36,37,38: #b] #Hb cases Hb
     774       |2,4: cases a1 #ad1 cases ad1
     775         [2,4,21,23: #b #Hb normalize @le_S @le_S @le_S @le_S @le_S @le_n
     776         |1,3,8,9,15,16,17,18,19,20,22,27,28,34,35,36,37,38: #b] #Hb cases Hb
    771777       ]
     778     |28,31,32,33,34,35,36: / by le_n/
     779     |38,39: cases x #ad cases ad
     780       [1,4,20,23: #b #Hb / by le_n/
     781       |2,3,8,9,15,16,17,18,19,21,22,27,28,34,35,36,37,38: #b] #Hb cases Hb
     782     |37,40,41,42,43,44,45: / by le_n/
     783     |46,47,48,49,50,51,52,53,54: / by le_n/
     784     |55,56,57,58,59,60,61,62,63: / by le_n/
     785     |64,65,66,67,68,69,70,71,72: / by le_n/
     786     |73,74,75,76,77,78,79,80,81: / by le_n/
    772787     ]
    773788   ]
    774789 ]
    775  cases daemon (* XXX see if it works first *)
    776790qed.
    777791
Note: See TracChangeset for help on using the changeset viewer.