import logos
import logos.tactics as tData Structures
Reasoning about pure functions on data — the foundation of verified algorithm design.
Reasoning About External Functions
When you can’t inspect a function’s source (C extensions, third-party libraries), declare it externally and axiomatize its contract:
# Declare Python's built-in sorted() as an external function
my_sorted = logos.extern("my_sorted", [list], list)
xs = logos.var("xs", list)
i = logos.var("i", int)
j = logos.var("j", int)
# Axiomatize what we know about sorted()
@logos.axiom
def sorted_length(xs: list):
return my_sorted(xs) == my_sorted(xs) # placeholder
# Verify concrete behavior with decide()
logos.check(logos.prove(
logos.lit(1) < logos.lit(3),
[t.decide()],
))
print("Ordering check: 1 < 3 ✓")Ordering check: 1 < 3 ✓Pure Accumulator Functions
Accumulators are a common pattern — prove properties about their results:
@logos.define
def increment(n: int):
"""n + 1"""
return n + logos.lit(1)
# increment is strictly greater than its input
@logos.theorem
def increment_gt(n: int):
return increment(n) > n
logos.check(increment_gt.proof(t.intro("n"), t.unfold(increment), t.linarith()))
print("increment(n) > n ✓")
# increment is non-negative when input is non-negative
@logos.theorem
def increment_nonneg(n: int):
return (n >= logos.lit(0)) >> (increment(n) >= logos.lit(0))
logos.check(increment_nonneg.proof(t.intro("n", "h"), t.unfold(increment), t.linarith()))
print("n ≥ 0 → increment(n) ≥ 0 ✓")increment(n) > n ✓
n ≥ 0 → increment(n) ≥ 0 ✓Monotone Functions
A function is monotone if x ≤ y → f(x) ≤ f(y). This property is essential for binary search correctness:
@logos.define
def linear_fn(x: int):
return logos.lit(3) * x + logos.lit(5)
@logos.theorem
def linear_fn_monotone(x: int, y: int):
return (x <= y) >> (linear_fn(x) <= linear_fn(y))
logos.check(linear_fn_monotone.proof(
t.intro("x", "y", "h"),
t.unfold(linear_fn),
t.linarith(),
))
print("3x + 5 is monotone ✓")
@logos.define
def square(x: int):
return x * x
# Algebraic identity: (x+1)² = x² + 2x + 1
@logos.theorem
def square_succ(x: int):
return square(x + logos.lit(1)) == square(x) + logos.lit(2) * x + logos.lit(1)
logos.check(square_succ.proof(t.intro("x"), t.unfold(square), t.ring()))
print("(x+1)² = x² + 2x + 1 ✓")
# Difference of squares: (x-y)*(x+y) = x² - y²
@logos.theorem
def square_diff(x: int, y: int):
return (x - y) * (x + y) == square(x) - square(y)
logos.check(square_diff.proof(t.intro("x", "y"), t.unfold(square), t.ring()))
print("(x-y)(x+y) = x² - y² ✓")3x + 5 is monotone ✓
(x+1)² = x² + 2x + 1 ✓
(x-y)(x+y) = x² - y² ✓Function Composition Properties
Composition of linear scaling functions: prove that applying a 2× scale twice equals a 4× scale.
@logos.define
def scale_2(x: int):
return logos.lit(2) * x
@logos.define
def scale_4(x: int):
return logos.lit(4) * x
# scale_2 ∘ scale_2 = scale_4
@logos.theorem
def double_twice_is_quadruple(x: int):
return scale_2(scale_2(x)) == scale_4(x)
logos.check(double_twice_is_quadruple.proof(
t.intro("x"), t.unfold(scale_2), t.unfold(scale_2), t.unfold(scale_4), t.ring()
))
print("2*(2*x) = 4*x ✓")
# scale_2 preserves the sign
@logos.theorem
def scale_2_nonneg(x: int):
return (x >= logos.lit(0)) >> (scale_2(x) >= logos.lit(0))
logos.check(scale_2_nonneg.proof(t.intro("x", "h"), t.unfold(scale_2), t.linarith()))
print("x ≥ 0 → 2x ≥ 0 ✓")2*(2*x) = 4*x ✓
x ≥ 0 → 2x ≥ 0 ✓Composing Function Properties
Prove properties of function compositions from properties of the parts:
@logos.define
def double(x: int):
return logos.lit(2) * x
@logos.define
def triple(x: int):
return logos.lit(3) * x
@logos.define
def sextuple(x: int):
return logos.lit(6) * x
@logos.theorem
def double_triple_is_sextuple(x: int):
return double(triple(x)) == sextuple(x)
logos.check(double_triple_is_sextuple.proof(
t.intro("x"), t.unfold(double), t.unfold(triple), t.unfold(sextuple), t.ring()
))
print("2 * (3 * x) = 6 * x ✓")
# And multiplication is commutative in composition order
@logos.theorem
def triple_double_is_sextuple(x: int):
return triple(double(x)) == sextuple(x)
logos.check(triple_double_is_sextuple.proof(
t.intro("x"), t.unfold(triple), t.unfold(double), t.unfold(sextuple), t.ring()
))
print("3 * (2 * x) = 6 * x ✓")2 * (3 * x) = 6 * x ✓
3 * (2 * x) = 6 * x ✓API Contracts as Theorems
A real-world pattern: encode a function’s postcondition as a logos theorem. If the proof breaks, the contract was violated:
# A pricing function that applies a fixed flat discount
@logos.define
def apply_flat_discount(price: int):
"""price - 10 (fixed $10 discount)"""
return price - logos.lit(10)
# Contract 1: discounted price is strictly less than original
@logos.theorem
def flat_discount_reduces_price(price: int):
return apply_flat_discount(price) < price
logos.check(flat_discount_reduces_price.proof(
t.intro("price"), t.unfold(apply_flat_discount), t.linarith()
))
print("Discount contract: discounted < original ✓")
# A shipping fee function
@logos.define
def add_shipping(price: int):
"""price + 5 (fixed $5 shipping)"""
return price + logos.lit(5)
# Contract 2: after shipping, total is always greater than base price
@logos.theorem
def shipping_increases_price(price: int):
return add_shipping(price) > price
logos.check(shipping_increases_price.proof(
t.intro("price"), t.unfold(add_shipping), t.linarith()
))
print("Shipping contract: total > base price ✓")
# Contract 3: discount then shipping equals shipping then discount
@logos.theorem
def order_matters(price: int):
return add_shipping(apply_flat_discount(price)) == apply_flat_discount(add_shipping(price))
logos.check(order_matters.proof(
t.intro("price"),
t.unfold(add_shipping), t.unfold(apply_flat_discount),
t.ring(),
))
print("discount∘shipping == shipping∘discount (same result) ✓")Discount contract: discounted < original ✓
Shipping contract: total > base price ✓
discount∘shipping == shipping∘discount (same result) ✓Ground Computation Verification
Verify that specific computations give the correct answer — essentially a proof-carrying unit test:
# Verify that our formulas compute the right values for concrete inputs
for n, expected in [(1, 1), (2, 4), (3, 9), (4, 16), (5, 25)]:
logos.check(logos.prove(
logos.lit(n) ** logos.lit(2) == logos.lit(expected),
[t.norm_num()],
))
print(f"{n}² = {expected} ✓")1² = 1 ✓
2² = 4 ✓
3² = 9 ✓
4² = 16 ✓
5² = 25 ✓