 Timestamp:
 May 16, 2012, 3:10:58 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r1950 r1956 256 256  Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in 257 257 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〉 in259 〈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〉))) 260 260 (bitvector_of_nat ? pc) (\snd (nth n ? program 〈None ?, Comment []〉)) 261 261 ] … … 301 301 (λhd.λx.λtl.λp.λacc. 302 302 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〉 in304 〈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〉))) 305 305 (bitvector_of_nat 16 (\fst sigma)) (\snd x))) 306 306 0. … … 315 315 λprogram. 316 316 \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) 319 320 qed. 320 321 … … 768 769 19,22,23,24,25,26,27: / by le_n/ 769 770 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 771 777 ] 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/ 772 787 ] 773 788 ] 774 789 ] 775 cases daemon (* XXX see if it works first *)776 790 qed. 777 791
Note: See TracChangeset
for help on using the changeset viewer.