%Patch files loaded: (patch2) version 2.399 $$$pvs-strategies (in-package 'pvs) ;;; peephole optimization ;;; bb proves a program sequence to be a basic block (defstep bb () (then* (skosimp) (repeat (expand "basic_block?"))) "(bb) : strategy to prove that a machine program is a basic block." "~%Applying bb-strategy") ;;; redefine strategy for proving subtype tcc's ;(defstep subtype-tcc () ; (THEN* (bb) (TCC :DEFS EXPLICIT)) ; "" ; "") (defstep subtype-tcc () (GRIND :theories "even") "" "") ;;; peephole optimization strategy ;(defstep pho (&optional theories rewrites exclude-theories exclude) ;(THEN* ; (SKOSIMP* :PREDS? T) ; (EXPAND "null_seq?") ; (EXPAND "correct?") ; (EXPAND "eq_bb") ; (SKOSIMP* :PREDS? T) ; (INSTALL-REWRITES :defs T theories rewrites exclude-theories exclude) ; (REPEAT (ASSERT)) ; (APPLY (THEN* (REPEAT (LIFT-IF)) (BDDSIMP) ; (GRIND :defs T theories rewrites exclude))) ; (REWRITE "singleton_lem") ; (REPEAT (APPLY-EXTENSIONALITY :HIDE? T)) ; (GRIND)) ; ; (THEN* (GRIND) (REPEAT (APPLY-EXTENSIONALITY :HIDE? T)))) ; "(pho &OPTIONAL THEORIES REWRITES EXCLUDE-THEORIES EXCLUDE) : ; Sets up auto-rewrites from definitions in the statement, from THEORIES and REWRITES, ; and stops rewriting on EXCLUDE-THEORIES and EXCLUDE. ; Then tries to prove the correctness of an optimizing pattern." ; "~%Applying peephole-optimization strategy") ;;; (defstep pho (&optional theories rewrites exclude) (THEN* (GRIND :defs ! theories rewrites exclude) (REWRITE "singleton_lem") (REPEAT (APPLY-EXTENSIONALITY :HIDE? T)) ; (GRIND :defs ! theories rewrites exclude) (REDUCE)) "(pho &OPTIONAL THEORIES REWRITES EXCLUDE) : Sets up auto-rewrites from definitions in the statement, from THEORIES and REWRITES, and stops rewriting on EXCLUDE. Then tries to prove the correctness of an optimizing pattern." "~%Applying peephole-optimization strategy") $$$top.pvs top : THEORY BEGIN IMPORTING stackm_top, tam_top END top $$$stackm_top.pvs % Peephole Optimizations on a Stack Machine stackm_top : THEORY BEGIN % --- stack machine IMPORTING stack_m_bv IMPORTING stackm_props % optimizations IMPORTING stack_m_pho1 IMPORTING stack_m_pho2 IMPORTING stack_m_pho3 IMPORTING stack_m_pho4 IMPORTING stack_m_pho5 IMPORTING stack_m_pho6 IMPORTING stack_m_pho7 IMPORTING stack_m_pho8 IMPORTING stack_m_pho9 END stackm_top $$$stack_m_bv.pvs stack_m_bv : THEORY BEGIN IMPORTING even % integer arithmetic % addresses have to be even ramadr : TYPE = (even) CONTAINING 0 value : TYPE = int IMPORTING stack[int] % instruction set (without jumps!) sm_inst : DATATYPE BEGIN add : add? adi(adi_n:value) : adi? ban : ban? blm(blm_n:ramadr) : blm? cmi : cmi? com : com? dec : dec? dev(dev_n:ramadr) : dev? div : div? dup : dup? inc : inc? inv(inv_n:ramadr) : inv? ior : ior? lav(lav_n:ramadr) : lav? ldf(ldf_n:ramadr) : ldf? ldv(ldv_n:ramadr) : ldv? loc(loc_n:value) : loc? lof(lof_n:ramadr) : lof? loi(loi_n:ramadr) : loi? lop(lop_n:ramadr) : lop? lov(lov_n:ramadr) : lov? mod : mod? mul : mul? neg : neg? nop : nop? not : not? rol : rol? ror : ror? sdf(sdf_n:ramadr) : sdf? sdv(sdv_n:ramadr) : sdv? shl : shl? shr : shr? stf(stf_n:ramadr) : stf? sti(sti_n:ramadr) : sti? stp(stp_n:ramadr) : stp? stv(stv_n:ramadr) : stv? sub : sub? teq : teq? tge : tge? tgt : tgt? tle : tle? tlt : tlt? tne : tne? xor : xor? zrv(zrv_n:ramadr) : zrv? END sm_inst % === semantics === memory : TYPE = [ramadr -> value] state : TYPE+ = [# mem : memory, stk : Stack #] s : VAR state i,v,v1,v2,t,t1,t2 : VAR value base,adr,n,m,k : VAR ramadr n1,n2,num : VAR nat bop : VAR [value, value -> value] uop : VAR [value -> value] rel : VAR [value,value -> bool] mem : VAR memory st : VAR Stack % --- use bit-vector library IMPORTING bitvectors@bv_top IMPORTING bitvectors@div IMPORTING bitvectors@mod bv,bv1,bv2 : VAR rng_2s_comp[16] bool_and(bv1,bv2) : value = bv2int(int2bv[16](bv1) AND int2bv[16](bv2)) bool_xor(bv1,bv2) : value = bv2int(int2bv[16](bv1) XOR int2bv[16](bv2)) bool_or(bv1,bv2) : value = bv2int(int2bv[16](bv1) OR int2bv[16](bv2)) bool_not(bv) : value = bv2int(NOT(int2bv[16](bv))) rol_sem(t,bv) : value = IF t <= 0 OR t >= 16 THEN bv ELSE bv2int[16](rotate_left(t,int2bv[16](bv))) ENDIF ror_sem(t,bv) : value = IF t <= 0 OR t >= 16 THEN bv ELSE bv2int[16](rotate_left(t,int2bv[16](bv))) ENDIF cmi_sem(t1,t2) : value = IF (t1 < t2) THEN -1 ELSIF (t1 = t2) THEN 0 ELSE 1 ENDIF not_sem(t:value) : value = IF (t = 0) THEN 1 ELSE 0 ENDIF % constants -1, 0, 1 min1 : bvec[16] = fill[16](1) zero : bvec[16] = fill[16](0) one : bvec[16] = LAMBDA (m:below(16)): IF m = 0 THEN 1 ELSE 0 ENDIF min1_prop : COROLLARY int2bv[16](-1) = min1 zero_prop : COROLLARY int2bv[16](0) = zero % --- some simple facts xor_not : LEMMA bool_xor(-1, bv) = bool_not(bv) ior_zero : LEMMA bool_or(bv, 0) = bv xor_zero : LEMMA bool_xor(bv, 0) = bv % ----------- the admissible predicate ------------ sm_admissible(p:sm_inst) : pred[state] = LAMBDA s: CASES p OF add : twotops?(stk(s)), adi(i) : nonempty?(stk(s)), ban : twotops?(stk(s)) & in_rng_2s_comp[16](top(stk(s))) & in_rng_2s_comp[16](top(pop(stk(s)))), blm(k) : twotops?(stk(s)) & (top(stk(s)) >= 0) & top(pop(stk(s))) >= 0 & even(top(stk(s))) & even(top(pop(stk(s)))), cmi : twotops?(stk(s)), com : nonempty?(stk(s)) & in_rng_2s_comp[16](top(stk(s))), dec : nonempty?(stk(s)), dev(k) : true, div : twotops?(stk(s)) & top(stk(s)) /= 0, dup : nonempty?(stk(s)), inc : nonempty?(stk(s)), inv(k) : true, ior : twotops?(stk(s)) & in_rng_2s_comp[16](top(stk(s))) & in_rng_2s_comp[16](top(pop(stk(s)))), lav(k) : true, ldf(k) : nonempty?(stk(s)) & (top(stk(s)) + k >= 0) & even(top(stk(s)) + k), ldv(k) : true, loc(i) : true, lof(k) : nonempty?(stk(s)) & (top(stk(s)) + k >= 0) & even(top(stk(s)) + k), loi(k) : nonempty?(stk(s)) & top(stk(s)) >= 0 & even(top(stk(s))), lop(k) : mem(s)(k) >= 0 & even(mem(s)(k)), lov(k) : true, mod : twotops?(stk(s)) & top(stk(s)) /= 0, mul : twotops?(stk(s)), neg : nonempty?(stk(s)), nop : true, not : nonempty?(stk(s)), rol : twotops?(stk(s)) & in_rng_2s_comp[16](top(stk(s))), ror : twotops?(stk(s)) & in_rng_2s_comp[16](top(stk(s))), sdf(k) : n_tops?(stk(s), 3) & (top(stk(s)) + k) >= 0 & even(top(stk(s))+k), sdv(k) : twotops?(stk(s)), shl : twotops?(stk(s)) & (top(stk(s)) >= 0), shr : twotops?(stk(s)) & (top(stk(s)) >= 0), stf(k) : twotops?(stk(s)) & (top(stk(s)) + k >= 0) & even(top(stk(s)) + k), sti(k) : nonempty?(stk(s)) & n_tops?(pop(stk(s)), div2(k)) & (top(stk(s)) >= 0) & even(top(stk(s))), stp(k) : nonempty?(stk(s)) & mem(s)(k) >= 0 & even(mem(s)(k)), stv(k) : nonempty?(stk(s)), sub : twotops?(stk(s)), teq : nonempty?(stk(s)), tge : nonempty?(stk(s)), tgt : nonempty?(stk(s)), tle : nonempty?(stk(s)), tlt : nonempty?(stk(s)), tne : nonempty?(stk(s)), xor : twotops?(stk(s)) & in_rng_2s_comp[16](top(stk(s))) & in_rng_2s_comp[16](top(pop(stk(s)))), zrv(k) : true ENDCASES % --- auxiliary functions loi_aux(m:memory, st:Stack, base:ramadr, num:nat) : RECURSIVE Stack = IF (num = 0) THEN st ELSE push(m(base - 2 + (2 * num)), loi_aux(m, st, base, num - 1)) ENDIF MEASURE num blm_aux(m:memory, t1,t2:ramadr, k:nat): RECURSIVE memory = IF (k = 0) THEN m ELSE blm_aux(m WITH [(t1 - 2 + (2 * k)) := m(t2 - 2 + (2 * k))], t1, t2, k - 1) ENDIF MEASURE k sti_aux(s:state, base:ramadr, num:{n1:nat | n_tops?(stk(s), n1)}) : RECURSIVE state = IF (num = 0) THEN s ELSE sti_aux(s WITH [(mem)(base + (2 * num) - 2) := top(stk(s)), (stk) := pop(stk(s))], base, num - 1) ENDIF MEASURE num % ------------- semantics of binary operations ------------------- binop_sem(bop)(s:{s1:state | twotops?(stk(s1))}) : state = LET t1 = top(stk(s)), t2 = top(pop(stk(s))) IN s WITH [(stk) := push(bop(t2,t1), pop(pop(stk(s))))] % -------------- semantics of unary operations ------------- unop_sem(uop)(s:{s1 : state | nonempty?(stk(s1))}) : state = LET t = top(stk(s)) IN s WITH [(stk) := push(uop(t), pop(stk(s)))] % ---------------- semantics of compare instructions ------- comp_sem(rel)(s:{s1:state | nonempty?(stk(s1))}) : state = LET t = top(stk(s)), newstk = (IF rel(t, 0) THEN push(1, pop(stk(s))) ELSE push(0, pop(stk(s))) ENDIF) IN s WITH [(stk) := newstk] % --------- the effect of each instruction ------------- sm_ip(p:sm_inst)(s:{s1:state | (sm_admissible(p))(s1)}) : state = CASES p OF add : binop_sem(LAMBDA v1,v2: v1 + v2)(s), adi(i) : s WITH [(stk) := push(top(stk(s)) + i, pop(stk(s)))], ban : s WITH [(stk) := push(bool_and(second(stk(s)), top(stk(s))), pop(pop(stk(s))))], blm(k) : s WITH [(mem) := blm_aux(mem(s), top(stk(s)), top(pop(stk(s))), div2(k)), (stk) := pop(pop(stk(s)))], cmi : binop_sem(LAMBDA v1,v2: IF (v1 < v2) THEN -1 ELSIF (v1 = v2) THEN 0 ELSE 1 ENDIF)(s), com : s WITH [(stk) := push(bool_xor(-1, top(stk(s))), pop(stk(s)))], dec : unop_sem(LAMBDA v: v - 1)(s), dev(k) : s WITH [(mem)(k) := mem(s)(k) - 1], div : s WITH [(stk) := push(div(second(stk(s)),top(stk(s))), pop(pop(stk(s))))], dup : s WITH [(stk) := push(top(stk(s)), stk(s))], inc : unop_sem(LAMBDA v: v + 1)(s), inv(k) : s WITH [(mem)(k) := mem(s)(k) + 1], ior : s WITH [(stk) := push(bool_or(second(stk(s)), top(stk(s))), pop(pop(stk(s))))], lav(k) : s WITH [(stk) := push(k, stk(s))], ldf(k) : s WITH [(stk) := LET t = top(stk(s)) IN push(mem(s)(k + t + 2), push(mem(s)(k + t), pop(stk(s))))], ldv(k) : s WITH [(stk) := push(mem(s)(k + 2), push(mem(s)(k), stk(s)))], loc(i) : s WITH [(stk) := push(i, stk(s))], lof(k) : s WITH [(stk) := push(mem(s)(top(stk(s)) + k), pop(stk(s)))], loi(k) : s WITH [(stk) := loi_aux(mem(s), pop(stk(s)), top(stk(s)), div2(k))], lop(k) : s WITH [(stk) := push(mem(s)(mem(s)(k)), stk(s))], lov(k) : s WITH [(stk) := push(mem(s)(k), stk(s))], mod : s WITH [(stk) := push(mod(second(stk(s)),top(stk(s))), pop(pop(stk(s))))], mul : binop_sem(LAMBDA v1,v2: v1 * v2)(s), neg : unop_sem(LAMBDA v: (-1) * v)(s), nop : s, not : unop_sem(LAMBDA v: IF (v = 0) THEN 1 ELSE 0 ENDIF)(s), rol : s WITH [(stk) := push(rol_sem(second(stk(s)), top(stk(s))), pop(pop(stk(s))))], ror : s WITH [(stk) := push(ror_sem(second(stk(s)), top(stk(s))), pop(pop(stk(s))))], sdf(k) : (LET t = top(stk(s)), t1 = top(pop(stk(s))), t2 = top(pop(pop(stk(s)))) IN s WITH [(mem) := mem(s) WITH [(k + t + 2) := t1, (k + t) := t2], (stk) := pop(pop(pop(stk(s))))]), sdv(k) : (LET t1 = top(stk(s)), t2 = top(pop(stk(s))) IN s WITH [(mem) := mem(s) WITH [(k + 2) := t1, (k) := t2], (stk) := pop(pop(stk(s)))]), shl : s WITH [(stk) := push(second(stk(s)) * power(2, top(stk(s))), pop(pop(stk(s))))], shr : s WITH [(stk) := push(div(second(stk(s)), power(2, top(stk(s)))), pop(pop(stk(s))))], stf(k) : (LET t1 = top(stk(s)), t2 = top(pop(stk(s))) IN s WITH [(mem)(t1 + k) := t2, (stk) := pop(pop(stk(s)))]), sti(k) : sti_aux(s WITH [(stk) := pop(stk(s))], top(stk(s)), div2(k)), stp(k) : s WITH [(mem)(mem(s)(k)) := top(stk(s)), (stk) := pop(stk(s))], stv(k) : s WITH [(mem)(k) := top(stk(s)), (stk) := pop(stk(s))], sub : binop_sem(LAMBDA v1,v2: v1 - v2)(s), teq : comp_sem(LAMBDA v1,v2: v1 = v2)(s), tge : comp_sem(LAMBDA v1,v2: v1 >= v2)(s), tgt : comp_sem(LAMBDA v1,v2: v1 > v2)(s), tle : comp_sem(LAMBDA v1,v2: v1 <= v2)(s), tlt : comp_sem(LAMBDA v1,v2: v1 < v2)(s), tne : comp_sem(LAMBDA v1,v2: v1 /= v2)(s), xor : s WITH [(stk) := push(bool_xor(second(stk(s)), top(stk(s))), pop(pop(stk(s))))], zrv(k) : s WITH [(mem)(k) := 0] ENDCASES END stack_m_bv $$$stack_m_bv.prf (|stack_m_bv| (|ramadr_TCC1| "" (GRIND) NIL) (|rol_sem_TCC1| "" (SUBTYPE-TCC) NIL) (|min1_TCC1| "" (SUBTYPE-TCC) NIL) (|zero_TCC1| "" (SUBTYPE-TCC) NIL) (|min1_prop_TCC1| "" (SUBTYPE-TCC) NIL) (|min1_prop| "" (USE "bv2int_inj[16]") (("" (EXPAND "injective?") (("" (INST?) (("1" (ASSERT) (("1" (HIDE 2) (("1" (AUTO-REWRITE-THEORY "bv_int[16]") (("1" (STOP-REWRITE "int2bv[16]") (("1" (REWRITE "bv2int_inv[16]") (("1" (GRIND) NIL) ("2" (HIDE 2) (("2" (GRIND) NIL))))))))))))) ("2" (GRIND) NIL))))))) (|zero_prop_TCC1| "" (SUBTYPE-TCC) NIL) (|zero_prop| "" (USE "bv2int_inj[16]") (("" (EXPAND "injective?") (("" (INST?) (("1" (ASSERT) (("1" (HIDE 2) (("1" (REWRITE "bv2int_inv[16]") (("1" (GRIND) NIL) ("2" (GRIND) NIL))))))) ("2" (GRIND) NIL))))))) (|xor_not| "" (AUTO-REWRITE-DEFS) (("" (STOP-REWRITE "int2bv") (("" (SKOSIMP* :PREDS? T) (("" (STOP-REWRITE "bv2int") (("" (ASSERT) (("" (USE "bv2int_inj[16]") (("" (ASSERT) (("" (EXPAND "injective?") (("" (CASE-REPLACE "(int2bv[16](-1) XOR int2bv[16](bv!1)) = NOT((int2bv[16](bv!1)))") (("" (HIDE -1) (("" (DELETE 2) (("" (REWRITE "min1_prop") (("" (GRIND :EXCLUDE ("int2bv" "bv2int")) (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))))))))))))))))))))))) (|ior_zero| "" (AUTO-REWRITE-DEFS) (("" (STOP-REWRITE "int2bv") (("" (SKOSIMP* :PREDS? T) (("" (STOP-REWRITE "bv2int") (("" (ASSERT) (("" (REWRITE "zero_prop") (("" (GRIND :EXCLUDE ("int2bv" "bv2int")) (("" (CASE-REPLACE "(int2bv[16](bv!1) OR fill[16](0)) = int2bv[16](bv!1)") (("1" (REWRITE "bv2int_inv[16]") NIL) ("2" (HIDE 2) (("2" (GRIND :EXCLUDE ("int2bv" "bv2int")) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND :EXCLUDE ("int2bv" "bv2int")) NIL))))))))))))))))))))))) (|xor_zero| "" (AUTO-REWRITE-DEFS) (("" (STOP-REWRITE "int2bv") (("" (SKOSIMP* :PREDS? T) (("" (STOP-REWRITE "bv2int") (("" (ASSERT) (("" (REWRITE "zero_prop") (("" (CASE-REPLACE "(int2bv[16](bv!1) XOR zero) = int2bv[16](bv!1)") (("1" (REWRITE "bv2int_inv[16]") NIL) ("2" (HIDE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND :EXCLUDE ("int2bv" "bv2int")) NIL))))))))))))))))))) (|sm_admissible_TCC1| "" (SUBTYPE-TCC) NIL) (|sm_admissible_TCC2| "" (SUBTYPE-TCC) NIL) (|sm_admissible_TCC3| "" (SUBTYPE-TCC) NIL) (|sm_admissible_TCC4| "" (SUBTYPE-TCC) NIL) (|sm_admissible_TCC5| "" (SUBTYPE-TCC) NIL) (|sm_admissible_TCC6| "" (SUBTYPE-TCC) NIL) (|sm_admissible_TCC7| "" (SUBTYPE-TCC) NIL) (|sm_admissible_TCC8| "" (SUBTYPE-TCC) NIL) (|sm_admissible_TCC9| "" (SUBTYPE-TCC) NIL) (|sm_admissible_TCC10| "" (SUBTYPE-TCC) NIL) (|sm_admissible_TCC11| "" (SUBTYPE-TCC) NIL) (|sm_admissible_TCC12| "" (SUBTYPE-TCC) NIL) (|sm_admissible_TCC13| "" (SUBTYPE-TCC) NIL) (|sm_admissible_TCC14| "" (SUBTYPE-TCC) NIL) (|sm_admissible_TCC15| "" (SUBTYPE-TCC) NIL) (|sm_admissible_TCC16| "" (SUBTYPE-TCC) NIL) (|loi_aux_TCC1| "" (SUBTYPE-TCC)) (|loi_aux_TCC2| "" (SUBTYPE-TCC) NIL) (|loi_aux_TCC3| "" (TERMINATION-TCC) NIL) (|blm_aux_TCC1| "" (TERMINATION-TCC) NIL) (|sti_aux_TCC1| "" (SUBTYPE-TCC)) (|sti_aux_TCC2| "" (SUBTYPE-TCC) NIL) (|sti_aux_TCC3| "" (SUBTYPE-TCC) NIL) (|sti_aux_TCC4| "" (TERMINATION-TCC) NIL) (|binop_sem_TCC1| "" (SUBTYPE-TCC) NIL) (|binop_sem_TCC2| "" (SUBTYPE-TCC) NIL) (|unop_sem_TCC1| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC1| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC2| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC3| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC4| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC5| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC6| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC7| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC8| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC9| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC10| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC11| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC12| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC13| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC14| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC15| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC16| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC17| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC18| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC19| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC20| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC21| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC22| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC23| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC24| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC25| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC26| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC27| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC28| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC29| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC30| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC31| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC32| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC33| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC34| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC35| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC36| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC37| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC38| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC39| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC40| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC41| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC42| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC43| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC44| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC45| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC46| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC47| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC48| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC49| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC50| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC51| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC52| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC53| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC54| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC55| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC56| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC57| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC58| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC59| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC60| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC61| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC62| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC63| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC64| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC65| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC66| "" (GRIND :THEORIES "even") (("" (USE "power_pos" :subst ("m" "top(stk(s!1))")) (("" (ASSERT) NIL))))) (|sm_ip_TCC67| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC68| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC69| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC70| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC71| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC72| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC73| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC74| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC75| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC76| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC77| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC78| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC79| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC80| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC81| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC82| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC83| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC84| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC85| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC86| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC87| "" (SUBTYPE-TCC) NIL) (|sm_ip_TCC88| "" (SUBTYPE-TCC) NIL)) $$$even.pvs even : THEORY BEGIN even(n:nat) : RECURSIVE bool = IF (n=0) THEN true ELSIF (n=1) THEN false ELSE even(n-2) ENDIF MEASURE n add_closed : LEMMA (FORALL (n1,n2:nat): even(n1) & even(n2) IMPLIES even(n1+n2)) JUDGEMENT + HAS_TYPE [(even), (even) -> (even)] n,m : VAR nat n1,n2 : VAR (even) mult2_even : LEMMA even(2 * n) power(n,m:nat): RECURSIVE nat = if (m = 0) then 1 else (n * power(n, m-1)) endif measure (lambda (n,m:nat): m) div2(n:nat) : RECURSIVE nat = IF (n <= 1) THEN 0 ELSE 1 + div2(n-2) ENDIF MEASURE n power_pos : LEMMA power(2,m) > 0 two_times_div : LEMMA (FORALL (n:nat): even(n) IMPLIES (2 * div2(n)) = n) even_prop : LEMMA n > 0 IMPLIES even(n1 - 2 + 2 * n) div2_split : LEMMA div2(n1 + n2) = div2(n1) + div2(n2) END even $$$even.prf (|even| (|even_TCC1| "" (SUBTYPE-TCC) NIL) (|even_TCC2| "" (TERMINATION-TCC) NIL) (|add_closed| "" (INDUCT "n1" :NAME "NAT_induction") (("" (SKOSIMP*) (("" (EXPAND "even" +) (("" (BDDSIMP) (("1" (ASSERT) (("1" (GRIND) (("1" (CASE-REPLACE "j!1 = 0") (("1" (GRIND) NIL) ("2" (GRIND) NIL))))))) ("2" (CASE-REPLACE "j!1 = 0") (("1" (ASSERT) (("1" (GRIND) NIL))) ("2" (ASSERT) (("2" (CASE-REPLACE "j!1 = 1") (("1" (GRIND) NIL) ("2" (INST - "j!1 - 2") (("1" (ASSERT) (("1" (INST - "n2!1") (("1" (ASSERT) (("1" (GRIND) NIL))))))) ("2" (ASSERT) NIL))))))))))))))))) (|plus_TCC1| "" (SKOSIMP) (("" (USE "add_closed") (("" (ASSERT) NIL))))) (|mult2_even| "" (INDUCT "n" :NAME "NAT_induction") (("" (SKOSIMP) (("" (EXPAND "even" +) (("" (BDDSIMP) (("" (CASE-REPLACE "j!1 = 0") (("1" (ASSERT) NIL) ("2" (INST - "j!1 - 1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))) (|power_TCC1| "" (SUBTYPE-TCC) NIL) (|power_TCC2| "" (TERMINATION-TCC) NIL) (|div2_TCC1| "" (SUBTYPE-TCC) NIL) (|div2_TCC2| "" (TERMINATION-TCC) NIL) (|power_pos| "" (INDUCT-AND-SIMPLIFY "m") NIL) (|two_times_div| "" (INDUCT "n" :NAME "NAT_induction") (("" (SKOSIMP*) (("" (CASE-REPLACE "j!1 = 0") (("1" (GRIND) NIL) ("2" (CASE-REPLACE "j!1 = 1") (("1" (GRIND) NIL) ("2" (INST - "j!1 - 2") (("1" (ASSERT) (("1" (BDDSIMP) (("1" (ASSERT) (("1" (GRIND) NIL))) ("2" (GRIND) NIL))))) ("2" (ASSERT) NIL))))))))))) (|even_prop_TCC1| "" (SUBTYPE-TCC) NIL) (|even_prop| "" (SKOSIMP* :PREDS? T) (("" (CASE-REPLACE "n1!1 - 2 + 2 * n!1 = n1!1 + 2 * (n!1 - 1)") (("1" (LEMMA "mult2_even") (("1" (INST - "n!1 - 1") (("1" (USE "add_closed") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))) ("2" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))) (|div2_split| "" (INDUCT "n1" :NAME "NAT_induction") (("1" (ASSERT) NIL) ("2" (SKOSIMP* :PREDS? T) (("2" (EXPAND "div2" 1 1) (("2" (LIFT-IF) (("2" (BDDSIMP) (("1" (GRIND) NIL) ("2" (CASE-REPLACE "j!1 = 0") (("1" (GRIND) NIL) ("2" (CASE-REPLACE "j!1 = 1") (("1" (GRIND) NIL) ("2" (INST - "j!1 - 2") (("1" (ASSERT) (("1" (AUTO-REWRITE-THEORY "even") (("1" (ASSERT) (("1" (INST - "n2!1") (("1" (REPLACE*) (("1" (ASSERT) NIL))))))))))) ("2" (ASSERT) NIL)))))))))))))))))) $$$stack.pvs stack [T:TYPE] : THEORY BEGIN Stack : DATATYPE BEGIN empty : empty? push(top:T,pop:Stack) : nonempty? END Stack first(s:(nonempty?)) : T = top(s) twotops?(s:Stack) : bool = IF nonempty?(s) THEN nonempty?(pop(s)) ELSE FALSE ENDIF second(s:(twotops?)) : T = top(pop(s)) n_tops?(st:Stack, n:nat): RECURSIVE bool = IF (n = 0) THEN true ELSIF nonempty?(st) THEN n_tops?(pop(st), n-1) ELSE FALSE ENDIF MEASURE n END stack $$$stack.prf (|stack| (|second_TCC1| "" (GRIND) NIL) (|second_TCC2| "" (SKOLEM-TYPEPRED) (("" (EXPAND "twotops?") (("" (ASSERT) NIL))))) (|n_tops?_TCC1| "" (GRIND) NIL) (|n_tops?_TCC2| "" (TERMINATION-TCC) NIL)) $$$stackm_props.pvs stackm_props % [ parameters ] : THEORY BEGIN IMPORTING stack_m_bv % --- some properties of the auxiliary functions s : VAR state v : VAR value base,adr,n,m,k : VAR ramadr n1,n2,num : VAR nat mem : VAR memory st : VAR Stack loi_comp2 : LEMMA loi_aux(mem, loi_aux(mem, st, base, n1), base + (2 * n1), n2) = loi_aux(mem, st, base, n1 + n2) loi_comp : COROLLARY loi_aux(mem, loi_aux(mem, st, n, div2(m)), m + n, div2(k)) = loi_aux(mem, st, n, div2(k + m)) sti_prop : LEMMA FORALL (s:state), (base:ramadr), (num:nat), (v:value): n_tops?(stk(s), num) & (adr >= base + (2 * num)) IMPLIES sti_aux(s, base, num) WITH [(mem)(adr) := v] = sti_aux(s WITH [(mem)(adr) := v], base, num) sti_prop2 : LEMMA n_tops?(stk(s), num) & ((adr >= base + (2 * num)) OR (adr < base)) IMPLIES mem(sti_aux(s, base, num))(adr) = mem(s)(adr) n_tops_prop : LEMMA nonempty?(st) IMPLIES n_tops?(pop(st), num) IMPLIES n_tops?(st, num) sti_stack_prop : LEMMA nonempty?(stk(s)) IMPLIES n_tops?(pop(stk(s)), num) IMPLIES nonempty?(stk(sti_aux(s, base, num))) sti_stack_prop2 : LEMMA nonempty?(stk(s)) & nonempty?(pop(stk(s))) IMPLIES n_tops?(pop(pop(stk(s))), num) IMPLIES nonempty?(pop(stk(sti_aux(s, base, num)))) sti_prop3 : LEMMA n_tops?(stk(s), num + 1) & (base >= 2) IMPLIES sti_aux(s, base, num) WITH [(mem)(base - 2) := top(stk(sti_aux(s, base, num))), (stk) := pop(stk(sti_aux(s, base, num)))] = sti_aux(s WITH [(mem)(base + (2 * num) - 2) := top(stk(s)), (stk) := pop(stk(s))], base - 2, num) sti_prop4 : LEMMA n_tops?(stk(s), num + 2) & (base >= 4) IMPLIES sti_aux(s, base, num) WITH [(mem) := mem(sti_aux(s, base, num)) WITH [ (base - 2) := top(stk(sti_aux(s, base, num))), (base - 4) := top(pop(stk(sti_aux(s, base, num))))], (stk) := pop(pop(stk(sti_aux(s, base, num))))] = sti_aux(s WITH [(mem) := mem(s) WITH [(base + (2 * num) - 2) := top(stk(s)), (base + (2 * num) - 4) := top(pop(stk(s)))], (stk) := pop(pop(stk(s)))], base - 4, num) END stackm_props $$$stackm_props.prf (|stackm_props| (|loi_comp2_TCC1| "" (SUBTYPE-TCC) NIL) (|loi_comp2| "" (INDUCT "n2") (("1" (GRIND) NIL) ("2" (SKOSIMP* :PREDS? T) (("2" (EXPAND "loi_aux" 1 1) (("2" (INST?) (("2" (REPLACE*) (("2" (EXPAND "loi_aux" 1 2) (("2" (PROPAX) NIL))))))))))) ("3" (GRIND :THEORIES "even") NIL))) (|loi_comp| "" (SKOSIMP* :PREDS? T) (("" (LEMMA "loi_comp2") (("" (INST - "n!1" "mem!1" "div2(m!1)" "div2(k!1)" "st!1") (("" (REWRITE "two_times_div") (("" (REPLACE*) (("" (ASSERT) (("" (REWRITE "div2_split") NIL))))))))))))) (|sti_prop_TCC1| "" (SUBTYPE-TCC) NIL) (|sti_prop| "" (INDUCT "num") (("1" (GRIND) NIL) ("2" (SKOSIMP* :PREDS? T) (("2" (EXPAND "sti_aux" +) (("2" (INST - "adr!1" "s!1 WITH [(mem)(base!1 + 2 * j!1) := top(stk(s!1)), (stk) := pop(stk(s!1))]" "base!1" "v!1") (("1" (ASSERT) (("1" (GRIND) NIL))) ("2" (GRIND) NIL) ("3" (GRIND :THEORIES "even") NIL))))))) ("3" (SKOSIMP*) NIL))) (|sti_prop2_TCC1| "" (SUBTYPE-TCC) NIL) (|sti_prop2| "" (INDUCT "num") (("1" (GRIND) NIL) ("2" (SKOSIMP* :PREDS? T) (("2" (EXPAND "sti_aux" +) (("2" (INST - "adr!1" "base!1" "s!1 WITH [(mem)(base!1 + 2 * j!1) := top(stk(s!1)), (stk) := pop(stk(s!1))]") (("1" (ASSERT) (("1" (AUTO-REWRITE-DEFS) (("1" (ASSERT) (("1" (BDDSIMP -5) (("1" (ASSERT) (("1" (BDDSIMP) (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (REPLACE*) (("2" (ASSERT) NIL))))) ("3" (ASSERT) NIL))))))))))))) ("2" (GRIND) NIL) ("3" (GRIND :THEORIES "even") NIL))))))) ("3" (GRIND) NIL))) (|n_tops_prop| "" (INDUCT "num") (("1" (GRIND) NIL) ("2" (SKOSIMP* :PREDS? T) (("2" (EXPAND "n_tops?" +) (("2" (ASSERT) (("2" (ASSERT) (("2" (EXPAND "n_tops?" -4) (("2" (BDDSIMP) (("2" (INST - "pop(st!1)") (("2" (ASSERT) NIL))))))))))))))))) (|sti_stack_prop_TCC1| "" (SKOSIMP* :PREDS? T) (("" (USE "n_tops_prop") (("" (ASSERT) NIL))))) (|sti_stack_prop| "" (INDUCT "num") (("1" (GRIND) NIL) ("2" (SKOSIMP* :PREDS? T) (("2" (EXPAND "sti_aux" +) (("2" (INST?) (("1" (ASSERT) (("1" (ASSERT) (("1" (EXPAND "n_tops?" -5) (("1" (BDDSIMP) (("1" (PROPAX) NIL))))))))) ("2" (AUTO-REWRITE-THEORY "even") (("2" (ASSERT) NIL))))))))) ("3" (SKOSIMP*) (("3" (USE "n_tops_prop") (("3" (ASSERT) NIL))))))) (|sti_stack_prop2_TCC1| "" (SUBTYPE-TCC) NIL) (|sti_stack_prop2_TCC2| "" (SUBTYPE-TCC) NIL) (|sti_stack_prop2_TCC3| "" (SKOSIMP* :PREDS? T) (("" (USE "n_tops_prop") (("" (ASSERT) (("" (LEMMA "n_tops_prop") (("" (INST? :SUBST ("st" "pop(stk(s!1))")) (("" (ASSERT) NIL))))))))))) (|sti_stack_prop2_TCC4| "" (SKOSIMP* :PREDS? T) (("" (USE "sti_stack_prop") (("" (ASSERT) (("" (USE "n_tops_prop") (("" (ASSERT) (("" (LEMMA "n_tops_prop") (("" (INST? :SUBST ("st" "pop(stk(s!1))")) (("" (ASSERT) NIL))))))))))))))) (|sti_stack_prop2| "" (INDUCT "num") (("1" (GRIND) NIL) ("2" (SKOSIMP* :PREDS? T) (("2" (EXPAND "sti_aux" +) (("2" (INST?) (("1" (ASSERT) (("1" (ASSERT) (("1" (EXPAND "n_tops?" -6) (("1" (BDDSIMP) (("1" (PROPAX) NIL))))))))) ("2" (AUTO-REWRITE-THEORY "even") (("2" (HIDE 2) (("2" (ASSERT) NIL))))))))))) ("3" (SKOSIMP*) (("3" (USE "sti_stack_prop") (("3" (ASSERT) (("3" (LEMMA "n_tops_prop") (("3" (INST? :SUBST ("st" "pop(stk(s!1))")) (("3" (ASSERT) NIL))))))))))) ("4" (SKOSIMP*) (("4" (LEMMA "n_tops_prop") (("4" (INST? :SUBST ("st" "pop(stk(s!1))")) (("1" (ASSERT) (("1" (LEMMA "n_tops_prop") (("1" (INST? :SUBST ("st" "stk(s!1)")) (("1" (ASSERT) NIL))))))) ("2" (PROPAX) NIL))))))) ("5" (SKOSIMP*) NIL) ("6" (SKOSIMP*) NIL))) (|sti_prop3_TCC1| "" (SKOSIMP* :PREDS? T) (("" (EXPAND "n_tops?" -) (("" (BDDSIMP) (("" (USE "n_tops_prop") (("" (ASSERT) NIL))))))))) (|sti_prop3_TCC2| "" (SUBTYPE-TCC) NIL) (|sti_prop3_TCC3| "" (SKOSIMP* :PREDS? T) (("" (EXPAND "n_tops?" -) (("" (BDDSIMP) (("" (USE "sti_stack_prop") (("" (ASSERT) NIL))))))))) (|sti_prop3_TCC4| "" (SUBTYPE-TCC) NIL) (|sti_prop3_TCC5| "" (SUBTYPE-TCC) NIL) (|sti_prop3_TCC6| "" (SUBTYPE-TCC) NIL) (|sti_prop3| "" (INDUCT "num") (("1" (GRIND) NIL) ("2" (SKOSIMP* :PREDS? T) (("2" (EXPAND "sti_aux" +) (("2" (ASSERT) (("2" (INST?) (("1" (ASSERT) (("1" (EXPAND "n_tops?" -) (("1" (PROPAX) NIL))))) ("2" (HIDE 2) (("2" (GRIND) NIL))) ("3" (AUTO-REWRITE-THEORY "even") (("3" (ASSERT) NIL))))))))))) ("3" (SKOSIMP) (("3" (EXPAND "n_tops?" -) (("3" (BDDSIMP) (("3" (PROPAX) NIL))))))) ("4" (SKOSIMP*) (("4" (EXPAND "n_tops?" -) (("4" (BDDSIMP) (("4" (PROPAX) NIL))))))) ("5" (SKOSIMP*) (("5" (ASSERT) (("5" (AUTO-REWRITE-THEORY "even") (("5" (ASSERT) (("5" (TYPEPRED "base!1") (("5" (ASSERT) NIL))))))))))) ("6" (SKOSIMP*) (("6" (EXPAND "n_tops?" -) (("6" (BDDSIMP) (("6" (REWRITE "sti_stack_prop") NIL))))))) ("7" (SKOSIMP*) (("7" (ASSERT) (("7" (GRIND) (("7" (TYPEPRED "base!1") (("7" (GRIND -) NIL))))))))) ("8" (SKOSIMP*) (("8" (EXPAND "n_tops?" -) (("8" (BDDSIMP) (("8" (USE "n_tops_prop") (("8" (ASSERT) NIL))))))))))) (|sti_prop4_TCC1| "" (SKOSIMP* :PREDS? T) (("" (AUTO-REWRITE "n_tops?") (("" (ASSERT) (("" (BDDSIMP) (("" (ASSERT) (("" (BDDSIMP) (("" (USE "n_tops_prop") (("" (ASSERT) (("" (LEMMA "n_tops_prop") (("" (INST? :SUBST ("st" "pop(stk(s!1))")) (("" (ASSERT) NIL))))))))))))))))))))) (|sti_prop4_TCC2| "" (SUBTYPE-TCC) NIL) (|sti_prop4_TCC3| "" (SKOSIMP* :PREDS? T) (("" (USE "sti_stack_prop") (("" (ASSERT) (("" (AUTO-REWRITE "n_tops?") (("" (ASSERT) (("" (BDDSIMP) (("" (ASSERT) (("" (BDDSIMP) (("" (ASSERT) (("" (LEMMA "n_tops_prop") (("" (INST? :SUBST ("st" "pop(stk(s!1))")) (("" (ASSERT) NIL))))))))))))))))))))))) (|sti_prop4_TCC4| "" (SUBTYPE-TCC) NIL) (|sti_prop4_TCC5| "" (SKOSIMP* :PREDS? T) (("" (AUTO-REWRITE "n_tops?") (("" (ASSERT) (("" (BDDSIMP) (("" (ASSERT) (("" (BDDSIMP) (("" (ASSERT) (("" (USE "sti_stack_prop2") (("" (ASSERT) NIL))))))))))))))))) (|sti_prop4_TCC6| "" (SUBTYPE-TCC) NIL) (|sti_prop4_TCC7| "" (SUBTYPE-TCC) NIL) (|sti_prop4_TCC8| "" (SUBTYPE-TCC) NIL) (|sti_prop4_TCC9| "" (SUBTYPE-TCC) NIL) (|sti_prop4_TCC10| "" (SUBTYPE-TCC) NIL) (|sti_prop4| "" (INDUCT "num") (("1" (GRIND) NIL) ("2" (SKOSIMP* :PREDS? T) (("2" (EXPAND "sti_aux" +) (("2" (INST?) (("1" (ASSERT) (("1" (HIDE 2) (("1" (GRIND) NIL))))) ("2" (HIDE 2) (("2" (GRIND) NIL))) ("3" (HIDE 2) (("3" (AUTO-REWRITE-THEORY "even") (("3" (ASSERT) NIL))))))))))) ("3" (SKOSIMP* :PREDS? T) (("3" (AUTO-REWRITE-DEFS) (("3" (ASSERT) (("3" (BDDSIMP) (("3" (ASSERT) (("3" (BDDSIMP) (("3" (ASSERT) NIL))))))))))))) ("4" (SKOSIMP*) (("4" (GRIND) NIL))) ("5" (SKOSIMP*) (("5" (ASSERT) (("5" (TYPEPRED "base!1") (("5" (AUTO-REWRITE-THEORY "even") (("5" (ASSERT) NIL))))))))) ("6" (SKOSIMP*) (("6" (GRIND) NIL))) ("7" (SKOSIMP*) (("7" (ASSERT) (("7" (AUTO-REWRITE-THEORY "even") (("7" (TYPEPRED "base!1") (("7" (ASSERT) NIL))))))))) ("8" (SKOSIMP*) (("8" (USE "sti_stack_prop2") (("8" (ASSERT) (("8" (GRIND :EXCLUDE "sti_aux") NIL))))))) ("9" (SKOSIMP*) (("9" (ASSERT) (("9" (TYPEPRED "base!1") (("9" (AUTO-REWRITE-THEORY "even") (("9" (ASSERT) NIL))))))))) ("10" (SKOSIMP*) (("10" (USE "sti_stack_prop") (("10" (ASSERT) (("10" (GRIND :EXCLUDE "sti_aux") (("10" (LEMMA "n_tops_prop") (("10" (INST? :SUBST ("st" "pop(stk(s!1))")) (("10" (ASSERT) NIL))))))))))))) ("11" (SKOSIMP*) (("11" (ASSERT) (("11" (TYPEPRED "base!1") (("11" (AUTO-REWRITE-THEORY "even") (("11" (ASSERT) NIL))))))))) ("12" (SKOSIMP*) (("12" (GRIND) (("12" (LEMMA "n_tops_prop") (("12" (INST? :SUBST ("st" "pop(stk(s!1))")) (("12" (ASSERT) (("12" (LEMMA "n_tops_prop") (("12" (INST? :SUBST ("st" "stk(s!1)")) (("12" (ASSERT) NIL)))))))))))))))))) $$$stack_m_pho1.pvs stack_m_pho1 : THEORY BEGIN % --- target language IMPORTING stack_m_bv % --- pho scheme IMPORTING pho [sm_inst, state, sm_admissible, sm_ip] a,b : VAR value bv,bv1,bv2 : VAR rng_2s_comp[16] n : VAR nat c : VAR nonzero_integer s : VAR state % --- foldings tan1 : LEMMA correct?( (# pattern := (: loc(a), loc(b), add :), replacement := (: loc(a + b) :), condition := true #)) tan2 : LEMMA correct?( (# pattern := (: loc(a), loc(b), sub :), replacement := (: loc(a - b) :), condition := true #)) tan3 : LEMMA correct?( (# pattern := (: loc(a), loc(b), mul :), replacement := (: loc(a * b) :), condition := true #)) tan4 : LEMMA correct?( (# pattern := (: loc(a), loc(c), div :), replacement := (: loc(div(a,c)) :), condition := true #)) tan5 : LEMMA correct?( (# pattern := (: loc(a), loc(c), mod :), replacement := (: loc(mod(a,c)) :), condition := true #)) tan6 : LEMMA correct?( (# pattern := (: loc(bv1), loc(bv2), ban :), replacement := (: loc(bool_and(bv1,bv2)) :), condition := true #)) tan7 : LEMMA correct?( (# pattern := (: loc(bv1), loc(bv2), ior :), replacement := (: loc(bool_or(bv1,bv2)) :), condition := true #)) tan8 : LEMMA correct?( (# pattern := (: loc(bv1), loc(bv2), xor :), replacement := (: loc(bool_xor(bv1,bv2)) :), condition := true #)) tan9 : LEMMA correct?( (# pattern := (: loc(a), loc(n), shl :), replacement := (: loc(a * power(2, n)) :), condition := true #)) tan10 : LEMMA correct?( (# pattern := (: loc(a), loc(n), shr :), replacement := (: loc(div(a, power(2, n))) :), condition := true #)) tan11 : LEMMA correct?( (# pattern := (: loc(a), loc(bv), rol :), replacement := (: loc(rol_sem(a,bv)) :), condition := true #)) tan12 : LEMMA correct?( (# pattern := (: loc(a), loc(bv), ror :), replacement := (: loc(ror_sem(a,bv)) :), condition := true #)) tan13 : LEMMA correct?( (# pattern := (: loc(a), loc(b), cmi :), replacement := (: loc(cmi_sem(a,b)) :), condition := true #)) tan14 : LEMMA correct?( (# pattern := (: loc(a), neg :), replacement := (: loc((-1) * a) :), condition := true #)) tan15 : LEMMA correct?( (# pattern := (: loc(bv), com :), replacement := (: loc(bool_not(bv)) :), condition := true #)) tan16 : LEMMA correct?( (# pattern := (: neg,sub :), replacement := (: add :), condition := true #)) tan17 : LEMMA correct?( (# pattern := (: neg,add :), replacement := (: sub :), condition := true #)) tan18 : LEMMA correct?( (# pattern := (: loc(1),not :), replacement := (: loc(0) :), condition := true #)) tan19 : LEMMA correct?( (# pattern := (: loc(0),not :), replacement := (: loc(1) :), condition := true #)) % tan20 betr. Prozeduren tan21 : LEMMA correct?( (# pattern := (: adi(a),adi(b) :), replacement := (: adi(a + b) :), condition := true #)) END stack_m_pho1 $$$stack_m_pho1.prf (|stack_m_pho1| (IMPORTING2_TCC1 "" (GRIND) NIL) (|tan1| "" (PHO) NIL) (|tan2| "" (PHO) NIL) (|tan3| "" (PHO) NIL) (|tan4| "" (PHO) NIL) (|tan5| "" (PHO) NIL) (|tan6| "" (PHO :EXCLUDE ("bv2int" "int2bv" "exp2" "in_rng_2s_comp[16]" "maxint" "minint")) NIL) (|tan7| "" (PHO :EXCLUDE ("bv2int" "int2bv" "exp2" "in_rng_2s_comp[16]" "maxint" "minint")) NIL) (|tan8| "" (PHO :EXCLUDE ("bv2int" "int2bv" "exp2" "in_rng_2s_comp[16]" "maxint" "minint")) NIL) (|tan9| "" (PHO) NIL) (|tan10_TCC1| "" (SKOSIMP) (("" (USE "power_pos") (("" (ASSERT) NIL))))) (|tan10| "" (PHO) NIL) (|tan11| "" (PHO :EXCLUDE ("bv2int" "int2bv" "exp2" "in_rng_2s_comp[16]" "maxint" "minint")) NIL) (|tan12| "" (PHO :EXCLUDE ("bv2int" "int2bv" "exp2" "in_rng_2s_comp[16]" "maxint" "minint")) NIL) (|tan13| "" (PHO) NIL) (|tan14| "" (PHO) NIL) (|tan15| "" (PHO :REWRITES "xor_not" :EXCLUDE ("bv2int" "int2bv" "exp2" "in_rng_2s_comp[16]" "maxint" "minint")) NIL) (|tan16| "" (PHO) NIL) (|tan17| "" (PHO) NIL) (|tan18| "" (PHO) NIL) (|tan19| "" (PHO) NIL) (|tan21| "" (PHO) NIL)) $$$pho.pvs % --- peephole optimization scheme --- pho [Instr : TYPE, state : TYPE+, admissible? : [Instr -> pred[state]], effect : [i:Instr -> [(admissible?(i)) -> state]] ] : THEORY BEGIN Code : TYPE = list[Instr] c,c1,c2,fp,lp : VAR Code i : VAR nat % --- concatenation of code sequences ; ++(c1,c2) : Code = append(c1,c2) ; IMPORTING relation[state,state] srel : TYPE = Relation f,g : VAR srel s,s1,s2 : VAR state % --- state transformer ++ ++(f, g) : srel = LAMBDA s: image(g,f(s)) singleton_lem : COROLLARY (s1 = s2) IMPLIES (singleton(s1) = singleton(s2)) % -------- basic block interpreter interprete(c)(s) : RECURSIVE set[state] = CASES c OF null : singleton(s), cons(i,r) : IF admissible?(i)(s) THEN interprete(r)(effect(i)(s)) ELSE emptyset ENDIF ENDCASES MEASURE length(c) JUDGEMENT interprete HAS_TYPE [Code -> PartialFunction[state,state]] interprete_split : LEMMA interprete(c1 ++ c2) = interprete(c1) ++ interprete(c2) % --- semantic equality of two linear code sequences ; ==(c1,c2) : [state -> bool] = LAMBDA s: interprete(c1)(s) = interprete(c2)(s) ; % --- peephole optimization rules rule : TYPE = [# pattern : Code, replacement : Code, condition : pred[state] #] % --- correctness of a rule p1,p2 : VAR pred[state] ; IMPLIES(p1,p2) : bool = FORALL s: p1(s) IMPLIES p2(s) correct?(r:rule) : bool = condition(r) IMPLIES pattern(r) == replacement(r) correct_rule : TYPE = (correct?) % --- redundant basic blocks (null sequences) null_seq?(pat:Code, start_cond : pred[state]) : bool = correct?((# pattern := pat, replacement := null, condition := start_cond #)) pred_state2bool(p1) : bool = FORALL s: p1(s) CONVERSION pred_state2bool % === replace correct pattern within a basic block ==- % --- applicability of an optimization step w.r.t. condition ac % --- fp ++ pattern(r) ++ lp ====> fp ++ replacement(r) ++ lp % --- condition of r holds after fp has been interpreted r : VAR correct_rule ac : VAR pred[state] applicable?(r, fp) : bool = FORALL (start:state): interprete(fp)(start) IMPLIES condition(r) % --- rule application is correct applicable_equal : THEOREM applicable?(r, fp) IMPLIES fp ++ pattern(r) ++ lp == fp ++ replacement(r) ++ lp % --- apply a rule r to a sequence c % --- if r is not applicable to c, c is returned unchanged apply_rule1(r, c) : {cc : Code | (EXISTS (fp,lp:Code): c = fp ++ pattern(r) ++ lp & applicable?(r, fp) & cc = fp ++ replacement(r) ++ lp) OR (cc = c)} rule_application_correct1 : COROLLARY c == apply_rule1(r, c) % definition of first_n, cut_n, prefix? IMPORTING list_prop[Instr] TRUE : pred[state] = LAMBDA s: true % --- implementation of a simple peephole optimizer % looks for a match, tests applicability and applies rule if possible find_match(r:correct_rule, c:Code, n:{i | i <= length(c) + 1}) : RECURSIVE Code = IF n > length(c) THEN c ELSIF prefix?(pattern(r), cut_n(c, n)) % --- pattern(r) is sublist of b THEN LET fp = first_n(c, n), lp = cut_n(cut_n(c, n), length(pattern(r))) IN IF applicable?(r, fp) % --- condition(r) holds THEN fp ++ replacement(r) ++ lp ELSE find_match(r, c, n + 1) ENDIF ELSE find_match(r, c, n + 1) ENDIF MEASURE length(c) + 1 - n % --- application of a rule does not change b's semantics find_match_correct : LEMMA FORALL (r:correct_rule), (c:Code), (n:{i | i <= length(c) + 1}): c == find_match(r, c, n) % --- apply find_match, start with n = 0 apply_rule(r, c) : Code = find_match(r, c, 0) rule_application_correct : COROLLARY c == apply_rule(r, c) % --- apply a list rs of correct rules to a basic block b rule_set : TYPE = list[correct_rule] rs : VAR rule_set % --- a simple peephole optimizer pho(rs, c) : RECURSIVE Code = CASES rs OF null : c, cons(r,rest) : pho(rest, apply_rule(r, c)) ENDCASES MEASURE length(rs) % --- application of a correct rule set to c does not change c's semantics pho_correct : THEOREM c == pho(rs, c) END pho $$$pho.prf (|pho| (|singleton_lem| "" (GRIND) NIL) (|interprete_TCC1| "" (TERMINATION-TCC) NIL) (|interprete_TCC2| "" (INDUCT "x1") (("1" (SKOSIMP) (("1" (INST?) (("1" (INST?) NIL))))) ("2" (GRIND) NIL) ("3" (SKOSIMP*) (("3" (AUTO-REWRITE "interprete") (("3" (ASSERT) (("3" (BDDSIMP) (("1" (INST?) (("1" (INST?) NIL))) ("2" (GRIND) NIL))))))))))) (|interprete_split| "" (INDUCT "c1") (("1" (SKOSIMP*) (("1" (GRIND :DEFS T) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL))))))))) ("2" (SKOSIMP*) (("2" (AUTO-REWRITE-DEFS) (("2" (INST - "c2!1") (("2" (ASSERT) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (REPLACE*) (("2" (HIDE -1) (("2" (LIFT-IF) (("2" (BDDSIMP) (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (GRIND) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SKOSIMP* :PREDS? T) (("2" (GRIND) NIL))))))))))))))))))))))))))))) (|applicable_equal| "" (SKOSIMP* :PREDS? T) (("" (AUTO-REWRITE-DEFS) (("" (STOP-REWRITE "++") (("" (ASSERT) (("" (SKOSIMP*) (("" (REWRITE "interprete_split") (("" (REWRITE "interprete_split") (("" (REWRITE "interprete_split") (("" (REWRITE "interprete_split") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (EXPAND "++") (("" (ASSERT) (("" (BDDSIMP) (("1" (ASSERT) (("1" (AUTO-REWRITE-DEFS) (("1" (ASSERT) (("1" (SKOSIMP* :PREDS? T) (("1" (ASSERT) (("1" (SKOSIMP* :PREDS? T) (("1" (ASSERT) (("1" (INST + "s!2") (("1" (INST + "s!3") (("1" (INST - "s!3") (("1" (ASSERT) (("1" (INST - "s!1" "s!3") (("1" (ASSERT) NIL))))))))))))))))))))))))) ("2" (ASSERT) (("2" (AUTO-REWRITE-DEFS) (("2" (ASSERT) (("2" (SKOSIMP* :PREDS? T) (("2" (ASSERT) (("2" (SKOSIMP* :PREDS? T) (("2" (ASSERT) (("2" (INST + "s!2") (("2" (INST + "s!3") (("2" (ASSERT) (("2" (INST - "s!3") (("2" (ASSERT) (("2" (INST - "s!1" "s!3") (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))) (|apply_rule1_TCC1| "" (INST + "LAMBDA (d:[correct_rule, Code]): proj_2(d)") NIL) (|rule_application_correct1| "" (SKOSIMP* :PREDS? T) (("" (TYPEPRED "apply_rule1(r!1, c!1)") (("" (BDDSIMP) (("1" (SKOSIMP*) (("1" (USE "applicable_equal") (("1" (ASSERT) NIL))))) ("2" (REPLACE*) (("2" (GRIND) NIL))))))))) (|find_match_TCC1| "" (GRIND) NIL) (|find_match_TCC2| "" (GRIND) NIL) (|find_match_TCC3| "" (SKOSIMP* :PREDS? T) (("" (REWRITE "prefix_length") NIL))) (|find_match_TCC4| "" (GRIND) NIL) (|find_match_TCC5| "" (GRIND) NIL) (|find_match_TCC6| "" (GRIND) NIL) (|find_match_TCC7| "" (GRIND) NIL) (|find_match_correct| "" (MEASURE-INDUCT "length(c) + 1 - n" ("c" "n")) (("" (SKOSIMP* :PREDS? T) (("" (AUTO-REWRITE-DEFS) (("" (STOP-REWRITE "++") (("" (ASSERT) (("" (SKOSIMP*) (("" (CASE-REPLACE "x!2 = 1 + length(x!1)") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (LIFT-IF) (("2" (BETA) (("2" (LIFT-IF) (("2" (BDDSIMP +) (("1" (USE "sublist_lem") (("1" (ASSERT) (("1" (NAME-REPLACE "m1" "first_n(x!1, x!2)") (("1" (NAME-REPLACE "m2" "cut_n(cut_n(x!1, x!2), length(pattern(r!1)))") (("1" (REPLACE -1 +) (("1" (CASE-REPLACE "append(m1, append(pattern(r!1), m2)) = m1 ++ pattern(r!1) ++ m2") (("1" (REWRITE "interprete_split") (("1" (REWRITE "interprete_split") (("1" (REWRITE "interprete_split") (("1" (REWRITE "interprete_split") (("1" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("1" (IFF) (("1" (AUTO-REWRITE-DEFS) (("1" (HIDE -7) (("1" (ASSERT) (("1" (BDDSIMP) (("1" (SKOSIMP* :PREDS? T) (("1" (ASSERT) (("1" (SKOSIMP* :PREDS? T) (("1" (INST + "s!2") (("1" (INST + "s!3") (("1" (INST?) (("1" (INST?) (("1" (ASSERT) NIL))))))))))))))) ("2" (SKOSIMP* :PREDS? T) (("2" (ASSERT) (("2" (SKOSIMP* :PREDS? T) (("2" (INST + "s!2") (("2" (INST + "s!3") (("2" (ASSERT) (("2" (INST?) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))) ("2" (EXPAND "++" +) (("2" (REWRITE "append_assoc") NIL))))))) ("2" (STOP-REWRITE) (("2" (HIDE 3) (("2" (HIDE -5) (("2" (REWRITE "prefix_length") (("2" (REWRITE "prefix_length") NIL))))))))))))))))) ("2" (INST - "x!1" "x!2 + 1") (("2" (ASSERT) (("2" (INST?) (("2" (INST?) NIL))))))) ("3" (INST - "x!1" "x!2 + 1") (("3" (ASSERT) (("3" (INST?) (("3" (INST?) NIL))))))))))))))))))))))))))))))) (|apply_rule_TCC1| "" (GRIND) NIL) (|rule_application_correct| "" (SKOSIMP*) (("" (EXPAND "apply_rule") (("" (REWRITE "find_match_correct") NIL))))) (|pho_TCC1| "" (GRIND) NIL) (|pho_correct| "" (INDUCT "rs") (("1" (GRIND) NIL) ("2" (SKOSIMP* :PREDS? T) (("2" (AUTO-REWRITE-DEFS) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST?) (("2" (INST - "find_match(cons1_var!1, c!1, 0)" "s!1") (("2" (REPLACE -3 + RL) (("2" (USE "find_match_correct") (("2" (GRIND :DEFS !) NIL)))))))))))))))))))) $$$relation.pvs relation [A,B : TYPE] : THEORY BEGIN Relation : TYPE = [A -> set[B]] a : VAR A b : VAR B R : VAR Relation S : VAR set[A] T : VAR set[B] image(R,S) : set[B] = {y:B | EXISTS (s:(S)): member(y,R(s))} inverse_image(R,T) : set[A] = {x:A | subset?(R(x),T)} IMPORTING deterministic[B] PartialFunction : TYPE = [A -> (deterministic?[B])] strans : TYPE = PartialFunction END relation $$$relation.prf (|relation| (|choose_TCC1| "" (GRIND) NIL)) $$$deterministic.pvs deterministic [B : TYPE] : THEORY BEGIN S : VAR set[B] b : VAR B singleton?(S) : bool = exists1! b: member(b,S) deterministic?(S) : bool = empty?(S) OR singleton?(S) % select(S:(singleton?)) : B = choose(S) % CONVERSION select JUDGEMENT singleton HAS_TYPE [B -> (deterministic?)] JUDGEMENT emptyset HAS_TYPE (deterministic?) singleton_is_deterministic : LEMMA deterministic?(singleton[B](b)) emptyset_is_deterministic : LEMMA deterministic?(emptyset[B]) END deterministic $$$deterministic.prf (|deterministic| (|singleton_TCC1| "" (GRIND) NIL) (|emptyset_TCC1| "" (GRIND) NIL) (|singleton_is_deterministic| "" (SKOSIMP) (("" (ASSERT) NIL))) (|emptyset_is_deterministic| "" (ASSERT) NIL)) $$$list_prop.pvs list_prop [T:TYPE] : THEORY BEGIN n,i : VAR nat l,l1,pf,sl : VAR list[T] % --- l without last element lead(l) : RECURSIVE list[T] = IF null?(l) THEN l ELSIF null?(cdr(l)) THEN null ELSE cons(car(l), lead(cdr(l))) ENDIF MEASURE length(l) % --- prefix pf of l prefix?(pf,l) : RECURSIVE bool = IF null?(pf) THEN true ELSIF null?(l) THEN false ELSE (car(pf) = car(l) & prefix?(cdr(pf), cdr(l))) ENDIF MEASURE length(l) % --- first n elements of l first_n(l:list[T], n:{i | i <= length(l)}) : RECURSIVE list[T] = IF (n = 0) THEN null ELSE cons(car(l), first_n(cdr(l), n-1)) ENDIF MEASURE n % --- cut n elements of l cut_n(l:list[T], n:{i | i <= length(l)}) : RECURSIVE list[T] = IF (n = 0) then l ELSE cut_n(cdr(l), n-1) ENDIF MEASURE n % --- sublist sl of l sublist?(sl,l) : bool = EXISTS (n:{i | i <= length(l)}): prefix?(sl, cut_n(l, n)) firstn_cutn : LEMMA n <= length(l) IMPLIES append(first_n(l, n), cut_n(l, n)) = l prefix_length : LEMMA prefix?(sl, l) IMPLIES length(sl) <= length(l) prefix_cutn : LEMMA prefix?(sl, l) IMPLIES l = append(sl, cut_n(l, length(sl))) sublist_lem : LEMMA n <= length(l) IMPLIES prefix?(sl, cut_n(l, n)) IMPLIES l = append(first_n(l, n), append(sl, cut_n(cut_n(l, n), length(sl)))) END list_prop $$$list_prop.prf (|list_prop| (|lead_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL))) (|lead_TCC2| "" (SKOSIMP) (("" (EXPAND "length" 3 2) (("" (ASSERT) NIL))))) (|prefix?_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL))) (|prefix?_TCC2| "" (GRIND) NIL) (|first_n_TCC1| "" (GRIND) NIL) (|first_n_TCC2| "" (GRIND) (("" (CASE-REPLACE "null?(l!1)") (("1" (GRIND) NIL) ("2" (EXPAND "length" -) (("2" (ASSERT) NIL))))))) (|first_n_TCC3| "" (TERMINATION-TCC) NIL) (|firstn_cutn| "" (INDUCT "n") (("1" (GRIND) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "first_n" +) (("2" (CASE-REPLACE "null?(l!1)") (("1" (GRIND) NIL) ("2" (EXPAND "cut_n" +) (("2" (EXPAND "append" +) (("2" (INST - "cdr(l!1)") (("1" (ASSERT) (("1" (EXPAND "length" -2) (("1" (ASSERT) (("1" (REPLACE*) (("1" (ASSERT) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))))))) ("2" (ASSERT) NIL))))))))))))))) (|prefix_length| "" (INDUCT "l") (("1" (GRIND) (("1" (EXPAND "prefix?") (("1" (BDDSIMP) (("1" (ASSERT) NIL))))))) ("2" (SKOSIMP*) (("2" (AUTO-REWRITE-DEFS) (("2" (ASSERT) (("2" (CASE-REPLACE "null?(cons2_var!1)") (("1" (ASSERT) (("1" (GRIND) NIL))) ("2" (EXPAND "prefix?" -2) (("2" (BDDSIMP) (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (ASSERT) (("2" (INST - "cdr(sl!1)") (("1" (ASSERT) (("1" (EXPAND "length" 2 1) (("1" (LIFT-IF) (("1" (ASSERT) (("1" (BDDSIMP) (("1" (ASSERT) NIL))))))))))) ("2" (ASSERT) NIL))))))))))))))))))) (|prefix_cutn_TCC1| "" (SKOSIMP) (("" (REWRITE "prefix_length") NIL))) (|prefix_cutn| "" (INDUCT "sl") (("1" (GRIND) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "prefix?" -2) (("2" (BDDSIMP) (("2" (INST?) (("1" (ASSERT) (("1" (EXPAND "append" +) (("1" (EXPAND "cut_n" +) (("1" (ASSERT) (("1" (AUTO-REWRITE-DEFS) (("1" (ASSERT) (("1" (REPLACE -1 + RL) (("1" (REPLACE -2) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))))))))))))) ("2" (ASSERT) NIL))))))))) ("3" (GRIND) (("3" (REWRITE "prefix_length") NIL))))) (|sublist_lem_TCC1| "" (SKOSIMP) (("" (REWRITE "prefix_length") NIL))) (|sublist_lem| "" (SKOSIMP) (("" (USE "prefix_cutn") (("" (ASSERT) (("" (REPLACE -1 + RL) (("" (REWRITE "firstn_cutn") NIL)))))))))) $$$stack_m_pho2.pvs stack_m_pho2 : THEORY BEGIN IMPORTING stack_m_bv IMPORTING pho[sm_inst,state,sm_admissible,sm_ip] s : VAR state n : VAR ramadr % ---- strength reduction --- tan22 : LEMMA correct?( (# pattern := (: loc(2), lov(n), mul :), replacement := (: lov(n), loc(1), shl :), condition := true #)) tan23 : LEMMA correct?( (# pattern := (: loc(2), mul :), replacement := (: loc(1), shl :), condition := true #)) tan24 : LEMMA correct?( (# pattern := (: loc(4), mul :), replacement := (: loc(2), shl :), condition := true #)) tan25 : LEMMA correct?( (# pattern := (: loc(8), mul :), replacement := (: loc(3), shl :), condition := true #)) tan26 : LEMMA correct?( (# pattern := (: loc(16), mul :), replacement := (: loc(4), shl :), condition := true #)) tan27 : LEMMA correct?( (# pattern := (: loc(32), mul :), replacement := (: loc(5), shl :), condition := true #)) tan28 : LEMMA correct?( (# pattern := (: loc(-1), lov(n), mul :), replacement := (: lov(n), neg :), condition := true #)) END stack_m_pho2 $$$stack_m_pho2.prf (|stack_m_pho2| (IMPORTING2_TCC1 "" (SUBTYPE-TCC) NIL) (|tan22| "" (PHO) NIL) (|tan23| "" (PHO) NIL) (|tan24| "" (PHO) NIL) (|tan25| "" (PHO) NIL) (|tan26| "" (PHO) NIL) (|tan27| "" (PHO) NIL) (|tan28| "" (PHO) NIL)) $$$stack_m_pho3.pvs stack_m_pho3 : THEORY BEGIN IMPORTING stack_m_bv pho_inst : THEORY = pho[sm_inst,state,sm_admissible,sm_ip] s : VAR state n : VAR ramadr stack_lft(p:pred[Stack]) : pred[state] = LAMBDA s: p(stk(s)) CONVERSION stack_lft % ---- null sequences --- tan29 : LEMMA null_seq?((: adi(0) :), nonempty?) % tan30 betr. Prozeduren tan31 : LEMMA null_seq?((: neg,neg :), nonempty?) tan32 : LEMMA null_seq?((: loc(0), add :), nonempty?) tan33 : LEMMA null_seq?((: loc(0), sub :), nonempty?) tan34 : LEMMA null_seq?((: loc(1), mul :), nonempty?) tan35 : LEMMA null_seq?((: loc(1), div :), nonempty?) tan36 : LEMMA null_seq?((: loc(0), ior :), LAMBDA s: nonempty?(stk(s)) & in_rng_2s_comp[16](top(stk(s)))) tan37 : LEMMA null_seq?((: loc(0), xor :), LAMBDA s: nonempty?(stk(s)) & in_rng_2s_comp[16](top(stk(s)))) tan38 : LEMMA null_seq?((: lov(n), stv(n) :), true) tan39 : LEMMA null_seq?((: ldv(n), sdv(n) :), true) tan40 : LEMMA correct?( (# pattern := (: loc(0), lov(n), add :), replacement := (: lov(n) :), condition := true #)) tan41 : LEMMA correct?( (# pattern := (: loc(1), lov(n), mul :), replacement := (: lov(n) :), condition := true #)) tan42 : LEMMA correct?( (# pattern := (: loc(0), lov(n), mul :), replacement := (: loc(0) :), condition := true #)) tan43 : LEMMA correct?( (# pattern := (: lov(n), loc(0), mul :), replacement := (: loc(0) :), condition := true #)) % tan44, tan45 betr. Prozeduren tan46 : LEMMA correct?( (# pattern := (: loc(0), cmi, teq :), replacement := (: teq :), condition := true #)) % tan47 : bra(a), lab(a) ist kein BB END stack_m_pho3 $$$stack_m_pho3.prf (|stack_m_pho3| (|pho_inst_TCC1| "" (SUBTYPE-TCC) NIL) (|tan29| "" (PHO) NIL) (|tan31| "" (PHO) NIL) (|tan32| "" (PHO) NIL) (|tan33| "" (PHO) NIL) (|tan34| "" (PHO) NIL) (|tan35| "" (PHO) NIL) (|tan36| "" (PHO :REWRITES "ior_zero" :EXCLUDE ("bv2int" "int2bv" "exp2" "in_rng_2s_comp[16]")) NIL) (|tan37| "" (PHO :REWRITES "xor_zero" :EXCLUDE ("bv2int" "int2bv" "exp2" "in_rng_2s_comp[16]")) NIL) (|tan38| "" (PHO) NIL) (|tan39| "" (PHO) NIL) (|tan40| "" (PHO) NIL) (|tan41| "" (PHO) NIL) (|tan42| "" (PHO) NIL) (|tan43| "" (PHO) NIL) (|tan46| "" (PHO) NIL)) $$$stack_m_pho4.pvs stack_m_pho4 : THEORY BEGIN IMPORTING stack_m_bv % --- some useful properties IMPORTING stackm_props IMPORTING pho[sm_inst,state,sm_admissible,sm_ip] s : VAR state l,m,n : VAR ramadr a : VAR value stack_lft(p:pred[Stack]) : pred[state] = LAMBDA s: p(stk(s)) CONVERSION stack_lft tan48 : LEMMA correct?( (# pattern := (: lov(n), lov(n + 2) :), replacement := (: ldv(n) :), condition := true #)) tan49 : LEMMA correct?( (# pattern := (: ldv(n), lov(n + 4) :), replacement := (: lav(n), loi(6) :), condition := true #)) tan50 : LEMMA correct?( (# pattern := (: ldv(n), ldv(n + 4) :), replacement := (: lav(n), loi(8) :), condition := true #)) tan51 : LEMMA correct?( (# pattern := (: lav(n), loi(m), lov(n+m) :), replacement := (: lav(n), loi(m + 2) :), condition := true #)) tan52 : LEMMA correct?( (# pattern := (: lav(n), loi(m), ldv(n+m) :), replacement := (: lav(n), loi(m + 4) :), condition := true #)) tan53 : LEMMA correct?( (# pattern := (: lav(n), loi(m), lav(n+m), loi(l) :), replacement := (: lav(n), loi(m + l) :), condition := true #)) tan54 : LEMMA correct?( (# pattern := (: lav(n), sti(m), loc(a), stv(n+m) :), replacement := (: loc(a), lav(n), sti(m + 2) :), condition := LAMBDA s: n_tops?(stk(s), div2(m)) & n_tops?(push(a, stk(s)), div2(m+2)) #)) tan55 : LEMMA correct?( (# pattern := (: lav(n), sti(m), lov(l), stv(n+m) :), replacement := (: lov(l), lav(n), sti(m + 2) :), condition := LAMBDA s: n_tops?(stk(s), div2(m)) & n_tops?(push(mem(s)(l),stk(s)), div2(m+2)) & (l >= (n + m) OR (l < n)) #)) END stack_m_pho4 $$$stack_m_pho4.prf (|stack_m_pho4| (IMPORTING3_TCC1 "" (SUBTYPE-TCC) NIL) (|tan48_TCC1| "" (SUBTYPE-TCC) NIL) (|tan48| "" (PHO) NIL) (|tan49_TCC1| "" (SUBTYPE-TCC) NIL) (|tan49_TCC2| "" (GRIND) NIL) (|tan49| "" (PHO) NIL) (|tan50_TCC1| "" (SUBTYPE-TCC) NIL) (|tan50| "" (PHO) NIL) (|tan51| "" (PHO :THEORIES "even") NIL) (|tan52| "" (PHO :THEORIES "even") NIL) (|tan53| "" (PHO :THEORIES ("even" "stack_m_bv" "stackm_props")) NIL) (|tan54| "" (GRIND) (("" (REWRITE "singleton_lem") (("1" (REWRITE "two_times_div") (("1" (ASSERT) (("1" (CASE-REPLACE "s!1 WITH [(stk) := stk(s!1)] = s!1") (("1" (CASE-REPLACE "sti_aux(s!1, n!1, div2(m!1)) WITH [(mem)(m!1 + n!1) := a!1, (stk) := stk(sti_aux(s!1, n!1, div2(m!1)))] = sti_aux(s!1, n!1, div2(m!1)) WITH [(mem)(m!1 + n!1) := a!1]") (("1" (HIDE 2) (("1" (CASE-REPLACE "s!1 WITH [(mem)(m!1 + n!1) := a!1, (stk) := stk(s!1)] = s!1 WITH [(mem)(m!1 + n!1) := a!1]") (("1" (LEMMA "sti_prop") (("1" (INST - "m!1 + n!1" "s!1" "n!1" "div2(m!1)" "a!1") (("1" (ASSERT) (("1" (REWRITE "two_times_div") (("1" (ASSERT) NIL))))))))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))) ("2" (REWRITE "two_times_div") (("2" (REWRITE "add_closed") NIL))))))) (|tan55| "" (SKOSIMP* :PREDS? T) (("" (AUTO-REWRITE-DEFS) (("" (AUTO-REWRITE-THEORIES ("even" "stack_m")) (("" (ASSERT) (("" (SKOSIMP* :PREDS? T) (("" (ASSERT) (("" (REWRITE "singleton_lem") (("" (HIDE 2) (("" (CASE-REPLACE "s!1 WITH [(stk) := stk(s!1)] = s!1") (("1" (CASE-REPLACE "sti_aux(s!1, n!1, div2(m!1)) WITH [(mem)(m!1 + n!1) := mem(sti_aux(s!1, n!1, div2(m!1)))(l!1), (stk) := stk(sti_aux(s!1, n!1, div2(m!1)))] = sti_aux(s!1, n!1, div2(m!1)) WITH [(mem)(m!1 + n!1) := mem(sti_aux(s!1, n!1, div2(m!1)))(l!1)]") (("1" (CASE-REPLACE "s!1 WITH [(mem)(m!1 + n!1) := mem(s!1)(l!1), (stk) := stk(s!1)] = s!1 WITH [(mem)(m!1 + n!1) := mem(s!1)(l!1)]") (("1" (LEMMA "sti_prop2") (("1" (INST - "l!1" "n!1" "div2(m!1)" "s!1") (("1" (ASSERT) (("1" (LEMMA "sti_prop") (("1" (INST - "m!1 + n!1" "s!1" "n!1" "div2(m!1)" "mem(s!1)(l!1)") (("1" (ASSERT) NIL))))))))))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL)))))))))))))))))))) $$$stack_m_pho5.pvs stack_m_pho5 : THEORY BEGIN IMPORTING stack_m_bv IMPORTING stackm_props IMPORTING pho[sm_inst,state,sm_admissible,sm_ip] s : VAR state m,n : VAR ramadr a : VAR value stack_lft(p:pred[Stack]) : pred[state] = LAMBDA s: p(stk(s)) CONVERSION stack_lft % ---- null sequences --- tan56 : LEMMA n >= 2 IMPLIES correct?( (# pattern := (: stv(n), stv(n - 2) :), replacement := (: sdv(n - 2) :), condition := true #)) tan57 : LEMMA n >= 2 IMPLIES correct?( (# pattern := (: sdv(n), stv(n - 2) :), replacement := (: lav(n - 2), sti(6) :), condition := true #)) tan58 : LEMMA n >= 4 IMPLIES correct?( (# pattern := (: sdv(n), sdv(n - 4) :), replacement := (: lav(n-4), sti(8) :), condition := true #)) tan59 : LEMMA n >= 2 IMPLIES correct?( (# pattern := (: lav(n), sti(m), stv(n-2) :), replacement := (: lav(n-2), sti(m + 2) :), condition := LAMBDA s: n_tops?(stk(s), div2(m + 2)) #)) tan60 : LEMMA n >= 4 IMPLIES correct?( (# pattern := (: lav(n), sti(m), sdv(n-4) :), replacement := (: lav(n - 4), sti(m + 4) :), condition := LAMBDA s: n_tops?(stk(s), div2(m + 4)) #)) tan61 : LEMMA correct?( (# pattern := (: stv(n), loc(a), stv(n + 2) :), replacement := (: loc(a), sdv(n) :), condition := true #)) % tan62_wrong : LEMMA correct?( % (# pattern := (: stv(n), lov(m), stv(n + 2) :), % replacement := (: lov(m), sdv(n) :), % condition := true #)) tan62 : LEMMA correct?( (# pattern := (: stv(n), lov(m), stv(n + 2) :), replacement := (: lov(m), sdv(n) :), condition := LAMBDA s: n /= m #)) tan63 : LEMMA correct?( (# pattern := (: sdv(n), loc(a), stv(n + 4) :), replacement := (: loc(a), lav(n), sti(6) :), condition := true #)) tan64 : LEMMA correct?( (# pattern := (: lav(n), blm(2) :), replacement := (: loi(2), stv(n) :), condition := true #)) tan65 : LEMMA correct?( (# pattern := (: lav(n), blm(4) :), replacement := (: loi(4), sdv(n) :), condition := LAMBDA s: nonempty?(stk(s)) & top(stk(s)) /= n + 2 #)) tan66 : LEMMA correct?( (# pattern := (: lov(n), blm(2) :), replacement := (: loi(2), stp(n) :), condition := true #)) END stack_m_pho5 $$$stack_m_pho5.prf (|stack_m_pho5| (IMPORTING3_TCC1 "" (SUBTYPE-TCC) NIL) (|tan56_TCC1| "" (SUBTYPE-TCC) NIL) (|tan56_TCC2| "" (SUBTYPE-TCC) NIL) (|tan56| "" (PHO) NIL) (|tan57_TCC1| "" (SUBTYPE-TCC) NIL) (|tan57| "" (PHO) NIL) (|tan58_TCC1| "" (SUBTYPE-TCC) NIL) (|tan58_TCC2| "" (SUBTYPE-TCC) NIL) (|tan58_TCC3| "" (SUBTYPE-TCC) NIL) (|tan58| "" (PHO) NIL) (|tan59_TCC1| "" (SUBTYPE-TCC) NIL) (|tan59| "" (GRIND) (("1" (REWRITE "singleton_lem") (("1" (HIDE 2) (("1" (REWRITE "two_times_div") (("1" (CASE-REPLACE "s!1 WITH [(stk) := stk(s!1)] = s!1") (("1" (USE "sti_prop3") (("1" (REWRITE "two_times_div") (("1" (ASSERT) NIL))))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))) ("2" (REWRITE "two_times_div") (("2" (STOP-REWRITE) (("2" (LEMMA "add_closed") (("2" (INST - "m!1" "n!1 - 2") (("2" (ASSERT) NIL))))))))))) ("2" (LEMMA "sti_stack_prop") (("2" (CASE-REPLACE "s!1 WITH [(stk) := stk(s!1)] = s!1") (("1" (INST - "n!1" "div2(m!1)" "s!1") (("1" (ASSERT) NIL))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))) ("3" (USE "n_tops_prop") (("3" (ASSERT) NIL))))) (|tan60_TCC1| "" (SUBTYPE-TCC) NIL) (|tan60| "" (GRIND) (("1" (CASE-REPLACE "s!1 WITH [(stk) := stk(s!1)] = s!1") (("1" (REWRITE "two_times_div") (("1" (ASSERT) (("1" (LEMMA "sti_prop4") (("1" (INST - "n!1" "div2(m!1)" "s!1") (("1" (REWRITE "two_times_div") (("1" (ASSERT) NIL))))))))))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))) ("2" (CASE-REPLACE "s!1 WITH [(stk) := stk(s!1)] = s!1") (("1" (LEMMA "sti_stack_prop") (("1" (HIDE 2) (("1" (LEMMA "sti_stack_prop2") (("1" (INST?) (("1" (ASSERT) NIL))))))))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))) ("3" (CASE-REPLACE "s!1 WITH [(stk) := stk(s!1)] = s!1") (("1" (LEMMA "sti_stack_prop") (("1" (INST?) (("1" (ASSERT) (("1" (LEMMA "n_tops_prop") (("1" (INST - "div2(m!1)" "pop(stk(s!1))") (("1" (ASSERT) NIL))))))))))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))) ("4" (LEMMA "n_tops_prop") (("4" (INST? :SUBST ("st" "stk(s!1)")) (("4" (ASSERT) (("4" (LEMMA "n_tops_prop") (("4" (INST? :SUBST ("st" "pop(stk(s!1))")) (("4" (ASSERT) NIL))))))))))))) (|tan61_TCC1| "" (SUBTYPE-TCC) NIL) (|tan61| "" (PHO) NIL) (|tan62| "" (PHO) NIL) (|tan63_TCC1| "" (SUBTYPE-TCC) NIL) (|tan63_TCC2| "" (SUBTYPE-TCC) NIL) (|tan63| "" (PHO) NIL) (|tan64_TCC1| "" (SUBTYPE-TCC) NIL) (|tan64| "" (PHO) (("1" (EXPAND "blm_aux") (("1" (PROPAX) NIL))) ("2" (EXPAND "blm_aux") (("2" (PROPAX) NIL))))) (|tan65_TCC1| "" (SUBTYPE-TCC) NIL) (|tan65| "" (PHO) (("1" (EXPAND "blm_aux") (("1" (EXPAND "blm_aux") (("1" (PROPAX) NIL))))) ("2" (EXPAND "blm_aux") (("2" (EXPAND "blm_aux") (("2" (PROPAX) NIL))))) ("3" (EXPAND "blm_aux") (("3" (EXPAND "blm_aux") (("3" (PROPAX) NIL))))))) (|tan66| "" (PHO :EXCLUDE "even") (("1" (EXPAND "blm_aux") (("1" (PROPAX) NIL))) ("2" (EXPAND "blm_aux") (("2" (PROPAX) NIL)))))) $$$stack_m_pho6.pvs stack_m_pho6 : THEORY BEGIN IMPORTING stack_m_bv IMPORTING stackm_props IMPORTING pho[sm_inst,state,sm_admissible,sm_ip] s : VAR state m,n : VAR ramadr stack_lft(p:pred[Stack]) : pred[state] = LAMBDA s: p(stk(s)) CONVERSION stack_lft tan67 : LEMMA n >= 2 IMPLIES correct?( (# pattern := (: lov(n), lov(n - 2), add :), replacement := (: ldv(n - 2), add :), condition := true #)) tan68 : LEMMA n >= 2 IMPLIES correct?( (# pattern := (: lov(n), lov(n - 2), mul :), replacement := (: ldv(n - 2), mul :), condition := true #)) tan69 : LEMMA n >= 2 IMPLIES correct?( (# pattern := (: lov(n), lov(n - 2), cmi, teq :), replacement := (: ldv(n - 2), cmi, teq :), condition := true #)) % --- tan70 contains a jumps %tan70 : LEMMA n >= 2 IMPLIES % correct?( % (# pattern := (: lov(n), lov(n - 2), beq(k) :), % replacement := (: ldv(n - 2), beq(k) :), % condition := true #)) tan71 : LEMMA correct?( (# pattern := (: lav(n), loi(2) :), replacement := (: lov(n) :), condition := true #)) tan72 : LEMMA correct?( (# pattern := (: lav(n), sti(2) :), replacement := (: stv(n) :), condition := true #)) tan73 : LEMMA correct?( (# pattern := (: lav(n), lof(m) :), replacement := (: lov(n+m) :), condition := true #)) tan74 : LEMMA correct?( (# pattern := (: lav(n), stf(m) :), replacement := (: stv(n+m) :), condition := true #)) tan75 : LEMMA correct?( (# pattern := (: lov(n), loi(2) :), replacement := (: lop(n) :), condition := true #)) tan76 : LEMMA correct?( (# pattern := (: lov(n), sti(2) :), replacement := (: stp(n) :), condition := true #)) tan77 : LEMMA correct?( (# pattern := (: lav(n), adi(m) :), replacement := (: lav(n+m) :), condition := true #)) % -- tan78 is wrong, correct version: (corresponds to No. 59) tan78 : LEMMA n >= 2 IMPLIES correct?( (# pattern := (: lav(n), sti(m), stv(n - 2) :), replacement := (: lav(n - 2), sti(m + 2) :), condition := LAMBDA s: n_tops?(stk(s), div2(m + 2)) #)) % -- tan79 is wrong, correct version: (corresponds to No. 60) tan79 : LEMMA n >= 4 IMPLIES correct?( (# pattern := (: lav(n), sti(m), sdv(n - 4) :), replacement := (: lav(n - 4), sti(m + 4) :), condition := LAMBDA s: n_tops?(stk(s), div2(m + 4)) #)) tan80 : LEMMA correct?( (# pattern := (: lav(n), loi(4) :), replacement := (: ldv(n) :), condition := true #)) tan81 : LEMMA correct?( (# pattern := (: lav(n), sti(4) :), replacement := (: sdv(n) :), condition := true #)) % --- incorrect rule %tan81_wrong : LEMMA % correct?( % (# pattern := (: lav(n), sti(4) :), % replacement := (: sdf(n) :), % condition := true #)) tan82 : LEMMA correct?( (# pattern := (: lav(n), ldf(m) :), replacement := (: ldv(n+m) :), condition := true #)) tan83 : LEMMA correct?( (# pattern := (: lav(n), sdf(m) :), replacement := (: sdv(n+m) :), condition := true #)) END stack_m_pho6 $$$stack_m_pho6.prf (|stack_m_pho6| (IMPORTING3_TCC1 "" (SUBTYPE-TCC) NIL) (|tan67_TCC1| "" (SUBTYPE-TCC) NIL) (|tan67_TCC2| "" (SUBTYPE-TCC) NIL) (|tan67| "" (PHO) NIL) (|tan68| "" (PHO) NIL) (|tan69| "" (PHO) NIL) (|tan71_TCC1| "" (SUBTYPE-TCC) NIL) (|tan71| "" (PHO) NIL) (|tan72| "" (PHO) NIL) (|tan73| "" (PHO) NIL) (|tan74| "" (PHO) NIL) (|tan75| "" (PHO) NIL) (|tan76| "" (PHO) NIL) (|tan77| "" (PHO) NIL) (|tan78_TCC1| "" (SUBTYPE-TCC) NIL) (|tan78| "" (GRIND) (("1" (REWRITE "singleton_lem") (("1" (HIDE 2) (("1" (REWRITE "two_times_div") (("1" (CASE-REPLACE "s!1 WITH [(stk) := stk(s!1)] = s!1") (("1" (USE "sti_prop3") (("1" (REWRITE "two_times_div") (("1" (ASSERT) NIL))))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))) ("2" (REWRITE "two_times_div") (("2" (STOP-REWRITE) (("2" (LEMMA "add_closed") (("2" (INST - "m!1" "n!1 - 2") (("2" (ASSERT) NIL))))))))))) ("2" (LEMMA "sti_stack_prop") (("2" (CASE-REPLACE "s!1 WITH [(stk) := stk(s!1)] = s!1") (("1" (INST - "n!1" "div2(m!1)" "s!1") (("1" (ASSERT) NIL))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))) ("3" (USE "n_tops_prop") (("3" (ASSERT) NIL))))) (|tan79_TCC1| "" (SUBTYPE-TCC) NIL) (|tan79_TCC2| "" (SUBTYPE-TCC) NIL) (|tan79_TCC3| "" (SUBTYPE-TCC) NIL) (|tan79| "" (GRIND) (("1" (CASE-REPLACE "s!1 WITH [(stk) := stk(s!1)] = s!1") (("1" (REWRITE "two_times_div") (("1" (ASSERT) (("1" (LEMMA "sti_prop4") (("1" (INST - "n!1" "div2(m!1)" "s!1") (("1" (REWRITE "two_times_div") (("1" (ASSERT) NIL))))))))))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))) ("2" (CASE-REPLACE "s!1 WITH [(stk) := stk(s!1)] = s!1") (("1" (LEMMA "sti_stack_prop") (("1" (HIDE 2) (("1" (LEMMA "sti_stack_prop2") (("1" (INST?) (("1" (ASSERT) NIL))))))))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))) ("3" (CASE-REPLACE "s!1 WITH [(stk) := stk(s!1)] = s!1") (("1" (LEMMA "sti_stack_prop") (("1" (INST?) (("1" (ASSERT) (("1" (LEMMA "n_tops_prop") (("1" (INST - "div2(m!1)" "pop(stk(s!1))") (("1" (ASSERT) NIL))))))))))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))) ("4" (LEMMA "n_tops_prop") (("4" (INST? :SUBST ("st" "stk(s!1)")) (("4" (ASSERT) (("4" (LEMMA "n_tops_prop") (("4" (INST? :SUBST ("st" "pop(stk(s!1))")) (("4" (ASSERT) NIL))))))))))))) (|tan80_TCC1| "" (SUBTYPE-TCC) NIL) (|tan80| "" (PHO) NIL) (|tan81| "" (PHO) NIL) (|tan82| "" (PHO) NIL) (|tan83| "" (PHO) NIL)) $$$stack_m_pho7.pvs stack_m_pho7 : THEORY BEGIN IMPORTING stack_m_bv IMPORTING pho[sm_inst,state,sm_admissible,sm_ip] s : VAR state m,n : VAR ramadr tan84 : LEMMA correct?( (# pattern := (: adi(n), loi(2) :), replacement := (: lof(n) :), condition := true #)) tan85 : LEMMA correct?( (# pattern := (: adi(n), lof(m) :), replacement := (: lof(n+m) :), condition := true #)) tan86 : LEMMA correct?( (# pattern := (: adi(n), sti(2) :), replacement := (: stf(n) :), condition := true #)) tan87 : LEMMA correct?( (# pattern := (: adi(n), stf(m) :), replacement := (: stf(n+m) :), condition := true #)) tan88 : LEMMA correct?( (# pattern := (: adi(n), loi(4) :), replacement := (: ldf(n) :), condition := true #)) tan89 : LEMMA correct?( (# pattern := (: adi(n), sti(4) :), replacement := (: sdf(n) :), condition := true #)) tan90 : LEMMA correct?( (# pattern := (: adi(n), ldf(m) :), replacement := (: ldf(n+m) :), condition := true #)) tan91 : LEMMA correct?( (# pattern := (: adi(n), sdf(m) :), replacement := (: sdf(n+m) :), condition := true #)) % tan92, tan93 contain jumps tan94 : LEMMA correct?( (# pattern := (: tlt, teq :), replacement := (: tge :), condition := true #)) % tan95, tan96 contain jumps END stack_m_pho7 $$$stack_m_pho7.prf (|stack_m_pho7| (IMPORTING2_TCC1 "" (SUBTYPE-TCC) NIL) (|tan84_TCC1| "" (GRIND) NIL) (|tan84_TCC2| "" (SUBTYPE-TCC) NIL) (|tan84_TCC3| "" (SUBTYPE-TCC) NIL) (|tan84| "" (PHO :EXCLUDE "even") NIL) (|tan85_TCC1| "" (SUBTYPE-TCC) NIL) (|tan85_TCC2| "" (SUBTYPE-TCC) NIL) (|tan85| "" (PHO :EXCLUDE "even") NIL) (|tan86_TCC1| "" (SUBTYPE-TCC) NIL) (|tan86_TCC2| "" (SUBTYPE-TCC) NIL) (|tan86| "" (PHO :EXCLUDE "even") NIL) (|tan87_TCC1| "" (SUBTYPE-TCC) NIL) (|tan87_TCC2| "" (SUBTYPE-TCC) NIL) (|tan87| "" (PHO :EXCLUDE "even") NIL) (|tan88_TCC1| "" (GRIND) NIL) (|tan88_TCC2| "" (SUBTYPE-TCC) NIL) (|tan88_TCC3| "" (SUBTYPE-TCC) NIL) (|tan88| "" (PHO :EXCLUDE "even") NIL) (|tan89_TCC1| "" (SUBTYPE-TCC) NIL) (|tan89_TCC2| "" (SUBTYPE-TCC) NIL) (|tan89| "" (PHO :EXCLUDE "even") NIL) (|tan90_TCC1| "" (SUBTYPE-TCC) NIL) (|tan90_TCC2| "" (SUBTYPE-TCC) NIL) (|tan90| "" (PHO :EXCLUDE "even") NIL) (|tan91_TCC1| "" (SUBTYPE-TCC) NIL) (|tan91_TCC2| "" (SUBTYPE-TCC) NIL) (|tan91| "" (PHO :EXCLUDE "even") NIL) (|tan92_TCC1| "" (SUBTYPE-TCC) NIL) (|tan92_TCC2| "" (SUBTYPE-TCC) NIL) (|tan92| "" (PHO) NIL) (|tan93_TCC1| "" (SUBTYPE-TCC) NIL) (|tan93_TCC2| "" (SUBTYPE-TCC) NIL) (|tan93| "" (PHO) NIL) (|tan94_TCC1| "" (SUBTYPE-TCC) NIL) (|tan94_TCC2| "" (SUBTYPE-TCC) NIL) (|tan94| "" (PHO) NIL) (|tan95_TCC1| "" (SUBTYPE-TCC) NIL) (|tan95_TCC2| "" (SUBTYPE-TCC) NIL) (|tan95| "" (PHO) NIL) (|tan96_TCC1| "" (SUBTYPE-TCC) NIL) (|tan96_TCC2| "" (SUBTYPE-TCC) NIL) (|tan96| "" (PHO) NIL)) $$$stack_m_pho8.pvs stack_m_pho8 : THEORY BEGIN IMPORTING stack_m_bv IMPORTING pho[sm_inst,state,sm_admissible,sm_ip] s : VAR state n : VAR ramadr tan97 : LEMMA correct?( (# pattern := (: loc(1), add :), replacement := (: inc :), condition := true #)) tan98 : LEMMA correct?( (# pattern := (: loc(1), sub :), replacement := (: dec :), condition := true #)) tan99 : LEMMA correct?( (# pattern := (: lov(n), inc, stv(n) :), replacement := (: inv(n) :), condition := true #)) tan100 : LEMMA correct?( (# pattern := (: lov(n), dec, stv(n) :), replacement := (: dev(n) :), condition := true #)) tan101 : LEMMA correct?( (# pattern := (: loc(-1), sub :), replacement := (: inc :), condition := true #)) tan102 : LEMMA correct?( (# pattern := (: loc(-1), add :), replacement := (: dec :), condition := true #)) tan103 : LEMMA correct?( (# pattern := (: loc(1), lov(n), add :), replacement := (: lov(n), inc :), condition := true #)) tan104 : LEMMA correct?( (# pattern := (: loc(-1), lov(n), add :), replacement := (: lov(n), dec :), condition := true #)) tan105 : LEMMA correct?( (# pattern := (: lov(n), loc(2), add, stv(n) :), replacement := (: inv(n), inv(n) :), condition := true #)) tan106 : LEMMA correct?( (# pattern := (: loc(2), lov(n), add, stv(n) :), replacement := (: inv(n), inv(n) :), condition := true #)) tan107 : LEMMA correct?( (# pattern := (: lov(n), loc(2), sub, stv(n) :), replacement := (: dev(n), dev(n) :), condition := true #)) tan108 : LEMMA correct?( (# pattern := (: loc(-1), mul :), replacement := (: neg :), condition := true #)) END stack_m_pho8 $$$stack_m_pho8.prf (|stack_m_pho8| (IMPORTING2_TCC1 "" (SUBTYPE-TCC) NIL) (|tan97_TCC1| "" (SUBTYPE-TCC) NIL) (|tan97_TCC2| "" (SUBTYPE-TCC) NIL) (|tan97| "" (PHO) NIL) (|tan98_TCC1| "" (SUBTYPE-TCC) NIL) (|tan98_TCC2| "" (SUBTYPE-TCC) NIL) (|tan98| "" (PHO) NIL) (|tan99_TCC1| "" (SUBTYPE-TCC) NIL) (|tan99_TCC2| "" (SUBTYPE-TCC) NIL) (|tan99| "" (PHO) NIL) (|tan100_TCC1| "" (SUBTYPE-TCC) NIL) (|tan100_TCC2| "" (SUBTYPE-TCC) NIL) (|tan100| "" (PHO) NIL) (|tan101_TCC1| "" (SUBTYPE-TCC) NIL) (|tan101| "" (PHO) NIL) (|tan102_TCC1| "" (SUBTYPE-TCC) NIL) (|tan102| "" (PHO) NIL) (|tan103_TCC1| "" (SUBTYPE-TCC) NIL) (|tan103_TCC2| "" (SUBTYPE-TCC) NIL) (|tan103| "" (PHO) NIL) (|tan104_TCC1| "" (SUBTYPE-TCC) NIL) (|tan104_TCC2| "" (SUBTYPE-TCC) NIL) (|tan104| "" (PHO) NIL) (|tan105_TCC1| "" (SUBTYPE-TCC) NIL) (|tan105_TCC2| "" (SUBTYPE-TCC) NIL) (|tan105| "" (PHO) NIL) (|tan106_TCC1| "" (SUBTYPE-TCC) NIL) (|tan106| "" (PHO) NIL) (|tan107_TCC1| "" (SUBTYPE-TCC) NIL) (|tan107_TCC2| "" (SUBTYPE-TCC) NIL) (|tan107| "" (PHO) NIL) (|tan108_TCC1| "" (SUBTYPE-TCC) NIL) (|tan108_TCC2| "" (SUBTYPE-TCC) NIL) (|tan108| "" (PHO) NIL)) $$$stack_m_pho9.pvs stack_m_pho9 : THEORY BEGIN IMPORTING stack_m_bv IMPORTING pho[sm_inst,state,sm_admissible,sm_ip] s : VAR state n : VAR ramadr a : VAR value tan109 : LEMMA correct?( (# pattern := (: loc(-1), div :), replacement := (: neg :), condition := true #)) tan110 : LEMMA correct?( (# pattern := (: loc(0), stv(n) :), replacement := (: zrv(n) :), condition := true #)) % --- tan111 - tan115 contain jumps tan116 : LEMMA correct?( (# pattern := (: stv(n), lov(n) :), replacement := (: dup, stv(n) :), condition := true #)) tan117 : LEMMA correct?( (# pattern := (: lov(n), lov(n) :), replacement := (: lov(n), dup :), condition := true #)) tan118 : LEMMA correct?( (# pattern := (: add, loc(a), add :), replacement := (: loc(a), add, add :), condition := true #)) tan119 : LEMMA correct?( (# pattern := (: add, loc(a), sub :), replacement := (: loc(a), sub, add :), condition := true #)) tan120 : LEMMA correct?( (# pattern := (: sub, loc(a), add :), replacement := (: loc(a), sub, sub :), condition := true #)) tan121 : LEMMA correct?( (# pattern := (: sub, loc(a), sub :), replacement := (: loc(a), add, sub :), condition := true #)) tan122 : LEMMA correct?( (# pattern := (: mul, neg :), replacement := (: neg, mul :), condition := true #)) tan123 : LEMMA correct?( (# pattern := (: div, neg :), replacement := (: neg, div :), condition := true #)) END stack_m_pho9 $$$stack_m_pho9.prf (|stack_m_pho9| (IMPORTING2_TCC1 "" (SUBTYPE-TCC) NIL) (|tan109| "" (PHO :THEORIES "div" :EXCLUDE "div") NIL) (|tan110| "" (PHO) NIL) (|tan116| "" (PHO) NIL) (|tan117| "" (PHO) NIL) (|tan118| "" (PHO) NIL) (|tan119| "" (PHO) NIL) (|tan120| "" (PHO) NIL) (|tan121| "" (PHO) NIL) (|tan122| "" (PHO) NIL) (|tan123| "" (PHO) NIL)) $$$tam_top.pvs % Peephole Optimizations on a 2-address machine tam_top : THEORY BEGIN IMPORTING tam IMPORTING tam_pho END tam_top $$$tam.pvs % A PDP-11 like two-address machine sketched in [DavFra80] and [Eck75]. % Integer arithmetic is used. tam : THEORY BEGIN % -------- basics --------------------------------------- % the machine consists of 7 general purpose register regnumber : TYPE = {n : nat | n <= 7} value : TYPE = int adr : TYPE = nat reg_file : TYPE = [regnumber -> value] memory : TYPE = [adr -> value] status_value : TYPE = {i:integer | (i = -1) OR (i = 0) OR (i = 1)} % 0 = result is positive, 1 = result is zero, -1 = result is negative set_status(i:value): status_value = IF (i > 0) THEN 0 ELSIF (i = 0) THEN 1 ELSE -1 ENDIF IMPORTING even % ----------- state ------ state : TYPE = [# mem : memory, reg : reg_file, flag : status_value #] s : VAR state % ---------- addressing modes -- Mode : DATATYPE BEGIN reg(reg_n:regnumber) : reg_word? autoinc(autoi_n:regnumber) : autoinc_word? autodec(autod_n:regnumber) : autodec_word? index_adr(ind_n1:adr, ind_n2:regnumber) : index_word? single_adr(single_n:adr) : single_adr_word? lit_value(li_n:value) : lit_value_word? END Mode % reference can be direct or indirect AMode : DATATYPE BEGIN direct(w_dir:Mode) : direct? indirect(w_ind:Mode) : indirect? END AMode % ----------- preconditions for the addressing modes -------- % memory addresses have to be positive! admissible_word(w:AMode) : pred[state] = LAMBDA s: CASES w OF direct(w1) : CASES w1 OF reg(n) : true, autoinc(n) : reg(s)(n) >= 0, autodec(n) : reg(s)(n) - 2 >= 0, index_adr(x,n) : reg(s)(n) + x >= 0, single_adr(x) : true, lit_value(i) : true ENDCASES, indirect(w1) : CASES w1 OF reg(n) : reg(s)(n) >= 0, autoinc(n) : reg(s)(n) >= 0 & mem(s)(reg(s)(n)) >= 0, autodec(n) : reg(s)(n) - 2 >= 0 & mem(s)(reg(s)(n) - 2) >= 0, index_adr(x,n) : reg(s)(n) + x >= 0 & mem(s)(reg(s)(n) + x) >= 0, single_adr(x) : mem(s)(x) >= 0, lit_value(i) : i >= 0 ENDCASES ENDCASES % ------- Semantics of (admissible) addressing modes ---------------- AMode_sem(w:AMode)(s:{s1:state | (admissible_word(w))(s1)}) : value = CASES w OF direct(w1) : CASES w1 OF reg(n) : reg(s)(n), autoinc(n) : mem(s)(reg(s)(n)), autodec(n) : mem(s)(reg(s)(n) - 2), index_adr(x,n) : mem(s)(reg(s)(n) + x), single_adr(x) : mem(s)(x), lit_value(i) : i ENDCASES, indirect(w1) : CASES w1 OF reg(n) : mem(s)(reg(s)(n)), autoinc(n) : mem(s)(mem(s)(reg(s)(n))), autodec(n) : mem(s)(mem(s)(reg(s)(n) - 2)), index_adr(x,n) : mem(s)(reg(s)(n) + x), single_adr(x) : mem(s)(mem(s)(x)), lit_value(i) : mem(s)(i) ENDCASES ENDCASES % ----------- Instruction Set ------------ % immed mode (lit_value - mode) direct can only be used by some instructions not_dir_immed_mode?(w:AMode) : bool = CASES w OF direct(w1) : CASES w1 OF lit_value(i) : false ELSE true ENDCASES, indirect(w1) : true ENDCASES inst : DATATYPE BEGIN tst(w_tst:(not_dir_immed_mode?)) : tst_inst? cmp(w_cmp1, w_cmp2:AMode) : cmp_inst? clr(w_clr:(not_dir_immed_mode?)) : clr_inst? mov(w_mov1 : AMode, w_mov2: (not_dir_immed_mode?)) : mov_inst? inc(w_inc:(not_dir_immed_mode?)) : inc_inst? dec(w_dec:(not_dir_immed_mode?)) : dec_inst? asl(w_asl:(not_dir_immed_mode?)) : asl_inst? asr(w_asr:(not_dir_immed_mode?)) : asr_inst? add(w_ad1:AMode, w_ad2:(not_dir_immed_mode?)) : add_inst? sub(w_sub1:AMode, w_sub2:(not_dir_immed_mode?)) : sub_inst? END inst % Updates the referenced location by a value res inst_sem_aux(w:(not_dir_immed_mode?), s:{s1:state | (admissible_word(w))(s1)}, res:value) : state = CASES w OF direct(w1) : CASES w1 OF reg(n) : s WITH [(reg)(n) := res], autoinc(n) : s WITH [(mem)(reg(s)(n)) := res, (reg)(n) := reg(s)(n) + 2], autodec(n) : s WITH [(mem)(reg(s)(n) - 2) := res, (reg)(n) := reg(s)(n) - 2], index_adr(x,n) : s WITH [(mem)(reg(s)(n) + x) := res], single_adr(x) : s WITH [(mem)(x) := res] ENDCASES, indirect(w1) : CASES w1 OF reg(n) : s WITH [(mem)(reg(s)(n)) := res], autoinc(n) : s WITH [(mem)(mem(s)(reg(s)(n))) := res, (reg)(n) := reg(s)(n) + 2], autodec(n) : s WITH [(mem)(mem(s)(reg(s)(n) - 2)) := res, (reg)(n) := reg(s)(n) - 2], index_adr(x,n) : s WITH [(mem)(mem(s)(reg(s)(n) + x)) := res], single_adr(x) : s WITH [(mem)(mem(s)(x)) := res], lit_value(i) : s WITH [(mem)(i) := res] ENDCASES ENDCASES % --------------- addmissible functional for instructions ----- admissible_inst(i:inst) : pred[state] = LAMBDA s: CASES i OF tst(op) : admissible_word(op)(s), cmp(op1,op2) : admissible_word(op1)(s) & admissible_word(op2)(s), clr(op) : admissible_word(op)(s), mov(op1,op2) : admissible_word(op1)(s) & admissible_word(op2)(s), inc(op) : admissible_word(op)(s), dec(op) : admissible_word(op)(s), asl(op) : admissible_word(op)(s), asr(op) : admissible_word(op)(s) & AMode_sem(op)(s) >= 0, add(op1,op2) : admissible_word(op1)(s) & admissible_word(op2)(s), sub(op1,op2) : admissible_word(op1)(s) & admissible_word(op2)(s) ENDCASES % ------------ Semantics of binary operations -------------------- binop_sem(op1: AMode, op2:(not_dir_immed_mode?), s:{s1:state | admissible_word(op1)(s1) & admissible_word(op2)(s1)}, bop : [value, value -> value]) : state = LET res1 = AMode_sem(op1)(s), res2 = AMode_sem(op2)(s), newstatus = set_status(bop(res1, res2)), res = inst_sem_aux(op2, s, bop(res1, res2)) IN res WITH [(flag) := newstatus] % ------------ Semantics of unary operations -------------------- unop_sem(op:(not_dir_immed_mode?), s:{s1:state | admissible_word(op)(s1)}, uop : [value -> value]) : state = LET res1 = AMode_sem(op)(s), newstatus = set_status(uop(res1)), res = inst_sem_aux(op, s, uop(res1)) IN res WITH [(flag) := newstatus] % ----------- One-Step-Interpreter ------------------------------- inst_sem(i:inst)(s:{s1:state | admissible_inst(i)(s1)}) : state = CASES i OF tst(op) : let result = AMode_sem(op)(s) in s WITH [(flag) := set_status(result)], cmp(op1,op2) : let res1 = AMode_sem(op1)(s), res2 = AMode_sem(op2)(s), cmpres = res1 - res2 in s WITH [(flag) := set_status(cmpres)], clr(op) : LET res = inst_sem_aux(op, s, 0) IN res WITH [(flag) := 1], mov(op1,op2) : LET res1 = AMode_sem(op1)(s), newstatus = set_status(res1), res = inst_sem_aux(op2, s, res1) IN res WITH [(flag) := newstatus], inc(op) : unop_sem(op, s, (LAMBDA (v:value): v + 1)), dec(op) : unop_sem(op, s, (LAMBDA (v:value): v - 1)), asl(op) : unop_sem(op, s, (LAMBDA (v:value): v * 2)), asr(op) : LET res1 = AMode_sem(op)(s), res = inst_sem_aux(op, s, div2(res1)) IN res WITH [(flag) := set_status(div2(res1))], add(op1,op2) : binop_sem(op1, op2, s, (LAMBDA (v1,v2:value): v2 + v1)), sub(op1,op2) : binop_sem(op1, op2, s, (LAMBDA (v1,v2:value): v2 - v1)) ENDCASES END tam $$$tam.prf (|tam| (|set_status_TCC1| "" (SKOSIMP) NIL) (|set_status_TCC2| "" (SKOSIMP) NIL) (|set_status_TCC3| "" (SKOSIMP) NIL) (|AMode_sem_TCC1| "" (GRIND) NIL) (|AMode_sem_TCC2| "" (GRIND) NIL) (|AMode_sem_TCC3| "" (GRIND) NIL) (|AMode_sem_TCC4| "" (GRIND) NIL) (|AMode_sem_TCC5| "" (GRIND) NIL) (|AMode_sem_TCC6| "" (SUBTYPE-TCC) (("" (TYPEPRED "s!1") (("" (GRIND) NIL))))) (|AMode_sem_TCC7| "" (GRIND) NIL) (|AMode_sem_TCC8| "" (GRIND) NIL) (|AMode_sem_TCC9| "" (GRIND) NIL) (|AMode_sem_TCC10| "" (GRIND) NIL) (|AMode_sem_TCC11| "" (GRIND) NIL) (|inst_sem_aux_TCC1| "" (GRIND) NIL) (|inst_sem_aux_TCC2| "" (GRIND) NIL) (|inst_sem_aux_TCC3| "" (GRIND) NIL) (|inst_sem_aux_TCC4| "" (GRIND) NIL) (|inst_sem_aux_TCC5| "" (GRIND) NIL) (|inst_sem_aux_TCC6| "" (GRIND) NIL) (|inst_sem_aux_TCC7| "" (GRIND) NIL) (|inst_sem_aux_TCC8| "" (GRIND) NIL) (|inst_sem_aux_TCC9| "" (GRIND) NIL) (|inst_sem_aux_TCC10| "" (GRIND) NIL) (|inst_sem_aux_TCC11| "" (GRIND) NIL) (|inst_sem_aux_TCC12| "" (GRIND) NIL) (|inst_sem_aux_TCC13| "" (GRIND) NIL) (|binop_sem_TCC1| "" (GRIND) NIL) (|binop_sem_TCC2| "" (GRIND) NIL) (|inst_sem_TCC1| "" (GRIND) NIL) (|inst_sem_TCC2| "" (GRIND) NIL) (|inst_sem_TCC3| "" (SKOSIMP* :PREDS? T) (("" (REPLACE*) (("" (GRIND) NIL))))) (|inst_sem_TCC4| "" (SKOSIMP* :PREDS? T) (("" (REPLACE*) (("" (GRIND) NIL))))) (|inst_sem_TCC5| "" (GRIND) NIL) (|inst_sem_TCC6| "" (SKOSIMP* :PREDS? T) (("" (REPLACE*) (("" (GRIND) NIL))))) (|inst_sem_TCC7| "" (SKOSIMP* :PREDS? T) (("" (REPLACE*) (("" (EXPAND "admissible_inst" -) (("" (FLATTEN) (("" (PROPAX) NIL))))))))) (|inst_sem_TCC8| "" (SKOSIMP* :PREDS? T) (("" (REPLACE*) (("" (GRIND) NIL))))) (|inst_sem_TCC9| "" (SKOSIMP* :PREDS? T) (("" (REPLACE*) (("" (GRIND) NIL))))) (|inst_sem_TCC10| "" (SKOSIMP* :PREDS? T) (("" (REPLACE*) (("" (GRIND) NIL))))) (|inst_sem_TCC11| "" (SKOSIMP* :PREDS? T) (("" (REPLACE*) (("" (GRIND) NIL))))) (|inst_sem_TCC12| "" (SKOSIMP* :PREDS? T) (("" (REPLACE*) (("" (EXPAND "admissible_inst") (("" (ASSERT) NIL))))))) (|inst_sem_TCC13| "" (SKOSIMP* :PREDS? T) (("" (REPLACE*) (("" (GRIND) NIL))))) (|inst_sem_TCC14| "" (SKOSIMP* :PREDS? T) (("" (REPLACE*) (("" (GRIND) NIL)))))) $$$tam_pho.pvs tam_pho : THEORY BEGIN % --- target language IMPORTING tam % --- pho scheme IMPORTING pho[inst,state,admissible_inst,inst_sem] n : VAR regnumber s : VAR state i1,i2 : VAR value sub_clr : LEMMA correct?( (# pattern := (: sub(direct(lit_value(2)), direct(reg(n))), clr(indirect(reg(n))) :), replacement := (: clr(direct(autodec(n))) :), condition := LAMBDA s: true #)) add_zero : LEMMA null_seq?((: add(direct(lit_value(0)), direct(reg(n))) :), LAMBDA s: flag(s) = set_status(reg(s)(n))) % constant folding cns_fold : LEMMA correct?( (# pattern := (: mov(direct(lit_value(i1)), direct(reg(n))), add(direct(lit_value(i2)), direct(reg(n))) :), replacement := (: mov(direct(lit_value(i1+i2)), direct(reg(n))) :), condition := LAMBDA s: flag(s) = set_status(i1+i2) #)) END tam_pho $$$tam_pho.prf (|tam_pho| (IMPORTING2_TCC1 "" (GRIND) NIL) (IMPORTING2_TCC2 "" (INST + "(# mem := LAMBDA (a:adr): 0, reg := LAMBDA (r:regnumber): 0, flag := 0 #)") NIL) (|sub_clr_TCC1| "" (GRIND) NIL) (|sub_clr_TCC2| "" (GRIND) NIL) (|sub_clr_TCC3| "" (SUBTYPE-TCC) NIL) (|sub_clr| "" (PHO) NIL) (|add_zero| "" (PHO) NIL) (|cns_fold| "" (PHO) NIL))