01Claude writes
fibHashMap: no Aeneas modeluse std::collections::HashMap;
pub fn fib(n: u64) -> u64 {
fn go(n: u64, memo: &mut HashMap<u64, u64>) -> u64 {
if n < 2 {
return n;
}
if let Some(&v) = memo.get(&n) {
return v;
}
let v = go(n - 1, memo) + go(n - 2, memo);
memo.insert(n, v);
v
}
go(n, &mut HashMap::new())
}
02Patched at build timebrick memo-to-accumulator · −13 +12
pub fn fib(n: u64) -> u64 {
if n == 0 {
return 0;
}
let mut a: u64 = 0;
let mut b: u64 = 1;
let mut i: u64 = 1;
while i < n {
let next = a + b;
a = b;
b = next;
i += 1;
}
b
}
03A theorem, English firstthen Lean
For every 64-bit integer n where n ≤ 93, fib(n) returns the n-th Fibonacci number.
def fib : Prop :=
∀ n : U64, n.val ≤ 93 →
∃ r, Generated.fib n = ok r ∧ r.val = fibSpec n.val
Found by the counterexample search
Found before the spec was proposed: fib(94) overflows u64. No unit test would say so.
04Checked by the Lean kernelend of the run
What a finished run records: a proof of Spec.fib with no
sorry and only allowed axioms,keyed to the hash of the patched tree that ships.