why3doc index index
module Get_str use int.Int use int.Abs use int.Power use array.Array use map.Map use mach.int.Int32 use mach.int.UInt32 use mach.c.UChar use import mach.int.UInt64GMP as Limb use mach.c.C use types.Types use types.Int32Eq use types.UInt64Eq use lemmas.Lemmas use powm.Powm use stringlemmas.String_lemmas use logical.Logical use int.ComputerDivision as CD use int.EuclideanDivision use base_info.BaseInfo let wmpn_get_str_bits (sp:ptr uchar) (bits:uint32) (up:ptr limb) (un:int32) (ghost ub:int32) : uint32 requires { 1 <= un } requires { valid up un } requires { 1 <= bits <= 8 } requires { valid sp (div (ub + bits - 1) bits) } requires { 0 <= ub } requires { value up un < power 2 ub } requires { (pelts up)[offset up + un - 1] > 0 } requires { 64 * un + 7 <= max_int32 } requires { writable sp } ensures { in_base (power 2 bits) (pelts sp) (offset sp) (offset sp + result) } ensures { svalue (power 2 bits) sp result = value up un } ensures { 0 < result <= (div (ub + bits - 1) bits) } ensures { (pelts sp)[offset sp] > 0 } ensures { forall j. j < offset sp \/ offset sp + (div (ub + bits - 1) bits) <= j -> (pelts sp)[j] = old (pelts sp)[j] } writes { sp.data.elts } = let um = C.get_ofs up (un - 1) in let sb = wmpn_limb_size_in_base_2 um in let e = 64 * (un-1) + Limb.to_int32 sb + UInt32.to_int32 bits - 1 in value_tail up (un-1); assert { power 2 (e-bits) <= value up un < power 2 (e-bits+1) by value up un = value up (un - 1) + power radix (un - 1) * (pelts up)[offset up + (un - 1)] = value up (un - 1) + power radix (un - 1) * um so power 2 (sb-1) <= um < power 2 sb so power radix (un - 1) = power 2 (64 * (un - 1)) so 0 <= value up (un - 1) < power radix (un - 1) = power 2 (64 * (un - 1)) so power radix (un - 1) * um >= power radix (un - 1) * power 2 (sb - 1) = power 2 (64 * (un - 1)) * power 2 (sb - 1) = power 2 (64 * (un - 1) + sb - 1) = power 2 (e - bits) so power 2 (e - bits) <= value up un so value up un < power radix (un - 1) + power radix (un - 1) * um = power radix (un - 1) * (1 + um) = power 2 (64 * (un - 1)) * (1 + um) <= power 2 (64 * (un - 1)) * power 2 sb = power 2 (64 * (un - 1) + sb) }; assert { e <= ub + bits - 1 by power 2 (e - bits) <= value up un < power 2 ub so if ub <= e - bits then power 2 ub * 1 <= power 2 ub * power 2 (e - bits - ub) = power 2 (e - bits) so false else e <= ub + bits - 1 }; let sn = e / UInt32.to_int32 bits in assert { offset sp + sn <= max sp by offset sp + div (ub + bits - 1) bits <= max sp so sn = div e bits so e <= ub + bits - 1 so let m' = mod e bits in let d = div (ub + bits - 1) bits in let m = mod (ub + bits - 1) bits in sn * bits + m' = e <= d * bits + m so m' <= bits - 1 so 0 <= m so bits * sn <= bits * d + (m-m') so - bits < m - m' < bits so sn <= d }; let b = lsl 1 (Limb.of_uint32 bits) in assert { b = power 2 bits }; assert { 2 <= b <= 256 by 1 <= bits <= 8 so power 2 2 = 4 so power 2 4 = 16 so power 2 5 = 32 so power 2 6 = 64 so power 2 7 = 128 so power 2 8 = 256 }; assert { power b (sn - 1) <= value up un < power b sn by e = bits * sn + CD.mod e bits so 0 <= CD.mod e bits < bits so bits * sn <= e < bits * sn + bits so bits * (sn - 1) <= e - bits so e - bits + 1 <= bits * sn so let d = e - bits - (bits * (sn - 1)) in 0 <= d so power b (sn - 1) = power (power 2 bits) (sn - 1) = power 2 (bits * (sn - 1)) <= power 2 (bits * (sn - 1)) * power 2 d = power 2 (e - bits) so power b sn = power (power 2 bits) sn = power 2 (bits * sn) >= power 2 (e - bits + 1) }; let ref i = 0 in let ref j = sn in let ref shift = 0 in let ghost ref udone : int = 0 in assert { sn = div e bits }; assert { sn * bits <= sn * bits + mod e bits = e }; while j > 0 do invariant { 0 <= i <= un } invariant { 0 <= j <= sn } invariant { (sn - j) * bits = udone } invariant { j > 0 -> udone = 64 * i + shift } invariant { 0 <= shift < Limb.length \/ i = un } invariant { in_base b (pelts sp) (offset sp + j) (offset sp + sn) } invariant { (svalue_sub b (pelts sp) (offset sp + j) (offset sp + sn) = valueb up udone /\ udone <= 64 * un) \/ (j = 0 /\ svalue b sp sn = value up un) } invariant { forall k. k < offset sp \/ offset sp + sn <= k -> (pelts sp)[k] = old (pelts sp)[k] } variant { j } assert { i < un by j > 0 so sn = div e bits so sn * bits <= sn * bits + mod e bits = e so 64 * i + shift = (sn - j) * bits <= sn * bits - bits <= e - bits <= 64 * un so i < un }; j <- j - 1; let lu = C.get_ofs up i in let ref digit = lsr_mod lu shift in let ghost low = mod (uint64'int lu) (power 2 (uint64'int shift)) in assert { lu = digit * power 2 shift + low by lu = power 2 shift * div lu (power 2 shift) + mod lu (power 2 shift) = power 2 shift * digit + low }; assert { div udone 64 = i /\ udone - 64 * i = shift }; let ghost oshift = shift in assert { power radix i * power 2 oshift = power b (sn - j - 1) by power radix i * power 2 oshift = power (power 2 64) i * power 2 oshift = power 2 (64 * i) * power 2 oshift = power 2 (64 * i + oshift) = power 2 ((sn - j - 1) * bits) = power (power 2 bits) (sn - j - 1) = power b (sn - j - 1) }; shift <- shift + Limb.of_uint32 bits; if shift >= 64 then begin value_tail up i; i <- i+1; assert { digit < power 2 (64 - oshift) by digit * power 2 oshift + low < radix so digit * power 2 oshift < radix = power 2 (64 - oshift) * power 2 oshift }; if i < un then begin shift <- shift - 64; let lu' = get_ofs up i in let ghost odigit = digit in let high = lsl_mod lu' (Limb.of_uint32 bits - shift) in assert { high = power 2 (bits - shift) * mod lu' (power 2 (64 - (bits - shift))) = power 2 (bits - shift) * mod lu' (power 2 oshift) by high = mod (lu' * power 2 (bits - shift)) radix so let d = div lu' (power 2 (64 - (bits - shift))) in let m = mod lu' (power 2 (64 - (bits - shift))) in lu' * power 2 (bits - shift) = d * (power 2 (64 - (bits - shift)) * power 2 (bits - shift)) + m * power 2 (bits - shift) = d * radix + m * power 2 (bits - shift) so 0 <= m < abs (power 2 (64 - (bits - shift))) = power 2 (64 - (bits - shift)) so power 2 (bits - shift) * m < power 2 (bits - shift) * power 2 (64 - (bits - shift)) = power 2 64 = radix so 0 <= m so 0 <= power 2 (bits - shift) so 0 <= m * power 2 (bits - shift) < radix so high = mod (radix * d + m * power 2 (bits - shift)) radix = mod (m * power 2 (bits - shift)) radix = m * power 2 (bits - shift) }; assert { digit + high < radix by digit < power 2 (64 - oshift) so shift = oshift + bits - 64 so 64 - oshift = bits - shift so digit + high < power 2 (bits - shift) + high = power 2 (bits - shift) * (1 + mod lu' (power 2 oshift)) <= power 2 (bits - shift) * power 2 oshift = power 2 (bits - shift + oshift) = power 2 64 = radix }; digit <- digit + high; (* TODO logical or *) assert { valueb up (udone + bits) = valueb up udone + mod digit b * power b (sn - j - 1) by valueb up udone = value up (i-1) + power radix (i-1) * low so oshift + bits >= 64 so div (udone + bits) 64 = i so udone = 64 * (i-1) + oshift so udone + bits - (64 * i) = 64 * (i-1) + oshift + bits - 64 * i = oshift + bits - 64 = shift so valueb up (udone + bits) = value up i + power radix i * mod lu' (power 2 shift) so value up i = value up (i-1) + power radix (i-1) * lu so lu = low + power 2 oshift * odigit so valueb up (udone + bits) - valueb up udone = power radix (i-1) * power 2 oshift * odigit + power radix i * mod lu' (power 2 shift) = power radix (i-1) * power 2 oshift * odigit + power radix (i-1) * radix * mod lu' (power 2 shift) = power radix (i-1) * (power 2 oshift * odigit + radix * mod lu' (power 2 shift)) = power radix (i-1) * (power 2 oshift * odigit + power 2 oshift * power 2 (64 - oshift) * mod lu' (power 2 shift)) = power radix (i-1) * power 2 oshift * (odigit + power 2 (64 - oshift) * mod lu' (power 2 shift)) = power b (sn - j - 1) * (odigit + power 2 (64 - oshift) * mod lu' (power 2 shift)) so power 2 (64 - oshift) * mod lu' (power 2 shift) = power 2 (bits - shift) * mod lu' (power 2 shift) = mod (lu' * power 2 (bits - shift)) (power 2 shift * power 2 (bits - shift)) = mod (lu' * power 2 (bits - shift)) (power 2 bits) so high = mod (lu' * power 2 (bits - shift)) radix so let d = div (lu' * power 2 (bits - shift)) radix in lu' * power 2 (bits - shift) = d * radix + high so radix = power 2 bits * power 2 (64 - bits) so mod (lu' * power 2 (bits - shift)) (power 2 bits) = mod (power 2 bits * (power 2 (64 - bits) * d) + high) (power 2 bits) = mod high (power 2 bits) = mod high b so odigit < power 2 (64 - oshift) = power 2 (bits - shift) so high = power 2 (bits - shift) * mod lu' (power 2 (64 - (bits - shift))) so mod high (power 2 (bits - shift)) = 0 so let d = div high (power 2 (bits - shift)) in high = d * power 2 (bits - shift) so let d' = div d (power 2 shift) in let m = mod d (power 2 shift) in high = (d' * power 2 shift + m) * power 2 (bits - shift) = d' * (power 2 shift * power 2 (bits - shift)) + m * power 2 (bits - shift) = d' * power 2 bits + power 2 (bits - shift) * m so shift < bits so 0 <= power 2 (bits - shift) so 0 <= m so 0 <= power 2 (bits - shift) * m < power 2 (bits - shift) * power 2 shift = b so div high b = d' so mod high b = high - b * div high b = m * power 2 (bits - shift) so 0 <= mod odigit b + mod high b = mod odigit b + m * power 2 (bits - shift) < power 2 (bits - shift) + m * power 2 (bits - shift) = power 2 (bits - shift) * (1 + m) <= power 2 (bits - shift) * power 2 shift = power 2 bits = b so odigit + mod high b = mod odigit b + mod high b = mod (mod odigit b + mod high b) b = mod (odigit + high) b = mod digit b so valueb up (udone + bits) - valueb up udone = power b (sn - j - 1) * (odigit + power 2 (64 - oshift) * mod lu' (power 2 shift)) = power b (sn - j - 1) * mod digit b }; end else begin assert { valueb up udone + mod digit b * power b (sn - j - 1) = value up un by i = un so div udone 64 = i - 1 so valueb up udone = value up (i-1) + power radix (i-1) * low so value up un = value up (i-1) + power radix (i-1) * lu so lu = low + digit * power 2 oshift so value up un = value up (i-1) + power radix (i-1) * (low + digit * power 2 oshift) = valueb up udone + power radix (i-1) * power 2 oshift * digit = valueb up udone + power b (sn - j - 1) * digit so digit < power 2 (64 - oshift) <= power 2 bits = b so mod digit b = digit }; assert { j = 0 by 64 * un <= udone + bits <= bits * (sn - j) so e < 64 * un + bits so sn = div e bits so sn * bits = e - mod e bits <= e < 64 * un + bits so bits * j <= sn * bits - 64 * un < bits so bits * j < bits * 1 so 0 < bits so j < 1 }; end end else begin assert { valueb up (udone + bits) = valueb up udone + mod digit b * power b (sn - j - 1) by valueb up udone = value up i + power radix i * low so oshift + bits = shift < 64 so div (udone + bits) 64 = i so valueb up (udone + bits) = value up i + power radix i * mod lu (power 2 (oshift + bits)) so let d = div digit (power 2 bits) in let m = mod digit (power 2 bits) in digit = d * power 2 bits + m so lu = digit * power 2 oshift + low = ((d * power 2 bits) + m) * power 2 oshift + low = d * power 2 (oshift + bits) + m * power 2 oshift + low so 0 <= low < power 2 oshift so 0 <= m < power 2 bits so 0 <= m * power 2 oshift so 0 <= m * power 2 oshift + low < m * power 2 oshift + power 2 oshift = power 2 oshift * (m+1) <= power 2 oshift * power 2 bits = power 2 (oshift + bits) so mod lu (power 2 (oshift + bits)) = mod (power 2 (oshift + bits) * d + (m * power 2 oshift + low)) (power 2 (oshift + bits)) = mod (m * power 2 oshift + low) (power 2 (oshift + bits)) = m * power 2 oshift + low so valueb up (udone + bits) = value up i + power radix i * (m * power 2 oshift + low) = value up i + power radix i * low + power radix i * (m * power 2 oshift) = valueb up udone + power radix i * m * power 2 oshift so 64 * i + oshift = (sn - j - 1) * bits so power radix i * power 2 oshift = power b (sn - j - 1) so valueb up (udone + bits) = valueb up udone + power b (sn - j - 1) * m }; end; (* TODO mask + logical and *) let sj = digit % b in assert { sj = mod digit b by div digit b = CD.div digit b so mod digit b = digit - b * div digit b = digit - b * CD.div digit b = CD.mod digit b = sj }; label Set in C.set_ofs sp j (UChar.of_uint64 sj); assert { forall i. offset sp + j < i -> (pelts sp)[i] = (pelts sp at Set)[i] }; assert { svalue_sub b (pelts sp) (offset sp + (j+1)) (offset sp + sn) = svalue_sub b (pelts sp at Set) (offset sp + (j+1)) (offset sp + sn) }; svalue_sub_tail (uint64'int b) (pelts sp) (offset sp + (int32'int j+1)) (offset sp + int32'int sn); assert { svalue_sub b (pelts sp) (offset sp + j) (offset sp + sn) = svalue_sub b (pelts sp) (offset sp + j + 1) (offset sp + sn) + power b (sn - (j + 1)) * sj = valueb up udone + mod digit b * power b (sn - j - 1) }; (* = valueb up (udone + bits) };*) udone <- udone + uint32'int bits; done; assert { udone <= 64 * un -> value up un = valueb up udone by udone = sn * bits = e - mod e bits = 64 * (un - 1) + sb + (bits - 1) - mod e bits >= 64 * (un - 1) + sb so un - 1 <= div udone 64 <= un so if div udone 64 = un - 1 then valueb up udone = value up (un-1) + power radix (un-1) * mod um (power 2 (udone - 64 * (un - 1))) so udone - 64 * (un - 1) >= sb so um < power 2 sb <= power 2 (udone - 64 * (un - 1)) so mod um (power 2 (udone - (64 * (un - 1)))) = um so valueb up udone = value up (un - 1) + power radix (un-1) * um = value up un else div udone 64 = un so udone = 64 * un so valueb up udone = value up un + power radix un * mod (pelts up)[offset up + un] (power 2 0) = value up un + power radix un * mod (pelts up)[offset up + un] 1 = value up un }; assert { sn <= div (ub + bits - 1) bits by sn = div e bits so e <= ub + bits - 1 so let m1 = mod e bits in let m2 = mod (ub + bits - 1) bits in let d = div (ub + bits - 1) bits in sn * bits + m1 = e <= d * bits + m2 so sn * bits <= d * bits + m2 - m1 < d * bits + bits so bits * sn < bits * (d + 1) so sn < d + 1 }; svalue_sub_tail (uint64'int b) (pelts sp) (offset sp + 1) (offset sp + int32'int sn); assert { (pelts sp)[offset sp] > 0 by value up un = svalue_sub b (pelts sp) (offset sp) (offset sp + sn) = power b (sn - 1) * (pelts sp)[offset sp] + svalue_sub b (pelts sp) (offset sp + 1) (offset sp + sn) so svalue_sub b (pelts sp) (offset sp + 1) (offset sp + sn) < power b (sn - 1) <= value up un }; UInt32.of_int32 sn use div.Div let wmpn_limb_get_str (sp: ptr uchar) (ghost sz:int32) (ref w:limb) (d1:limb) (di:limb) (shift:limb) (ghost binfo:wmpn_base_info) : uint32 requires { 2 <= binfo.b <= 256 } requires { writable sp } requires { d1 >= div radix 2 } requires { 0 <= shift <= 63 } requires { binfo.b * power 2 shift = d1 } requires { reciprocal di d1 } requires { valid sp sz } requires { 0 < sz } requires { w < power binfo.b sz } ensures { svalue_le binfo.b sp result = old w } ensures { 0 <= result <= sz } ensures { result > 0 -> (pelts sp)[offset sp + result - 1] > 0 } ensures { forall i. i < offset sp \/ offset sp + result <= i -> (pelts sp)[i] = old (pelts sp)[i] } ensures { in_base binfo.b (pelts sp) (offset sp) (offset sp + result) } = let ref i = 0 in let ghost ow = pure { w } in let ghost base = binfo.b in assert { radix = power 2 shift * power 2 (64 - shift) }; assert { shift > 0 by base <= 256 so base * power 2 shift >= div radix 2 > 256 so power 2 shift > 1 }; while w > 0 do invariant { 0 <= w < radix } invariant { 0 <= i <= sz } invariant { w > 0 -> 0 <= i < sz } invariant { in_base base (pelts sp) (offset sp) (offset sp + i) } invariant { w = 0 -> i > 0 -> (pelts sp)[offset sp + i - 1] > 0 } invariant { ow = svalue_le base sp i + power base i * w } invariant { forall j. j < offset sp \/ offset sp + i <= j -> (pelts sp)[j] = old (pelts sp)[j] } variant { w } label StartLoop in let h = lsr_mod w (64 - shift) in let l = lsl_mod w shift in assert { l + radix * h = power 2 shift * w by h = div w (power 2 (64 - shift)) so l = mod (power 2 shift * w) radix = mod (power 2 shift * w) (power 2 shift * power 2 (64 - shift)) = power 2 shift * mod w (power 2 (64 - shift)) so radix * h = power 2 shift * power 2 (64-shift) * h so l + radix * h = power 2 shift * (power 2 (64 - shift) * h + mod w (power 2 (64 - shift))) = power 2 shift * w }; assert { h < d1 by h = div w (power 2 (64 - shift)) so shift <= 63 so power 2 (64 - shift) >= 2 so w < radix so h * 2 <= h * power 2 (64 - shift) = div w (power 2 (64 - shift)) * power 2 (64 - shift) = w - mod w (power 2 (64 - shift)) <= w < radix so h <= div radix 2 }; let q, r = div2by1_inv h l d1 di in assert { r = power 2 shift * (w - base * q) by q * d1 + r = power 2 shift * w so q * d1 + r = power 2 shift * base * q + r }; assert { mod r (power 2 shift) = 0 by r = power 2 shift * (w - base * q) so mod r (power 2 shift) = mod (power 2 shift * (w - base * q) + 0) (power 2 shift) = 0 }; assert { ow = svalue_le base sp i + power base i * (w - base * q) + power base (i+1) * q by ow = svalue_le base sp i + power base i * w so power base i * (w - base * q) + power base (i+1) * q = power base i * (w - base * q) + power base i * base * q = power base i * w }; let ghost osp = pure { sp } in let ghost nr = lsr r shift in assert { nr = w - base * q }; assert { 0 <= nr < 256 by r < d1 so nr * power 2 shift = r so base * power 2 shift = d1 so nr < base <= 256 }; C.set_ofs sp i (UChar.of_uint64 (lsr r shift)); svalue_le_sub_frame base (pelts sp) (pelts osp) (offset sp) (offset sp + int32'int i); assert { in_base base (pelts sp) (offset sp) (offset sp + i + 1) }; svalue_le_sub_tail base (pelts sp) (offset sp) (offset sp + int32'int i); assert { q < w by q * d1 <= power 2 shift * w so d1 = base * power 2 shift > power 2 shift > 0 so w * power 2 shift < w * d1 so d1 * q < d1 * w }; assert { svalue_le base sp (i+1) + power base (i+1) * q = ow by svalue_le base sp (i+1) = svalue_le base sp i + power base i * (pelts sp)[offset sp + i] = svalue_le base sp i + power base i * (w - base * q) = svalue_le base (sp at StartLoop) i + power base i * (w - base * q) }; assert { q > 0 -> i + 1 < sz by power base sz > ow so power base (i+1) <= power base (i+1) * q = ow - svalue_le base sp (i+1) <= ow so power base (i+1) < power base sz }; assert { q = 0 -> nr > 0 by r = power 2 shift * w >= power 2 shift }; w <- q; i <- i + 1; done; UInt32.of_int32 i use util.UtilOld let wmpn_get_str_other (sp: ptr uchar) (ghost sz:int32) (base:int32) (info:wmpn_base_info) (up: ptr limb) (un: int32) : uint32 requires { valid up un } requires { 1 <= un } requires { info.b = base } requires { writable up } requires { writable sp } requires { (pelts up)[offset up + un - 1] > 0 } requires { 0 < sz } requires { valid sp sz } requires { value up un < power base (sz-1) } ensures { 0 <= result < sz } ensures { svalue base sp result = old value up un } ensures { in_base base (pelts sp) (offset sp) (offset sp + result) } ensures { (pelts sp)[offset sp] > 0 } ensures { forall j. j < offset sp \/ offset sp + sz <= j -> (pelts sp)[j] = old (pelts sp)[j] } = let shift = Limb.of_int32 (Limb.count_leading_zeros (Limb.of_int32 base)) in let d1 = lsl (Limb.of_int32 base) shift in assert { d1 >= div radix 2 by 2 * power 2 shift * base >= radix so d1 = power 2 shift * base so 2 * d1 >= radix }; let di = invert_limb d1 in let ghost vu = value up (int32'int un) in let ref sn = 0 in let ref n = un in begin ensures { svalue_le base sp sn + power base sn * value up 1 = vu } ensures { in_base base (pelts sp) (offset sp) (offset sp + sn) } ensures { 0 <= sn < sz } ensures { 0 < value up 1 } ensures { forall j. j < offset sp \/ offset sp + sz <= j -> (pelts sp)[j] = old (pelts sp)[j] } if n > 1 then begin let tp = salloc (UInt32.of_int32 n) in let ghost ref loopi : int = 0 in while n > 1 do variant { value up n } invariant { svalue_le base sp sn + power base sn * value up n = vu } invariant { 1 <= n <= un } invariant { un - n <= loopi } invariant { 0 <= sn < sz } (*invariant { power radix n <= power base (sz - 1 - sn) }*) invariant { sn = loopi * info.exp } invariant { in_base base (pelts sp) (offset sp) (offset sp + sn) } invariant { (pelts up)[offset up + n - 1] > 0 } invariant { forall j. j < offset sp \/ offset sp + sz <= j -> (pelts sp)[j] = old (pelts sp)[j] } label StartLoop in let ghost osn = sn in let ref w = wmpn_divrem_1 tp up n info.bb in value_tail up (n-1); assert { sn + info.exp < sz by value up n >= power radix (n-1) * (pelts up)[offset up + n - 1] >= power radix (n-1) so n - 1 >= 1 so power radix (n-1) >= radix so vu < power base (sz - 1) so power base sn * power base info.exp < power base sn * radix <= power base sn * value up n <= vu < power base (sz - 1) so power base (sn + info.exp) < power base (sz - 1) }; label Size in wmpn_copyi up tp n; value_sub_frame_shift (pelts up) (pelts tp) (offset up) (offset tp) (int32'int n); n <- n - if C.get_ofs up (n-1) = 0 then 1 else 0; value_tail up n; assert { value up n = value tp n at Size by if (pelts up)[offset up + n - 1 at Size] = 0 then n = n-1 at Size so value up n = value up (n+1) = value tp n at Size else n = n at Size so value up n = value tp n at Size }; assert { (pelts up)[offset up + n - 1] > 0 by if (pelts up)[offset up + n - 1 at Size] = 0 then n = n-1 at Size so value up n at StartLoop = value up (n-1) at StartLoop + (power radix (n-1) * (pelts up)[offset up + (n - 1)] at StartLoop) >= (power radix (n-1) * (pelts up)[offset up + (n - 1)] at StartLoop) >= power radix (n-1 at StartLoop) so value up n at StartLoop = info.bb * value up n + w so info.bb < radix so value up n * info.bb < value up n * radix so w < radix so info.bb * value up n + w < info.bb * value up n + radix < value up n * radix + radix = radix * (value up n + 1) so radix * power radix (n-1) = power radix n < radix * (value up n + 1) so power radix (n-1) < value up n + 1 so power radix (n-1) <= value up n = value up (n-1) + power radix (n-1) * (pelts up)[offset up + n - 1] < power radix (n-1) + power radix (n-1) * (pelts up)[offset up + n - 1] = power radix (n-1) * (1 + (pelts up)[offset up + n - 1]) so 1 < (1 + (pelts up)[offset up + n - 1]) else true }; let spn = C.incr sp sn in let ghost osp = pure { sp } in let ref sdone = wmpn_limb_get_str spn (UInt32.to_int32 info.exp + 1) w d1 di shift info in svalue_le_sub_frame (int32'int base) (pelts sp) (pelts osp) (offset sp) (offset sp + int32'int sn); assert { forall j. j < offset sp \/ offset sp + sz <= j -> (pelts sp)[j] = (pelts osp)[j] by j < offset sp <= offset spn \/ offset spn + sdone <= offset sp + sz <= j}; assert { svalue_le base sp sn = svalue_le base sp sn at StartLoop }; in_base_concat (int32'int base) (pelts sp) (offset sp) (offset sp + int32'int sn) (offset sp + int32'int sn + uint32'int sdone); svalue_le_concat (int32'int base) sp sn (sn + UInt32.to_int32 sdone); ghost (if sdone > 0 then svalue_le_tail (int32'int base) spn (UInt32.to_int32 sdone - 1)); assert { svalue_le base sp (sn + sdone) + power base (sn + info.exp) * value up n = vu by svalue_le base sp (sn + sdone) = svalue_le base sp sn at StartLoop + power base sn * (w at Size) so power base sn * value up n at StartLoop = power base sn * (power base info.exp * value up n + (w at Size)) = power base (sn + info.exp) * value up n + power base sn * (w at Size) }; sn <- sn + UInt32.to_int32 sdone; assert { info.bb * value up n + (w at Size) = value up n at StartLoop }; assert { 0 <= value up n < value up n at StartLoop by info.bb * value up n <= value up n at StartLoop so info.bb > 1 so if value up n = 0 then value up n at StartLoop = value up (n-1) + power radix (n-1) * (pelts up)[offset up + n - 1] at StartLoop >= power radix (n-1) * (pelts up)[offset up + n - 1] at StartLoop > 0 else value up n = value up n * 1 < value up n * info.bb }; assert { sdone <= info.exp by w at Size < info.bb = power base info.exp so svalue_le base spn sdone = w at Size so if sdone = 0 then true else (pelts spn)[offset spn + sdone - 1] > 0 so svalue_le base spn sdone = svalue_le base spn (sdone - 1) + power base (sdone - 1) * (pelts spn)[offset spn + sdone - 1] >= power base (sdone - 1) * (pelts spn)[offset spn + sdone - 1] >= power base (sdone - 1) so 0 <= power base (sdone - 1) < power base info.exp so sdone - 1 < info.exp }; while sdone < info.exp do variant { info.exp - sdone } invariant { sdone <= info.exp } invariant { sn = osn + sdone } invariant { in_base base (pelts sp) (offset sp) (offset sp + sn) } invariant { svalue_le base sp sn + power base (sn - sdone + info.exp) * value up n = vu } invariant { forall j. j < offset sp \/ offset sp + sz <= j -> (pelts sp)[j] = old (pelts sp)[j] } label Loop2 in let ghost osp = pure { sp } in C.set_ofs sp sn 0; svalue_le_sub_frame (int32'int base) (pelts sp) (pelts osp) (offset sp) (offset sp + int32'int sn); svalue_le_tail (int32'int base) sp sn; assert { svalue_le base sp (sn+1) = svalue_le base sp sn at Loop2 }; sn <- sn + 1; sdone <- sdone + 1; done; loopi <- loopi + 1; done; end end; let ref lu = C.get up in assert { value up 1 = lu }; let ghost osp = pure { sp } in let spn = C.incr sp sn in assert { lu < power base (sz - 1 - sn) by svalue_le base sp sn + power base sn * lu = vu so svalue_le base sp sn + power base sn * lu >= power base sn * lu so vu < power base (sz-1) = power base sn * power base (sz - 1 - sn) }; let sdone = wmpn_limb_get_str spn (sz - 1 - sn) lu d1 di shift info in assert { (pelts spn)[offset spn + sdone - 1] > 0 }; assert { forall j. j < offset sp \/ offset sp + sz <= j -> (pelts sp)[j] = (pelts osp)[j] by j < offset sp <= offset spn \/ offset spn + sdone <= offset sp + sz <= j }; svalue_le_sub_frame (int32'int base) (pelts sp) (pelts osp) (offset sp) (offset sp + int32'int sn); in_base_concat (int32'int base) (pelts sp) (offset sp) (offset sp + int32'int sn) (offset sp + int32'int sn + uint32'int sdone); svalue_le_concat (int32'int base) sp sn (sn + UInt32.to_int32 sdone); sn <- sn + UInt32.to_int32 sdone; assert { (pelts sp)[offset sp + sn - 1] > 0 }; assert { svalue_le base sp sn = vu }; let ghost osp = pure { sp } in let ref i = 0 in assert { valid sp sn }; while (2 * i + 1 < sn) do variant { sn - i } invariant { 0 <= 2 * i + 1 <= sn + 1 } invariant { forall j. offset sp + i <= j < offset sp + sn - i -> (pelts sp)[j] = (pelts osp)[j] } invariant { in_base base (pelts sp) (offset sp) (offset sp + sn) } invariant { svalue_sub base (pelts sp) (offset sp) (offset sp + i) = svalue_le_sub base (pelts osp) (offset sp + sn - i) (offset sp + sn) } invariant { svalue_sub base (pelts sp) (offset sp + sn - i) (offset sp + sn) = svalue_le_sub base (pelts osp) (offset sp) (offset sp + i) } invariant { svalue_le_sub base (pelts sp) (offset sp + i) (offset sp + sn - i) = svalue_le_sub base (pelts osp) (offset sp + i) (offset sp + sn - i) } invariant { i > 0 -> (pelts sp)[offset sp] > 0 } invariant { forall j. j < offset sp \/ offset sp + sz <= j -> (pelts sp)[j] = old (pelts sp)[j] } let ghost osp' = pure { sp } in assert { 0 <= i < sn }; let t = C.get_ofs sp i in assert { t = (pelts osp)[offset sp + i] }; assert { (pelts sp)[offset sp + sn - i - 1] = (pelts osp)[offset sp + sn - i - 1] }; assert { forall j. offset sp <= j < offset sp + sn -> 0 <= (pelts sp)[j] < base }; C.set_ofs sp i (C.get_ofs sp (sn - i - 1)); assert { forall j. offset sp <= j < offset sp + sn -> 0 <= (pelts sp)[j] < base }; C.set_ofs sp (sn - i - 1) t; assert inbase { forall j. offset sp <= j < offset sp + sn -> 0 <= (pelts sp)[j] < base }; svalue_sub_frame (int32'int base) (pelts sp) (pelts osp') (offset sp) (offset sp + int32'int i); svalue_sub_frame (int32'int base) (pelts sp) (pelts osp') (offset sp + int32'int i + 1) (offset sp + int32'int sn - int32'int i - 1); svalue_sub_frame (int32'int base) (pelts sp) (pelts osp') (offset sp + int32'int sn - int32'int i) (offset sp + int32'int sn); svalue_le_sub_tail (int32'int base) (pelts osp) (offset sp) (offset sp + int32'int i); svalue_le_sub_head (int32'int base) (pelts osp) (offset sp + (int32'int sn - int32'int i - 1)) (offset sp + int32'int sn); svalue_sub_head (int32'int base) (pelts sp) (offset sp) (offset sp + int32'int i + 1); svalue_sub_tail (int32'int base) (pelts sp) (offset sp + int32'int sn - int32'int i) (offset sp + int32'int sn); assert { svalue_sub base (pelts sp) (offset sp) (offset sp + i + 1) = base * svalue_sub base (pelts sp) (offset sp) (offset sp + i) + (pelts sp)[offset sp + i] = base * svalue_sub base (pelts osp') (offset sp) (offset sp + i) + (pelts sp)[offset sp + i] = base * svalue_le_sub base (pelts osp) (offset sp + sn - i) (offset sp + sn) + (pelts sp)[offset sp + i] = base * svalue_le_sub base (pelts osp) (offset sp + sn - i) (offset sp + sn) + (pelts osp)[offset sp + sn - i - 1] = svalue_le_sub base (pelts osp) (offset sp + sn - i - 1) (offset sp + sn) }; assert { svalue_sub base (pelts sp) (offset sp + sn - i - 1) (offset sp + sn) = svalue_sub base (pelts sp) (offset sp + sn - i) (offset sp + sn) + power base i * (pelts sp)[offset sp + sn - i - 1] = svalue_sub base (pelts osp') (offset sp + sn - i) (offset sp + sn) + power base i * (pelts sp)[offset sp + sn - i - 1] = svalue_le_sub base (pelts osp) (offset sp) (offset sp + i) + power base i * (pelts sp)[offset sp + sn - i - 1] = svalue_le_sub base (pelts osp) (offset sp) (offset sp + i) + power base i * (pelts osp)[offset sp + i] = svalue_le_sub base (pelts osp) (offset sp) (offset sp + i + 1) }; svalue_le_sub_frame (int32'int base) (pelts sp) (pelts osp) (offset sp + int32'int i + 1) (offset sp + int32'int sn - int32'int i - 1); i <- i + 1; done; assert { svalue_le_sub base (pelts sp) (offset sp + i) (offset sp + sn - i) = svalue_sub base (pelts sp) (offset sp + i) (offset sp + sn - i) by if 2 * i + 1 = sn then svalue_le_sub base (pelts sp) (offset sp + i) (offset sp + sn - i) = (pelts sp)[offset sp + i] so sn - i = i + 1 so svalue_sub base (pelts sp) (offset sp + i) (offset sp + sn - i) = svalue_sub base (pelts sp) (offset sp + i) (offset sp + i + 1) = (pelts sp)[offset sp + i] + base * svalue_sub base (pelts sp) (offset sp + i) (offset sp + i) = (pelts sp)[offset sp + i] else i = sn - i so svalue_le_sub base (pelts sp) (offset sp + i) (offset sp + sn - i) = 0 = svalue_sub base (pelts sp) (offset sp + i) (offset sp + sn - i) }; svalue_sub_concat (int32'int base) (pelts sp) (offset sp) (offset sp + int32'int i) (offset sp + int32'int sn); svalue_sub_concat (int32'int base) (pelts sp) (offset sp + int32'int i) (offset sp + (int32'int sn - int32'int i)) (offset sp + int32'int sn); svalue_le_sub_concat (int32'int base) (pelts osp) (offset sp) (offset sp + int32'int i) (offset sp + int32'int sn); svalue_le_sub_concat (int32'int base) (pelts osp) (offset sp + int32'int i) (offset sp + (int32'int sn - int32'int i)) (offset sp + int32'int sn); assert { vu = svalue_le_sub base (pelts osp) (offset sp) (offset sp + i) + power base i * svalue_le_sub base (pelts osp) (offset sp + i) (offset sp + sn - i) + power base (sn - i) * svalue_le_sub base (pelts osp) (offset sp + sn - i) (offset sp + sn) by vu = svalue_le_sub base (pelts osp) (offset sp) (offset sp + sn) = svalue_le_sub base (pelts osp) (offset sp) (offset sp + i) + power base i * svalue_le_sub base (pelts osp) (offset sp + i) (offset sp + sn) = svalue_le_sub base (pelts osp) (offset sp) (offset sp + i) + power base i * (svalue_le_sub base (pelts osp) (offset sp + i) (offset sp + sn - i) + power base (sn - i - i) * svalue_le_sub base (pelts osp) (offset sp + sn - i) (offset sp + sn)) = svalue_le_sub base (pelts osp) (offset sp) (offset sp + i) + power base i * svalue_le_sub base (pelts osp) (offset sp + i) (offset sp + sn - i) + power base i * power base (sn - i - i) * svalue_le_sub base (pelts osp) (offset sp + sn - i) (offset sp + sn) = svalue_le_sub base (pelts osp) (offset sp) (offset sp + i) + power base i * svalue_le_sub base (pelts osp) (offset sp + i) (offset sp + sn - i) + power base (sn - i) * svalue_le_sub base (pelts osp) (offset sp + sn - i) (offset sp + sn) }; assert { svalue base sp sn = svalue_sub base (pelts sp) (offset sp) (offset sp + sn) = power base (sn - i) * svalue_sub base (pelts sp) (offset sp) (offset sp + i) + power base i * svalue_sub base (pelts sp) (offset sp + i) (offset sp + sn - i) + svalue_sub base (pelts sp) (offset sp + sn - i) (offset sp + sn) = power base (sn - i) * svalue_le_sub base (pelts osp) (offset sp + sn - i) (offset sp + sn) + power base i * svalue_le_sub base (pelts osp) (offset sp + i) (offset sp + sn - i) + svalue_le_sub base (pelts osp) (offset sp) (offset sp + i) = vu }; UInt32.of_int32 sn let wmpn_get_str (sp: ptr uchar) (ghost sz: int32) (base: int32) (up: ptr limb) (un: int32) : uint32 requires { 0 < sz } requires { 0 < un } requires { valid sp sz } requires { valid up un } requires { writable sp } requires { writable up } requires { power radix un <= power base (sz - 1) } requires { (pelts up)[offset up + un - 1] > 0 } requires { 2 <= base <= 256 } requires { 64 * un + 7 <= max_int32 } ensures { in_base base (pelts sp) (offset sp) (offset sp + result) } ensures { svalue base sp result = old (value up un) } ensures { 0 < result < sz } ensures { (pelts sp)[offset sp] > 0 } = let bits = wmpn_base_power_of_two_p (Limb.of_int32 base) in if (bits <> 0) then begin assert { div (64 * un + bits - 1) bits < sz by power 2 (64 * un) = power radix un <= power base (sz - 1) = power (power 2 bits) (sz - 1) = power 2 (bits * (sz - 1)) so if bits * (sz - 1) < 64 * un then power 2 (bits * (sz - 1)) * 1 < power 2 (bits * (sz - 1)) * power 2 (64 * un - (bits * (sz - 1))) = power 2 (64 * un) so false else 64 * un <= bits * (sz - 1) so 64 * un + bits - 1 < bits * sz so let d = div (64 * un + bits - 1) bits in 64 * un + bits - 1 >= bits * d so bits * d < bits * sz so d < sz }; wmpn_get_str_bits sp bits up un (64 * un); end else begin let info = wmpn_get_base_info (Limb.of_int32 base) in wmpn_get_str_other sp sz base info up un end end
Generated by why3doc 1.7.0