$$$top.pvs top: THEORY BEGIN IMPORTING div_top, bv_top END top $$$exp2_table.pvs exp2_table: THEORY BEGIN IMPORTING exp2 exp2_0: LEMMA exp2(0) = 1 exp2_1: LEMMA exp2(1) = 2 exp2_2: LEMMA exp2(2) = 4 exp2_3: LEMMA exp2(3) = 8 exp2_4: LEMMA exp2(4) = 16 exp2_8: LEMMA exp2(8) = 256 exp2_16: LEMMA exp2(16) = 65536 END exp2_table $$$exp2_table.prf (|exp2_table| (|exp2_0| "" (EXPAND "exp2") (("" (PROPAX) NIL))) (|exp2_1| "" (EXPAND "exp2") (("" (EXPAND "exp2") (("" (PROPAX) NIL))))) (|exp2_2| "" (EXPAND "exp2") (("" (EXPAND "exp2") (("" (EXPAND "exp2") (("" (PROPAX) NIL))))))) (|exp2_3| "" (EXPAND "exp2") (("" (EXPAND "exp2") (("" (EXPAND "exp2") (("" (EXPAND "exp2") (("" (PROPAX) NIL))))))))) (|exp2_4| "" (LEMMA "exp2_sum") (("" (INST -1 "2" "2") (("" (LEMMA "exp2_2") (("" (ASSERT) NIL))))))) (|exp2_8| "" (LEMMA "exp2_sum") (("" (INST -1 "4" "4") (("" (LEMMA "exp2_4") (("" (ASSERT) NIL))))))) (|exp2_16| "" (LEMMA "exp2_sum") (("" (INST -1 "8" "8") (("" (LEMMA "exp2_8") (("" (ASSERT) NIL)))))))) $$$bv_rules.pvs bv_rules [N: posnat]: THEORY BEGIN IMPORTING exp2_table, bv_arith_nat, mod_lems i, i1, i2: VAR int n, k, n1, n2: VAR nat m: VAR posnat bv: VAR bvec[N] % some rules for exp2 exp2_3: LEMMA exp2(3) = 8 exp2_16: LEMMA exp2(16) = 65536 % some rules about mod arithmetic mod_mod_lemma: LEMMA mod(mod(i, m), m) = mod(i, m) % The following rule characterizes the property that incrementing % modulo m wraps around the zero point. mod_wrap_around: LEMMA n < m & (k <= m & k >= m-n) => mod(n+k, m) = n - (m-k) % some properties about bit-vector arithmetic word0: bvec[16] = (LAMBDA (i: below(16)): 0) word0_nat: LEMMA bv2nat[16](word0) = 0 IMPORTING bv_nat % The following rules normalize expressions involving multiple bit-vector % increments and decrements into a cannonical form in which there is a % single increment/decrement. bv_minus_def: LEMMA bv - i = bv + (-i) bv_plus_assoc: LEMMA bv + i1 + i2 = bv + (i1+i2) bv_minus_0: LEMMA n=0 => bv + (-n) = bv bv_plus_0: LEMMA n=0 => bv + n = bv bv2nat_minus: LEMMA i<0 & (-i) <= bv2nat(bv) => bv2nat(bv + i) = bv2nat(bv) + i % The following rules convert the bv2nat of a "bv+n" expression % into an expression of bv2nat of bv. bv2nat_plus: LEMMA n < (exp2(N) - bv2nat(bv)) => bv2nat(bv + n) = bv2nat(bv) + n % The following rule states the equivalent of the mod-wrap-around, % stated above, for bit-vector incrementing. bv2nat_plus2: LEMMA n < exp2(N) & bv2nat(bv)+n >= exp2(N) => bv2nat(bv + n) = bv2nat(bv) - (exp2(N) - n) % The following rules convert (under certain conditions) an % equality/disequality checks on bit-vector inc/dec expressions into % equality/disequality on integers bv_equal_lemma0: LEMMA (bv = bv + i) = (bv + 0 = bv + i) bv_equal_lemma1: LEMMA 0 <= n & n < exp2(N) & 0 <= k & k < exp2(N) IMPLIES (bv + n = bv + k) = (n = k) bv_equal_lemma2: LEMMA 0 <= -i1 & -i1 < exp2(N) & 0 <= -i2 & -i2 < exp2(N) IMPLIES (bv + i1 = bv + i2) = (i1 = i2) bv_equal_lemma3: LEMMA 0 <= n & n < exp2(N) & 0 < -i1 & -i1 < exp2(N) IMPLIES (bv + n = bv + i1) = ((n-i1) = exp2(N)) END bv_rules $$$bv_rules.prf (|bv_rules| (|exp2_3| "" (LEMMA "exp2_table.exp2_3") (("" (PROPAX) NIL))) (|exp2_16| "" (LEMMA "exp2_table.exp2_16") (("" (PROPAX) NIL))) (|mod_mod_lemma| "" (SKOSIMP*) (("" (LEMMA "mod_of_mod") (("" (INST -1 "0" "i!1" "m!1") (("" (ASSERT) NIL))))))) (|mod_wrap_around| "" (SKOSIMP*) (("" (LEMMA "mod_wrap_around") (("" (INST?) (("" (ASSERT) NIL))))))) (|word0_TCC1| "" (TCC) NIL) (|word0_nat| "" (LEMMA "bv2nat_bvec0[16]") (("" (EXPAND "word0") (("" (EXPAND "bvec0") (("" (PROPAX) NIL))))))) (|bv_minus_def| "" (SKOSIMP*) (("" (EXPAND "-" 1 1) (("" (PROPAX) NIL))))) (|bv_plus_assoc| "" (SKOSIMP*) (("" (EXPAND "+") (("" (CASE "mod(bv2nat[N](nat2bv[N](mod(bv2nat(bv!1) + i1!1, exp2(N)))) + i2!1, exp2(N)) = mod(bv2nat[N](bv!1) + i1!1 + i2!1, exp2(N))") (("1" (ASSERT) NIL) ("2" (HIDE 2) (("2" (CASE "bv2nat[N](nat2bv[N](mod(bv2nat(bv!1) + i1!1, exp2(N)))) = mod(bv2nat(bv!1) + i1!1, exp2(N))") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "mod_of_mod") (("1" (INST -1 "i2!1" "bv2nat(bv!1) + i1!1" "exp2(N)") (("1" (ASSERT) NIL))))))))) ("2" (HIDE 2) (("2" (LEMMA "bv2nat_inv[N]") (("2" (INST -1 "mod(bv2nat(bv!1) + i1!1, exp2(N))") (("2" (ASSERT) (("2" (HIDE 2) (("2" (REWRITE "mod_pos") NIL))))))))))))))) ("3" (ASSERT) (("3" (REWRITE "mod_pos") NIL))))))))) (|bv_minus_0| "" (SKOSIMP*) (("" (REPLACE -1) (("" (HIDE -1) (("" (EXPAND "+") (("" (LEMMA "mod_lt_nat") (("" (INST?) (("" (ASSERT) (("" (REPLACE -1) (("" (HIDE -1) (("" (LEMMA "nat2bv_inv[N]") (("" (INST?) NIL))))))))))))))))))))) (|bv_plus_0| "" (SKOSIMP*) (("" (EXPAND "+") (("" (REPLACE -1) (("" (HIDE -1) (("" (REWRITE "mod_lt_nat") (("" (REWRITE "nat2bv_inv[N]") NIL))))))))))) (|bv2nat_minus| "" (SKOSIMP*) (("" (EXPAND "+") (("" (LEMMA "bv2nat_inv[N]") (("" (INST?) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (REWRITE "mod_lt_nat") NIL))))) ("2" (HIDE 2) (("2" (REWRITE "mod_pos") NIL))))))))))) (|bv2nat_plus| "" (SKOSIMP*) (("" (REWRITE "bv_plus[N]") (("" (REWRITE "mod_lt_nat") NIL))))) (|bv2nat_plus2| "" (SKOSIMP*) (("" (EXPAND "+") (("" (LEMMA "bv2nat_inv[N]") (("" (INST?) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "mod_wrap_around") (("1" (INST -1 "bv2nat(bv!1)" "exp2(N)" "n!1") (("1" (SPLIT -1) (("1" (ASSERT) NIL) ("2" (PROPAX) NIL) ("3" (ASSERT) NIL) ("4" (ASSERT) NIL))))))))))) ("2" (ASSERT) (("2" (HIDE 2) (("2" (REWRITE "mod_pos") NIL))))))))))))) (|bv_equal_lemma0| "" (SKOSIMP*) (("" (EXPAND "+") (("" (LEMMA "mod_lt_nat") (("" (INST -1 "exp2(N)" "bv2nat(bv!1)") (("" (ASSERT) (("" (REPLACE -1) (("" (HIDE -1) (("" (LEMMA "nat2bv_inv[N]") (("" (INST?) (("" (ASSERT) NIL))))))))))))))))))) (|bv_equal_lemma1| "" (SKOSIMP*) (("" (IFF 1) (("" (SPLIT 1) (("1" (FLATTEN) (("1" (EXPAND "+") (("1" (LEMMA "nat2bv_bij[N]") (("1" (EXPAND "bijective?") (("1" (FLATTEN) (("1" (HIDE -2) (("1" (EXPAND "injective?") (("1" (INST -1 "mod(bv2nat(bv!1) + n!1, exp2(N))" "mod(bv2nat(bv!1) + k!1, exp2(N))") (("1" (ASSERT) (("1" (HIDE -2) (("1" (LEMMA "mod_inj1") (("1" (INST?) (("1" (ASSERT) NIL))))))))) ("2" (ASSERT) (("2" (HIDE 2) (("2" (REWRITE "mod_pos") NIL))))) ("3" (REWRITE "mod_pos") NIL))))))))))))))))) ("2" (FLATTEN) (("2" (ASSERT) NIL))))))))) (|bv_equal_lemma2| "" (SKOSIMP*) (("" (IFF 1) (("" (SPLIT 1) (("1" (FLATTEN) (("1" (EXPAND "+") (("1" (LEMMA "nat2bv_bij[N]") (("1" (EXPAND "bijective?") (("1" (FLATTEN) (("1" (HIDE -2) (("1" (EXPAND "injective?") (("1" (INST -1 "mod(bv2nat(bv!1) + i1!1, exp2(N))" "mod(bv2nat(bv!1) + i2!1, exp2(N))") (("1" (ASSERT) (("1" (HIDE -2) (("1" (LEMMA "mod_inj2") (("1" (INST -1 "-i2!1" "exp2(N)" "-i1!1" "bv2nat(bv!1)") (("1" (ASSERT) NIL))))))))) ("2" (ASSERT) (("2" (HIDE -1 -2 -3 -4 -5 2) (("2" (REWRITE "mod_pos") NIL))))) ("3" (HIDE -1 -2 -3 -4 -5 2) (("3" (REWRITE "mod_pos") NIL))))))))))))))))))) ("2" (FLATTEN) (("2" (ASSERT) NIL))))))))) (|bv_equal_lemma3| "" (SKOSIMP*) (("" (EXPAND "+") (("" (LEMMA "nat2bv_bij[N]") (("" (EXPAND "bijective?") (("" (FLATTEN) (("" (HIDE -2) (("" (EXPAND "injective?") (("" (INST -1 "mod(bv2nat(bv!1) + n!1, exp2(N))" "mod(bv2nat(bv!1) + i1!1, exp2(N))") (("1" (IFF 1) (("1" (SPLIT 1) (("1" (FLATTEN) (("1" (ASSERT) (("1" (HIDE -1) (("1" (LEMMA "mod_wrap_inj") (("1" (INST -1 "n!1" "-i1!1" "exp2(N)" "bv2nat(bv!1)") (("1" (CASE "n!1=0") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (HIDE -1) (("1" (REWRITE "mod_lt_nat") (("1" (LEMMA "mod_lt") (("1" (INST?) (("1" (EXPAND "abs") (("1" (EXPAND "sgn") (("1" (LIFT-IF) (("1" (ASSERT) NIL))))))))))))))))))) ("2" (ASSERT) NIL))))))))))))) ("2" (FLATTEN) (("2" (ASSERT) (("2" (CASE-REPLACE "i1!1 = n!1 - exp2(N)") (("1" (HIDE -1 -2) (("1" (LEMMA "mod_sum") (("1" (INST -1 "bv2nat(bv!1) + n!1 - exp2(N)" "exp2(N)" "1") (("1" (ASSERT) NIL))))))) ("2" (ASSERT) NIL))))))))))) ("2" (ASSERT) (("2" (HIDE -1 -2 -3 -4 2) (("2" (REWRITE "mod_pos") NIL))))) ("3" (HIDE -1 -2 -3 -4 2) (("3" (REWRITE "mod_pos") NIL)))))))))))))))))))) $$$bv_select.pvs bv_select[n:posnat, l:posnat ]: THEORY %------------------------------------------------------------------------ % The bit vector binary ops restricted theory defines functions that % take two bit vectors as their primary inputs where the second bit % must be smaller or the same size as the first bit vector. The theory % is instantiated with the sizes of the two bit vectors. %------------------------------------------------------------------------ BEGIN ASSUMING leq: ASSUMPTION l <= n ENDASSUMING IMPORTING bv_arithmetic ii: VAR below(n) %------------------------------------------------------------------------ % Bv_select selects bits s+l-1 to s of a bit vector. %------------------------------------------------------------------------ bv_select(bvn: bvec[n], s: upto(n-l)): bvec[l] = bvn^(s+l-1,s) %------------------------------------------------------------------------ % Bv_assign replaces bits s+l-1 to s of a bit vector. %------------------------------------------------------------------------ bv_assign(bvn: bvec[n], s: upto(n-l), bvl: bvec[l]): bvec[n] = (LAMBDA ii: IF ii >= s AND ii <= s+l-1 THEN bvl(ii-s) ELSE bvn(ii) ENDIF) % === Some Lemmas ========================================================= i,j: VAR below(n) bvn: VAR bvec[n] s : VAR upto(n-l) select_2step: LEMMA i >= j IMPLIES bvn^(i,j) = (bvn^(i, 0))^(i,j) bv_select_lem: LEMMA bv2nat(bv_select(bvn,s)) = div(mod(bv2nat(bvn),exp2(s+l)), exp2(s)) bv_assign_lem: LEMMA bv_assign(bvn,s,bv_select(bvn,s)) = bvn caret_i_lem : LEMMA bvn^ii = bv2nat[1](bvn^(ii,ii)) END bv_select $$$bv_select.prf (|bv_select| (|bv_select_TCC1| "" (SUBTYPE-TCC) NIL) (|bv_select_TCC2| "" (SUBTYPE-TCC) NIL) (|bv_assign_TCC1| "" (SUBTYPE-TCC) NIL) (|s_TCC1| "" (USE "leq") (("" (ASSERT) NIL))) (|select_2step_TCC1| "" (SUBTYPE-TCC) NIL) (|select_2step_TCC2| "" (SUBTYPE-TCC) NIL) (|select_2step_TCC3| "" (SUBTYPE-TCC) NIL) (|select_2step_TCC4| "" (SUBTYPE-TCC) NIL) (|select_2step_TCC5| "" (SUBTYPE-TCC) NIL) (|select_2step| "" (SKOSIMP) (("" (EXPAND "^") (("" (PROPAX) NIL))))) (|bv_select_lem| "" (SKOSIMP*) (("" (EXPAND "bv_select") (("" (LEMMA "select_2step") (("" (INST?) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "bv_shift[s!1+l]") (("1" (INST?) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "bv_bottom[n]") (("1" (INST?) (("1" (REPLACE -1) (("1" (ASSERT) NIL))))))))))))))))))))) ("2" (ASSERT) NIL) ("3" (ASSERT) NIL))))))))) (|bv_assign_lem| "" (SKOLEM 1 ("bvn!1" "s!1")) (("" (EXPAND "bv_select") (("" (EXPAND "bv_assign") (("" (APPLY-EXTENSIONALITY 1) (("1" (HIDE 2) (("1" (LIFT-IF 1) (("1" (SPLIT 1) (("1" (FLATTEN) (("1" (EXPAND "^") (("1" (PROPAX) NIL))))) ("2" (FLATTEN) (("2" (PROPAX) NIL))))))))) ("2" (HIDE 2) (("2" (SKOLEM 1 ("jj!1")) (("2" (FLATTEN) (("2" (ASSERT) NIL))))))) ("3" (HIDE 2) (("3" (SKOSIMP) (("3" (ASSERT) NIL))))) ("4" (HIDE 2) (("4" (SKOSIMP) (("4" (ASSERT) NIL))))))))))))) (|caret_i_lem_TCC1| "" (SUBTYPE-TCC) NIL) (|caret_i_lem| "" (GRIND) NIL)) $$$bv_bitwise_lems.pvs bv_bitwise_lems [N: nat] : THEORY BEGIN IMPORTING bv_bitwise, bv_extractors[N] bv, bv1, bv2: VAR bvec[N] sel_pair: TYPE = [i1: below(N), upto(i1)] sp: VAR sel_pair bv_OR : LEMMA (bv1 OR bv2)^sp = (bv1^sp OR bv2^sp) bv_AND : LEMMA (bv1 AND bv2)^sp = (bv1^sp AND bv2^sp) bv_IFF : LEMMA (bv1 IFF bv2)^sp = (bv1^sp IFF bv2^sp) bv_XOR : LEMMA XOR(bv1,bv2)^sp = XOR(bv1^sp,bv2^sp) bv_NOT : LEMMA (NOT bv)^sp = NOT(bv^sp) END bv_bitwise_lems $$$bv_bitwise_lems.prf (|bv_bitwise_lems| (|bv_OR_TCC1| "" (GRIND) NIL) (|bv_OR| "" (SKOLEM 1 ("bv1!1" "bv2!1" "sp!1")) (("" (EXPAND "^") (("" (EXPAND "OR") (("" (PROPAX) NIL))))))) (|bv_AND| "" (SKOLEM 1 ("bv1!1" "bv2!1" "sp!1")) (("" (EXPAND "AND") (("" (EXPAND "^") (("" (PROPAX) NIL))))))) (|bv_IFF| "" (SKOLEM 1 ("bv1!1" "bv2!1" "sp!1")) (("" (EXPAND "IFF") (("" (EXPAND "^") (("" (PROPAX) NIL))))))) (|bv_XOR| "" (SKOSIMP*) (("" (EXPAND "XOR") (("" (EXPAND "^") (("" (PROPAX) NIL))))))) (|bv_NOT| "" (SKOLEM 1 ("bvn!1" "sp!1")) (("" (EXPAND "NOT") (("" (EXPAND "^") (("" (PROPAX) NIL)))))))) $$$bv_arith_nat.pvs bv_arith_nat[N: nat]: THEORY %------------------------------------------------------------------------ % Defines functions over bit vectors interpreted as natural numbers. % % Introduces: % % > : bv1 > bv2 % >=: bv1 >= bv2 % < : bv1 < bv2 % <=: bv1 <= bv1 % + : bv1 + i % - : bv1 - i % + : bv1 + bv2 % * : bv1 * bv2 % carryout: [bvec, bvec -> bvec[1]] % %------------------------------------------------------------------------ BEGIN IMPORTING bv_nat[N], mod % ---------------------------------------------------------------------- % Definition of inequalities over the bit vectors. % ---------------------------------------------------------------------- < (bv1: bvec, bv2: bvec): bool = bv2nat(bv1) < bv2nat(bv2) ; <=(bv1: bvec, bv2: bvec): bool = bv2nat(bv1) <= bv2nat(bv2) ; > (bv1: bvec, bv2: bvec): bool = bv2nat(bv1) > bv2nat(bv2) ; >=(bv1: bvec, bv2: bvec): bool = bv2nat(bv1) >= bv2nat(bv2) ; % ---------------------------------------------------------------------- % Increments a bit vector by a integer modulo 2**N. % ---------------------------------------------------------------------- +(bv: bvec, i: int): bvec = nat2bv(mod(bv2nat(bv) + i, exp2(N))) ; % ---------------------------------------------------------------------- % Decrements a bit vector by a integer modulo 2**N. % ---------------------------------------------------------------------- -(bv: bvec,i: int): bvec = bv + (-i) ; % ---------------------------------------------------------------------- % Addition of two bit vectors interpreted as natural numbers. % ---------------------------------------------------------------------- +(bv1: bvec, bv2: bvec): bvec = IF bv2nat(bv1) + bv2nat(bv2) < exp2(N) THEN nat2bv(bv2nat(bv1) + bv2nat(bv2)) ELSE nat2bv(bv2nat(bv1) + bv2nat(bv2) - exp2(N)) ENDIF ; % ========= Properties of these functions ================================ i : VAR int n : VAR below(N) bv, bv1, bv2 : VAR bvec bv_smallest : LEMMA (FORALL bv: bv >= bvec0) bv_greatest : LEMMA (FORALL bv: bv <= bvec1) bv_plus : LEMMA bv2nat(bv + i) = mod(bv2nat(bv) + i, exp2(N)) bv_plus1 : LEMMA bv2nat(bv + 1) = IF bv2nat(bv) = (exp2(N)-1) THEN 0 ELSE bv2nat(bv) + 1 ENDIF bv_minus : LEMMA bv2nat(bv - i) = mod(bv2nat(bv) - i, exp2(N)) bv_minus1 : LEMMA bv2nat(bv - 1) = IF bv2nat(bv) = 0 THEN exp2(N)-1 ELSE bv2nat(bv) - 1 ENDIF bv_minus_plus: LEMMA (bv-1)+1 = bv bv_plus_minus: LEMMA (bv+1)-1 = bv bv_add : LEMMA bv2nat(bv1 + bv2) = IF bv2nat(bv1) + bv2nat(bv2) < exp2(N) THEN bv2nat(bv1) + bv2nat(bv2) ELSE bv2nat(bv1) + bv2nat(bv2) - exp2(N) ENDIF bv_addcomm : THEOREM bv1 + bv2 = bv2 + bv1 % ================== Additional functions ================================ IMPORTING bv_nat % ---------------------------------------------------------------------- % The operator * denotes unsigned multiplication two n-bit bvecs. % ---------------------------------------------------------------------- *(bv1: bvec[N], bv2: bvec[N]): bvec[2*N] = nat2bv[2*N](bv2nat(bv1) * bv2nat(bv2)) ; m1, m2 : VAR nat mult_lem : LEMMA m1 < exp2(N) AND m2 < exp2(N) IMPLIES m1 * m2 < exp2(2 * N) bv_mult : LEMMA bv2nat(bv1 * bv2) = bv2nat(bv1) * bv2nat(bv2) % ---------------------------------------------------------------------- % Function carryout returns a bvec[1]. The value of the bit is 1 iff the % addition of two bit vectors yields a carry out of the msb position. % ---------------------------------------------------------------------- carryout(bv1: bvec, bv2: bvec, Cin: bvec[1]): bvec[1] = (LAMBDA (bb: below(1)): bool2bit(bv2nat(bv1) + bv2nat(bv2) + bv2nat(Cin) >= exp2(N))) ; END bv_arith_nat $$$bv_arith_nat.prf (|bv_arith_nat| (|plus_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|bv_smallest| "" (EXPAND ">=") (("" (SKOLEM 1 ("bv!1")) (("" (ASSERT) (("" (LEMMA "bv2nat_bvec0") (("" (ASSERT) NIL))))))))) (|bv_greatest| "" (EXPAND "<=") (("" (LEMMA "bv2nat_bvec1") (("" (SKOLEM 1 ("bv!1")) (("" (ASSERT) NIL))))))) (|bv_plus| "" (SKOLEM!) (("" (EXPAND "+" 1 1) (("" (LEMMA "bv2nat_inv") (("" (INST?) NIL))))))) (|bv_plus1| "" (SKOLEM!) (("" (REWRITE "bv_plus") (("" (EXPAND "mod") (("" (LIFT-IF) (("" (GROUND) (("" (REWRITE "floor_small") (("1" (LIFT-IF) (("1" (ASSERT) (("1" (PROP) (("1" (ASSERT) (("1" (REWRITE "pos_div_ge") NIL))))))))) ("2" (EXPAND "abs") (("2" (ASSERT) NIL))))))))))))))) (|bv_minus| "" (EXPAND "-") (("" (SKOSIMP*) (("" (REWRITE "bv_plus") (("" (ASSERT) NIL))))))) (|bv_minus1| "" (SKOSIMP*) (("" (REWRITE "bv_minus") (("" (LIFT-IF) (("" (GROUND) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (CASE "N=0") (("1" (REPLACE -1) (("1" (EXPAND "exp2") (("1" (EXPAND "mod") (("1" (ASSERT) NIL))))))) ("2" (REWRITE "mod_lt") (("1" (EXPAND "sgn") (("1" (PROPAX) NIL))) ("2" (EXPAND "abs") (("2" (HIDE 3) (("2" (EXPAND "exp2") (("2" (ASSERT) NIL))))))))))))))) ("2" (REWRITE "mod_lt_nat") NIL))))))))) (|bv_minus_plus| "" (SKOSIMP *) (("" (LEMMA "bv2nat_inj") (("" (EXPAND "injective?") (("" (INST?) (("" (ASSERT) (("" (HIDE 2) (("" (LEMMA "bv_minus1") (("" (INST?) (("" (LEMMA "bv_plus1") (("" (INST?) (("" (LIFT-IF) (("" (GROUND) NIL))))))))))))))))))))))) (|bv_plus_minus| "" (SKOLEM!) (("" (LEMMA "bv2nat_inj") (("" (EXPAND "injective?") (("" (INST?) (("" (ASSERT) (("" (HIDE 2) (("" (LEMMA "bv_plus1") (("" (INST?) (("" (LEMMA "bv_minus1") (("" (INST?) (("" (LIFT-IF) (("" (GROUND) NIL))))))))))))))))))))))) (|bv_add| "" (SKOLEM!) (("" (EXPAND "+") (("" (LEMMA "bv2nat_inv") (("" (LIFT-IF) (("" (GROUND) (("1" (INST?) NIL) ("2" (INST?) NIL))))))))))) (|bv_addcomm| "" (SKOSIMP*) (("" (EXPAND "+") (("" (PROPAX) NIL))))) (|times_TCC1| "" (SKOSIMP*) (("" (LEMMA "exp2_sum") (("" (INST -1 "N" "N") (("" (REPLACE -1) (("" (HIDE -1) (("" (TYPEPRED "bv2nat[N](bv1!1)") (("" (TYPEPRED "bv2nat[N](bv2!1)") (("" (LEMMA "lt_times_lt_pos1") (("" (INST?) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (ASSERT) NIL))))))))))))))))))) (|mult_lem| "" (SKOSIMP*) (("" (LEMMA "exp2_sum") (("" (INST - "N" "N") (("" (REPLACE -1) (("" (CASE "forall (l,m,n:nat): ll*m bvec] % - : [bvec, bvec -> bvec] % overflow : [bvec, bvec -> bool] % underflow : [bvec, bvec -> bool] % %------------------------------------------------------------------------ BEGIN IMPORTING bv_int[N], bv_arith_shift[N] bv, bv1, bv2 : VAR bvec % ---------------------------------------------------------------------- % 2's complement negation of a bit vector % ---------------------------------------------------------------------- -(bv: bvec): bvec = int2bv( IF bv2int(bv) = minint THEN bv2int(bv) ELSE -(bv2int(bv)) ENDIF ) ; % ---------------------------------------------------------------------- % 2's complement subtraction of two bit vectors % ---------------------------------------------------------------------- -(bv1, bv2): bvec = (bv1 + (-bv2)) % ---------------------------------------------------------------------- % Define conditions for 2's complement overflow % ---------------------------------------------------------------------- overflow(bv1,bv2): bool = (bv2int(bv1) + bv2int(bv2)) > maxint OR (bv2int(bv1) + bv2int(bv2)) < minint % === Properties of these additional functions ================================ % ---------------------------------------------------------------------- % If the result is in the range of 2s complement integers, addition of % two bit vectors is the same as for a natural number interpretation % ---------------------------------------------------------------------- intaddlem : THEOREM in_rng_2s_comp(bv2int(bv1) + bv2int(bv2)) IMPLIES bv2int(bv1 + bv2) = bv2int(bv1) + bv2int(bv2) unaryminus : LEMMA bv2int(-bv) = IF bv2int(bv) = minint THEN bv2int(bv) ELSE -(bv2int(bv)) ENDIF minus1lem : LEMMA bv2int(bv1) > minint AND bv2int(bv) = 1 IMPLIES bv2int(bv1 - bv) = bv2int(bv1) - 1 IMPORTING bv_bitwise[N] n : VAR upto(N) compl_max : THEOREM bv2nat_rec(n, bv) + bv2nat_rec(n, NOT bv) = exp2(n) - 1 % ---------------------------------------------------------------------- % The 2s complement of a number is its 1s complement + 1 % ---------------------------------------------------------------------- twos_compl : THEOREM -bv2int(bv) = bv2int(NOT bv) + 1; END bv_arithmetic $$$bv_arithmetic.prf (|bv_arithmetic| (|difference_TCC1| "" (SKOLEM 1 ("bv!1")) (("" (FLATTEN) (("" (TYPEPRED "bv2int(bv!1)") (("" (ASSERT) (("" (EXPAND "minint") (("" (EXPAND "maxint") (("" (ASSERT) NIL))))))))))))) (|intaddlem| "" (SKOSIMP*) (("" (AUTO-REWRITE "bv2int_lem") (("" (EXPAND "in_rng_2s_comp") (("" (EXPAND "maxint") (("" (EXPAND "minint") (("" (ASSERT) (("" (EXPAND "+") (("" (LIFT-IF) (("" (LEMMA "bv2nat_top_bit") (("" (INST -1 "bv1!1") (("" (LEMMA "bv2nat_top_bit") (("" (INST -1 "bv2!1") (("" (SPLIT -1) (("1" (SPLIT -2) (("1" (FLATTEN) (("1" (SPLIT 1) (("1" (FLATTEN) (("1" (LEMMA "bv2nat_inv") (("1" (INST?) (("1" (LEMMA "bv2nat_top_bit") (("1" (INST -1 "nat2bv(bv2nat(bv1!1) + bv2nat(bv2!1))") (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (ASSERT) NIL))) ("2" (FLATTEN) (("2" (ASSERT) NIL))))))))))))))) ("2" (FLATTEN) (("2" (EXPAND "exp2" 1) (("2" (ASSERT) NIL))))))))) ("2" (FLATTEN) (("2" (SPLIT 2) (("1" (FLATTEN) (("1" (LEMMA "bv2nat_inv") (("1" (INST?) (("1" (LEMMA "bv2nat_top_bit") (("1" (INST -1 "nat2bv(bv2nat(bv1!1) + bv2nat(bv2!1))") (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (ASSERT) NIL))) ("2" (FLATTEN) (("2" (ASSERT) NIL))))))))))))))) ("2" (FLATTEN) (("2" (LEMMA "bv2nat_inv") (("2" (INST?) (("1" (LEMMA "bv2nat_top_bit") (("1" (INST -1 "nat2bv(bv2nat(bv1!1) + bv2nat(bv2!1) - exp2(N))") (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (EXPAND "exp2" -1 1) (("1" (EXPAND "exp2" 1) (("1" (ASSERT) NIL))))))) ("2" (FLATTEN) (("2" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))))))))))) ("2" (FLATTEN) (("2" (SPLIT -2) (("1" (FLATTEN) (("1" (SPLIT 2) (("1" (FLATTEN) (("1" (LEMMA "bv2nat_inv") (("1" (INST?) (("1" (LEMMA "bv2nat_top_bit") (("1" (INST -1 "nat2bv(bv2nat(bv1!1) + bv2nat(bv2!1))") (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (ASSERT) NIL))) ("2" (FLATTEN) (("2" (ASSERT) NIL))))))))))))))) ("2" (FLATTEN) (("2" (LEMMA "bv2nat_inv") (("2" (INST?) (("1" (LEMMA "bv2nat_top_bit") (("1" (INST -1 "nat2bv(bv2nat(bv1!1) + bv2nat(bv2!1) - exp2(N))") (("1" (SPLIT -1) (("1" (ASSERT) NIL) ("2" (FLATTEN) (("2" (REPLACE -2) (("2" (HIDE -1 -2) (("2" (REPLACE -2) (("2" (REPLACE -3) (("2" (HIDE -2 -3) (("2" (ASSERT) NIL))))))))))))))) ("2" (HIDE -1) (("2" (REPLACE -2) (("2" (REPLACE -3) (("2" (HIDE -2 -3) (("2" (ASSERT) NIL))))))))))))) ("2" (REPLACE -2) (("2" (REPLACE -3) (("2" (HIDE -2 -3) (("2" (ASSERT) NIL))))))))))))))))) ("2" (FLATTEN) (("2" (LEMMA "bv2nat_inv") (("2" (SPLIT 3) (("1" (FLATTEN) (("1" (EXPAND "exp2" -1) (("1" (ASSERT) NIL))))) ("2" (FLATTEN) (("2" (INST?) (("1" (LEMMA "bv2nat_top_bit") (("1" (INST -1 "nat2bv(bv2nat(bv1!1) + bv2nat(bv2!1) - exp2(N))") (("1" (CASE "exp2(N) = 2*exp2(N-1)") (("1" (ASSERT) NIL) ("2" (HIDE -1 -2 -3 -4 -5 -6 2 3 4 5) (("2" (EXPAND "exp2" 1 1) (("2" (PROPAX) NIL))))))) ("2" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))) (|unaryminus| "" (SKOLEM 1 ("bv!1")) (("" (EXPAND "-" 1 1) (("" (CASE " bv2int(bv!1) = minint") (("1" (ASSERT) (("1" (LEMMA "bv2int_inv") (("1" (INST?) NIL))))) ("2" (ASSERT) (("2" (LEMMA "bv2int_inv") (("2" (INST?) (("2" (ASSERT) (("2" (TYPEPRED "bv2int(bv!1)") (("2" (EXPAND "minint") (("2" (EXPAND "maxint") (("2" (ASSERT) NIL))))))))))))))))))))) (|minus1lem| "" (SKOLEM 1 ("bv!1" "bv1!1")) (("" (FLATTEN) (("" (EXPAND "-" 1 1) (("" (LEMMA "unaryminus") (("" (INST?) (("" (EXPAND "minint") (("" (ASSERT) (("" (ASSERT) (("" (LEMMA "intaddlem") (("" (INST?) (("" (EXPAND "in_rng_2s_comp") (("" (REPLACE -3) (("" (EXPAND "minint") (("" (ASSERT) NIL))))))))))))))))))))))))))) (|compl_max| "" (INDUCT "n") (("1" (TCC) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (EXPAND "bv2nat_rec" +) (("2" (INST - "bv!1") (("2" (HIDE -1) (("2" (TCC) NIL))))))))))))) (|twos_compl| "" (SKOSIMP*) (("" (LEMMA "compl_max") (("" (AUTO-REWRITE "bv2int_lem") (("" (DO-REWRITE) (("" (EXPAND "bv2nat") (("" (INST?) (("" (EXPAND "NOT") (("" (EXPAND "NOT") (("" (ASSERT) (("" (LIFT-IF) (("" (GROUND) NIL)))))))))))))))))))))) $$$bv_extend.pvs bv_extend [N: posnat] : THEORY % ----------------------------------------------------------------------- % Introduces: % zero_extend: [k: above(N) -> [bvec[N] -> bvec[l]]] = % sign_extend: [k: above(N) -> [bvec[N] -> bvec[l]]] = % zero_extend_lsend: [k: above(N) -> [bvec[N] -> bvec[l]]] % lsb_extend: [k: above(N) -> [bvec[N] -> bvec[l]]] = % % ----------------------------------------------------------------------- BEGIN IMPORTING bv_extractors, bv_concat bv: VAR bvec[N] k: VAR above(N) %------------------------------------------------------------------------ % zero_extend returns a function that extends a bit vector to length k % such that its interpretation as a natural number remains unchanged. % That is, it fills 0's at the most significant positions. %------------------------------------------------------------------------ zero_extend(k: above(N)): [bvec[N] -> bvec[k]] = (LAMBDA bv: bvec0[k-N] o bv) %------------------------------------------------------------------------ % sign_extend returns a function that extends a bit vector to length k % by repeating the most significant bit of the given bit vector. % The set above(N) contains nat numbers greater than n. %------------------------------------------------------------------------ sign_extend(k: above(N)): [bvec[N] -> bvec[k]] = (LAMBDA bv: IF bv(N-1) = 1 THEN bvec1[k-N] o bv ELSE bvec0[k-N] o bv ENDIF) %------------------------------------------------------------------------ % zero_extend_lsend returns a function that extends a bit vector to % length k by padding 0's at the least significant end of bvec. % That is, the bv2nat interpretation of the argument increases by 2**(k-N) %------------------------------------------------------------------------ zero_extend_lsend(k: above(N)): [bvec[N] -> bvec[k]] = (LAMBDA bv: bv o bvec0[k-N]) %------------------------------------------------------------------------ % lsb_extend returns a function that extends a bit vector to % length k by repeating the lsb of the bit vector at its % least significant end. %------------------------------------------------------------------------ lsb_extend(k: above(N)): [bvec[N] -> bvec[k]] = (LAMBDA bv: IF bv^0 = 0 THEN bv o bvec0[k-N] ELSE bv o bvec1[k-N] ENDIF) % ======= Useful theorems ================================================= IMPORTING bv_bitwise, bv_arithmetic zero_extend_lem : THEOREM bv2nat[k](zero_extend(k)(bv)) = bv2nat(bv) sign_to_zero : THEOREM sign_extend(k)(bv) = IF bv(N-1) = 1 THEN NOT(zero_extend(k)(NOT(bv))) ELSE zero_extend(k)(bv) ENDIF sign_extend_lem : THEOREM bv2int[k](sign_extend(k)(bv)) = bv2int(bv) zero_extend_lsend: THEOREM bv2nat(zero_extend_lsend(k)(bv)) = bv2nat(bv) * exp2(k-N) END bv_extend $$$bv_extend.prf (|bv_extend| (|zero_extend_TCC1| "" (GRIND) NIL) (|zero_extend_TCC2| "" (TCC :DEFS !) NIL) (|sign_extend_TCC1| "" (GROUND) NIL) (|sign_extend_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|sign_extend_TCC3| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|lsb_extend_TCC1| "" (GROUND) NIL) (|lsb_extend_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|lsb_extend_TCC3| "" (AUTO-REWRITE "bv_extractors.^" "bit.islow") (("" (GROUND) NIL))) (|zero_extend_lem| "" (SKOSIMP*) (("" (EXPAND "zero_extend") (("" (REWRITE "bvconcat2nat[k!1-N,N]") (("" (LEMMA "bv2nat_bvec0[k!1-N]") (("" (ASSERT) NIL))))))))) (|sign_to_zero_TCC1| "" (SUBTYPE-TCC) NIL) (|sign_to_zero| "" (SKOLEM 1 ("bv!1" "k!1")) (("" (EXPAND "sign_extend") (("" (EXPAND "zero_extend") (("" (LIFT-IF 1) (("" (SPLIT 1) (("1" (FLATTEN) (("1" (EXPAND "NOT") (("1" (EXPAND "NOT") (("1" (EXPAND "o ") (("1" (EXPAND "bvec1") (("1" (EXPAND "bvec0") (("1" (APPLY-EXTENSIONALITY 1) (("1" (HIDE 2) (("1" (LIFT-IF 1) (("1" (SPLIT 1) (("1" (FLATTEN) (("1" (ASSERT) (("1" (LIFT-IF 1) (("1" (ASSERT) NIL))))))) ("2" (FLATTEN) (("2" (PROPAX) NIL))))))))))))))))))))))) ("2" (FLATTEN) (("2" (PROPAX) NIL))))))))))))) (|sign_extend_lem_TCC1| "" (SKOSIMP*) (("" (TYPEPRED "k!1") (("" (ASSERT) NIL))))) (|sign_extend_lem| "" (SKOSIMP*) (("" (REWRITE "sign_to_zero") (("" (LIFT-IF) (("" (SPLIT 1) (("1" (FLATTEN) (("1" (LEMMA "twos_compl[k!1]") (("1" (INST -1 "NOT (zero_extend(k!1)(NOT bv!1))") (("1" (ASSERT) (("1" (CASE "bv2int(NOT (zero_extend(k!1)(NOT bv!1))) = -bv2int(zero_extend(k!1)(NOT bv!1)) - 1") (("1" (HIDE -2) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (CASE "bv2nat(zero_extend(k!1)(NOT bv!1)) = bv2nat(NOT bv!1)") (("1" (LEMMA "bv2int_lem[k!1]") (("1" (INST?) (("1" (REPLACE -1 1) (("1" (HIDE -1) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (CASE "zero_extend(k!1)(NOT bv!1)(k!1 - 1) = 0") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "twos_compl[N]") (("1" (INST?) (("1" (LEMMA "bv2int_lem[N]") (("1" (INST?) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "bv2int_lem[N]") (("1" (INST -1 "NOT bv!1") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (REPLACE -2) (("1" (CASE "(NOT bv!1)(N - 1) = 0") (("1" (ASSERT) NIL) ("2" (HIDE -1 2) (("2" (EXPAND "NOT") (("2" (EXPAND "NOT") (("2" (PROPAX) NIL))))))))))))))))))))))))))))))))))) ("2" (ASSERT) (("2" (HIDE -1 -2 2) (("2" (EXPAND "zero_extend") (("2" (EXPAND "NOT") (("2" (EXPAND "NOT") (("2" (EXPAND "o ") (("2" (EXPAND "bvec0") (("2" (PROPAX) NIL))))))))))))))))))))))))))))) ("2" (TYPEPRED "k!1") (("2" (ASSERT) (("2" (LEMMA "zero_extend_lem") (("2" (INST?) NIL))))))))))))))) ("2" (HIDE 2) (("2" (CASE "(NOT NOT (zero_extend(k!1)(NOT bv!1))) = zero_extend(k!1)(NOT bv!1)") (("1" (REPLACE -1 -2) (("1" (HIDE -1) (("1" (ASSERT) NIL))))) ("2" (HIDE -1 -2 2) (("2" (EXPAND "NOT") (("2" (APPLY-EXTENSIONALITY 1) (("2" (HIDE 2) (("2" (EXPAND "NOT") (("2" (ASSERT) (("2" (LIFT-IF 1) (("2" (LIFT-IF) (("2" (SPLIT 1) (("1" (FLATTEN) (("1" (ASSERT) NIL))) ("2" (FLATTEN) (("2" (SPLIT 2) (("1" (FLATTEN) (("1" (ASSERT) NIL))) ("2" (FLATTEN) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))) ("2" (TYPEPRED "k!1") (("2" (ASSERT) (("2" (TYPEPRED "k!1") (("2" (FLATTEN) (("2" (LEMMA "zero_extend_lem") (("2" (INST?) (("2" (LEMMA "bv2int_lem[k!1]") (("2" (INST?) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (LEMMA "bv2int_lem[N]") (("2" (INST?) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (EXPAND "zero_extend") (("2" (EXPAND "o ") (("2" (EXPAND "bvec0") (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))))) (|zero_extend_lsend| "" (SKOSIMP*) (("" (EXPAND "zero_extend_lsend") (("" (LEMMA "bvconcat2nat[N, k!1 - N]") (("" (INST?) (("" (REPLACE -1) (("" (HIDE -1) (("" (ASSERT) (("" (LEMMA "bv2nat_bvec0[k!1-N]") (("" (PROPAX) NIL)))))))))))))))))) $$$bv_manipulations.pvs bv_manipulations[n, m: posnat] : THEORY BEGIN IMPORTING bv_concat, bv_extractors i: VAR below(n) bvn: VAR bvec[n] bvm: VAR bvec[m] caret_bvec0 : LEMMA (FORALL (i: below(n)),(j: upto(i)): bvec0[n]^(i,j) = bvec0[i-j+1]) caret_bvec1 : LEMMA (FORALL (i: below(n)),(j: upto(i)): bvec1[n]^(i,j) = bvec1[i-j+1]) caret_concat_bot : THEOREM (FORALL (i: below(n)), (j: upto(i)): i < m IMPLIES (bvn o bvm)^(i,j) = bvm^(i,j)) caret_concat_top : THEOREM (FORALL (i: below(n)), (j: upto(i)): i >= m AND j >= m IMPLIES (bvn o bvm)^(i,j) = bvn^(i-m, j-m)) caret_concat_all : THEOREM (FORALL (i: below(n)), (j: upto(i)): i >= m AND j < m IMPLIES (bvn o bvm)^(i,j) = bvn^(i-m,0) o bvm^(m-1,j) ) concat_bottom : THEOREM (bvn o bvm)^((m-1), 0) = bvm concat_top : THEOREM (bvn o bvm)^((n+m-1), m) = bvn END bv_manipulations $$$bv_manipulations.prf (|bv_manipulations| (|caret_bvec0_TCC1| "" (AUTO-REWRITE-THEORY "integers") (("" (ASSERT) NIL))) (|caret_bvec0_TCC2| "" (TCC :DEFS !) NIL) (|caret_bvec0_TCC3| "" (AUTO-REWRITE-THEORY "integers") (("" (ASSERT) NIL))) (|caret_bvec0| "" (SKOLEM 1 ("i!1" "j!1")) (("" (EXPAND "^") (("" (EXPAND "bvec0") (("" (PROPAX) NIL))))))) (|caret_bvec1| "" (SKOLEM 1 ("i!1" "j!1")) (("" (EXPAND "^") (("" (EXPAND "bvec1") (("" (PROPAX) NIL))))))) (|caret_concat_bot_TCC1| "" (GROUND) (("" (SKOLEM 1 ("i!1")) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL))))) (|caret_concat_bot| "" (SKOSIMP*) (("" (EXPAND "^") (("" (APPLY-EXTENSIONALITY 1) (("" (HIDE 2) (("" (EXPAND "o") (("" (PROPAX) NIL))))))))))) (|caret_concat_top_TCC1| "" (GRIND) NIL) (|caret_concat_top_TCC2| "" (GROUND) (("" (SKOLEM 1 ("i!2" "j!1")) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL))))) (|caret_concat_top_TCC3| "" (SKOLEM 1 ("i!2" "j!1")) (("" (FLATTEN) (("" (ASSERT) NIL))))) (|caret_concat_top| "" (SKOSIMP*) (("" (EXPAND "^") (("" (APPLY-EXTENSIONALITY 1) (("" (HIDE 2) (("" (EXPAND "o ") (("" (PROPAX) NIL))))))))))) (|caret_concat_all_TCC1| "" (GRIND) NIL) (|caret_concat_all_TCC2| "" (GRIND) NIL) (|caret_concat_all_TCC3| "" (GROUND) (("" (SKOLEM 1 ("i!2" "j!1")) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL))))) (|caret_concat_all_TCC4| "" (GROUND) (("" (SKOLEM 1 ("i!2" "j!1")) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL))))) (|caret_concat_all_TCC5| "" (GROUND) (("" (SKOLEM 1 ("i!2" "j!1")) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL))))) (|caret_concat_all_TCC6| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|caret_concat_all_TCC7| "" (GRIND) NIL) (|caret_concat_all| "" (SKOSIMP*) (("" (EXPAND "o ") (("" (EXPAND "^") (("" (CASE "i!1 - j!1 + 1 = i!1 + 1 - j!1") (("1" (APPLY-EXTENSIONALITY 1) (("1" (HIDE 2) (("1" (LIFT-IF) (("1" (GROUND) NIL))))) ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (ASSERT) NIL))))) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (ASSERT) NIL))))) ("4" (HIDE 2) (("4" (SKOSIMP*) (("4" (ASSERT) NIL))))))) ("2" (HIDE 2) (("2" (ASSERT) NIL))))))))))) (|concat_bottom_TCC1| "" (ASSERT) (("" (ASSERT) (("" (ASSERT) NIL))))) (|concat_bottom_TCC2| "" (ASSERT) NIL) (|concat_bottom| "" (SKOLEM 1 ("bvm!1" "bvn!1")) (("" (EXPAND "o ") (("" (EXPAND "^") (("" (APPLY-EXTENSIONALITY 1) NIL))))))) (|concat_top_TCC1| "" (ASSERT) NIL) (|concat_top_TCC2| "" (ASSERT) NIL) (|concat_top| "" (SKOLEM 1 ("bvm!1" "bvn!1")) (("" (EXPAND "o ") (("" (EXPAND "^") (("" (APPLY-EXTENSIONALITY 1) NIL)))))))) $$$bv_rotate.pvs bv_rotate [N: posnat ] : THEORY %----------------------------------------------------------------------- % Defines rotate operations. % Introduces: % rotate_right(k: upto(N), bv: bvec[N]): bvec[N] % rotate_left(k: upto(N), bv: bvec[N]): bvec[N] % rot_r1(bv: bvec[N]): bvec[N] % rot_l1(bv: bvec[N]): bvec[N] %----------------------------------------------------------------------- BEGIN IMPORTING bv_concat, bv_extractors rotate_right(k: upto(N), bv: bvec[N]): bvec[N] = IF (k = 0) OR (k = N) THEN bv ELSE bv^(k-1,0) o bv^(N-1, k) ENDIF rotate_left(k: upto(N), bv: bvec[N]): bvec[N] = IF (k=0) OR (k = N) THEN bv ELSE bv^(N-k-1, 0) o bv^(N-1,N-k) ENDIF rot_r1(bv: bvec[N]): bvec[N] = rotate_right(1,bv) rot_l1(bv: bvec[N]): bvec[N] = rotate_left(1,bv) i: VAR below(N) k: VAR upto(N) bv: VAR bvec[N] rotate_right_0 : LEMMA rotate_right(0,bv)= bv rotate_right_lem : LEMMA rotate_right(k,bv)^i = IF i+k < N THEN bv^(i+k) ELSE bv^(i+k-N) ENDIF rotate_left_0 : LEMMA rotate_left(0,bv)= bv rotate_left_lem : LEMMA rotate_left(k,bv)^i = IF i-k >= 0 THEN bv^(i-k) ELSE bv^(N+i-k) ENDIF iterate_rot_r1 : LEMMA iterate(rot_r1,k)(bv) = rotate_right(k,bv) iterate_rot_l1 : LEMMA iterate(rot_l1,k)(bv) = rotate_left(k,bv) END bv_rotate $$$bv_rotate.prf (|bv_rotate| (|rotate_right_TCC1| "" (AUTO-REWRITE-THEORY "integers") (("" (ASSERT) NIL))) (|rotate_right_TCC2| "" (TCC :DEFS !) NIL) (|rotate_right_TCC3| "" (TCC :DEFS !) NIL) (|rotate_right_TCC4| "" (TCC :DEFS !) NIL) (|rotate_right_TCC5| "" (TCC :DEFS !) NIL) (|rotate_left_TCC1| "" (TCC :DEFS !) NIL) (|rotate_left_TCC2| "" (GRIND) NIL) (|rotate_left_TCC3| "" (TCC :DEFS !) NIL) (|rot_r1_TCC1| "" (TCC :DEFS !) NIL) (|rotate_right_0_TCC1| "" (TCC :DEFS !) NIL) (|rotate_right_0| "" (SKOSIMP*) (("" (EXPAND "rotate_right") (("" (PROPAX) NIL))))) (|rotate_right_lem_TCC1| "" (TCC :DEFS !) NIL) (|rotate_right_lem| "" (SKOSIMP*) (("" (EXPAND "rotate_right") (("" (EXPAND "^") (("" (EXPAND "o") (("" (LIFT-IF) (("" (LIFT-IF) (("" (ASSERT) NIL))))))))))))) (|rotate_left_0| "" (TCC :DEFS !) NIL) (|rotate_left_lem_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|rotate_left_lem_TCC2| "" (TCC :DEFS !) NIL) (|rotate_left_lem| "" (GRIND) NIL) (|iterate_rot_r1| "" (INDUCT "k" 1 "upto_induction[N]") (("1" (SKOSIMP*) (("1" (EXPAND "iterate") (("1" (EXPAND "rotate_right") (("1" (PROPAX) NIL))))))) ("2" (SKOSIMP*) (("2" (EXPAND "iterate" +) (("2" (INST -2 "bv!1") (("2" (REPLACE -2) (("2" (HIDE -2) (("2" (EXPAND "rotate_right") (("2" (EXPAND "rot_r1") (("2" (EXPAND "rotate_right") (("2" (EXPAND "^") (("2" (LIFT-IF) (("2" (ASSERT) (("2" (EXPAND "o") (("2" (LIFT-IF) (("2" (PROP) (("1" (ASSERT) NIL) ("2" (APPLY-EXTENSIONALITY 2) NIL) ("3" (REPLACE -1) (("3" (HIDE -1) (("3" (ASSERT) NIL))))) ("4" (ASSERT) (("4" (APPLY-EXTENSIONALITY 2) (("1" (HIDE 3) (("1" (LIFT-IF) (("1" (GROUND) NIL))))) ("2" (HIDE 2 3 4) (("2" (SKOSIMP*) (("2" (ASSERT) NIL))))) ("3" (HIDE 2 3 4) (("3" (SKOSIMP*) (("3" (ASSERT) NIL))))) ("4" (HIDE 2 3 4) (("4" (SKOSIMP*) (("4" (ASSERT) NIL))))) ("5" (HIDE 2 3 4) (("5" (SKOSIMP*) (("5" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))) (|iterate_rot_l1| "" (INDUCT "k" 1 "upto_induction[N]") (("1" (SKOSIMP*) (("1" (EXPAND "iterate") (("1" (EXPAND "rotate_left") (("1" (PROPAX) NIL))))))) ("2" (SKOSIMP*) (("2" (EXPAND "iterate" 1) (("2" (EXPAND "rotate_left" 1) (("2" (INST -2 "bv!1") (("2" (REPLACE -2) (("2" (HIDE -2) (("2" (EXPAND "rotate_left") (("2" (EXPAND "rot_l1") (("2" (EXPAND "rotate_left") (("2" (EXPAND "^") (("2" (LIFT-IF) (("2" (ASSERT) (("2" (EXPAND "o") (("2" (LIFT-IF) (("2" (PROP) (("1" (ASSERT) NIL) ("2" (APPLY-EXTENSIONALITY 2) NIL) ("3" (REPLACE -1) (("3" (HIDE -1) (("3" (ASSERT) NIL))))) ("4" (ASSERT) (("4" (APPLY-EXTENSIONALITY 2) (("1" (HIDE 3) (("1" (LIFT-IF) (("1" (GROUND) NIL))))) ("2" (HIDE 2 3 4) (("2" (SKOSIMP*) (("2" (ASSERT) NIL))))) ("3" (HIDE 2 3 4) (("3" (SKOSIMP*) (("3" (ASSERT) NIL))))) ("4" (HIDE 2 3 4) (("4" (SKOSIMP*) (("4" (ASSERT) NIL))))) ("5" (HIDE 2 3 4) (("5" (SKOSIMP*) (("5" (ASSERT) NIL))))) ("6" (HIDE 2 3 4) (("6" (SKOSIMP*) (("6" (ASSERT) NIL)))))))))))))))))))))))))))))))))))))))))) $$$bv_shift.pvs bv_shift [N: nat ] : THEORY %----------------------------------------------------------------------- % Defines shift operations. % Introduces: % left_shift(i: nat, bv: bvec[N]): bvec[N] % right_shift(i: nat, bv: bvec[N]): bvec[N] % left_shift_with(k: upto(N), bvk: bvec[k], bv: bvec[N]): bvec[N] % right_shift_with(k: upto(N), bvk: bvec[k], bv: bvec[N]): bvec[N] %----------------------------------------------------------------------- BEGIN IMPORTING bv_concat, bv_extractors %------------------------------------------------------------------------ % right_shift (left_shift) shifts a bit vector by a given number of % positions to the right (left) filling 0's to the shifted bits %------------------------------------------------------------------------ right_shift(i: nat, bv: bvec[N]): bvec[N] = IF i = 0 THEN bv ELSIF i < N THEN bvec0[i] o bv^(N-1, i) ELSE bvec0[N] ENDIF left_shift(i: nat, bv: bvec[N]): bvec[N] = IF i = 0 THEN bv ELSIF i < N THEN bv^(N-i-1, 0) o bvec0[i] ELSE bvec0[N] ENDIF %------------------------------------------------------------------------ % left_shift_with (right_shift_with) shifts a bit vector by a given % number of positions to the left (right) replacing the shifted bits % by the bit vector given as the second argument. %------------------------------------------------------------------------ left_shift_with(k: upto(N), bvk: bvec[k], bv: bvec[N]): bvec[N] = IF k = N THEN bvk ELSE bv^(N-k-1, 0) o bvk ENDIF right_shift_with(k: upto(N), bvk: bvec[k], bv: bvec[N]): bvec[N] = IF k = N THEN bvk ELSE bvk o bv^(N-1, k) ENDIF END bv_shift $$$bv_shift.prf (|bv_shift| (|right_shift_TCC1| "" (GRIND) NIL) (|right_shift_TCC2| "" (GROUND) (("" (SKOLEM!) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL))))) (|right_shift_TCC3| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|left_shift_TCC1| "" (GROUND) (("" (SKOLEM!) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL))))) (|left_shift_TCC2| "" (GRIND) NIL) (|left_shift_with_TCC1| "" (GROUND) (("" (SKOLEM!) (("" (FLATTEN) (("" (REPLACE -1) (("" (ASSERT) NIL))))))))) (|left_shift_with_TCC2| "" (GROUND) NIL) (|left_shift_with_TCC3| "" (GROUND) (("" (SKOLEM!) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL))))) (|left_shift_with_TCC4| "" (GRIND) NIL) (|right_shift_with_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|right_shift_with_TCC2| "" (GROUND) (("" (SKOLEM!) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL)))))) $$$sums.pvs sums: THEORY %------------------------------------------------------------------------------ % The summations theory introduces and defines properties of the sigma % function that sums an arbitrary function F: [nat -> nat] over a range % from low to high % % high % ---- % sigma(low, high, F) = \ F(j) % / % ---- % j = low % %------------------------------------------------------------------------------ BEGIN low, high, rng, l, h, n, m, x: VAR nat F, G: VAR function[nat -> nat] sigma(low, high, F): RECURSIVE nat = IF low > high THEN 0 ELSIF high = low THEN F(low) ELSE F(high) + sigma(low, high-1, F) ENDIF MEASURE (LAMBDA low, high, F: high) % sigma_rec(high, F): RECURSIVE nat % = IF high = 0 THEN F(0) % ELSE F(high) + sigma_rec(high-1, F) % ENDIF % MEASURE high % % sigma(low, high, F): nat % = IF low > high THEN 0 % ELSE sigma_rec(high - low, (LAMBDA n: F(n + low))) % ENDIF sigma_mult: THEOREM sigma(low, high, (LAMBDA n -> nat : x * F(n))) = x * sigma(low, high, F) sigma_split: THEOREM m >= low AND high > m IMPLIES sigma(low, high, F) = sigma(low, m, F) + sigma(m+1, high, F) sigma_shift: THEOREM sigma(low+m,high+m,F) = sigma(low,high, (LAMBDA n: F(n+m))) restrict(F, low, high): function[nat -> nat] = (LAMBDA n: IF n < low OR n > high THEN 0 ELSE F(n) ENDIF ) sigma_restrict_eq: THEOREM restrict(F,low,high) = restrict(G,low,high) IMPLIES sigma(low,high,F) = sigma(low,high,G) END sums $$$sums.prf (|sums| (|sigma_TCC1| "" (TCC) NIL) (|sigma_TCC2| "" (TCC) NIL) (|sigma_mult| "" (INDUCT "high") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (LIFT-IF) (("1" (GROUND) NIL))))))) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (ASSERT) (("2" (INST?) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (LIFT-IF) (("2" (GROUND) NIL))))))))))))))))) (|sigma_split| "" (INDUCT "high") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (LIFT-IF) (("1" (GROUND) NIL))))))) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1 1) (("2" (EXPAND "sigma" 1 2) (("2" (ASSERT) (("2" (CASE "j!1=m!1") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (ASSERT) NIL))))) ("2" (INST -1 "F!1" "low!1" "m!1") (("2" (ASSERT) NIL))))))))))))))) (|sigma_shift| "" (INDUCT "high") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (LIFT-IF) (("1" (GROUND) NIL))))))) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (LIFT-IF) (("2" (LIFT-IF) (("2" (ASSERT) (("2" (INST?) (("2" (GROUND) NIL))))))))))))))) (|sigma_restrict_eq| "" (INDUCT "high") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (EXPAND "restrict") (("1" (LIFT-IF) (("1" (GROUND) (("1" (CASE "(LAMBDA (n: nat): IF n > 0 THEN 0 ELSE F!1(n) ENDIF)(low!1) = (LAMBDA (n: nat): IF n > 0 THEN 0 ELSE G!1(n) ENDIF)(low!1)") (("1" (HIDE -2) (("1" (BETA -1) (("1" (LIFT-IF) (("1" (GROUND) NIL))))))) ("2" (HIDE 2 3) (("2" (REPLACE -1) (("2" (PROPAX) NIL))))))))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (LIFT-IF) (("2" (GROUND) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (HIDE -1) (("1" (EXPAND "restrict") (("1" (CASE " (LAMBDA (n: nat): IF n < low!1 OR n > low!1 THEN 0 ELSE F!1(n) ENDIF)(low!1) = (LAMBDA (n: nat): IF n < low!1 OR n > low!1 THEN 0 ELSE G!1(n) ENDIF)(low!1)") (("1" (HIDE -2) (("1" (BETA -1) (("1" (GROUND) NIL))))) ("2" (HIDE 2 3) (("2" (REPLACE -1) (("2" (PROPAX) NIL))))))))))))))) ("2" (INST -1 "F!1" "G!1" "low!1") (("2" (SPLIT -1) (("1" (ASSERT) (("1" (HIDE -1) (("1" (EXPAND "restrict") (("1" (CASE " (LAMBDA (n: nat): IF n < low!1 OR n > j!1 + 1 THEN 0 ELSE F!1(n) ENDIF)(j!1+1) = (LAMBDA (n: nat): IF n < low!1 OR n > j!1 + 1 THEN 0 ELSE G!1(n) ENDIF)(j!1+1)") (("1" (BETA -1) (("1" (HIDE -2) (("1" (LIFT-IF) (("1" (GROUND) NIL))))))) ("2" (REPLACE -1) (("2" (HIDE -1 2 3 4) (("2" (BETA 1) (("2" (LIFT-IF) (("2" (GROUND) NIL))))))))))))))))) ("2" (HIDE 3) (("2" (EXPAND "restrict") (("2" (HIDE 3) (("2" (APPLY-EXTENSIONALITY 1) (("2" (LIFT-IF) (("2" (GROUND) (("2" (CASE " (LAMBDA (n: nat): IF n < low!1 OR n > j!1 + 1 THEN 0 ELSE F!1(n) ENDIF)(x!1) = (LAMBDA (n: nat): IF n < low!1 OR n > j!1 + 1 THEN 0 ELSE G!1(n) ENDIF)(x!1)") (("1" (HIDE -2) (("1" (BETA -1) (("1" (LIFT-IF) (("1" (GROUND) NIL))))))) ("2" (REPLACE -1) (("2" (BETA 1) (("2" (ASSERT) NIL)))))))))))))))))))))))))))))))))) $$$bv_sum.pvs bv_sum[N: nat]: THEORY %------------------------------------------------------------------------------ % The bv_sum theory defines bv2nat as a summation over the bits in bv: % % N-1 % ---- % bv2nat_rec(bv) = \ exp2(n) * bv(n) % / % ---- % n = 0 % %------------------------------------------------------------------------------ BEGIN IMPORTING bv_nat, sums bv: VAR bvec[N] nn: VAR nat n, ii: VAR below(N) F: VAR function[below(N) -> nat] extend(F): function[nat -> nat] = (LAMBDA nn: IF nn < N THEN F(nn) ELSE 0 ENDIF) bv2nat_rec_as_sum: LEMMA bv2nat_rec(n+1,bv) = sigma(0,n, extend((LAMBDA ii: exp2(ii) * bv(ii)))) bv2nat_as_sum: THEOREM bv2nat(bv) = IF N = 0 THEN 0 ELSE sigma(0,N-1, extend((LAMBDA ii: exp2(ii) * bv(ii)))) ENDIF END bv_sum $$$bv_sum.prf (|bv_sum| (|bv2nat_rec_as_sum_TCC1| "" (TCC :DEFS !) NIL) (|bv2nat_rec_as_sum| "" (AUTO-REWRITE :NAMES ("bv2nat_rec" "sigma" "extend")) (("" (INDUCT "n" 1 NIL) (("1" (SKOSIMP*) (("1" (ASSERT) NIL))) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (LIFT-IF) (("2" (APPLY (THEN* (ASSERT) (BDDSIMP) (SKOSIMP*) (IF (LET* ((VAR '"n") (FNUM '1) (REWRITES '("bv2nat_rec" "sigma" "extend")) (NAME 'NIL) (DEFS 'NIL) (IF-MATCH 'BEST) (THEORIES 'NIL)) IF-MATCH) (INST? :IF-MATCH BEST) (SKIP)) (LIFT-IF)) "Applying assert, propositional simplification, instantiation, skolemization, and if-lifting") NIL))))))))))) (|bv2nat_as_sum_TCC1| "" (TCC) NIL) (|bv2nat_as_sum| "" (SKOSIMP*) (("" (LIFT-IF) (("" (EXPAND "bv2nat") (("" (GROUND) (("1" (EXPAND "bv2nat_rec") (("1" (PROPAX) NIL))) ("2" (LEMMA "bv2nat_rec_as_sum") (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))) $$$bv_concat_lems.pvs bv_concat_lems: THEORY BEGIN IMPORTING bv_concat null_bv: bvec[0] %% zero-length bit-vector % ===== (bvec,o,1) is a monoid =========================================== concat_identity_r : LEMMA (FORALL (n: nat), (bvn:bvec[n]): bvn o null_bv = bvn) concat_identity_l : LEMMA (FORALL (n: nat), (bvn:bvec[n]): null_bv o bvn = bvn) concat_associative : LEMMA (FORALL (m,n,p: nat), (bvm:bvec[m]), (bvn:bvec[n]), (bvp:bvec[p]): (bvm o bvn) o bvp = bvm o (bvn o bvp)) END bv_concat_lems $$$bv_concat_lems.prf (|bv_concat_lems| (|concat_identity_r| "" (SKOSIMP*) (("" (APPLY-EXTENSIONALITY 1) (("" (HIDE 2) (("" (EXPAND "o ") (("" (PROPAX) NIL))))))))) (|concat_identity_l| "" (SKOSIMP*) (("" (APPLY-EXTENSIONALITY 1) (("" (HIDE 2) (("" (EXPAND "o ") (("" (PROPAX) NIL))))))))) (|concat_associative| "" (SKOSIMP*) (("" (APPLY-EXTENSIONALITY 1) (("" (HIDE 2) (("" (EXPAND "o ") (("" (LIFT-IF) (("" (GROUND) NIL)))))))))))) $$$bv_concat_nat.pvs bv_concat_nat [n:nat, m:nat ]: THEORY BEGIN IMPORTING bv_concat_lems, bv_sum bvn: VAR bvec[n] bvm: VAR bvec[m] nm: VAR below(n+m) bvconcat2nat: THEOREM bv2nat[n+m](bvn o bvm) = bv2nat[n](bvn) * exp2(m) + bv2nat[m](bvm) END bv_concat_nat $$$bv_concat_nat.prf (|bv_concat_nat| (|bvconcat2nat_TCC1| "" (SAME-NAME-TCC) NIL) (|bvconcat2nat| "" (SKOSIMP*) (("" (CASE "m = 0") (("1" (REPLACE -1) (("1" (EXPAND "bv2nat" 1 3) (("1" (EXPAND "bv2nat_rec") (("1" (REWRITE "bvconcat_bot0") (("1" (EXPAND "exp2") (("1" (REPLACE -1) (("1" (ASSERT) (("1" (SAME-NAME "bv2nat[n + m]" "bv2nat[n]") (("1" (ASSERT) NIL))))))))))))))))) ("2" (CASE "n = 0") (("1" (EXPAND "bv2nat" + 2) (("1" (SAME-NAME "bv2nat[n + m]" "bv2nat[m]") (("1" (REPLACE -1) (("1" (EXPAND "bv2nat_rec") (("1" (ASSERT) (("1" (REWRITE "bvconcat_top0") NIL))))))) ("2" (PROPAX) NIL))))) ("2" (REWRITE "bv2nat_as_sum[n+m]") (("2" (LEMMA "sigma_split") (("2" (INST -1 "extend((LAMBDA (ii: below(n + m)): exp2(ii) * (bvn!1 o bvm!1)(ii)))" "n+m-1" "0" "m-1") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (CASE "sigma(0, m - 1, extend((LAMBDA (ii: below(n + m)): exp2(ii) * (bvn!1 o bvm!1)(ii)))) = bv2nat[m](bvm!1)") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (ASSERT) (("1" (LEMMA "sigma_shift") (("1" (EXPAND "extend") (("1" (EXPAND "o ") (("1" (INST -1 " (LAMBDA (nn: nat): IF nn < n + m THEN exp2(nn) * IF nn < m THEN bvm!1(nn) ELSE bvn!1(nn - m) ENDIF ELSE 0 ENDIF)" "n-1" "0" "m") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (REWRITE "bv2nat_as_sum[n]") (("1" (LEMMA "sigma_mult") (("1" (INST -1 "extend((LAMBDA (ii: below(n)): exp2(ii) * bvn!1(ii)))" "n-1" "0" "exp2(m)") (("1" (REPLACE -1 + RL) (("1" (HIDE -1) (("1" (EXPAND "extend") (("1" (REWRITE "sigma_restrict_eq") (("1" (HIDE 2 3 4) (("1" (EXPAND "restrict") (("1" (APPLY-EXTENSIONALITY 1) (("1" (HIDE 2) (("1" (LIFT-IF) (("1" (LEMMA "exp2_sum") (("1" (INST?) (("1" (GROUND) NIL))))))))) ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (ASSERT) NIL))))))))))) ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (ASSERT) NIL))))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (ASSERT) NIL))))))))))))))))) ("2" (ASSERT) (("2" (HIDE 4) (("2" (REWRITE "bv2nat_as_sum[m]") (("2" (REWRITE "sigma_restrict_eq") (("2" (HIDE 2) (("2" (EXPAND "extend") (("2" (EXPAND "restrict") (("2" (APPLY-EXTENSIONALITY 1) (("1" (HIDE 2) (("1" (LIFT-IF) (("1" (GROUND) (("1" (EXPAND "o ") (("1" (PROPAX) NIL))))))))) ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (ASSERT) NIL))))) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (ASSERT) NIL))))))))))))))))))))))))))))) ("2" (ASSERT) NIL) ("3" (ASSERT) NIL)))))))))))))) $$$bv_int.pvs bv_int[N: posnat]: THEORY %------------------------------------------------------------------------------ % This theory introduces the functions bv2int and int2bv that convert % between bit vectors and natural numbers. These are based upon % twos-complement interpretation. % % Introduces: % bv2int : [bvec -> rng_2s_comp] % int2bv : [rng_2s_comp -> bvec] %------------------------------------------------------------------------------ BEGIN IMPORTING bv_nat[N] n: VAR upto(N) bv, bv1, bv2: VAR bvec % === Range of bv2int ========================================================= minint: int = -exp2(N-1) maxint: int = exp2(N-1) - 1 in_rng_2s_comp(i: int): bool = (minint <= i AND i <= maxint) rng_2s_comp: TYPE = {i: int | minint <= i AND i <= maxint} % === Preliminary results needed for proofs of TCCs =========================== bv2nat_top_bit: THEOREM IF bv2nat(bv) < exp2(N-1) THEN bv(N-1) = 0 ELSE bv(N-1) = 1 ENDIF % === Interpretation of a bit vector as an integer =========================== bv2int(bv: bvec): rng_2s_comp = IF bv2nat(bv) < exp2(N-1) THEN bv2nat(bv) ELSE bv2nat(bv) - exp2(N) ENDIF int2bv(iv: rng_2s_comp):bvec = inverse(bv2int)(iv) ; % === Properties of bv2int and int2bv ========================================= iv: VAR rng_2s_comp % ---------------------------------------------------------------------- % bv2int_inj is injective, i.e., % (FORALL (x, y: bvec[N]): (bv2int(x) = bv2int(y) => (x = y))) % ---------------------------------------------------------------------- bv2int_inj: THEOREM injective?(bv2int) % ---------------------------------------------------------------------- % bv2int is surjective, i.e., % (FORALL (y: rng_2s_comp): (EXISTS (x: bvec[N]): bv2int(x) = y)) % ---------------------------------------------------------------------- bv2int_surj: THEOREM surjective?(bv2int) % ---------------------------------------------------------------------- % b2int and int2bv are bijective (injective and surjective) % ---------------------------------------------------------------------- bv2int_bij : THEOREM bijective?(bv2int) bv2int_inv : THEOREM bv2int(int2bv(iv))=iv; bv2int_lem : THEOREM bv2int(bv) = bv2nat(bv) - exp2(N) * bv(N - 1) END bv_int $$$bv_int.prf (|bv_int| (|minint_TCC1| "" (ASSERT) NIL) (|bv2nat_top_bit_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|bv2nat_top_bit_TCC2| "" (AUTO-REWRITE-EXPLICIT) (("" (GROUND) (("" (SKOLEM 1 ("bv!1")) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL))))))) (|bv2nat_top_bit| "" (SKOSIMP*) (("" (EXPAND "bv2nat") (("" (EXPAND "bv2nat_rec") (("" (LIFT-IF) (("" (ASSERT) (("" (ASSERT) (("" (LEMMA "bv_lem") (("" (INST?) (("" (GROUND) (("" (REPLACE -1) (("" (ASSERT) (("" (REWRITE "bv2nat_rec_bound") NIL))))))))))))))))))))))) (|bv2int_TCC1| "" (SKOSIMP*) (("" (EXPAND "minint") (("" (EXPAND "maxint") (("" (ASSERT) NIL))))))) (|bv2int_TCC2| "" (SKOSIMP*) (("" (EXPAND "minint") (("" (EXPAND "maxint") (("" (ASSERT) (("" (EXPAND "exp2" 2 2) (("" (ASSERT) NIL))))))))))) (|bv2int_inj| "" (EXPAND "injective?") (("" (SKOSIMP *) (("" (LEMMA "bv2nat_inj") (("" (EXPAND "injective?") (("" (INST?) (("" (EXPAND "bv2int") (("" (LIFT-IF) (("" (SPLIT -2) (("1" (LIFT-IF) (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (ASSERT) NIL))) ("2" (FLATTEN) (("2" (ASSERT) NIL))))))) ("2" (FLATTEN) (("2" (LIFT-IF -1) (("2" (SPLIT -1) (("1" (FLATTEN) (("1" (ASSERT) NIL))) ("2" (FLATTEN) (("2" (ASSERT) NIL))))))))))))))))))))))))) (|bv2int_surj| "" (EXPAND "surjective?") (("" (SKOSIMP *) (("" (CASE "(FORALL (m: {i:int | i >= minint AND i < 0}): (EXISTS bv: bv2int(bv) = m))") (("1" (CASE "(FORALL (m: {i:int | i >= 0 AND i <= maxint}): (EXISTS bv: bv2int(bv) = m))") (("1" (CASE "y!1 >= 0") (("1" (INST -2 "y!1") NIL) ("2" (INST -2 "y!1") (("2" (ASSERT) NIL))))) ("2" (HIDE -1 2) (("2" (SKOSIMP *) (("2" (EXPAND "bv2int") (("2" (TYPEPRED "m!1") (("2" (LEMMA "bv2nat_surj") (("2" (EXPAND "surjective?") (("2" (INST -1 "m!1") (("1" (SKOLEM -1 ("bv!1")) (("1" (INST 1 "bv!1") (("1" (EXPAND "maxint") (("1" (ASSERT) NIL))))))) ("2" (EXPAND "maxint") (("2" (EXPAND "exp2" 1) (("2" (HIDE 2) (("2" (LIFT-IF 1) (("2" (SPLIT 1) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))))))))))))))) ("2" (HIDE 2) (("2" (SKOSIMP *) (("2" (EXPAND "bv2int") (("2" (TYPEPRED "m!1") (("2" (LEMMA "bv2nat_surj") (("2" (EXPAND "surjective?") (("2" (INST -1 "m!1 + exp2(N)") (("1" (SKOLEM -1 ("bv!1")) (("1" (INST 1 "bv!1") (("1" (EXPAND "minint") (("1" (ASSERT) (("1" (LIFT-IF 1) (("1" (SPLIT 1) (("1" (FLATTEN) (("1" (ASSERT) (("1" (EXPAND "exp2" -2) (("1" (ASSERT) NIL))))))) ("2" (FLATTEN) (("2" (ASSERT) NIL))))))))))))))) ("2" (EXPAND "minint") (("2" (EXPAND "exp2" 1) (("2" (HIDE 2) (("2" (LIFT-IF 1) (("2" (SPLIT 1) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))))))))))))))))))) (|bv2int_bij| "" (EXPAND "bijective?") (("" (LEMMA "bv2int_inj") (("" (LEMMA "bv2int_surj") (("" (ASSERT) NIL))))))) (|bv2int_inv| "" (SKOLEM!) (("" (EXPAND "int2bv") (("" (LEMMA "surj_right" ("f" "bv2int")) (("" (EXPAND "right_inverse?") (("" (REWRITE "bv2int_surj") (("" (ASSERT) (("" (INST?) NIL))))))))))))) (|bv2int_lem_TCC1| "" (TCC) NIL) (|bv2int_lem| "" (SKOLEM 1 ("bv!1")) (("" (EXPAND "bv2int") (("" (LIFT-IF) (("" (LEMMA "bv2nat_top_bit") (("" (INST -1 "bv!1") (("" (SPLIT 1) (("1" (FLATTEN) (("1" (ASSERT) NIL))) ("2" (FLATTEN) (("2" (ASSERT) NIL)))))))))))))))) $$$bv_extractors.pvs bv_extractors[N: nat]: THEORY %----------------------------------------------------------------------- % An extractor operation decomposes a bvec into smaller % bit vectors. In the following, we define a number of % extractors for bvec. % % Introduces: % bv^(i,j) creates bv[i-j+1] from bits i through j % % %----------------------------------------------------------------------- BEGIN IMPORTING bv %----------------------------------------------------------------------- % The following operator (^) extracts a contiguous fragment of % a bit vector between two given positions. %----------------------------------------------------------------------- ^(bv: bvec[N], sp:[i1: below(N), upto(i1)]): bvec[proj_1(sp)-proj_2(sp)+1] = (LAMBDA (ii: below(proj_1(sp) - proj_2(sp) + 1)): bv(ii + proj_2(sp))) ; % === Useful Lemmas and Theorems ========================================= bv: VAR bvec[N] caret_all: LEMMA N > 0 IMPLIES bv^(N-1, 0) = bv END bv_extractors $$$bv_extractors.prf (|bv_extractors| (|caret_TCC1| "" (GRIND) NIL) (|caret_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|caret_TCC3| "" (GRIND) NIL) (|caret_TCC4| "" (SUBTYPE-TCC) NIL) (|caret_all_TCC1| "" (FLATTEN) (("" (ASSERT) NIL))) (|caret_all_TCC2| "" (GROUND) NIL) (|caret_all| "" (SKOSIMP*) (("" (EXPAND "^") (("" (APPLY-EXTENSIONALITY 1) NIL)))))) $$$bv_fract.pvs bv_fract [N: above(1)]: THEORY %------------------------------------------------------------------------------ % Defines an interpretation of bit vectors as 2's complement fractions. % % Introduces: % bv2fract: function [bvec[N] -> bv2fract_range] %------------------------------------------------------------------------------ BEGIN IMPORTING bv, exp2 %---------------------------------------------------------------------------- % Using a 2's complement representation, a bit vector of size N can % represent any fraction of the form i/exp2(N-1) as a rational number, % where i ranges over all integers representable by a bit vector of size N. % The predicate bv2fract_range characterizes this set of rationals. %--------------------------------------------------------------------------- fract_numerator_range: TYPE = {i: int| i >= -exp2(N-1) & i < exp2(N-1)} bv2fract_range(r: rational): bool = (EXISTS (i: fract_numerator_range): (r = i/exp2(N-1)) ) bv2fract_range: TYPE = (bv2fract_range) CONTAINING 0 bv2fract: [bvec[N] -> bv2fract_range] %--------------------------------------------------------------------------- % The following min and max definitions ignore 0 and -1, instead % naming their nearest fractional representations. %--------------------------------------------------------------------------- min_pos_fract: bv2fract_range = 1/exp2(N-1) max_pos_fract: bv2fract_range = 1 - 1/exp2(N-1) min_neg_fract: bv2fract_range = -1/exp2(N-1) max_neg_fract: bv2fract_range = -1 + 1/exp2(N-1) END bv_fract $$$bv_fract.prf (|bv_fract| (|fract_numerator_range_TCC1| "" (GROUND) NIL) (|bv2fract_range_TCC1| "" (TCC) NIL) (|bv2fract_TCC1| "" (ASSERT) NIL) (|min_pos_fract_TCC1| "" (ASSERT) (("" (EXPAND "bv2fract_range") (("" (INST 1 "1") (("" (ASSERT) (("" (EXPAND "exp2") (("" (ASSERT) NIL))))))))))) (|max_pos_fract_TCC1| "" (EXPAND "bv2fract_range") (("" (INST 1 "exp2(N-1) - 1") (("1" (ASSERT) NIL) ("2" (AUTO-REWRITE-THEORY "integers") (("2" (ASSERT) NIL))) ("3" (ASSERT) NIL))))) (|min_neg_fract_TCC1| "" (EXPAND "bv2fract_range") (("" (INST 1 "-1") (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "integers") (("" (ASSERT) NIL))))))))) (|max_neg_fract_TCC1| "" (EXPAND "bv2fract_range") (("" (AUTO-REWRITE-THEORY "integers") (("" (INST 1 "1 - exp2(N-1)") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (ASSERT) NIL)))))))) $$$bv_concat.pvs bv_concat [n:nat, m:nat ]: THEORY %------------------------------------------------------------------------ % This theory defines the concatenation operator o for bitvectors: % % o: [bvec[n], bvec[m] -> bvec[n+m]] % % The bit vector binary ops theory defines functions that take % two bit vectors as their primary inputs. The theory is % instantiated with the sizes of the input bit vectors. %------------------------------------------------------------------------ BEGIN IMPORTING bv o(bvn: bvec[n], bvm: bvec[m]): bvec[n+m] = (LAMBDA (nm: below(n+m)): IF nm < m THEN bvm(nm) ELSE bvn(nm - m) ENDIF) bvn: VAR bvec[n] bvm: VAR bvec[m] bvconcat_bot0: THEOREM m = 0 IMPLIES bvn o bvm = bvn bvconcat_top0: THEOREM n = 0 IMPLIES bvn o bvm = bvm %------------------------------------------------------------------------ % See bv_concat_lems for proof that (bvec,o,null_bv) is a monoid % See bv_concat_nat for lemma giving bv2nat(bvn o bvm) %------------------------------------------------------------------------ END bv_concat $$$bv_concat.prf (|bv_concat| (|oh_TCC1| "" (TCC) NIL) (|oh_TCC2| "" (SUBTYPE-TCC) NIL) (|bvconcat_bot0_TCC1| "" (SUBTYPE-TCC) NIL) (|bvconcat_bot0| "" (SKOSIMP*) (("" (EXPAND "o ") (("" (APPLY-EXTENSIONALITY 1) (("" (REPLACE -1) (("" (ASSERT) NIL))))))))) (|bvconcat_top0_TCC1| "" (SUBTYPE-TCC) NIL) (|bvconcat_top0| "" (SKOSIMP*) (("" (EXPAND "o ") (("" (APPLY-EXTENSIONALITY 1) (("" (REPLACE -1) (("" (ASSERT) NIL)))))))))) $$$exp2.pvs exp2: THEORY BEGIN n,m, x1, x2: VAR nat exp2(n: nat): RECURSIVE posnat = IF n = 0 THEN 1 ELSE 2 * exp2(n - 1) ENDIF MEASURE n % === Properties of exp2 =================================================== exp2_def : LEMMA exp2(n) = 2^n exp2pos : LEMMA exp2(n)>0 exp2_n : LEMMA exp2(n+1) = 2*exp2(n) exp2_sum : LEMMA exp2(n + m) = exp2(n) * exp2(m) exp2_minus : LEMMA (FORALL n,(k:upto(n)): exp2(n-k)=exp2(n)/exp2(k)) exp2_strictpos : LEMMA n > 0 IMPLIES exp2(n) > 1 exp2_lt : LEMMA n < m IMPLIES exp2(n) < exp2(m) exp_prop : LEMMA x1 < exp2(n) AND x2 < exp2(m) IMPLIES x1 * exp2(m) + x2 < exp2(n + m) END exp2 $$$exp2.prf (|exp2| (|exp2_TCC1| "" (SKOLEM 1 ("n!1")) (("" (FLATTEN) (("" (ASSERT) NIL))))) (|exp2_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|exp2_def| "" (INDUCT-AND-REWRITE "n" 1 "^" "expt" "exp2") NIL) (|exp2pos| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|exp2_n| "" (SKOSIMP*) (("" (REWRITE "exp2_def") (("" (REWRITE "expt_plus") (("" (REWRITE "expt_x1") (("" (REWRITE "exp2_def") NIL))))))))) (|exp2_sum| "" (SKOSIMP*) (("" (REWRITE "exp2_def") (("" (REWRITE "expt_plus") (("" (REWRITE "exp2_def") (("" (REWRITE "exp2_def") (("" (ASSERT) NIL))))))))))) (|exp2_minus_TCC1| "" (SUBTYPE-TCC) NIL) (|exp2_minus| "" (SKOSIMP*) (("" (REWRITE "exp2_def") (("" (REWRITE "exp2_def") (("" (REWRITE "exp2_def") (("" (REWRITE "minus_add") (("" (ASSERT) (("" (TYPEPRED "k!1") (("" (CASE "k!1=0") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "expt_x0") (("1" (INST -1 "2") (("1" (ASSERT) NIL))))))))))) ("2" (ASSERT) (("2" (REWRITE "expt_plus") (("2" (EXPAND "^") (("2" (ASSERT) NIL))))))))))))))))))))))) (|exp2_strictpos| "" (INDUCT "n") (("1" (EXPAND "exp2") (("1" (PROPAX) NIL))) ("2" (SKOLEM 1 ("j!1")) (("2" (FLATTEN) (("2" (LEMMA "exp2_n" ("n" "j!1")) (("2" (TYPEPRED "j!1") (("2" (CASE "j!1 = 0") (("1" (ASSERT) (("1" (ASSERT) (("1" (EXPAND "exp2") (("1" (ASSERT) NIL))))))) ("2" (ASSERT) NIL))))))))))))) (|exp2_lt| "" (INDUCT "m" 1) (("1" (SKOLEM 1 ("j!1")) (("1" (FLATTEN) (("1" (ASSERT) NIL))))) ("2" (SKOLEM 1 ("j!1")) (("2" (FLATTEN) (("2" (SKOLEM 1 ("n!1")) (("2" (FLATTEN) (("2" (INST -1 "n!1") (("2" (EXPAND "exp2" 1 2) (("2" (CASE "n!1 = j!1") (("1" (REPLACE -1 * RL) (("1" (ASSERT) NIL))) ("2" (ASSERT) NIL))))))))))))))))) (|exp_prop| "" (SKOSIMP*) (("" (REWRITE "exp2_sum") (("" (LEMMA "both_sides_times_pos_le1") (("" (INST -1 "exp2(m!1)" "x1!1" "exp2(n!1)-1") (("" (ASSERT) NIL)))))))))) $$$bv_nat.pvs bv_nat[N: nat]: THEORY % ----------------------------------------------------------------------- % This theory introduces the functions bv2nat and nat2bv that convert % between bit vectors and natural numbers. % % Introduces: % bv2nat: function[bvec -> below(exp2(N))] % nat2bv: function[below(exp2(N)) -> bvec] % ----------------------------------------------------------------------- BEGIN IMPORTING bv[N], exp2 % === Interpretation of a bit vector as a natural number ================ % ---------------------------------------------------------------------- % bv2nat_rec is an auxilliary function used only to define bv2nat. % It interprets the lower portion of a bit vector as a natural number. % ---------------------------------------------------------------------- bv2nat_rec(n: upto(N), bv:bvec): RECURSIVE nat = IF n = 0 THEN 0 ELSE exp2(n-1) * bv(n-1) + bv2nat_rec(n - 1, bv) ENDIF MEASURE n bv_lem: LEMMA (FORALL (n: below(N)),(bv: bvec): bv(n) = 0 OR bv(n) = 1) bv2nat_rec_bound: LEMMA (FORALL (n: upto(N)),(bv: bvec): bv2nat_rec(n, bv) < exp2(n)) bv2nat(bv:bvec): below(exp2(N)) = bv2nat_rec(N, bv) nat2bv(val:below(exp2(N))): bvec = inverse(bv2nat)(val) % === Properties of bv2nat and nat2bv =================================== n : VAR upto(N) val : VAR below(exp2(N)) bv, bv1, bv2: VAR bvec uniqueness: LEMMA N /= 0 IMPLIES bvec0 /= bvec1 % ---------------------------------------------------------------------- % bv2nat_rec is injective over the lower n bits. % ---------------------------------------------------------------------- bv2nat_inj_rec: LEMMA bv2nat_rec(n, bv1) = bv2nat_rec(n, bv2) <=> (FORALL (m: below(N)): (m < n) => bv1(m) = bv2(m)) % ---------------------------------------------------------------------- % bv2nat_rec is surjective over the lower n bits. % ---------------------------------------------------------------------- bv2nat_surj_rec: LEMMA FORALL (y:below(exp2(n))): EXISTS bv:bv2nat_rec(n, bv) = y % ---------------------------------------------------------------------- % bv2nat is injective, i.e. % (FORALL (x, y: bvec): (bv2nat(x) = bv2nat(y) => (x = y))) % ---------------------------------------------------------------------- bv2nat_inj : THEOREM injective?(bv2nat) % ---------------------------------------------------------------------- % bv2nat is surjective, i.e. % (FORALL (y: below(exp2(N))): (EXISTS (x: bvec): bv2nat(x) = y)) % ---------------------------------------------------------------------- bv2nat_surj : THEOREM surjective?(bv2nat) % ---------------------------------------------------------------------- % bv2nat is bijective (injective and surjective) % ---------------------------------------------------------------------- bv2nat_bij : THEOREM bijective?(bv2nat) bv2nat_inv : THEOREM bv2nat(nat2bv(val)) = val % === Useful lemmas ===================================================== nat2bv_bij : THEOREM bijective?(nat2bv) nat2bv_inv : THEOREM nat2bv(bv2nat(bv)) = bv bv2nat_rec_bvec0 : LEMMA bv2nat_rec(n, bvec0) = 0 bv2nat_bvec0 : LEMMA bv2nat(bvec0) = 0 bv2nat_rec_bvec1 : LEMMA bv2nat_rec(n, bvec1) = exp2(n)-1 bv2nat_bvec1 : LEMMA bv2nat(bvec1) = exp2(N)-1 END bv_nat $$$bv_nat.prf (|bv_nat| (|bv2nat_rec_TCC1| "" (GROUND) (("" (SKOLEM 1 ("n!1")) (("" (APPLY (THEN (GROUND) (ASSERT))) NIL))))) (|bv2nat_rec_TCC2| "" (GROUND) (("" (TCC) NIL))) (|bv2nat_rec_TCC3| "" (TCC) NIL) (|bv2nat_rec_TCC4| "" (TCC) NIL) (|bv_lem| "" (SKOSIMP) (("" (ASSERT) NIL))) (|bv2nat_rec_bound| "" (INDUCT-AND-REWRITE "n" 1 "bv2nat_rec" "exp2") (("" (LEMMA "bv_lem") (("" (INST - "jt!1" "bv!1") (("" (GROUND) NIL))))))) (|bv2nat_TCC1| "" (GROUND) NIL) (|bv2nat_TCC2| "" (SKOSIMP*) (("" (REWRITE "bv2nat_rec_bound") NIL))) (|uniqueness| "" (CASE "bvec0(0)=bvec1(0)") (("1" (TCC) NIL) ("2" (PROP) (("2" (REPLACE -1) (("2" (PROPAX) NIL))))) ("3" (ASSERT) NIL))) (|bv2nat_inj_rec| "" (INDUCT "n") (("1" (TCC) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (EXPAND "bv2nat_rec" +) (("2" (INST - "bv1!1" "bv2!1") (("2" (BDDSIMP) (("1" (SKOSIMP*) (("1" (INST?) (("1" (ASSERT) (("1" (ASSERT) (("1" (REWRITE "both_sides_times2") NIL))))))))) ("2" (ASSERT) (("2" (INST -4 "jt!1") (("2" (ASSERT) NIL))))) ("3" (LEMMA "bv2nat_rec_bound") (("3" (INST-CP - "jt!1" "bv1!1") (("3" (INST - "jt!1" "bv2!1") (("3" (LEMMA "bv_lem") (("3" (INST-CP - "jt!1" "bv1!1") (("3" (INST - "jt!1" "bv2!1") (("3" (GROUND) NIL))))))))))))) ("4" (SKOSIMP*) (("4" (INST?) (("4" (ASSERT) NIL))))))))))))))))) (|bv2nat_surj_rec| "" (INDUCT "n" 1 "upto_induction[N]") (("1" (SKOSIMP*) (("1" (TYPEPRED "y!1") (("1" (TCC) (("1" (INST + "bvec0") NIL))))))) ("2" (SKOSIMP*) (("2" (TYPEPRED "y!1") (("2" (EXPAND "exp2") (("2" (EXPAND "bv2nat_rec" +) (("2" (CASE "forall bv,(b:bit),(n:below(N)),(m:{n1:below(N)|n<=n1}): bv2nat_rec(n,bv)=bv2nat_rec(n,bv with [(m):=b])") (("1" (CASE "y!1 bit] % ^(bv, (i: below(N))): bit % ----------------------------------------------------------------------- BEGIN IMPORTING bit bvec : TYPE = [below(N) -> bit] bvec1: bvec = (LAMBDA (n: below(N)) : 1) bvec0: bvec = (LAMBDA (n: below(N)) : 0) fill(b: bit): bvec = (LAMBDA (n: below(N)): b) fill_lem: LEMMA fill(0) = bvec0 AND fill(1) = bvec1 unspecified_bool : bool unspecified_bit : bit unspecified_bvec : bvec %----------------------------------------------------------------------- % The implementation of the bitvector can be hidden through use of % the ^ function below. %----------------------------------------------------------------------- ^(bv: bvec, (i: below(N))): bit = bv(i) END bv $$$bv.prf (|bv| (|bvec1_TCC1| "" (TCC) NIL) (|bvec0_TCC1| "" (TCC) NIL) (|fill_lem_TCC1| "" (SUBTYPE-TCC) NIL) (|fill_lem_TCC2| "" (SUBTYPE-TCC) NIL) (|fill_lem| "" (EXPAND "fill") (("" (EXPAND "bvec0") (("" (EXPAND "bvec1") (("" (PROPAX) NIL))))))) (|unspecified_bit_TCC1| "" (INST 1 "0") NIL)) $$$bv_top.pvs bv_top[N: nat]: THEORY %------------------------------------------------------------------------ % Top of bit-vectors theory. % -------------------------- % Authors: Paul Miner % Ricky W. Butler % Mandayam Srivas % Steve Miller % Dave Greve % % Index: % ------ % bv -- basic definition of bitvector type "bvec" % bv_nat -- interpretes bvec as a natural number % bv_int -- interpretes bvec as an integer % bv_arithmetic -- defines basic operators (i.e. + - >) over % bitvectors % bv_extractors -- defines extractor operator ^ that % bv_concat -- defines concatenation operator o % creates smaller bitvectors from larger % bv_concat_lems: establishes that concat is a monoid % bv_concat_nat: formula for bv2nat of concat % bv_manipulations -- lemmas concerning ^ and o % bv_bitwise -- defines bit-wise logical operations on bitvectors % bv_bitwise_lems: lemmas about bit-wise logical operations % bv_shift -- defines shift operations % bv_extend -- zero and sign extend operations % bv_fract -- defines fractional interpretation of a bitvector % bv_select -- defines operators bv_select and bv_assign % bv_rules -- rewrite-oriented bv lemmas % % % bv % | % ------------------------------------------------------------ % | | | | | % bv_bitwise bv_nat bv_concat bv_fract bv_extractors % | | | | | % | | -------- ------------------------------- | % | | | | | | | | % | | bv_int | bv_concat_nat bv_concat_lems | | % | | | | | | | % | | | | | ========================================== % | | | bv_arith_nat | || || || || % | | | | | bv_shift bv_rotate bv_manipulations bv_extend % | | | | | / % | | | | | / % | | | | | / % | | | | | | % | | | bv_arith_shift % | | | | % | bv_arithmetic % | % bv_bitwise_lems %---------------------------------------------------------------------------- BEGIN IMPORTING bv, bv_bitwise, bv_nat, bv_concat, bv_fract, bv_extractors, bv_int, bv_concat_nat, bv_concat_lems, bv_shift, bv_rotate, bv_manipulations, bv_extend, bv_arithmetic, bv_bitwise_lems, bv_select, bv_rules END bv_top $$$div_nt_alt.pvs div_nt_alt: THEORY BEGIN IMPORTING div_nt n: VAR nat m: VAR posnat natdiv(n,m): RECURSIVE nat = (IF n>=m THEN 1+natdiv(n-m, m) ELSE 0 ENDIF) MEASURE (LAMBDA n,m: n) i,k: VAR int j: VAR nonzero_integer is_multiple(i,j): bool = (EXISTS k: i = k*j) rdiv(i,j): integer = IF sgn(i) = sgn(j) THEN natdiv(abs(i),abs(j)) ELSIF is_multiple(i,j) THEN -natdiv(abs(i),abs(j)) ELSE -natdiv(abs(i),abs(j))-1 ENDIF floor_is_natdiv: LEMMA natdiv(n,m) = floor(n/m) rdiv_lem: LEMMA div(i,j) = rdiv(i,j) END div_nt_alt $$$div_nt_alt.prf (|div_nt_alt| (|natdiv_TCC1| "" (TCC :DEFS !) NIL) (|natdiv_TCC2| "" (TCC :DEFS !) NIL) (|floor_is_natdiv| "" (INDUCT "n" 1 "NAT_induction") (("" (SKOSIMP*) (("" (CASE "j!1 < m!1") (("1" (REWRITE "floor_small") (("1" (HIDE -2) (("1" (EXPAND "natdiv") (("1" (ASSERT) (("1" (REWRITE "pos_div_ge") NIL))))))) ("2" (EXPAND "abs") (("2" (PROPAX) NIL))))) ("2" (EXPAND "natdiv" 2) (("2" (ASSERT) (("2" (INST -1 "j!1-m!1") (("2" (ASSERT) (("2" (INST?) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (LEMMA "floor_plus_int") (("2" (INST -1 "-1" "j!1/m!1") (("2" (ASSERT) NIL))))))))))))))))))))))))) (|rdiv_lem| "" (SKOSIMP*) (("" (EXPAND "div") (("" (EXPAND "rdiv") (("" (LIFT-IF) (("" (LEMMA "floor_is_natdiv") (("" (INST -1 "abs(j!1)" "abs(i!1)") (("" (REPLACE -1) (("" (HIDE -1) (("" (LEMMA "floor_neg") (("" (INST?) (("" (CASE-REPLACE "integer_pred(i!1/j!1) IFF is_multiple(i!1,j!1)") (("1" (HIDE -1) (("1" (EXPAND "sgn") (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (ASSERT) (("1" (GROUND) (("1" (EXPAND "is_multiple") (("1" (INST 1 "i!1/j!1") (("1" (ASSERT) NIL))))) ("2" (EXPAND "is_multiple") (("2" (INST 1 "i!1/j!1") (("2" (ASSERT) NIL))))) ("3" (EXPAND "integer?") (("3" (EXPAND "is_multiple") (("3" (PROPAX) NIL))))) ("4" (EXPAND "is_multiple") (("4" (PROPAX) NIL))))))))))))))))))) ("2" (HIDE -1 2) (("2" (SPLIT 1) (("1" (FLATTEN) (("1" (EXPAND "is_multiple") (("1" (INST 1 "i!1/j!1") (("1" (ASSERT) NIL))))))) ("2" (FLATTEN) (("2" (EXPAND "is_multiple") (("2" (SKOSIMP*) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (ASSERT) NIL)))))))))))))))))))))))))))))))))))))) $$$div_alt.pvs div_alt: THEORY BEGIN IMPORTING div n: VAR nat m: VAR posnat natdiv(n,m): RECURSIVE nat = (IF n>=m THEN 1+natdiv(n-m, m) ELSE 0 ENDIF) MEASURE (LAMBDA n,m: n) i: VAR int j: VAR nonzero_integer rdiv(i,j): integer = sgn(i)*sgn(j)*natdiv(abs(i),abs(j)) natdiv_is_floor: LEMMA natdiv(n,m) = floor(n/m) rdiv_lem: LEMMA div(i,j) = rdiv(i,j) END div_alt $$$div_alt.prf (|div_alt| (|natdiv_TCC1| "" (TCC :DEFS !) NIL) (|natdiv_TCC2| "" (TCC :DEFS !) NIL) (|natdiv_is_floor| "" (INDUCT "n" 1 "NAT_induction") (("" (SKOSIMP*) (("" (CASE "j!1 < m!1") (("1" (REWRITE "floor_small") (("1" (HIDE -2) (("1" (EXPAND "natdiv") (("1" (ASSERT) (("1" (REWRITE "pos_div_ge") NIL))))))) ("2" (EXPAND "abs") (("2" (PROPAX) NIL))))) ("2" (EXPAND "natdiv" 2) (("2" (ASSERT) (("2" (INST -1 "j!1-m!1") (("2" (ASSERT) (("2" (INST?) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (LEMMA "floor_plus_int") (("2" (INST -1 "-1" "j!1/m!1") (("1" (ASSERT) NIL) ("2" (AUTO-REWRITE-THEORY "integers") (("2" (ASSERT) NIL))))))))))))))))))))))))))) (|rdiv_lem| "" (SKOSIMP*) (("" (EXPAND "div") (("" (EXPAND "rdiv") (("" (REWRITE "natdiv_is_floor") (("" (ASSERT) NIL)))))))))) $$$mod_lems.pvs mod_lems: THEORY %------------------------------------------------------------------------ % Develops lemmas about mod % % This version of "mod" is based upon the Ada Reference Manual's % definition. These depend upon the use of a division theory that truncates % toward zero on a negative argument. % % AUTHOR % ------ % % Ricky W. Butler email: r.w.butler@larc.nasa.gov % Mail Stop 130 fax: (804) 864-4234 % NASA Langley Research Center phone: (804) 864-6198 % Hampton, Virginia 23681-0001 %------------------------------------------------------------------------ BEGIN IMPORTING mod i,j,k: VAR int m: VAR posnat n,a,b,c,x: VAR nat % The following rule characterizes the property that incrementing % modulo m wraps around the zero point. mod_wrap_around: LEMMA n < m & (c <= m & c >= m-n) => mod(n+c, m) = n - (m-c) mod_wrap2: LEMMA c < m IMPLIES mod(m+c, m) = c % Injection-like properties for mod for limited ranges mod_inj1: LEMMA x < m AND n < m AND c < m AND mod(x + n, m) = mod(x + c, m) IMPLIES n = c mod_inj2: LEMMA x < m AND n < m AND c < m AND mod(x - n, m) = mod(x - c, m) IMPLIES n = c mod_wrap_inj: LEMMA x < m AND a < m AND b < m AND a > 0 IMPLIES (mod(x + a, m) = mod(x - b, m)) = (a + b = m) kk, vv: VAR nat mod_neg_limited: LEMMA 0 <= kk AND kk < m AND vv < m AND vv - kk < 0 IMPLIES mod(vv - kk,m) = m + vv - kk END mod_lems $$$mod_lems.prf (|mod_lems| (|mod_wrap_around| "" (SKOSIMP*) (("" (EXPAND "mod") (("" (LEMMA "floor_val") (("" (INST?) (("" (INST -1 "1") (("" (GROUND) NIL))))))))))) (|mod_wrap2| "" (SKOSIMP*) (("" (EXPAND "mod") (("" (CASE "(m!1 + c!1) / m!1 = 1 + c!1/m!1") (("1" (LEMMA "floor_plus_int") (("1" (INST -1 "1" "c!1/m!1") (("1" (LEMMA "floor_small") (("1" (INST?) (("1" (EXPAND "abs") (("1" (ASSERT) NIL))))))))))) ("2" (ASSERT) NIL))))))) (|mod_inj1| "" (SKOSIMP*) (("" (EXPAND "mod") (("" (LEMMA "floor_val") (("" (CASE "floor((x!1 + n!1) / m!1) = 0 OR floor((x!1 + n!1) / m!1) = 1") (("1" (CASE "floor((x!1 + c!1) / m!1) = 0 OR floor((x!1 + c!1) / m!1) = 1") (("1" (GROUND) NIL) ("2" (CASE "x!1 + c!1 < m!1") (("1" (FLATTEN) (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (FLATTEN) (("2" (INST -2 "x!1+c!1" "m!1" "1") (("2" (ASSERT) NIL))))))))) ("2" (CASE "x!1 + n!1 < m!1") (("1" (INST?) (("1" (FLATTEN) (("1" (ASSERT) NIL))))) ("2" (FLATTEN) (("2" (INST -1 "x!1+n!1" "m!1" "1") (("2" (ASSERT) NIL))))))))))))))) (|mod_inj2| "" (SKOSIMP*) (("" (EXPAND "mod") (("" (REWRITE "floor_small") (("1" (REWRITE "floor_small") (("1" (TCC-BDD) NIL) ("2" (TCC-BDD) NIL))) ("2" (TCC-BDD) NIL))))))) (|mod_wrap_inj| "" (SKOSIMP*) (("" (IFF 1) (("" (SPLIT 1) (("1" (FLATTEN) (("1" (CASE "abs(x!1-b!1) < abs(m!1)") (("1" (LEMMA "mod_lt") (("1" (INST -1 "x!1-b!1" "m!1") (("1" (ASSERT) (("1" (LEMMA "mod_lt") (("1" (INST -1 "x!1+a!1" "m!1") (("1" (LEMMA "mod_wrap_around") (("1" (INST?) (("1" (EXPAND "sgn") (("1" (LIFT-IF) (("1" (ASSERT) (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL))))))))))))))))))))))))) ("2" (HIDE -1 2) (("2" (EXPAND "abs") (("2" (LIFT-IF) (("2" (GROUND) NIL))))))))))) ("2" (FLATTEN) (("2" (CASE-REPLACE "a!1 = m!1-b!1") (("1" (LEMMA "mod_sum") (("1" (INST -1 "x!1-b!1" "m!1" "1") (("1" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))))))))) (|mod_neg_limited| "" (SKOSIMP*) (("" (LEMMA "mod_lt") (("" (INST?) (("" (EXPAND "abs") (("" (ASSERT) (("" (EXPAND "sgn") (("" (PROPAX) NIL)))))))))))))) $$$mod_div_lems.pvs mod_div_lems: THEORY %------------------------------------------------------------------------ % % %------------------------------------------------------------------------ BEGIN IMPORTING floor_div_props, rem, mod i: VAR int j: VAR nonzero_integer mod_rem: LEMMA mod(i,j)= IF sgn(i) = sgn(j) OR integer?(i/j) THEN rem(i,j) ELSE j + rem(i,j) ENDIF END mod_div_lems $$$mod_div_lems.prf (|mod_div_lems| (|rem_rng| "" (SKOSIMP*) (("" (EXPAND "rem") (("" (REWRITE "div_def") (("" (LIFT-IF) (("" (SPLIT 3) (("1" (FLATTEN) (("1" (CASE "i!1 = 0") (("1" (ASSERT) (("1" NIL NIL))) ("2" (HIDE 2 4) (("2" (EXPAND "sgn") (("2" (LEMMA "pos_div_ge") (("2" (INST?) (("2" (LEMMA "div_eq_zero") (("2" (INST?) (("2" (GROUND) (("2" NIL NIL))))))))))))))))))) ("2" (FLATTEN) (("2" (SPLIT 2) (("1" (FLATTEN) (("1" (PROPAX) (("1" NIL NIL))))) ("2" (FLATTEN) (("2" (LEMMA "pos_div_ge") (("2" (INST?) (("2" (FLATTEN) (("2" (HIDE -2) (("2" (HIDE 1 5) (("2" (EXPAND "sgn") (("2" (EXPAND "abs") (("2" (LIFT-IF) (("2" (LIFT-IF) (("2" (GROUND) (("2" NIL NIL))))))))))))))))))))))))))))))))))))) (|mod_rem| "" (SKOSIMP*) (("" (EXPAND "rem") (("" (EXPAND "div") (("" (EXPAND "mod") (("" (EXPAND "sgn") (("" (LIFT-IF) (("" (LIFT-IF) (("" (ASSERT) (("" (LIFT-IF) (("" (EXPAND "abs") (("" (LEMMA "floor_neg") (("" (INST?) (("" (LIFT-IF) (("" (GROUND) NIL)))))))))))))))))))))))))))) $$$div_nt.pvs div_nt: THEORY %------------------------------------------------------------------------ % Defines natural and integer division (Number Theory Style) % % There is no universally agreed semantics for integer division for a % negative argument. For a negative argument, division can be defined % with truncation towards or away from zero. The definition in this % theory truncates away from zero (i.e. div(-7,3) = -3). This is is the % approach used in most number theory books. This approach has the % advantage that div(i,m) = the greatest integer less than i/m. The % alternate approach (i.e. truncation towards zero: div(-7,3) = -2) is % simpler to compute because div(-i,m) = -div(i,m) under that % definition. It is the method defined in tha Ada reference manual. % %% AUTHOR % ------ % % Ricky W. Butler email: r.w.butler@larc.nasa.gov % Mail Stop 130 fax: (804) 864-4234 % NASA Langley Research Center phone: (804) 864-6198 % Hampton, Virginia 23681-0001 %------------------------------------------------------------------------ BEGIN IMPORTING floor_div_props negint: TYPE = {i: int | i < 0} CONTAINING -1 i,k: VAR int n: VAR nat m: VAR posnat j: VAR nonzero_integer x: VAR real div(i,j): integer = floor(i/j) JUDGEMENT div HAS_TYPE [nat,posnat -> nat] JUDGEMENT div HAS_TYPE [negint,posnat -> negint] JUDGEMENT div HAS_TYPE [negint,negint -> nonneg_int] JUDGEMENT div HAS_TYPE [posnat,negint -> negint] div_nat: LEMMA div(n,m) = IF n>=m THEN 1 + div(n-m, m) ELSE 0 ENDIF div_neg_d: LEMMA div(i,-j) = IF integer?(i/j) THEN -div(i,j) ELSE -div(i,j)-1 ENDIF div_neg: LEMMA div(-i,j) = IF integer?(i/j) THEN -div(i,j) ELSE -div(i,j)-1 ENDIF div_def: THEOREM div(i,m) = IF i >= m THEN 1 + div(i-m, m) ELSIF i >= 0 THEN 0 ELSIF integer?(i/m) THEN -div(-i,m) ELSE -1 - div(-i,m) ENDIF div_sgn: LEMMA div(i,-j) = div(-i,j) div_value: LEMMA i >= k*j AND i < (k+1)*j IMPLIES div(i,j) = k % ================== div for special values ============================= div_zero: LEMMA div(0,j) = 0 div_one: LEMMA abs(j) > 1 IMPLIES div(1,j) = IF j >= 0 THEN 0 ELSE -1 ENDIF div_eq_arg: LEMMA div(j,j) = 1 div_by_one: LEMMA div(i,1) = i div_eq_0: LEMMA div(i,j) = 0 IMPLIES i = 0 OR (sgn(i) = sgn(j) AND abs(i) < abs(j)) div_lt: LEMMA abs(i) < abs(j) IMPLIES div(i,j) = IF i = 0 OR sgn(i) = sgn(j) THEN 0 ELSE -1 ENDIF div_parity: LEMMA sgn(i) = sgn(j) IMPLIES div(i,j) >= 0 div_parity_neg: LEMMA sgn(i) /= sgn(j) IMPLIES div(i,j) <= 0 div_smaller: LEMMA m * div(n,m) <= n div_abs: LEMMA abs(div(i,j)) = IF integer?(i/j) OR sgn(i) = sgn(j) THEN div(abs(i),abs(j)) ELSE div(abs(i),abs(j)) + 1 ENDIF div_max: LEMMA abs(j) * abs(div(i,j)) <= abs(i) + abs(j) % ================== div over addition ================================= div_multiple: LEMMA div(k*j,j) = k div_sum: LEMMA div(i+k*j,j) = div(i,j) + k END div_nt $$$div_nt.prf (|div_nt| (|negint_TCC1| "" (TCC) NIL) (|div_TCC1| "" (SKOSIMP*) (("" (ASSERT) (("" (EXPAND "div") (("" (LEMMA "pos_div_ge") (("" (INST -1 "x2!1" "x1!1") (("" (GROUND) NIL))))))))))) (|div_TCC2| "" (SKOSIMP*) (("" (EXPAND "div") (("" (LEMMA "pos_div_ge") (("" (INST -1 "x2!1" "x1!1") (("" (GROUND) NIL))))))))) (|div_TCC3| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|div_TCC4| "" (SKOSIMP*) (("" (EXPAND "div") (("" (LEMMA "pos_div_ge") (("" (INST?) (("" (FLATTEN) (("" (GROUND) NIL))))))))))) (|div_TCC5| "" (SKOSIMP*) (("" (EXPAND "div") (("" (LEMMA "pos_div_ge") (("" (INST -1 "x2!1" "x1!1") (("" (GROUND) NIL))))))))) (|div_nat| "" (SKOSIMP*) (("" (LIFT-IF) (("" (EXPAND "div") (("" (SPLIT 1) (("1" (FLATTEN) (("1" (CASE "(n!1 - m!1) / m!1 = n!1/m!1 - 1") (("1" (LEMMA "floor_plus_int") (("1" (INST -1 "-1" "n!1/m!1") (("1" (GROUND) NIL))))) ("2" (ASSERT) NIL))))) ("2" (FLATTEN) (("2" (LEMMA "floor_small") (("2" (INST?) (("2" (EXPAND "abs") (("2" (ASSERT) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (LIFT-IF) (("2" (LEMMA "pos_div_ge") (("2" (INST?) (("2" (GROUND) NIL))))))))))))))))))))))))))))) (|div_neg_d| "" (SKOSIMP*) (("" (EXPAND "div") (("" (LIFT-IF) (("" (LEMMA "floor_neg") (("" (INST -1 "i!1/j!1") (("" (LIFT-IF) (("" (GROUND) NIL))))))))))))) (|div_neg| "" (SKOSIMP*) (("" (EXPAND "div") (("" (LIFT-IF) (("" (LEMMA "floor_neg") (("" (INST -1 "i!1/j!1") (("" (LIFT-IF) (("" (GROUND) NIL))))))))))))) (|div_def_TCC1| "" (TCC) NIL) (|div_def| "" (SKOSIMP*) (("" (LIFT-IF) (("" (SPLIT 1) (("1" (FLATTEN) (("1" (LEMMA "div_nat") (("1" (INST?) (("1" (LIFT-IF) (("1" (ASSERT) NIL))) ("2" (ASSERT) NIL))))))) ("2" (FLATTEN) (("2" (SPLIT 2) (("1" (FLATTEN) (("1" (LEMMA "div_nat") (("1" (INST?) (("1" (LIFT-IF) (("1" (ASSERT) NIL))))))))) ("2" (FLATTEN) (("2" (SPLIT 2) (("1" (FLATTEN) (("1" (LEMMA "div_neg") (("1" (INST?) (("1" (LIFT-IF) (("1" (ASSERT) NIL))))))))) ("2" (FLATTEN) (("2" (LEMMA "div_neg") (("2" (INST?) (("2" (LIFT-IF) (("2" (ASSERT) NIL))))))))))))))))))))))) (|div_sgn| "" (SKOSIMP*) (("" (EXPAND "div") (("" (ASSERT) NIL))))) (|div_value| "" (SKOSIMP*) (("" (EXPAND "div") (("" (LEMMA "floor_val") (("" (INST?) (("" (ASSERT) NIL))))))))) (|div_zero| "" (SKOSIMP*) (("" (EXPAND "div") (("" (ASSERT) NIL))))) (|div_one| "" (SKOSIMP*) (("" (EXPAND "div") (("" (LEMMA "floor_small") (("" (INST -1 "1" "j!1") (("" (EXPAND "abs" -1 1) (("" (ASSERT) (("" (LEMMA "pos_div_ge") (("" (INST -1 "j!1" "1") (("" (FLATTEN) (("" (ASSERT) (("" (LIFT-IF) (("" (LEMMA "div_eq_zero") (("" (INST -1 "j!1" "1") (("" (GROUND) NIL))))))))))))))))))))))))))) (|div_eq_arg| "" (SKOSIMP*) (("" (EXPAND "div") (("" (ASSERT) NIL))))) (|div_by_one_TCC1| "" (ASSERT) NIL) (|div_by_one| "" (SKOSIMP*) (("" (EXPAND "div") (("" (ASSERT) NIL))))) (|div_eq_0| "" (SKOSIMP*) (("" (EXPAND "div") (("" (LEMMA "floor_eq_0") (("" (INST -1 "i!1/j!1") (("" (SPLIT -1) (("1" (FLATTEN) (("1" (LEMMA "pos_div_ge") (("1" (INST?) (("1" (LEMMA "div_eq_zero") (("1" (INST?) (("1" (FLATTEN) (("1" (EXPAND "sgn") (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (ASSERT) (("1" (GROUND) (("1" (HIDE 1 3) (("1" (LEMMA "both_sides_times_pos_lt1") (("1" (INST -1 "-j!1" "1" "i!1/j!1") (("1" (ASSERT) NIL))))))) ("2" (LEMMA "both_sides_times_pos_lt1") (("2" (INST -1 "j!1" "1" "i!1/j!1") (("2" (ASSERT) NIL))))))))))))))))))))))))))))) ("2" (PROPAX) NIL))))))))))) (|div_lt| "" (SKOSIMP*) (("" (EXPAND "div") (("" (LEMMA "floor_small") (("" (INST?) (("" (ASSERT) (("" (CASE "(i!1 = 0 OR sgn(i!1) = sgn(j!1)) = (i!1 / j!1 >= 0)") (("1" (LIFT-IF) (("1" (EXPAND "sgn") (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (GROUND) NIL))))))))) ("2" (HIDE -1 -2 2) (("2" (IFF 1) (("2" (SPLIT 1) (("1" (FLATTEN) (("1" (EXPAND "sgn") (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (GROUND) (("1" (LEMMA "pos_div_ge") (("1" (INST -1 "j!1" "i!1") (("1" (ASSERT) NIL))))) ("2" (LEMMA "pos_div_ge") (("2" (INST -1 "-j!1" "-i!1") (("2" (GROUND) NIL))))))))))))))) ("2" (FLATTEN) (("2" (EXPAND "sgn") (("2" (LIFT-IF) (("2" (LIFT-IF) (("2" (LEMMA "pos_div_ge") (("2" (INST -1 "j!1" "i!1") (("2" (LEMMA "div_eq_zero") (("2" (INST?) (("2" (GROUND) NIL))))))))))))))))))))))))))))))))))) (|div_parity| "" (SKOSIMP*) (("" (EXPAND "div") (("" (EXPAND "sgn") (("" (LIFT-IF) (("" (LEMMA "pos_div_ge") (("" (INST?) (("" (FLATTEN) (("" (LIFT-IF) (("" (GROUND) NIL))))))))))))))))) (|div_parity_neg| "" (SKOSIMP*) (("" (EXPAND "div") (("" (EXPAND "sgn") (("" (LIFT-IF) (("" (LEMMA "pos_div_ge") (("" (INST?) (("" (FLATTEN) (("" (LIFT-IF) (("" (GROUND) NIL))))))))))))))))) (|div_smaller| "" (SKOSIMP*) (("" (EXPAND "div") (("" (ASSERT) (("" (TYPEPRED "floor(n!1 / m!1)") (("" (LEMMA "both_sides_times_pos_lt1") (("" (INST -1 "m!1" "floor(n!1 / m!1)" "n!1 / m!1") (("" (FLATTEN) (("" (GROUND) NIL))))))))))))))) (|div_abs| "" (SKOSIMP*) (("" (EXPAND "div") (("" (EXPAND "abs") (("" (LIFT-IF) (("" (LIFT-IF) (("" (LIFT-IF) (("" (LEMMA "floor_neg") (("" (INST?) (("" (LIFT-IF) (("" (EXPAND "sgn") (("" (LIFT-IF) (("" (ASSERT) (("" (LEMMA "pos_div_ge") (("" (INST?) (("" (GROUND) NIL))))))))))))))))))))))))))))) (|div_max| "" (SKOSIMP*) (("" (LEMMA "div_smaller") (("" (INST -1 "abs(j!1)" "abs(i!1)") (("" (LEMMA "div_abs") (("" (INST?) (("" (REPLACE -1) (("" (HIDE -1) (("" (LIFT-IF) (("" (GROUND) NIL))))))))))))))))) (|div_multiple| "" (SKOSIMP*) (("" (EXPAND "div") (("" (ASSERT) NIL))))) (|div_sum| "" (SKOSIMP*) (("" (EXPAND "div") (("" (LEMMA "floor_plus_int") (("" (INST -1 "k!1*j!1/j!1" "i!1/j!1") (("" (ASSERT) NIL)))))))))) $$$rem.pvs rem: THEORY %------------------------------------------------------------------------ % Defines remainder (rem) (Ada Style) % % This version of "rem" is based upon the Ada Reference Manual's % definition. These depend upon the use of a division theory that truncates % toward zero on a negative argument. % % AUTHORS % ------- % Ricky W. Butler email: r.w.butler@larc.nasa.gov % Mail Stop 130 fax: (804) 864-4234 % NASA Langley Research Center phone: (804) 864-6198 % Hampton, Virginia 23681-0001 % %------------------------------------------------------------------------ BEGIN IMPORTING div i,k,cc: VAR int m: VAR posnat n,a,b,c: VAR nat j: VAR nonzero_integer % ======================= define rem(i,m) ======================== ml1: LEMMA n - m * div(n,m) < m ml3: LEMMA abs(i - m * div(i,m)) < m rem(i,j): {k| abs(k) < abs(j)} = i - j*div(i,j) rem_neg: LEMMA rem(-i,j) = -rem(i,j) rem_neg_d: LEMMA rem(i,-j) = rem(i,j) rem_even: LEMMA integer?(i/j) IMPLIES rem(i,j) = 0 rem_eq_arg: LEMMA rem(j,j) = 0 rem_zero: LEMMA rem(0,j) = 0 rem_lt: LEMMA abs(i) < abs(j) IMPLIES rem(i,j) = i rem_it_is: LEMMA a = b + m*c AND b < m IMPLIES b = rem(a,m) rem_eq_0: LEMMA rem(i,j) = 0 IMPLIES integer?(i/j) rem_one: LEMMA rem(1,j) = IF abs(j) = 1 THEN 0 ELSE 1 ENDIF JUDGEMENT rem HAS_TYPE [nat, m:posnat -> below(m)] END rem $$$rem.prf (|rem| (|ml1| "" (SKOLEM!) (("" (EXPAND "div") (("" (EXPAND "sgn") (("" (EXPAND "abs") (("" (ASSERT) (("" (LEMMA "both_sides_times_pos_lt1") (("" (INST - "m!1" "n!1/m!1" "floor(n!1/m!1)+1") (("" (FLATTEN) (("" (GROUND) NIL))))))))))))))))) (|ml3| "" (SKOSIMP*) (("" (CASE "i!1 >= 0") (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (SPLIT 1) (("1" (FLATTEN) (("1" (LEMMA "div_smaller") (("1" (INST?) (("1" (ASSERT) NIL))))))) ("2" (FLATTEN) (("2" (LEMMA "ml1") (("2" (INST?) NIL))))))))))) ("2" (EXPAND "abs") (("2" (LIFT-IF) (("2" (LEMMA "div_neg") (("2" (INST?) (("2" (SPLIT 2) (("1" (FLATTEN) (("1" (LEMMA "ml1") (("1" (INST -1 "m!1" "-i!1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))) ("2" (FLATTEN) (("2" (LEMMA "div_smaller") (("2" (INST -1 "m!1" "-i!1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))))))))) (|rem_TCC1| "" (SKOSIMP*) (("" (LEMMA "ml3") (("" (CASE "j!1 >= 0") (("1" (INST?) (("1" (EXPAND "abs" 1 2) (("1" (ASSERT) NIL))) ("2" (ASSERT) NIL))) ("2" (INST -1 "i!1" "-j!1") (("1" (LEMMA "div_neg_d") (("1" (INST?) (("1" (REPLACE -1) (("1" (EXPAND "abs" 2 2) (("1" (ASSERT) NIL))))))))) ("2" (ASSERT) NIL))))))))) (|rem_neg| "" (SKOSIMP*) (("" (EXPAND "rem") (("" (REWRITE "div_neg") (("" (ASSERT) NIL))))))) (|rem_neg_d| "" (SKOSIMP*) (("" (EXPAND "rem") (("" (REWRITE "div_neg_d") (("" (ASSERT) NIL))))))) (|rem_even| "" (SKOSIMP*) (("" (EXPAND "rem") (("" (REWRITE "div_even") NIL))))) (|rem_eq_arg| "" (SKOLEM!) (("" (EXPAND "rem") (("" (REWRITE "div_eq_arg") (("" (ASSERT) NIL))))))) (|rem_zero| "" (SKOSIMP*) (("" (EXPAND "rem") (("" (REWRITE "div_zero") (("" (ASSERT) NIL))))))) (|rem_lt| "" (SKOSIMP*) (("" (EXPAND "rem") (("" (REWRITE "div_lt") (("" (ASSERT) NIL))))))) (|rem_it_is| "" (SKOSIMP*) (("" (EXPAND "rem") (("" (CASE "div(a!1,m!1) = c!1") (("1" (ASSERT) NIL) ("2" (HIDE 2) (("2" (EXPAND "div") (("2" (EXPAND "sgn") (("2" (EXPAND "abs") (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (LEMMA "floor_plus_int") (("2" (CASE "(b!1 + m!1 * c!1) / m!1 = b!1 / m!1 + c!1") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (INST -1 "c!1" "b!1/m!1") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "floor_small") (("1" (INST?) (("1" (EXPAND "abs") (("1" (ASSERT) NIL))))))))))))))))) ("2" (HIDE -1 -2 2) (("2" (ASSERT) NIL))))))))))))))))))))))))) (|rem_eq_0| "" (SKOSIMP) (("" (REWRITE "is_multiple") (("" (EXPAND "rem") (("" (INST + "div(i!1, j!1)") (("" (ASSERT) NIL))))))))) (|rem_one| "" (SKOSIMP*) (("" (LIFT-IF) (("" (SPLIT 1) (("1" (FLATTEN) (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (LEMMA "rem_eq_arg") (("1" (INST -1 "1") (("1" (LEMMA "rem_neg_d") (("1" (INST -1 "1" "1") (("1" (ASSERT) NIL))))))))))) ("2" (FLATTEN) (("2" (LEMMA "rem_eq_arg") (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))) ("2" (FLATTEN) (("2" (LEMMA "rem_lt") (("2" (INST?) (("2" (EXPAND "abs") (("2" (LIFT-IF) (("2" (GROUND) NIL))))))))))))))))) (|rem_TCC2| "" (INDUCT "x1" :NAME "NAT_induction") (("" (SKOSIMP) (("" (SKOSIMP) (("" (SPLIT) (("1" (EXPAND "rem" +) (("1" (LEMMA "div_nat") (("1" (INST -1 "x2!1" "j!1") (("1" (LIFT-IF) (("1" (PROP) (("1" (ASSERT) NIL) ("2" (INST -2 "j!1-x2!1") (("1" (ASSERT) (("1" (INST -2 "x2!1") (("1" (FLATTEN) (("1" (EXPAND "rem" -2) (("1" (ASSERT) NIL))))))))) ("2" (ASSERT) NIL))))))))))))) ("2" (TYPEPRED "rem(j!1, x2!1)") (("2" (EXPAND "abs") (("2" (ASSERT) NIL)))))))))))))) $$$div.pvs div: THEORY %------------------------------------------------------------------------ % Defines natural and integer division (Ada Style) % % There is no universally agreed semantics for integer division for a % negative argument. For a negative argument, division can be defined % with truncation towards or away from zero. The definition in this % theory truncates toward zero (i.e. div(-7,3) = -2). This is % simpler to compute because div(-i,m) = -div(i,m) and is the % method defined in tha Ada reference manual. The alternate method % (i.e. truncation away from zero: div(-7,3) = -3) is the approach % used in most number theory books. This approach has the % advantage that div(i,m) = the greatest integer less than i/m. % % AUTHOR % ------ % % Ricky W. Butler email: r.w.butler@larc.nasa.gov % Mail Stop 130 fax: (804) 864-4234 % NASA Langley Research Center phone: (804) 864-6198 % Hampton, Virginia 23681-0001 %------------------------------------------------------------------------ BEGIN IMPORTING floor_div_props i,k: VAR int n: VAR nat m: VAR posnat j: VAR nonzero_integer x: VAR real div(i,j): integer = sgn(i)*sgn(j)*floor(abs(i)/abs(j)) div_nat: LEMMA div(n,m) = IF n < m THEN 0 ELSE 1 + div(n-m,m) ENDIF div_def: LEMMA div(i,j) = IF i/j >= 0 THEN floor(i/j) ELSIF integer?(i/j) THEN floor(i/j) ELSE floor(i/j) + 1 ENDIF div_value: LEMMA IF sgn(i) = sgn(j) THEN i >= k*j AND i < (k+1)*j IMPLIES div(i,j) = k ELSE i > (k-1)*j AND i <= k*j IMPLIES div(i,j) = k ENDIF div_neg: LEMMA div(-i,j) = -div(i,j) div_neg_d: LEMMA div(i,-j) = -div(i,j) % ================== div for special values ============================= div_zero: LEMMA div(0,j) = 0 div_one: LEMMA abs(j) > 1 IMPLIES div(1,j) = 0 div_minus1: LEMMA abs(j) > 1 IMPLIES div(-1, j) = 0 div_eq_arg: LEMMA div(j,j) = 1 div_by_one: LEMMA div(i,1) = i div_eq_0: LEMMA div(i,j) = 0 IMPLIES abs(i) < abs(j) div_lt: LEMMA abs(i) < abs(j) IMPLIES div(i,j) = 0 div_lt_nat: LEMMA n < m IMPLIES div(n,m) = 0 div_is_0: LEMMA div(i,j) = 0 IFF abs(i) < abs(j) div_parity: LEMMA (sgn(i) = sgn(j) AND abs(i) >= abs(j)) IMPLIES div(i,j) > 0 div_parity_neg: LEMMA (sgn(i) /= sgn(j) AND abs(i) >= abs(j)) IMPLIES div(i,j) < 0 div_ge_0: LEMMA (sgn(i) = sgn(j) IMPLIES div(i,j) >= 0) AND (div(i,j) >= 0 IMPLIES abs(i) < abs(j) OR sgn(i) = sgn(j)) div_le_0: LEMMA (sgn(i) /= sgn(j) IMPLIES div(i,j) <= 0) AND (div(i,j) <= 0 IMPLIES abs(i) < abs(j) OR sgn(i) /= sgn(j)) div_smaller: LEMMA m * div(n,m) <= n div_abs: LEMMA abs(div(i,j)) = div(abs(i),abs(j)) div_max: LEMMA abs(j)*abs(div(i,j)) <= abs(i) % ================== div over addition ================================= div_multiple: LEMMA div(k*j,j) = k div_even: LEMMA integer?(i/j) IMPLIES i - j*div(i,j) = 0 div_sum: LEMMA IF integer?(i/j) OR sgn(i+k*j) = sgn(i) THEN div(i+k*j,j) = div(i,j) + k ELSE div(i+k*j,j) = div(i,j) + k + sgn(i)*sgn(j) ENDIF b: VAR nat div_sum_nat: LEMMA div(n+b*m,m) = div(n,m) + b nonposint: TYPE = {i: int | i <= 0} CONTAINING -1 negint: TYPE = {i: int | i < 0} CONTAINING -1 JUDGEMENT div HAS_TYPE [nat,posnat -> nat] JUDGEMENT div HAS_TYPE [nonposint,posnat -> nonposint] JUDGEMENT div HAS_TYPE [nonposint,negint -> nat] JUDGEMENT div HAS_TYPE [posnat,negint -> nonposint] END div $$$div.prf (|div| (|div_nat| "" (SKOSIMP*) (("" (EXPAND "div") (("" (EXPAND "sgn") (("" (LIFT-IF) (("" (EXPAND "abs") (("" (SPLIT 1) (("1" (FLATTEN) (("1" (LEMMA "floor_small") (("1" (INST?) (("1" (EXPAND "abs") (("1" (ASSERT) NIL))))))))) ("2" (FLATTEN) (("2" (LEMMA "floor_plus_int") (("2" (INST -1 "-1" "n!1/ m!1") (("2" (ASSERT) NIL))))))))))))))))))) (|div_def| "" (SKOSIMP*) (("" (EXPAND "div") (("" (EXPAND "abs") (("" (EXPAND "sgn") (("" (LEMMA "floor_neg") (("" (INST -1 "i!1/j!1") (("" (LEMMA "div_eq_zero") (("" (INST?) (("" (LEMMA "pos_div_lt") (("" (INST?) (("" (ASSERT) (("" (APPLY (REPEAT (LIFT-IF))) (("" (ASSERT) (("" (EXPAND "integer?") (("" (GROUND) NIL))))))))))))))))))))))))))))) (|div_value| "" (SKOSIMP*) (("" (EXPAND "div") (("" (EXPAND "sgn") (("" (EXPAND "abs") (("" (LIFT-IF) (("" (LIFT-IF) (("" (LIFT-IF) (("" (LIFT-IF) (("" (ASSERT) (("" (GROUND) (("1" (TYPEPRED "floor(-i!1 / j!1)") (("1" (LEMMA "both_sides_div_pos_lt1") (("1" (INST -1 "j!1" "-i!1" "-k!1*j!1 + j!1") (("1" (ASSERT) (("1" (LEMMA "both_sides_div_pos_le1") (("1" (INST -1 "j!1" "-k!1*j!1" "-i!1") (("1" (ASSERT) (("1" (CASE "(-k!1 * j!1 + j!1) / j!1 = -k!1 + 1") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (NAME "X" "-i!1/j!1") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (HIDE -7 -8) (("1" (CASE "-k!1 * j!1 / j!1 = -k!1") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))))))))))))) ("2" (ASSERT) NIL))))))))))))))))) ("2" (TYPEPRED "floor(i!1 / j!1)") (("2" (LEMMA "both_sides_div_pos_lt1") (("2" (INST -1 "j!1" "i!1" "k!1 * j!1 + j!1") (("2" (ASSERT) (("2" (CASE "(k!1 * j!1 + j!1) / j!1 = k!1 + 1") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "both_sides_div_pos_le1") (("1" (INST -1 "j!1" "k!1 * j!1" "i!1") (("1" (ASSERT) (("1" (CASE "k!1 * j!1 / j!1 = k!1") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (NAME "X" "i!1/j!1") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (HIDE -6 -7) (("1" (ASSERT) NIL))))))))))))) ("2" (ASSERT) NIL))))))))))))) ("2" (ASSERT) NIL))))))))))))))))))))))))))))))) (|div_neg| "" (SKOSIMP*) (("" (EXPAND "div") (("" (EXPAND "abs") (("" (EXPAND "sgn") (("" (LIFT-IF) (("" (LIFT-IF) (("" (LIFT-IF) (("" (LIFT-IF) (("" (LIFT-IF) (("" (LIFT-IF) (("" (ASSERT) (("" (LEMMA "floor_neg") (("" (INST -1 "i!1/j!1") (("" (LIFT-IF) (("" (GROUND) NIL))))))))))))))))))))))))))))) (|div_neg_d| "" (SKOSIMP*) (("" (EXPAND "div") (("" (EXPAND "abs") (("" (EXPAND "sgn") (("" (LIFT-IF) (("" (LIFT-IF) (("" (LIFT-IF) (("" (LIFT-IF) (("" (LIFT-IF) (("" (LIFT-IF) (("" (ASSERT) NIL))))))))))))))))))))) (|div_zero| "" (SKOSIMP*) (("" (REWRITE "div_def") (("" (ASSERT) NIL))))) (|div_one| "" (SKOSIMP*) (("" (LEMMA "div_nat") (("" (INST -1 "abs(j!1)" "1") (("" (CASE "j!1 >= 0") (("1" (EXPAND "abs") (("1" (ASSERT) (("1" (ASSERT) NIL))))) ("2" (EXPAND "abs") (("2" (ASSERT) (("2" (ASSERT) (("2" (LEMMA "div_neg_d") (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))) (|div_minus1| "" (SKOSIMP*) (("" (LEMMA "div_neg") (("" (INST?) (("" (LEMMA "div_one") (("" (INST?) (("" (ASSERT) NIL))))))))))) (|div_eq_arg| "" (SKOSIMP*) (("" (EXPAND "div") (("" (EXPAND "sgn") (("" (EXPAND "abs") (("" (LIFT-IF) (("" (LIFT-IF) (("" (GROUND) NIL))))))))))))) (|div_by_one| "" (ASSERT) (("" (SKOSIMP*) (("" (EXPAND "div") (("" (EXPAND "sgn") (("" (EXPAND "abs") (("" (LIFT-IF) (("" (LIFT-IF) (("" (LEMMA "floor_neg") (("" (INST -1 "i!1") (("" (EXPAND "integer?") (("" (ASSERT) NIL))))))))))))))))))))) (|div_eq_0| "" (SKOSIMP*) (("" (EXPAND "div") (("" (LEMMA "floor_eq_0") (("" (INST -1 "abs(i!1) / abs(j!1)") (("" (CASE "abs(j!1) /= 0") (("1" (SPLIT -2) (("1" (FLATTEN) (("1" (LEMMA "floor_eq_0") (("1" (INST?) (("1" (EXPAND "sgn") (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (LEMMA "both_sides_times_pos_lt1") (("1" (INST -1 "abs(j!1)" "abs(i!1)/abs(j!1)" "1") (("1" (GROUND) NIL))))))))))))))))) ("2" (EXPAND "sgn") (("2" (LIFT-IF) (("2" (LIFT-IF) (("2" (GROUND) NIL))))))))) ("2" (HIDE -1 -2 2) (("2" (EXPAND "abs") (("2" (LIFT-IF) (("2" (ASSERT) NIL))))))))))))))))) (|div_lt| "" (SKOSIMP*) (("" (CASE "i!1 = 0") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "div_zero") (("1" (INST?) NIL))))))) ("2" (EXPAND "div") (("2" (LEMMA "floor_small") (("2" (INST?) (("2" (SPLIT -1) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LIFT-IF) (("1" (LEMMA "pos_div_ge") (("1" (INST?) (("1" (FLATTEN) (("1" (EXPAND "sgn") (("1" (LIFT-IF) (("1" (ASSERT) NIL))))))))))))))))) ("2" (HIDE 2 3) (("2" (EXPAND "abs") (("2" (LIFT-IF) (("2" (LIFT-IF) (("2" (GROUND) NIL))))))))))))))))))))) (|div_lt_nat| "" (SKOSIMP*) (("" (LEMMA "div_lt") (("" (INST?) (("" (EXPAND "abs") (("" (ASSERT) NIL))))))))) (|div_is_0| "" (SKOSIMP*) (("" (LEMMA "div_eq_0") (("" (INST?) (("" (LEMMA "div_lt") (("" (INST?) (("" (GROUND) NIL))))))))))) (|div_parity| "" (SKOSIMP*) (("" (EXPAND "div") (("" (LEMMA "both_sides_div_pos_le1") (("" (INST -1 "abs(j!1)" "abs(j!1)" "abs(i!1)") (("" (ASSERT) (("" (EXPAND "sgn") (("" (HIDE -3) (("" (LIFT-IF) (("" (LIFT-IF) (("" (ASSERT) NIL))))))))))))))))))) (|div_parity_neg| "" (SKOSIMP*) (("" (EXPAND "div") (("" (LEMMA "both_sides_div_pos_le1") (("" (INST -1 "abs(j!1)" "abs(j!1)" "abs(i!1)") (("" (ASSERT) (("" (EXPAND "sgn") (("" (LIFT-IF) (("" (LIFT-IF) (("" (ASSERT) (("" (GROUND) NIL))))))))))))))))))) (|div_ge_0| "" (SKOSIMP*) (("" (LEMMA "div_parity") (("" (INST?) (("" (LEMMA "div_is_0") (("" (INST?) (("" (LEMMA "div_parity_neg") (("" (INST?) (("" (GROUND) NIL))))))))))))))) (|div_le_0| "" (SKOSIMP*) (("" (LEMMA "div_parity") (("" (INST?) (("" (LEMMA "div_is_0") (("" (INST?) (("" (LEMMA "div_parity_neg") (("" (INST?) (("" (GROUND) NIL))))))))))))))) (|div_smaller| "" (SKOSIMP*) (("" (EXPAND "div") (("" (EXPAND "sgn") (("" (EXPAND "abs") (("" (ASSERT) (("" (TYPEPRED "floor(n!1 / m!1)") (("" (LEMMA "both_sides_times_pos_le1") (("" (INST -1 "m!1" "floor(n!1 / m!1)" "n!1/m!1") (("" (FLATTEN) (("" (ASSERT) NIL))))))))))))))))))) (|div_abs| "" (EXPAND "div") (("" (GRIND) NIL))) (|div_max| "" (SKOSIMP*) (("" (LEMMA "div_smaller") (("" (LEMMA "div_abs") (("" (INST?) (("" (REPLACE -1) (("" (HIDE -1) (("" (INST?) NIL))))))))))))) (|div_multiple| "" (SKOSIMP*) (("" (REWRITE "div_def") (("" (LEMMA "floor_int") (("" (EXPAND "integer?") (("" (INST?) (("" (ASSERT) NIL))))))))))) (|div_even| "" (SKOSIMP*) (("" (EXPAND "integer?") (("" (LEMMA "div_multiple") (("" (CASE "(EXISTS k: j!1*k = i!1)") (("1" (SKOSIMP*) (("1" (INST -2 "j!1" "k!1") (("1" (ASSERT) NIL))))) ("2" (INST 1 "i!1/j!1") (("2" (ASSERT) NIL))))))))))) (|div_sum| "" (SKOSIMP*) (("" (EXPAND "div") (("" (EXPAND "abs") (("" (LIFT-IF) (("" (EXPAND "sgn") (("" (LIFT-IF) (("" (ASSERT) (("" (LIFT-IF) (("" (LIFT-IF) (("" (LEMMA "floor_plus_int") (("" (INST -1 "k!1" "i!1/j!1") (("" (LEMMA "floor_neg") (("" (INST -1 "i!1/j!1") (("" (LEMMA "floor_plus_int") (("" (INST -1 "-k!1" "-i!1/j!1") (("" (LIFT-IF) (("" (GROUND) NIL))))))))))))))))))))))))))))))))) (|div_sum_nat| "" (SKOSIMP*) (("" (LEMMA "div_sum") (("" (INST?) (("" (EXPAND "sgn") (("" (LIFT-IF) (("" (GROUND) NIL))))))))))) (|nonposint_TCC1| "" (TCC :DEFS !) NIL) (|negint_TCC1| "" (TCC) NIL) (|div_TCC1| "" (GRIND) NIL) (|div_TCC2| "" (GRIND) NIL) (|div_TCC3| "" (GRIND) NIL) (|div_TCC4| "" (GRIND) NIL) (|div_TCC5| "" (GRIND) NIL)) $$$floor_div_props.pvs floor_div_props: THEORY BEGIN IMPORTING floor_ceil i,k: VAR int j: VAR nonzero_integer x: VAR real sgn(x): int = IF x >= 0 THEN 1 ELSE -1 ENDIF floor_val: LEMMA i >= k*j AND i < (k+1)*j IMPLIES floor(i/j) = k floor_small: LEMMA abs(i) < abs(j) IMPLIES floor(i/j) = IF i/j >= 0 THEN 0 ELSE -1 ENDIF floor_eq_0: LEMMA floor(x) = 0 IMPLIES x >= 0 AND x < 1 is_multiple: LEMMA integer?(i/j) = (EXISTS k: i = k*j) END floor_div_props $$$floor_div_props.prf (|floor_div_props| (|floor_val| "" (SKOSIMP*) (("" (CASE "j!1 >= 0") (("1" (LEMMA "both_sides_div_pos_lt1") (("1" (INST -1 "j!1" "i!1" "(k!1 + 1) * j!1") (("1" (LEMMA "both_sides_div_pos_ge1") (("1" (INST -1 "j!1" "i!1" "k!1 * j!1") (("1" (FLATTEN) (("1" (HIDE -1 -3) (("1" (ASSERT) (("1" (CASE "floor(i!1 / j!1) > k!1 - 1 AND floor(i!1 / j!1) < k!1 + 1") (("1" (FLATTEN) (("1" (ASSERT) (("1" (ASSERT) (("1" (ASSERT :FLUSH? T) NIL))))))) ("2" (ASSERT) NIL))))))))) ("2" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))) ("2" (LEMMA "both_sides_div_neg_lt1") (("2" (INST -1 "j!1" "(k!1 + 1) * j!1" "i!1") (("1" (FLATTEN) (("1" (HIDE -1) (("1" (LEMMA "both_sides_div_neg_ge1") (("1" (INST -1 "j!1" "k!1 * j!1" "i!1") (("1" (FLATTEN) (("1" (HIDE -1) (("1" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))))))) ("2" (ASSERT) NIL))))))))) (|floor_small| "" (SKOSIMP*) (("" (LEMMA "pos_div_ge") (("" (INST?) (("" (LIFT-IF) (("" (EXPAND "abs") (("" (LIFT-IF) (("" (GROUND) (("1" (LEMMA "floor_val") (("1" (INST -1 "-i!1" "-j!1" "0") (("1" (ASSERT) NIL))))) ("2" (LEMMA "floor_val") (("2" (INST?) (("2" (ASSERT) NIL))))) ("3" (LEMMA "floor_val") (("3" (INST -1 "-i!1" "-j!1" "-1") (("3" (ASSERT) NIL))))) ("4" (LEMMA "floor_val") (("4" (INST -1 "i!1" "j!1" "-1") (("4" (ASSERT) NIL))))))))))))))))))) (|floor_eq_0| "" (TCC) NIL) (|is_multiple| "" (SKOSIMP*) (("" (IFF 1) (("" (EXPAND "integer?") (("" (SPLIT 1) (("1" (FLATTEN) (("1" (INST 1 "i!1/j!1") (("1" (ASSERT) NIL))))) ("2" (FLATTEN) (("2" (SKOSIMP*) (("2" (ASSERT) NIL)))))))))))))) $$$mod.pvs mod: THEORY %------------------------------------------------------------------------ % % mod function as defined in `Concrete Mathematics' % The Ada definition of mod is consistent with this definition % % Author: % Paul S. Miner | email: p.s.miner@larc.nasa.gov % 1 South Wright St. / MS 130 | fax: (804) 864-4234 % NASA Langley Research Center | phone: (804) 864-6201 % Hampton, Virginia 23681 | %------------------------------------------------------------------------ BEGIN IMPORTING floor_div_props i,k,cc: VAR int m: VAR posnat n,a,b,c: VAR nat j: VAR nonzero_integer ml3: LEMMA abs(i - m * floor(i/m)) < m ml4: LEMMA abs(i + m * floor(-i/m)) < m mod(i,j): {k| abs(k) < abs(j)} = i-j*floor(i/j) mod_even: LEMMA integer?(i/j) IMPLIES mod(i,j) = 0 mod_neg: LEMMA mod(-i,j) = IF integer?(i/j) THEN 0 ELSE j - mod(i,j) ENDIF mod_neg_d: LEMMA mod(i,-j) = IF integer?(i/j) THEN 0 ELSE mod(i,j) - j ENDIF mod_eq_arg: LEMMA mod(j,j) = 0 mod_lt: LEMMA abs(i) < abs(j) IMPLIES mod(i,j) = IF sgn(i) = sgn(j) OR i = 0 THEN i ELSE i + j ENDIF mod_lt_nat: LEMMA n < m IMPLIES mod(n,m) = n mod_sum_pos: LEMMA mod(i+k*m,m) = mod(i,m) mod_sum: LEMMA mod(i+k*j,j) = mod(i,j) mod_it_is: LEMMA a = b + m*c AND b < m IMPLIES b = mod(a,m) mod_Ada: LEMMA (EXISTS k: i = k*j + mod(i,j)) mod_zero: LEMMA mod(0,j) = 0 mod_one: LEMMA mod(1,j) = IF abs(j) = 1 THEN 0 ELSIF j > 0 THEN 1 ELSE j + 1 ENDIF mod_of_mod: LEMMA mod(i + mod(k,m), m) = mod(i+k, m) mod_pos: LEMMA mod(i,m) >= 0 AND mod(i,m) < m JUDGEMENT mod HAS_TYPE [int, m:posnat -> below(m)] END mod $$$mod.prf (|mod| (|ml3| "" (SKOSIMP*) (("" (EXPAND "abs") (("" (LIFT-IF) (("" (GROUND) (("1" (LEMMA "both_sides_times_pos_lt1") (("1" (INST -1 "m!1" "floor(i!1 / m!1)" "i!1 / m!1") (("1" (FLATTEN) (("1" (ASSERT) NIL))))))) ("2" (TYPEPRED "floor(i!1 / m!1)") (("2" (LEMMA "both_sides_times_pos_lt1") (("2" (INST -1 "m!1" "i!1 / m!1" " 1 + floor(i!1 / m!1)") (("2" (FLATTEN) (("2" (HIDE -1) (("2" (ASSERT) NIL))))))))))))))))))) (|ml4| "" (SKOSIMP*) (("" (EXPAND "abs") (("" (LIFT-IF) (("" (GROUND) (("1" (TYPEPRED "floor(-i!1 / m!1)") (("1" (LEMMA "both_sides_times_pos_lt1") (("1" (INST -1 "m!1" "-i!1 / m!1" "1 + floor(-i!1 / m!1)") (("1" (FLATTEN) (("1" (HIDE -1) (("1" (ASSERT) NIL))))))))))) ("2" (LEMMA "both_sides_times_pos_lt1") (("2" (INST -1 "m!1" "floor(-i!1 / m!1)" "-i!1 / m!1") (("2" (FLATTEN) (("2" (HIDE -1) (("2" (ASSERT) NIL))))))))))))))))) (|mod_TCC1| "" (SKOSIMP*) (("" (CASE "j!1 >= 0") (("1" (LEMMA "ml3") (("1" (INST?) (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL))))) ("2" (ASSERT) NIL))))) ("2" (LEMMA "ml4") (("2" (INST -1 "i!1" "-j!1") (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL))))) ("2" (ASSERT) NIL))))))))) (|mod_even| "" (SKOSIMP*) (("" (EXPAND "integer?") (("" (EXPAND "mod") (("" (REWRITE "floor_int") (("" (ASSERT) NIL))))))))) (|mod_neg| "" (AUTO-REWRITE-THEORY "integers") (("" (SKOSIMP*) (("" (LIFT-IF) (("" (EXPAND "mod") (("" (CASE "-i!1/j!1 = -(i!1/j!1)") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (GROUND) (("1" (REWRITE "floor_int") (("1" (ASSERT) NIL))) ("2" (REWRITE "floor_neg") (("2" (LIFT-IF) (("2" (GROUND) (("2" (CASE "integer_pred(--(i!1/j!1))") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))) ("2" (ASSERT) NIL))))))))))) (|mod_neg_d| "" (AUTO-REWRITE-THEORY "integers") (("" (SKOSIMP*) (("" (LIFT-IF) (("" (EXPAND "mod") (("" (CASE "i!1/-j!1=-(i!1/j!1)") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (REWRITE "floor_neg") (("1" (LIFT-IF) (("1" (GROUND) (("1" (REWRITE "floor_int") (("1" (ASSERT) NIL))) ("2" (ASSERT) (("2" (CASE "integer_pred(--(i!1/j!1))") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))) ("2" (ASSERT) NIL))))))))))) (|mod_eq_arg| "" (TCC) NIL) (|mod_lt| "" (SKOSIMP*) (("" (LIFT-IF) (("" (EXPAND "mod") (("" (EXPAND "abs") (("" (EXPAND "sgn") (("" (LIFT-IF) (("" (LIFT-IF) (("" (GROUND) (("1" (REWRITE "floor_small") (("1" (LIFT-IF) (("1" (GROUND) (("1" (REWRITE "pos_div_ge") NIL))))) ("2" (EXPAND "abs") (("2" (PROPAX) NIL))))) ("2" (REWRITE "floor_small") (("1" (LIFT-IF) (("1" (GROUND) (("1" (REWRITE "pos_div_ge") NIL))))) ("2" (EXPAND "abs") (("2" (PROPAX) NIL))))) ("3" (REWRITE "floor_small") (("1" (LIFT-IF) (("1" (GROUND) (("1" (REWRITE "pos_div_ge") NIL))))) ("2" (EXPAND "abs") (("2" (PROPAX) NIL))))) ("4" (REWRITE "floor_small") (("1" (LIFT-IF) (("1" (GROUND) (("1" (REWRITE "pos_div_ge") NIL))))) ("2" (EXPAND "abs") (("2" (PROPAX) NIL))))))))))))))))))))) (|mod_lt_nat| "" (SKOSIMP*) (("" (REWRITE "mod_lt") (("1" (EXPAND "sgn") (("1" (PROPAX) NIL))) ("2" (EXPAND "abs") (("2" (PROPAX) NIL))))))) (|mod_sum_pos| "" (SKOSIMP*) (("" (EXPAND "mod") (("" (LEMMA "floor_plus_int") (("" (INST - "k!1*m!1/m!1" "i!1/m!1") (("" (REPLACE -1) (("" (ASSERT) NIL))))))))))) (|mod_sum| "" (SKOSIMP*) (("" (EXPAND "mod") (("" (LEMMA "floor_plus_int") (("" (INST - "k!1*j!1/j!1" "i!1/j!1") (("" (REPLACE -1) (("" (ASSERT) NIL))))))))))) (|mod_it_is| "" (SKOSIMP*) (("" (REPLACE -1) (("" (HIDE -1) (("" (LEMMA "mod_sum") (("" (INST - "b!1" "m!1" "c!1") (("" (REPLACE -1) (("" (HIDE -1) (("" (REWRITE "mod_lt") (("1" (LIFT-IF) (("1" (EXPAND "sgn") (("1" (PROPAX) NIL))))) ("2" (EXPAND "abs") (("2" (PROPAX) NIL))))))))))))))))))) (|mod_Ada| "" (SKOLEM!) (("" (EXPAND "mod") (("" (INST + "floor(i!1/j!1)") (("" (ASSERT) NIL))))))) (|mod_zero| "" (TCC) NIL) (|mod_one| "" (GRIND) (("1" (REWRITE "floor_small") (("1" (LIFT-IF) (("1" (GROUND) (("1" (REWRITE "pos_div_ge") NIL))))))) ("2" (LEMMA "div_cancel3") (("2" (INST -1 "j!1" "1" "0") (("2" (ASSERT) (("2" (REWRITE "floor_small") (("2" (LIFT-IF) (("2" (GROUND) (("2" (REWRITE "pos_div_ge") NIL))))))))))))))) (|mod_of_mod| "" (SKOSIMP*) (("" (REWRITE "mod") (("" (LEMMA "mod_sum") (("" (INST - "i!1+k!1" "m!1" "-floor(k!1/m!1)") (("" (ASSERT) NIL))))))))) (|mod_pos| "" (SKOSIMP*) (("" (TYPEPRED "mod(i!1,m!1)") (("" (TCC) (("" (LEMMA "both_sides_times_pos_le1") (("" (INST -1 "m!1" "floor(i!1 / m!1)" "i!1/m!1") (("" (ASSERT) NIL))))))))))) (|mod_TCC2| "" (SKOSIMP) (("" (REWRITE "mod_pos") NIL)))) $$$div_top.pvs div_top: THEORY %------------------------------------------------------------------------ % Defines "div" and "mod" in two different manners. % (1) according to the Ada Reference Manual % (2) according to standard number theory text. % % The Ada theory truncates toward zero on a negative argument while % the number theory truncates away from zero on a negative argument. % % div -- Ada Reference Manual division theory % div_nt -- Number theory division theory % div_alt -- Ada div defined recursively % div_nt_alt -- Number theory div defined recursively % mod -- mod theory % rem -- Ada Reference Manual rem theory % mod_lems -- Additional lemmas about mod % % AUTHOR % ------ % % Ricky W. Butler email: r.w.butler@larc.nasa.gov % Mail Stop 130 fax: (804) 864-4234 % NASA Langley Research Center phone: (804) 864-6198 % Hampton, Virginia 23681-0001 % % % Paul S. Miner | email: p.s.miner@larc.nasa.gov % 1 South Wright St. / MS 130 | fax: (804) 864-4234 % NASA Langley Research Center | phone: (804) 864-6201 % Hampton, Virginia 23681 | %------------------------------------------------------------------------ BEGIN IMPORTING mod, div, rem, div_nt, mod_div_lems, mod_lems, div_alt, div_nt_alt END div_top