Fixed-coupon bond pricing: present value of coupons plus redemption, current yield, and a par/premium/discount classifier
Discounts each coupon over a range, sum() of the discounted stream.
A Soma program from the finance part of the verified corpus: 49 lines, cells BondPricer, BondTests. It passes soma check with soma 3.2.4.
How it is built
The cell BondPricer declares 3 signals in its face: price(face_val: Float, coupon_rate: Float, ytm: Float, years: Int) -> Float, current_yield(annual_coupon: Float, price: Float) -> Float and classify(price: Float, face_val: Float) -> String. Handlers: price (line 13), current_yield (line 23) and classify (line 28).
The file also holds 1 test cell (BondTests) with 6 assertions, run by soma test.
The source
bond_pricer.cell
// Fixed-coupon bond pricing: present value of coupons plus redemption,
// current yield, and a par/premium/discount classifier. Discounts each
// coupon over a range, sum() of the discounted stream.
cell BondPricer {
face {
signal price(face_val: Float, coupon_rate: Float, ytm: Float, years: Int) -> Float
signal current_yield(annual_coupon: Float, price: Float) -> Float
signal classify(price: Float, face_val: Float) -> String
}
// P = sum_t C/(1+y)^t + F/(1+y)^n, annual coupons
on price(face_val: Float, coupon_rate: Float, ytm: Float, years: Int) {
let coupon = face_val * coupon_rate
let pv = 0.0
for t in range(1, years + 1) {
pv = pv + coupon / pow(1.0 + ytm, t)
}
pv = pv + face_val / pow(1.0 + ytm, years)
return pv
}
on current_yield(annual_coupon: Float, price: Float) {
if price == 0.0 { return 0.0 }
return annual_coupon / price
}
on classify(price: Float, face_val: Float) {
if abs(price - face_val) < 0.01 { return "par" }
if price > face_val { return "premium" }
return "discount"
}
}
cell test BondTests {
rules {
// coupon == ytm → bond prices at par (1000)
assert abs(price(1000.0, 0.05, 0.05, 10) - 1000.0) < 0.01
assert classify(price(1000.0, 0.05, 0.05, 10), 1000.0) == "par"
// ytm > coupon → trades at a discount
assert price(1000.0, 0.05, 0.08, 10) < 1000.0
assert classify(price(1000.0, 0.05, 0.08, 10), 1000.0) == "discount"
// ytm < coupon → premium
assert classify(price(1000.0, 0.05, 0.03, 10), 1000.0) == "premium"
// current yield on a $950 5% bond > 5%
assert current_yield(50.0, 950.0) > 0.05
}
}What the toolchain says
$ soma check bond_pricer.cell
✓ All checks passed.$ soma test bond_pricer.cell
test BondTests ...
✓ assert abs(price(1000.0, 0.05, 0.05, 10) - 1000.0) < 0.01
✓ assert classify(price(1000.0, 0.05, 0.05, 10), 1000.0) == "par"
✓ assert price(1000.0, 0.05, 0.08, 10) < 1000.0
✓ assert classify(price(1000.0, 0.05, 0.08, 10), 1000.0) == "discount"
✓ assert classify(price(1000.0, 0.05, 0.03, 10), 1000.0) == "premium"
✓ assert current_yield(50.0, 950.0) > 0.05
6 tests: 6 passed, 0 failed$ soma verify bond_pricer.cell
Verifying bond_pricer.cell...
No state machine in this program: nothing to prove beyond `soma check` (invariants and lifecycles are what verify proves).
VERIFY OK (vacuous — no state machine)