Changeset 2652 for src/ASM/Policy.ma


Ignore:
Timestamp:
Feb 8, 2013, 11:49:55 AM (7 years ago)
Author:
sacerdot
Message:

String type changed definition.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2318 r2652  
    312312lemma measure_full: ∀program.∀policy.
    313313  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
    314   is_jump (\snd (nth i ? program 〈None ?,Comment []〉)) →
     314  is_jump (\snd (nth i ? program 〈None ?,Comment EmptyString〉)) →
    315315  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump.
    316316#program #policy elim program in ⊢ (% → ∀i.% → ? → %);
     
    570570            #H @H ]
    571571            #i #Hi
    572             inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
     572            inversion (is_jump (\snd (nth i ? program 〈None ?, Comment EmptyString〉)))
    573573            [1,3: #Hj whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*85s*)
    574574              >Feq in Geq; normalize nodelta cases Fno_ch
     
    675675| #ppc #ppc_ok normalize nodelta
    676676  >(?:\fst (fetch_pseudo_instruction (pi1 … (\snd program)) ppc ppc_ok) =
    677        \snd (nth (nat_of_bitvector … ppc) ? (\snd program) 〈None ?, Comment []〉))
     677       \snd (nth (nat_of_bitvector … ppc) ? (\snd program) 〈None ?, Comment EmptyString〉))
    678678  [2: whd in match fetch_pseudo_instruction; normalize nodelta
    679    >(nth_safe_nth … 〈None ?, Comment []〉)
    680    cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
     679   >(nth_safe_nth … 〈None ?, Comment EmptyString〉)
     680   cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment EmptyString〉)
    681681   #lbl #ins % ]
    682682  lapply (Hfpol3 ? (nat_of_bitvector ? ppc) ppc_ok)
     
    750750                >Hxpc in Hpcompact; >HSxpc whd in match create_label_map; #H
    751751                @(plus_equals_zero (2^16)) whd in match fetch_pseudo_instruction;
    752                 normalize nodelta >(nth_safe_nth … 〈None ?, Comment []〉)
    753                 cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment []〉) in H;
     752                normalize nodelta >(nth_safe_nth … 〈None ?, Comment EmptyString〉)
     753                cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment EmptyString〉) in H;
    754754                #lbl #ins normalize nodelta #X @sym_eq @X
    755755              ]
Note: See TracChangeset for help on using the changeset viewer.