Instructor: Jianan Yao

LEC: Th1:10-3:00PM MC252

assn*4 40%
project 50%

• Week 1. Sep 10
• Week 2. Sep. 17
• Week 3. Sep 24
• Week 4. Oct 1
• Week 5. Oct 8
• Week 6. Oct 15
• Week 7. Oct 23

Week 1. Sep 10

types of program synthesis

• programming by example (PBE): generate program matching given examples (FlashFill)
• formal specs: generate a program satisfying the given constraint formulas, e.g. SyGuS.
• natural language specs
• combinations: synthesis using multiple sources of specs

formal verification: use formal methods of math to verify a program satisfying its specs.

timeline of major verification tools and systems

• theory
  • hoare logic (1969)
  • temporal logic (1977)
  • separation logic
• prover
  • isabelle (1986)
  • coq (1989)
  • z3 smt (2008)
• verified system
  • compCert compiler (2006)
  • seL4 microkernel (2009)
  • Verdi & IronFleet (2015)

Flashfill: excel feature to autofill cells based on examples.

Alan Turing       AT
John McCarthy     JM    
Donald E. Knuth   DEK
Edsger Dijstra    // guess ED
Leslie B. Lamport

suffers from ambiguity (too few examples - if keep 1st cell only, then it may guess JMC).

eg. given input: (425)-706-7709, output: 425-706-7709. for simplicity, restrict the synthesized program to be a finite substring concat:

output = substring + constant + substring + ...

for "706" there are many possible expressions deriving it:

• 2nd number
• substring between the first and last "-"
• first number after first "-"
• constant
• ...

suppose there are 10 different ways to derive "425" in the output, 10 ways for "706" and 10 ways for "7709". there are 1000 candidate programs. use a compact set representation instead of enumerating all:

[1st number between 1st pair of "()": "425"], ...
"-"
[2nd number between 1st and 2nd "-": "706"], ...
"-"
[3rd number after 2nd "-": "7709"], ...

if there are more examples, the synthesized program must satisfy all. so we need to intersect the candidate sets for each part of the output.

this however assumes a linear structure (split by "-"). to improve we use a DAG representation.

        ┌────────────────────┐             ┌────────────────────┐             ┌────────────────────┐
        │ 1st number between │   ┌─────┐   │ 2nd number between │   ┌─────┐   │ 3rd number         │
start ●─┤ 1st pair of "()"   ├─●─┤ "-" ├─●─┤ 1st and 2nd "-"    ├─●─┤ "-" ├─●─┤ 1st number after   ├─● end
        │ "425"              │ │ └─────┘ │ │ "706"              │   └─────┘   │ last "-"  "7709"   │ │
        │ ...                │ │         │ │ ...                │             │ ...                │ │
        └────────────────────┘ │         │ └────────────────────┘             └────────────────────┘ │
                               │         │             ┌────────────────────┐                        │
                               │         │             │ after 1st "-"      │                        │
                               │         └─────────────┤ last 8 characters  ├────────────────────────┤
                               │                       │ "706-7709"         │                        │
                               │                       │ ...                │                        │
                               │                       └────────────────────┘                        │
                               │                       ┌────────────────────┐                        │
                               └───────────────────────┤ after first ")"    ├────────────────────────┘
                                                       │ ...                │
                                                       └────────────────────┘

what if no single program works for every example? the intersections of DAGs can be empty.

(425)-706-7709  425-706-7709
604 910 2026    604-910-2026
978-5804        416-978-5804
946 8727        416-946-8727

FlashFill greedily groups examples that share a common program. then synthesize a classifier (e.g. boolean) to separate examples. The final output:

if input has 3 numbers
then SubStr(input, 1st number) + “-” + SubStr(input, 2nd number) + “-” + SubStr(input, 3rd number)
else “416-” + SubStr(input, 1st number) + “-” + SubStr(input, 2nd number)

Week 2. Sep. 17

correctness: starting from any state satisfying P (precondition), we want to ensure running this code lands in a state satisfying Q (postcondition).

pre- and postconditions divide responsibilities between caller and callee

consequences:

• stronger precondition makes impl's job easier and caller's harder, and vice versa
• both extremes are degenerate
  • a precond that no caller can satisfy makes every impl correct
  • a postcond that promises nothing can be met by every impl

eg. specifying min

// pre: true
int min(int a, int b) {
    if (a < b) r = a;
    else r = b;
    return r;
}
// post: r <= a && r <= b && (r == a || r == b)

central trade of formal verification: burden of being right moves from a large operational artifact (the code) to a small declarative one (the specification). specs are usually far shorter and far easier to review, but they are now the thing that must be right.

defn. (hoare triple) { P } C { Q }, where P is the precondition (an assertion), C is the program (command), and Q is the postcondition (an assertion).

• it holds if for every state s satisfying P, if executing C from s terminates in a state s', then s' satisfies Q.
• partial correctness:
  • we promise nothing about starting states that do not satisfy P.
  • we promise nothing if C fails to terminate
  • we promise only Q, and only on the final state

notation.

• ⊨ {P} C {Q}: triple is true of the actual execution behaviour (semantics)
• ⊢ {P} C {Q}: triple is derivable using the rules of hoare logic (syntax)

hoare logic is sound: anything derivable is true. It is also complete relative to the assertion language (Cook, 1978) - if a triple is true, a derivation exists, provided we can prove the arithmetic facts it needs.

notation.

• {P} C {Q}: partial correctness; if C terminates, Q holds
• [P] C [Q]: total correctness; C terminates, and Q holds
  • = partial correctness + termination

eg. with unbounded integers

• {true} while (true) {} {1=2}: holds under partial correctness
• {x=y} ++x {x=y}: failure
• {false} x:=1 {x=2}: vacuously holds

we use one rule per construct.

defn. (skip axiom)

$$\frac{}{\{P\} \textrm{ skip } \{Q\}}$$

defn. (assignment axiom)

$$\frac{}{\{Q[e/x]\}\ x:=e\ \{Q\}}$$

Q[e/x] means: Q with every free occurrence of x replaced by the expression e.

side conditions that matter in real language:

• e must be side-effect free, or the state after the assignment is not described by Q[e/x] alone
• e must be well-defined. if e can divide by zero or dereference a null pointer, a real verifier emits an extra proof obligation for that

eg. we read assignment backwards. to guarantee Q after the assignment, require beforehand what Q says about x.

eg. the following forward rule is incorrect: {P} x:=e {P∧x=e}. take P as x=5 and command as x:=x+1. the post cond yields x=5 ∧ x=x+1, which is false.

there is a correct forward rule (sound, but introduces an existential quantifier):

$$\{P\}\ x:=e\ \{\exists x_0.P[x_0/x]\land x=e[x_0/x]\}$$

defn. (sequence rule)

$$\frac{\{P\}\ C_1\ \{R\}\ \ \ \{R\}\ C_2\ \{Q\}}{\{P\}\ C_1;C_2\ \{Q\}}$$

• R is intermediate assertion: what holds between two commands
• applied forward, rule asks us to find R; backwards, it does not: compute the precondition of C₂ from Q, then use that as the postcondition of C₁.
• breaks when Q is a loop, because there is not last statement

we may always strengthen the precondition and weaken the postcondition (conseq rule):

$$\frac{P\Rightarrow P'\ \ \ \{P'\}\ C\ \{Q'\}\ \ \ Q'\Rightarrow Q}{\{P\}\ C\ \{Q\}}$$

• here P is stronger than P' (describes fewer states);. false the strongest assertion of all; true is the weakest.
• the premises P⇒P' and Q⇒Q' are not programs but ordinary 1st order formulas
• why it is needed: given a precondition Q[e/x]. our spec says a different one P, we close the gap at the price of proving p⇒Q[e/x].

defn. (conditional rule)

$$\frac{\{P\land b\}\ C_1\ \{Q\}\ \ \ \{P\land \neg b\}\ C_2\ \{Q\}}{\{P\}\ \text{if } B \text{ then } C_1 \text{ else } C_2\ \{Q\}}$$

• each branch is verified separately, under extra assumption that it guard holds.
• both branches must establish the same Q. if different, weaken to their disjunction using rule of consequence.
• guard b is assumed side-effect free, so evaluating it does not change state.

eg. show $\vdash\{x\geq1\}\ \ \ y:=x+5;z:=y\cdot y\ \ \ \{z\geq36\}$.

1. assign on z:=y*y with Q={z≥36}:
   $\{y\cdot y\geq36\}\ \ \ z:=y\cdot y\ \ \ \{z\geq36\}$
2. assign on y:=x+5 with Q={y*y≥36}:
   $\{(x+5)\cdot (x+5)\geq36\}\ \ \ y:=x+5\ \ \ \{y\cdot y\geq36\}$
3. seq, taking R={y*y≥36}:
   $\{(x+5)\cdot (x+5)\geq36\}\ \ \ y:=x+5;z:=y\cdot y\ \ \ \{z\geq36\}$
4. conseq, which requires x≥1 ⇒ (x+5)*(x+5)≥36.
   $\{x\geq1\}\ \ \ y:=x+5;z:=y\cdot y\ \ \ \{z\geq36\}$

steps 1-3 are mechanical, step 4 is the only genuine obligation (and it is not related to program).

eg. show $\vdash \{\text{true}\}\ \ \ \text{if}\ (a<b)\ r:=a\ \text{else}\ r:=b\ \ \ \{Q\}$, where $Q\equiv r\leq a\land r\leq b\land (r=a\lor r=b)$.

• if branch:
  $\{\text{true}\land a<b\}\ \ \ r:=a\ \ \ \{Q\}$
  $Q[a/r]\equiv a\leq a\land a\leq b\land(a=a\lor a=b)\equiv a\leq b$
  leaving $a<b\Rightarrow a\leq b$
• else branch: $\{\text{true}\land \neg(a<b)\}\ \ \ r:=b\ \ \ \{Q\}$
  $Q[b/r]\equiv b\leq a\land b\leq b\land(b=a\lor b=b)\equiv b\leq a$
  leaving $\neg(a<b)\Rightarrow b\leq a$

observation:

• which rule to apply is determined by syntax of program
• assertions at each point are determined by substitution
• only implications require any thought

plan:

1. compute the weakest assertion that must hold before C to guarantee Q (weakest precondition)
2. emit the one implication remaining (verification condition)
3. hand that implication to an automatic prover

defn. wp(C, Q) is the weakest assertion P such that {P} C {Q} holds, meaning:

1. {wp(C, Q) C {Q} holds and,
2. for every P', with {P'} C {Q}, we have P' ⇒ wp(C, Q).

if our actual precondition P does not imply wp, non proof {P} C {Q} exists. there single check P ⇒ wp(C, Q) is therefore sound and complete.

note. under partial correctness, this is strictly the weakest liberal precondition (wlp), which does not require termination. for loop-free programs, wp=wlp.

eg. Q={z≥36}, C={y=x+5; z=y*y}, find wp(C, Q).

  // {(x + 5) * (x + 5) >= 36} <-- wp(C, Q)
y = x + 5;
  // {y * y >= 36} <-- wp(z := y*y, Q)
z = y * y;
  // {z >= 36} <-- Q

start from bottom with Q, and push it upwards one statement at a time. we end up at the top is a formula over program's input only.

caveat: by substitution, we may have duplicate large expressions. real tools avoid blow-up with SSA form and shared term representations.

defn. given spec (P, Q) and loop-free program C, the verification condition is a single formula: VC(P, C, Q) ≡ P ⇒ wp(C, Q).

• soundness: if VC(P,C,Q) holds, then {P} C {Q} holds.
• completeness (loop-free): if {P} C {Q} holds, then VC(P,C,Q) holds.

for our example, it is x≥1 ⇒ (x+5)*(x+5)≥36.

verification condition generation:

1. given program C, spec P, Q
2. use VC generator to create wp, SSA (knows the programming language)
3. get the verification condition formula
4. use automatic prover (only knows logic)

the verification condition is the interface separating compilation and search.

eg. given $Q\equiv r\leq a\land r\leq b\land(r=a\lor r=b)$, then

$$\begin{align*} &\mathrm{wp}(\text{if }a<b\text{ then }r:=a\text{ else }r:=b, Q)\\ ={}&(a<b\Rightarrow Q[a/r]) \land (\neg(a<b)\Rightarrow Q[b/r])\\ ={}&(a<b\Rightarrow (a\leq a\land a\leq b\land(a=a\lor a=b))) \\ &\land (\neg(a<b)\Rightarrow (b\leq a\land b\leq b\land(b=a\lor b=b)))\\ \end{align*}$$

and VC ≡ true ⇒ formula above.

note if there are n conditionals, then there are 2^n paths to consider. VC has joined the implications so it grows linearly. case analysis is moved inside the solver.

defn. a formula is valid if it is true under every interpretation of its free variables. a formula is satisfiable if it is true under some interpretation.

• free variables are implicitly universally quantified (e.g. x≥1 ⇒ (x+5)*(x+5)≥36 means for all x)
• F is valid iff ¬F is unsatisfiable

given a VC, we ask whether ¬VC is satisfiable:

• if unsat, then no counterexample exists, and VC is valid (the program is correct)
• if sat, then program is incorrect with a counterexample

eg. if F = x≥1 ⇒ (x+5)²≥36, then ¬F = x≥1 ∧ (x+5)²<36. we feed this into solver.

SAT: given boolean formula F over variables x₁, x₂, ..., xₙ, find an assignment of true/false to those variables making F true, or prove that none exists

• works for booleans only
• convert input to conjunctive normal form
• SAT is np-complete, but there exist algos in practice: DPLL, CDCL.

satisfiability modulo theories (SMT): given a first-order formula F in which some function and predicate symbols carry a fixed interpretation prescribed by a background theory T, decide whether F is satisfiable in T.

• atoms are theory constraints; symbols of T (e.g. +, ≤) mean what T says they mean

common theories:

undecidable means no procedure works for all input, but there may be that works for some.

how solvers work:

• eager: bit-blasting
  • translate formula into propositional logic and call SAT solver. excellent for bit vectors (fixed length ints), hopeless for unbounded arithmetic.
• lazy: DPLL(T) - the standard architecture
  • abstract every theory atom (say x+y≤3) to a fresh boolean variable
  • let a CDCL SAT solver find an assignment to that bool abstraction
  • hand corresponding conjunction of theory literals to a theory solver
  • if theory-consistent, report sat. if not, the theory solver returns an explanation, which becomes a new clause, and the SAT solver carries on with that conflict ruled out
  • multiple theories are combined by exchanging equalities between vars they share (nelson-oppen)
  • quantifiers are handled by instantiation heuristics - E-matching, model-based quantifier instantiation (incomplete, may time out)

using Z3:

from z3 import *

x = Int('x')
pre  = x >= 1
post = (x + 5) * (x + 5) >= 36    # this is wp(C, z >= 36)
s = Solver()
s.add(pre, Not(post))  # assert negation of VC
s.check()  # unsat => correct
# or prove(Implies(pre, post)) 

# using SSA
x, y, z = Ints('x y z')
s = Solver()
s.add(x >= 1)
s.add(y == x + 5)
s.add(z == y * y)
s.add(Not(z >= 36))
s.check()  # unsat => correct

# incorrect
s.add(z==y+y)
s.check()  # sat => incorrect
s.model()  # [y = 6, x = 1, z = 12]

# min function
a, b, r = Ints('a b r')
s = Solver()
s.add(r == If(a < b, a, b))  # program
s.add(Not(And(r <= a, r <= b, Or(r == a, r == b))))  # negated postcond
s.check()  # unsat  =>  correct

Week 3. Sep 24

suppose we have a while loop while b do C, we can unwrap it once:

$$\begin{align*} \text{while }b \text{ do } C &= \text{if } b \text{ then } (C; \text{while } b \text{ do } C) \text{ else skip}\\ \mathrm{wp}(\text{while } b \text{ do } C, Q) &= (\neg b\land Q)\lor (\ b \land \mathrm{wp}(C, \mathrm{wp}(\text{while } b \text{ do } C, Q))) \end{align*}$$

the math solution is its fixed point. we can also unwrap it k times: this is bounded model checking (bug-finding technique, not a proof). idea is to find an assertion every step.

defn. a loop invariant is an assertion I attached to the top to the loop.

• I holds every time control reaches the loop head: before 1st iteration, between iterations, and the final test that exits the loop: {I} while b do C {I ∧ ¬b}
• after the loop, I still holds, and guard has become false

defn. (while rule)

$$\frac{\{I\land b\}\ \ \ C\ \ \ \{I\}}{\{I\}\ \ \ \text{while }b\text{ do }C\ \ \ \{I\land\lnot b\}}$$

I is not part of program. proof writer has to find it.

proof obligations:

eg. summing 0 to n-1

// pre: n >= 0
i = 0;
s = 0;
// inv: 0 <= i <= n
//   && 2 * s == i * (i - 1)
while (i < n) {
    s = s + i;
    i = i + 1;
}
// post: 2 * s == n * (n - 1)

i <= n so that the loop exit is covered.

from z3 import *
i, s, n, i2, s2 = Ints('i s n i2 s2')
 
def Inv(i, s): return And(0 <= i, i <= n, 2*s == i*(i-1))

# establishment: n≥0 ⇒ I(i=0,s=0)
prove(Implies(n >= 0, Inv(0, 0)))
# preservation: I(i,s) ∧ i<n ⇒ I(i+1,s+i)
prove(Implies(And(Inv(i, s), i < n,
                  s2 == s + i, i2 == i + 1), Inv(i2, s2)))
# exit: I(i,s) ∧ ¬(i<n) ⇒ 2*s == n*(n-1)
prove(Implies(And(Inv(i, s), Not(i < n)), 2*s == n*(n-1)))

eg. finding maximal element in array

// pre:  n >= 1
m = A[0];
i = 1;
// inv:  1 <= i <= n
//    && (∀ k. 0 <= k < i ==> A[k] <= m)
//    && (∃ k. 0 <= k < i && A[k] == m)
while (i < n) {
    if (A[i] > m)  m = A[i];
    i = i + 1;
}
// post: (∀ k. 0 <= k < n ==> A[k] <= m)
//    && (∃ k. 0 <= k < n && A[k] == m)

eg. invariant patterns

• pattern: replace final value of loop counter by current value, add add counter's bounds
• on exit ¬(i<n) gives i≥n, plus I we get i=n - which collapses the invariant to the postcondition.

invariant vs. inductive variant

• invariant: I is true at loop head on every actual execution starting from a state satisfying P.
• inductive variant: {I ∧ b ⇒ wp(C, I)} is valid on its own: from any sate satisfying I ∧ b, executing C will result in a state satisfying I.
• inductive + established gives invariant. converse not true.
• a checker can only verify the inductive version. I has to be true for reasons local to one iteration.

defn. a counterexample to induction (CTI) is a state satisfying I ∧ b but its successor violates I.

• it is either a real bug, or a hole in the invariant

eg. true but not inductive

// pre: True
x = 0;
// inv: x <= 10
while (x < 10) {
    x = x + 2;
}
// post: x == 10

the invariant is true, but setting x=9 yields false (we have x≤10 ∧ x<10 !⇒ x+2≤10), although x=9 never happens. strengthening it to x≤10 ∧ x%2=0 can go through.

the strengthen loop algo:

• guess a candidate I.
• check three obligations.
• if preservation fails, solver hands back a CTI. decide wether it is reachable. if not, add a conjunct excluding it and repeat.
• there is no guarantee of termination - one can strengthen forever; some loops have no invariant expressible in the assertion language. in practice few rounds suffice.
• weakening may be needed, as strongest invariant may not be proved inductive by solver.

eg. which are inductive invariants?

// pre:  true
x = 0;
y = 0;
while (x < 10) {
    x = x + 1;
    y = y + 2;
}
// post: y == 20

check establish, preserve, and postcond

• x≤10 - inductive, but week: final run x≥10 ∧ x≤10 says nothing about y
• y=2x - inductive, but weak: nothing pins x to 10 on exit
• x≤9 - not an invariant: x=10 at the final test
• y=2x ∧ x≤10 - inductive and strong enough. ← answer
• y=20 - not established: y=0 on entry. too strong
• x=10 ⇒ y=20 - true at every visit, but not inductive. CTI: x=9, y=17

when a check fails: three diagnoses

only when a preservation check fails with a reachable CTI can it indicate a bug in the program.

eg. nested loops: each loop needs its own invariant.

// inv_outer: A[0..i) is sorted && 0<=i<=n
while (i < n) {
    j = i;
    // inv_inner: ... && 0<=j<=i
    while (j > 0 && A[j-1] > A[j]) {
        swap(A, j-1, j);
        j = j - 1;
    }
    i = i + 1;
}

• inner loop is just a statement inside the outer body, so preservation of the outer invariant is proved using the inner loop's rule
• the two must fit together: outer invariant must be strong enough to establish the inner one every pass, inner one must be strong enough to re-establish the outer one on exit

finding invariant automatically:

• abstract interpretation: computes invariants in a fixed abstract domain (intervals, octagons, polyhedra). sound and fast, limited to what the domain expresses
• Houdini: starts from a large conjunction of candidate facts, deletes ones that fail preservation until what remains is inductive
• IC3/PDR: builds inductive invariant incrementally out of counterexamples
• CEGIS: searches a grammar of candidates guided by counterexamples (lec 5)
• LLMs: propose candidates, checker filters them (lec 10)
• all strengthen/weaken loop, with different guessers plugged in - the checker never changes

eg. a partially correct program

// pre:  n >= 0
i = 0;
// inv:  0 <= i
while (i != n) {
    i = i + 2;
}
// post: i == n

• establishment: 0≤0=i
• preservation: 0≤i ⇒ 0≤i+2
• exit: ¬(i≠n) ⇒ i=n when it terminates, it is correct. however for odd n the program does not stop.

defn. a ranking function (variant) for a loop is an integer expression V over the program such that

• I ∧ b ⇒ V≥0 (it is bounded below) and
• {I ∧ b ∧ V=v₀} C {V<v₀} (every iteration decreases it) where v₀ is value of V at start of iteration

together they force termination. ℕ is common choice but anything without infinite descending chains works (e.g. tuples, structural orders).

defn. (while-total rule)

$$\frac{I\land b\Rightarrow V\geq0\ \ \ [I\land b\land V=v_0]\ \ \ C\ \ \ [I\land V<v_0]}{[I]\ \ \ \text{while }b\text{ do }C\ \ \ [I\land\lnot b]}$$

called invariant and decreases clauses in Dafny and Verus.

eg. ranking functions

eg. lexicographic ranking function

// pre: x >= 0, y >= 0, N >= 0
while (x > 0) {
    if (y > 0) {
        y = y - 1;
    } else {
        x = x - 1;
        y = N;
    }
}

• take pair (x,y) ∈ ℕ×ℕ ordered lexicographically
• written decreases x, y in Dafny/Verus. also the natural measure for nested loops and recursive functions

termination in practice:

• termination is undecidable - no method is complete
• ranking functions are sound, and for restricted shapes (linear expressions over program vars) can be searched automatically
• tools: Terminator, AProVE, size-change termination, Dafny/Verus built-in heuristics
• most real loops are counting loops and the measure is inferred - write one only when the tool can't

the complete picture:

program C   ─┐
spec P,Q    ─┼─► VC generator ─► verif. conditions ─► SMT solver ─► verified/counterexample/unknown
inv+ranking ─┘

what can go wrong:

• spec - wrong/too weak/too strong, and verification won't tell. mitigate: write specs first, sanity-test them, prove they imply what you actually care about
• model - int assumed unbounded, but real machines wrap (32-bit). overflow, aliasing, floats, UB need explicit modelling
• solver - unknown/timeouts are routine; performance can shift sharply on small changes
• trusted computing base - "verified" trusts the VC generator, solver, and language semantics. solvers can have bugs; proof-producing/checked certificates help, at a perf cost

Week 4. Oct 1

verus is SMT-based verifier based on Z3 solver as backend.

why rust? ownership simplifies proof:

fn set_both(p: &mut u32, q: &mut u32)
  ensures
    *final(p) == 1,
    *final(q) == 2,
{
  // p and q must be different
  *p = 1;
  *q = 2;
}

vstd::prelude::*;

verus! {
fn min(a: u64, b: u64) -> (r: u64)
  ensures
    r <= a && r <= b,
    r == a || r == b
{
  if a < b { a } else { b }
}
} // verus!

two paths for program:

      ┍ erase ghost code ──► rustc ──► exec
      │ (spec, pf, ...)
code ━┥
      │ mode check ──► verification cond. ──► Z3
      ┕ VIR->AIR          SMT-LIB             sat?

ghost code may use math types: int, nat (unbounded), Seq, Set, Map. they have no machine repr and exist only for verification.

specs:

spec is mathematical:

fn avg(a: u32, b: u32) -> (r: u32)
  ensures r == (a + b) / 2,
{
  // a / 2 + b / 2 + (a % 2 + b % 2) / 2
  (a + b) / 2
}
// error: may overflow

caller sees only the contract:

fn min(a: u64, b: u64) -> (r: u64)
  ensures r <= a && r <= b,
{
  if a < b { a } else { b }
}

fn caller() {
  let m = min(3, 7);
  assert(m <= 3); // verified
  assert(m == 3); // fails (need to add another ensures)
}

spec functions:

spec fn is_even(x: int) -> bool {
  x % 2 == 0
}

// 1 + 2 + ... + n
spec fn triangle(n: nat) -> nat
  decreases n,
{
  if n == 0 { 0 }
  else { n + triangle((n - 1) as nat) }
}

mutable states:

struct Counter { count: u64, limit: u64 }
impl Counter {
  spec fn wf(&self) -> bool {
    self.count <= self.limit
  }

  fn inc(&mut self)
    requires
      old(self).wf(),
      old(self).count < old(self).limit,
    ensures
      final(self).wf(),
      final(self).count == old(self).count + 1,
      final(self).limit == old(self).limit,
  {
    self.count = self.count + 1;
  }
}

• wf (well-formed): invariant on data; every method may assume it and must reestablish it
• old(self): when method is called
• final(self): when method returns. also written as self.

loop:

fn ten() -> (x: u32)
  ensures x == 10,
{
  let mut x: u32 = 0;
  while x < 10
    invariant
      x <= 10,
      x % 2 == 0,
    decreases 10 - x,
  {
    x = x + 2;
  }
  x
}

queries:

; function with loop cut
assume x == 0            ; P ⇒ I 
assert x <= 10           ; before loop
assert x % 2 == 0
havoc x                  ; forget x ...
assume x <= 10           ; ... keep I
assume x % 2 == 0
assume !(x < 10)         ; loop has exited
assert x == 10           ; postcondition

; one iteration of loop body
assume x <= 10           ; I holds
assume x % 2 == 0
assume x < 10            ; guard holds
assert 0 <= x + 2 < 2^32 ; overflow check
x := x + 2
assert x <= 10           ; I preserved
assert x % 2 == 0
assert decreased(10 - x) ; termination

inside loop body, verifier knows only the invariant and loop condition:

fn f(n: u64)
  requires n > 5,
{
  let x: u64 = 7;
  let mut i: u64 = 0;
  while i < 3
    invariant i <= 3,
    decreases 3 - i,
  {
    // assert(n > 5); // fails
    // assert(x == 7); // fails
    i = i + 1;
  }
  assert(n > 5); // verified
  assert(i == 3); // verified
}

if body needs a fact, put in invariant.

Seq:

• immutable mathematical sequence. executable uses Vec
• v@: the Seq<T> that a Vec<T> represents
• for a Vec v, v[i] in a spec means v@[i]
• after assert(s1 =~= s2), verus knows s1 == s2

with quantifier:

fn max(v: &Vec<u64>) -> (m: u64)
  requires v.len() >= 1,
  ensures
    forall|k: int| 0 <= k < v.len() ==> v[k] <= m,
    exists|k: int| 0 <= k < v.len() && v[k] == m,
{
  let mut m = v[0];
  let mut i: usize = 1;
  while i < v.len()
    invariant
      1 <= i <= v.len(),
      forall|k: int| 0 <= k < i ==> v[k] <= m,
      exists|k: int| 0 <= k < i && v[k] == m,
    decreases v.len() - i,
  {
    if v[i] > m { m = v[i]; }
    i = i + 1;
  }
  m
}

why quantifiers are hard:

• hard case: need to find a term from many possibilities
• Z3 uses heuristic E matching, Verus needs triggers

proof fn some_zero(s: Seq<int>)
  requires
    s.len() > 0,
    forall|i: int| 0 <= i < s.len() ==> s[i] == 0,
  ensures
    exists|k: int| 0 <= k < s.len() && s[k] == 0,
{
  // will not verify unless this is added
  assert(s[0] == 0);
}

• a trigger is a term that mentions every quantified variable: s[i]
• triggers are func applications or indexing. arithmetic ops do not trigger
• 0≤0<|s| ⇒ s[0]=0 is instantiated, other are not

proof fn third_even(s: Seq<int>)
 requires
    s.len() == 10,
    forall|i: int| 0 <= i < s.len()
      ==> #[trigger] is_even(s[i]),
{
  assert(is_even(s[3])); // not verifying unless added
  assert(s[3] % 2 == 0);
}

verus can choose triggers automatically:

==> is_even(#[trigger] s[i])

requires
  s.len() == 10,
  forall|i: int| 0 <= i < s.len() - 1
    ==> #[trigger] s[i] <= s[i + 1],

with this trigger, to show s[0] <= s[3], term s[0] gives an instance for i = 0, s[1] gives an instance for i = 1, and so on.

forall |x: int| #[trigger] f(x) < f(x + 1)

in principle it does not stop. Z3 cuts chains off with heuristics, so one can get failure, timeout, or pf that breaks after unrelated edit.

trigger rules:

• if quantified fact 'should' apply but does not, mention term it needs (e.g. assert(s[0] == 0))
• for an exist goal, assert the witness explicitly
• inspect Verus's chosen triggers (--log triggers) when quantifiers behave unexpectedly
• prefer triggers appearing naturally in goals
• avoid ones that create further matching terms
• put properties in named spec functions (e.g. is_sorted(s)) to control when they expand
• quantifier-related proof failures are often trigger issues, not false statements

lemmas:

proof fn lemma_triangle_mono(i: nat, j: nat)
  requires
    i <= j,
  ensures
    triangle(i) <= triangle(j),
  decreases j,
{
  if i < j {
    lemma_triangle_mono(i, (j - 1) as nat);
  }
}

• want to show: for all i <= j, triangle(i) <= triangle(j)
• base case: i == j, nothing to do
• step i < j: the recursive call gives triangle(i) <= triangle(j - 1). one unfolding of triangle(j) adds j >= 0.

induction as recursion:

Calling a lemma on a smaller input assumes it holds for smaller inputs; decreases rules out circular reasoning.

lemma with sequences:

spec fn sum(s: Seq<u32>) -> int
  decreases s.len(),
{
  if s.len() == 0 { 0 }
  else { sum(s.drop_last()) + s.last() }
}

proof fn lemma_sum_bound(s: Seq<u32>)
  requires
    forall|k: int| 0 <= k < s.len() ==> s[k] <= 1000,
  ensures
    sum(s) <= 1000 * s.len(),
  decreases s.len(),
{
  if s.len() > 0 {
    lemma_sum_bound(s.drop_last());
  }
}

fn total(v: &Vec<u32>) -> (t: u32)
  requires
    v.len() <= 1000,
    forall|k: int| 0 <= k < v.len() ==> v[k] <= 1000,
  ensures t == sum(v@),
{
  let mut t: u32 = 0;
  let mut i: usize = 0;
  while i < v.len()
    invariant
      i <= v.len() <= 1000,
      forall|k: int| 0 <= k < v.len() ==> v[k] <= 1000,
      t == sum(v@.subrange(0, i as int)),
      decreases v.len() - i,
  {
    proof {
      lemma_sum_bound(v@.subrange(0, i as int)); // (1)
      assert(v@.subrange(0, i + 1).drop_last()
        =~= v@.subrange(0, i as int)); // (2)
    }
    t = t + v[i];
    i = i + 1;
  }
  assert(v@.subrange(0, v.len() as int) =~= v@); // (3)
  t
}

1. gives t <= 1000 * i < 2^32. without: possible overflow
2. connects sum of first i+1 elems to sum of first i. without: invariant not satisfied at end of loop body
   • given sum is defined by taking off last item, summing what remains, then adding last item. so we want to show sum(new prefix) = sum(old prefix) + v@[i]
   • we show new prefix except v[i] is the old prefix.
   • loop already knows t == sum(old prefix)
   • after t = t + v[i], t == sum(new prefix) as desired
3. whole prefix is whole vector. without: postcond not satisfied

verus explicit escape hatches:

• assume(P): take P without proof
• admit(): give up on rest of proof
• #[verifier::external_body]: trust a func's body without checking

Week 5. Oct 8

so far: synthesize from examples (lec 1), verify against logical specs (lec 2-4). today: synthesize from logical specs.

• verification: given C, is ∀x. φ(C, x) valid? query on ¬φ(C, x)
• synthesis: find f such that ∀x. φ(f, x) is valid, i.e. ∃f. ∀x. φ(f, x), not just 'yes'
  • ∃ is over programs: an infinite space of syntax trees
  • ∃∀ alternation makes synthesis harder than verification

eg. max2: post r≥x ∧ r≥y ∧ (r=x ∨ r=y). many solutions: ite(x<=y, y, x), ite(y<=x, x, y); we need only one.

asking Z3 directly (f as uninterpreted function) fails:

f = Function('f', IntSort(), IntSort(), IntSort())
s.add(ForAll([x, y], And(f(x, y) >= x, f(x, y) >= y,
                         Or(f(x, y) == x, f(x, y) == y))))
s.check()  # unknown, timeout after 1 min

even on success, it gives a Z3 model, not a program in a language we chose.

we can restrict the syntax with a grammar:

E ::= x | y | 0 | 1 | E+E | E-E | ite(B, E, E)
B ::= E <= E | E = E | B and B | not B

size = number of rules used to build it. ite(x<=y, y, x) has size 6.

why restrict syntax?

• search space: fewer building blocks, fewer candidates
• target language: result must run somewhere (spreadsheet formula, machine instructions, invariant a verifier can read)
• user hints: no * in grammar says 'doable without multiplication'
• readable answers: without grammar, solver may return something correct but useless

syntax-guided synthesis (SyGuS):

• given
  • background theory T
  • spec φ(f, x) mentioning unknown function f
  • grammar G
• want to find an expression e in G such that ∀x. φ(e, x) is valid in T.
• two constraints on e: semantic (φ) and syntactic (G)

eg. max2 in SyGuS input format:

(set-logic LIA)

; unknown function with grammar
(synth-fun max2 ((x Int) (y Int)) Int
  ((E Int) (B Bool))
  ((E Int (x y 0 1 (+ E E) (- E E) (ite B E E)))
   (B Bool ((<= E E) (= E E) (and B B) (not B)))))

; inputs, implicitly ∀
(declare-var x Int)
(declare-var y Int)
; spec
(constraint (>= (max2 x y) x))
(constraint (>= (max2 x y) y))
(constraint (or (= (max2 x y) x) (= (max2 x y) y)))
(check-synth)
; (define-fun max2 ((x Int) (y Int)) Int (ite (<= x y) y x))

one format, many problems:

eg. BV average:

(set-logic BV)
; true average: add with one extra bit (33 bits), so nothing overflows
(define-fun spec ((a (_ BitVec 32)) (b (_ BitVec 32))) (_ BitVec 32)
  ((_ extract 31 0) (bvlshr (bvadd ((_ zero_extend 1) a) ((_ zero_extend 1) b))
                            (_ bv1 33))))
(synth-fun avg ((a (_ BitVec 32)) (b (_ BitVec 32))) (_ BitVec 32)
  ((E (_ BitVec 32)))
  ((E (_ BitVec 32) (a b (_ bv1 32)
                     (bvand E E) (bvor E E) (bvxor E E)
                     (bvadd E E) (bvsub E E) (bvlshr E E)))))
(declare-var a (_ BitVec 32))
(declare-var b (_ BitVec 32))
(constraint (= (avg a b) (spec a b)))
(check-synth)
; cvc5 (17s): (bvadd (bvand a b) (bvlshr (bvxor a b) #b0...01))

• (_ bv1 33): 33-bit constant 1
• (_ extract 31 0): bits 31 through 0 (lower 32 bits)

eg. FlashFill: constraints are just the examples.

(set-logic SLIA)
(synth-fun f ((s String)) String
  ((S String) (I Int))
  ((S String (s "-" (str.++ S S) (str.substr s I I)))
   (I Int (0 1 3 (str.len s) (+ I I) (- I I) (str.indexof s "-" I)))))
(constraint (= (f "(425)-706-7709") "425-706-7709"))
(constraint (= (f "(510)-220-5586") "510-220-5586"))
(check-synth)
; (str.++ (str.substr s 1 3) (str.substr s (str.indexof s "-" 0) (str.len s)))

enumerative search: list expressions from smallest to largest, check each against spec, return first that passes.

• small programs tend to generalize (FlashFill also prefers simple programs)
• if a solution exists, the search reaches it

bottom-up enumeration:

bank[1] = [x, y, 0, 1]
for n = 2, 3, 4, ...:
  for each rule: # e.g. E ::= E + E
    for each way to split n-1 among children:
      combine expressions from bank
  bank[n] = everything built this round
  check each new E against spec

• size 3 from two size-1 pieces: x+y, y-1, ...
• nothing is parsed: every expr is a new node on top of existing children
• memory grows with # expressions kept

we can check against examples first:

• running an expr on one input takes µs, an SMT query takes ms or more
• keep a small set of input examples, compute what the specification requires on each, and test candidates on those first
• candidate that passes every example goes to verifier

eg. observational equivalence:

each column is an example input (x,y). first 4 rows agree on every example. they are the same expression. we can keep only smallest expression of each output signature.

where do examples come from?

• too few: first fit is wrong (overfitting, as in FlashFill)
• too many: every candidate costs more to test
• verifier knows which inputs matter: a counterexample is an input on which the candidate fails
• so let the verifier choose examples, one at a time

counterexample-guided inductive synthesis (CEGIS):

• learner: find e in G correct on all examples so far (PBE, lec 1)
• verifier: is e correct on every input? one SMT query (lec 2)
• if yes, verified, return e
• else counterexample is added to examples, learner tries again
• neither has to handle ∃∀

eg. verifier is a standard verification query:

def spec(r):
    return And(r >= x, r >= y, Or(r == x, r == y))

def verify(r):  # r: candidate as Z3 term
    s = Solver()
    s.add(Not(spec(r)))  # does some input break it?
    if s.check() == unsat:
        return None      # verified
    return s.model()     # counterexample

verify(x + (y + 1))      # [y = 0, x = 0]
verify(If(x <= y, y, x)) # None

eg. CEGIS on max2

does CEGIS terminate?

• yes, if a solution exists and learner returns the smallest expr consistent with examples:
  • true solution fits every example, so learner never goes past its size
  • each counterexample rules out the current candidate for good
  • finitely many expressions up to that size
• if grammar contains no solution, enumerative learner runs forever (grammar is infinite). real solvers bound size or time
• verifier must always answer: it does for LIA and BV

however, search space grows exponentially. while smallest solution to max2 is size 6, smallest solution to max3 is size 16.

sketching: a program with hols (??). the synthesizer fills the hols so program meets spec.

eg. avg(a, b) = (a ?? b) + ((a ?? b) >> ??): first two holes are &, |, ^, +, third is a shift amount.

• encode each hole as an SMT var: op1, op2 ∈ {0,1,2,3} choose operator, k is shift
• learner: find holes such that sketch agrees with spec on every example so far. finitely many examples => one big conjunction, no ∀, ordinary sat query
• verifier: find input where filled-in sketch disagrees with spec
• CEGIS splits ∃holes. ∀inputs into two quantifier-free problems and alternates between them

a, b = BitVecs('a b', 32)
op1, op2 = Ints('op1 op2')  # holes: which operator
k = BitVec('k', 32)         # hole: shift amount

def OP(h, x, y):  # 0: &  1: |  2: ^  3: +
    return If(h == 0, x & y, If(h == 1, x | y, If(h == 2, x ^ y, x + y)))

def sketch(x, y):
    return OP(op1, x, y) + LShR(OP(op2, x, y), k)

def spec(x, y):   # true average, one extra bit
    return Extract(31, 0, LShR(ZeroExt(1, x) + ZeroExt(1, y), 1))

examples = []
while True:
    learner = Solver()
    # find holes that fit examples
    learner.add(0 <= op1, op1 <= 3, 0 <= op2, op2 <= 3)
    for (x, y) in examples:
        learner.add(sketch(x, y) == spec(x, y))
    if learner.check() == unsat:
        break  # no completion of the sketch works
    h = learner.model()
    holes = [(v, h.eval(v, True)) for v in (op1, op2, k)]
    candidate = substitute(sketch(a, b), *holes)  # a, b stay free

    # look for a counterexample
    verifier = Solver()
    verifier.add(candidate != spec(a, b))
    if verifier.check() == unsat:
        break  # verified
    m = verifier.model()
    examples.append((m.eval(a, True), m.eval(b, True)))

# (a & b) + ((a & b) >> 0)   counterexample: a, b = (1840699758, 613567268)
# verified: (a & b) + ((a ^ b) >> 1)

two kinds of learner:

eg. invariant synthesis as a SyGuS problem:

(set-logic LIA)
; x = 0; y = 0; while (x < 10) { x = x + 1; y = y + 2; }   post: y == 20
(synth-fun inv ((x Int) (y Int)) Bool)
(declare-var x Int)
(declare-var y Int)
(declare-var x1 Int)  ; x, y after one iteration
(declare-var y1 Int)
; establishment
(constraint (=> (and (= x 0) (= y 0)) (inv x y)))
; preservation
(constraint (=> (and (inv x y) (< x 10) (= x1 (+ x 1)) (= y1 (+ y 2)))
                (inv x1 y1)))
; exit
(constraint (=> (and (inv x y) (>= x 10)) (= y 20)))
(check-synth)

without a grammar, cvc5 returns the disjunction of all 11 reachable states (x=0 ∧ y=0) ∨ (x=1 ∧ y=2) ∨ ... ∨ (x=10 ∧ y=20): correct but useless. we can add grammar:

; x = 0; y = 0 while (x < 10) { x = x + 1; y = y + 2; }
(synth-fun inv ((x Int) (y Int)) Bool
  ((B Bool) (E Int))
  ((B Bool ((<= E E) (= E E) (and B B)))
   (E Int ((+ E E) x y 0 1 2 10)))
)
; (and (<= x 10) (= y (+ x x)))

; x = 0; while (x < 10) { x += 2; }
(synth-fun inv ((x Int)) Bool
  ((B Bool) (E Int))
  ((B Bool ((<= E E) (= E E) (and B B)))
   (E Int ((+ E E) (mod E 2) x 0 1 2 10)))
)
; (and (<= x 10) (= y (+ x x)))

Week 6. Oct 15

houdini: to make I, it needs a finite list built from templates, filled in with variables and constants in the program:

start big, then delete:

1. let I be conjunction of all candidate facts (far too strong)
2. establishment: delete every fact that is false in the initial
3. perservation: ask Z3 for CTI: a state s that satisfies I and loop guard, but successor s' fails I
4. if there is, delete every fact that is false at s', and go back to step 3
5. else I is inductive. check exit: if it holds, I proves the postcond

facts are only deleted never added.

why deleting is safe:

• establishment: fact that is false in initial state and false in a reachable state. no invariant can contain it
• preservation: let s⇒s' be a CTI, and let f be a fact that is false at s'
  • take any inductive J made of remaining facts. s satisfies all remaining facts, so satisfies J
  • if J contained f, one iteration from s would leave J. J would not be inductive
  • so no inductive conjunction of remaining facts contains f. deleting it loses nothing
• consequence: largest inductive conjunction of the candidates is returned. if that fails the exit check, no conjunction of the candidates works.

correct: but larger than neeed: x≥0 ∧ y≥0 ∧ y≤20 add nothing.

if we had removed 'x even constraint':

x = 0;
while (x < 10) x = x + 2;
// post: x == 10

then CTX x=9⇒11 deletes x≤10, and x≥0 alone cannot show x=10.

if the true invariant requires a ∨ b and the list does not contain it, houdini also fails.

three kinds of counterexample:

the third kind does not tell whether s is reachable.

why not just pick a label? take implication (0,-2) ⇒ (1,0); neither is reachable.

• label (1,0) positive: I must contain (1,0), (2,2), ..., (10,18). but (10,18) exits with x≠10 - no invariant fits, learner fails
• label (0,-2) negative: harmless here, but if s were reachable, learner would have to exclude a reachable state - again no invariant fits
• so keep the implication and let the learner decide exclude s, or include s'

ICE learning:

• learner: finds I consistent with all data so far
• verifier: check three obligations
• consistent means: every positive state is in I; no negative state is in I; and for every implication s ⇒ s′, if s ∈ I then s′ ∈ I.

                              candidate I
┌───────────────────────────┐             ┌──────────────────────┐
│          learner          │ ==========> │       verifier       │
│ find I that is consistent │             │ check establishment, │
│ with all the data so far  │ <========== │  preservation, exit  │
└───────────────────────────┘             └──────────────────────┘
                   positive / negative / implication

what learner must satisfy:

picking candidate:

def learn(pos, neg, imp):
    for size in range(0, len(FACTS) + 1):
        for conj in combinations(FACTS, size):
            if all(holds(conj, p) for p in pos) and \
              not any(holds(conj, n) for n in neg) and \
              all(not holds(conj, s) or holds(conj, t) for s, t in imp):
          return conj
    return None # no conjunction fits

• searches over grammar I ::= fact | I ∧ I
• holds evaluates facts on concrete states: plain python, no solver
• leaner is free to enumerate arithmetic exprs from a grammar, or fix a template with unknown constants ax+by≤c, and let SMT solver find a, b, c that fit data

comparison:

the complete picture:

spec + grammar/sketch ─► learner (search) ⇄ verifier (SMT) ─► program
                         enumeration        Z3 / cvc5
                         sketch holes       lec 2-4
                         ICE learning

to compute max3, an enumerator that goes from smallest first must get past 97b smaller expressions:

(define-fun max3 ((x Int) (y Int) (z Int)) Int
  (ite (<= z y) (ite (<= x y) y x) (ite (<= z x) x z)))

looking at answer, every branch returns x, y or z. all difficulty is in deciding which one to return. we can search two parts separately.

divide and conquer (terms and conditions):

• terms: enumerate small exprs without ite, until every example is solved by at least one of them. for max3: x, y, z
• conditions: enumerate small boolean exprs: x≤y, x≤z, y≤z, ...
• combine: build a decision tree. each condition splits the examples; each leaf returns a term correct on every example reaching it
• every piece is small, so every search is small
• (same as lec 1 FlashFill conditionals)

building the decision tree:

1. pick the condition that splits the examples most cleanly
2. split each side again, until one term is correct on every example in the leaf
3. read the tree back as nested ite

                    x≤z?
           yes /           \ no
            y≤z?            x≤y?
       yes /   \ no    yes /   \ no
    return z  return y  return y  return x
   (0,-1,1)   (0,1,0)   (0,1,-1)  (1,0,0)
   (0,0,1)                        (1,0,-1)
   (-1,0,1)

ite(x <= z, ite(y <= z, z, y), ite(x <= y, y, x))

bottom-up vs top-down:

• bottom-up: builds complete exprs from smaller complete ones. an expr can only be tested once finished
• top-down: starts at the root and fills one hole ?? at a time like sketch. a partial program (with holes) can already be checked against spec

eg. (deduction) we have examples [1,2,3] ⇒ [2,4,6], [5,0] ⇒ [10,0]. every program is one block applied to xs: xs, map(f, xs), filter(p, xs), reverse(xs), sort(xs). and f, p are small exprs over v, e.g. f ::= v | 0 | 1 | 2 | f + f | f * f.

reject a partial program early:

rejecting filter(??p, xs) rejects every p at once, without building or running any of them. bottom-up would build and test each filter(p, xs) separately.

split the problem:

• map(??f, xs) must map elem by elem: f(1)=2, f(2)=4, f(3)=6, f(5)=10, f(0)=0
• new smaller problem with its own examples, for f alone. enumerate f: v, 0, 1, 2 fail; v+v fits all five, so answer: map(v+v, xs)
• each block needs its own rules (map keeps length, filter keeps a sublist), written once per block

eg. (component-based synthesis), we want a small program to turn off the rightmost 1 bit of a 32-bit integer.

def slow(x):
    for i in range(32):
        if (x >> i) & 1:
            return x & ~(1 << i)
    return x

def fast(x): return x & (x - 1) # (Hacker's Delight)

a program is a list of lines:

t1 = ?? op ??
t2 = ?? op ??
...
return the last line

• each line applies one component, an op from a library: + - & | ^ >>
• each ?? is an input (x), the constant 1, or an earlier line
• holes: which op on each line, and which values it reads i.e. wiring components together
• a sketch where the programmer only says how many lines
• rightmost bit: t1 = x - 1; t2 = t1 & x; from 24*54 programs
• avg: t1 = a & b; t2 = a ^ b; t3 = t2 >> 1; t4 = t3 + t1 from 168m programs

eg. (preferring likely programs) to write max2, smaller program is not always best:

• x + (y + 1) size 5 ⇐ no one will write
• ite(x <= y, y, x) size 6

real programs follow patterns: comparisons sit inside ite, constants are small, etc. ⇒ search programs in order of how likely they are.

• x + (y + 1) = 0.1*0.25*0.10*0.25*0.1 ≈ 0.00006
• ite(x <= y, y, x) = 0.15*0.6*0.25*0.25*0.25*0.25 ≈ 0.00035 ⇐ tried first
• probabilities come from counting rules in programs that solved earlier problems
• LLM gives prob for every next token, given task desc and everything before it

Week 7. Oct 23

automatic vs. interactive proving:

• automatic (Verus): solver searches for the proof. on failure we guess which hint is missing. Z3 can't do induction, and quantifiers need triggers
• interactive (Lean): write the proof one step at a time; after each step Lean shows the goals that remain and checks the step
• more effort, but predictable, and statements can use any math that can be defined

Lean 4: functional programming language + proof assistant. programs, specs and proofs in one language, checked by one small kernel.

def double (n : Nat) : Nat := n + n
#eval double 21  -- 42

a theorem = name + statement + proof:

theorem double_eq (n : Nat) : double n = 2 * n := by
  unfold double  -- replace double by its body
  omega          -- finish with arithmetic

Lean accepts it only if the proof establishes exactly this statement. no error = proved.

writing statements: a statement is itself a value, of type Prop.

hypotheses are arguments:

theorem le_chain (a b c : Nat) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by ...
-- same theorem
theorem le_chain : ∀ a b c : Nat, a ≤ b → b ≤ c → a ≤ c := by ...

• arguments before the colon are another way to write ∀ and →
• hypotheses ≈ Verus requires, statement after the colon ≈ ensures
• hypotheses are named because tactics refer to them by name

proof state:

a b c : Nat     ┐
h1 : a ≤ b      ├ context: variables and hypotheses available
h2 : b ≤ c      ┘
⊢ a ≤ c         ← goal: what remains to be proved

• a tactic changes the proof state: closes the goal, replaces it by simpler goals, or adds facts to the context
• proof is finished when no goals are left

eg. one tactic at a time

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by
  intro h                -- h : p ∧ q          ⊢ q ∧ p
  obtain ⟨hp, hq⟩ := h    -- hp : p, hq : q     ⊢ q ∧ p
  constructor            -- two goals: ⊢ q (case left), ⊢ p (case right)
  · exact hq
  · exact hp

· focuses on one goal at a time.

lemmas are functions:

#check Nat.le_trans
-- Nat.le_trans {n m k : Nat} : n ≤ m → m ≤ k → n ≤ k

theorem le_chain (a b c : Nat) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by
  apply Nat.le_trans h1  -- ⊢ b ≤ c
  exact h2
  -- or in one step: exact Nat.le_trans h1 h2

• from a proof of n≤m and a proof of m≤k, it produces a proof of n≤k
• apply supplies the first proof; the missing one becomes the new goal
• args in {} are implicit: inferred from the goal (n=a, m=b, k=c)

rw: replace equals by equals

theorem rw_demo (a b c : Nat) (h1 : a = b) (h2 : b = c) : a + 1 = c + 1 := by
  rw [h1]  -- ⊢ b + 1 = c + 1
  rw [h2]  -- ⊢ c + 1 = c + 1, closed by rfl

• rw [h] for h : x = y replaces every x in the goal by y, then tries rfl (closes any goal whose two sides are identical)
• rw [← h]: right to left. rw [h] at h3: rewrite hypothesis h3 instead of goal
• any proved equation works, including library lemmas: rw [Nat.add_comm]

sorry: closes a goal without proof (placeholder). Lean warns about every one, like Verus's admit().

automation for small steps:

• decision procedures like those inside SMT solvers, applied to a single goal
• typical proof: a few tactics to bring the goal into shape, finish with one of these

inductive types:

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

inductive List (α : Type) where
  | nil : List α                          -- []
  | cons (x : α) (xs : List α) : List α   -- x :: xs

every value is built from finitely many constructors ⇒ functions defined by recursion, properties proved by induction

recursive definition:

def triangle : Nat → Nat
  | 0 => 0
  | n + 1 => (n + 1) + triangle n

#eval triangle 4  -- 10

lean checks termination itself (triangle (n + 1) calls triangle n), no decreases needed

induction:

theorem triangle_formula (n : Nat) : 2 * triangle n = n * (n + 1) := by
  induction n with
  | zero => rfl            -- ⊢ 2 * triangle 0 = 0 * (0 + 1): both sides evaluate to 0
  | succ k ih =>           -- ih : 2 * triangle k = k * (k + 1)
                           -- ⊢ 2 * triangle (k + 1) = (k + 1) * (k + 1 + 1)
    rw [triangle]          -- ⊢ 2 * (k + 1 + triangle k) = (k + 1) * (k + 1 + 1)
    rw [Nat.mul_add, ih]   -- ⊢ 2 * (k + 1) + k * (k + 1) = (k + 1) * (k + 1 + 1)
    grind                  -- polynomial identity, no triangle left

• induction n gives one goal per constructor of Nat. in succ case, ih is the statement for k, goal is the statement for k+1
• Nat.mul_add distributes 2 * (...) so that 2 * triangle k appears, then ih replaces it
• Z3 cannot do induction on its own; in Lean it's a single tactic, and the remaining arithmetic is still automatic
• omega fails on the last goal: linear only, it treats each product as an unknown

a proof is a term:

#print and_swap
-- theorem and_swap : ∀ (p q : Prop), p ∧ q → q ∧ p :=
--   fun p q h => And.casesOn h fun hp hq => ⟨hq, hp⟩

• tactics build a proof term: a small program whose type is the statement. here: a function that takes p, q and a proof h of p∧q, splits h, and pairs the parts in the other order
• Lean's kernel (a small type checker) checks the term against the statement
• only the kernel and the statement need to be trusted. not the tactics, nor whoever wrote the proof (human or AI)

Mathlib: Lean's library of mathematics. much of the work is finding the right lemma: exact? searches the library (for le_chain it suggests exact Nat.le_trans h1 h2).

eg. Euclid: there are infinitely many primes

theorem infinitely_many_primes (n : ℕ) : ∃ p, n ≤ p ∧ p.Prime := by
  let p := Nat.minFac (n.factorial + 1)   -- smallest prime factor of n!+1
  have hp : p.Prime := Nat.minFac_prime
    (by have := Nat.factorial_pos n; omega)
  refine ⟨p, ?_, hp⟩                      -- witness p; goal left: n ≤ p
  by_contra h                             -- suppose p < n
  have h1 : p ∣ n.factorial :=            -- then p | n!
    Nat.dvd_factorial hp.pos (by omega)
  have h2 : p ∣ n.factorial + 1 := Nat.minFac_dvd _   -- and p | n!+1
  have h3 : p ∣ 1 := (Nat.dvd_add_right h1).mp h2     -- so p | 1
  exact hp.ne_one (Nat.dvd_one.mp h3)     -- but p is prime: contradiction

• each line of the paper proof becomes one or two tactics
• have: prove an intermediate fact and name it. by_contra: assume negation of goal, goal becomes False

with an AI model proposing proofs and Lean checking them, this is CEGIS's propose-and-check loop with a far larger generator. Lean still can't tell whether the formal statement matches the intended claim (same as spec vs. intent in software).

functional programs are already Lean definitions:

def sum : List Nat → Nat
  | [] => 0
  | x :: xs => x + sum xs

theorem sum_append (xs ys : List Nat) : sum (xs ++ ys) = sum xs + sum ys := by
  induction xs with
  | nil => simp [sum]
  | cons x xs ih =>
    simp [sum, ih]
    omega

real code has machine integers, mutation, loops, panics ⇒ translate it into Lean definitions, prove theorems about those.

Rust to Lean with Aeneas:

           Charon            Aeneas
Rust crate ──────► LLBC ──────────► Lean code ◄── proofs (developer)
 lib.rs        Rust's internal      Code.lean      Proofs.lean
               form, cleaned up

• each Rust function becomes a Lean function computing the same result, or the same panic
• specs are Lean theorems about those functions, proved with tactics as before

what the translation looks like:

pub fn avg_bad(a: u32, b: u32) -> u32 {
    (a + b) / 2
}

def avg_bad (a : Std.U32) (b : Std.U32) : Result Std.U32 := do
  let i ← a + b
  i / 2#u32

inductive Result (α : Type) where
  | ok (v : α)
  | fail (e : Error)   -- e.g. integerOverflow
  | div                -- does not terminate

theorem avg_bad_overflows :
    avg_bad 4294967295#u32 1#u32 = fail .integerOverflow := by
  rfl   -- concrete input: evaluate both sides

• U32 is Lean's model of u32: a number with 0 ≤ val < 2³². x.val is displayed as ↑x
• let i ← a + b stops the whole function if the addition fails (like ? in Rust)

a specification is a theorem:

-- pub fn avg(a: u32, b: u32) -> u32 { a / 2 + b / 2 + (a % 2 + b % 2) / 2 }
theorem avg_spec (a b : U32) :
    avg a b ⦃ r => r.val = (a.val + b.val) / 2 ⦄ := by
  unfold avg
  step*

• f x ⦃ r => P r ⦄: f x does not fail, and its result r satisfies P r (= ensures + absence of panics)
• a.val, b.val are Nat, so a.val + b.val cannot overflow
• step* walks the generated code one let at a time, proving each step automatically

#check @U32.add_spec
-- U32.add_spec : ∀ {x y : U32}, ↑x + ↑y ≤ U32.max → x + y ⦃ z => ↑z = ↑x + ↑y ⦄

• step applies the spec of the first let's operation; for addition, the requirement that the sum fits in 32 bits becomes a goal
• for avg_bad, step* leaves case hmax ⊢ ↑a + ↑b ≤ U32.max, which cannot be proved: the bug appears as an open goal

mutable references become return values:

pub fn swap(a: &mut u32, b: &mut u32) {
    let t = *a;
    *a = *b;
    *b = t;
}

def swap (a : Std.U32) (b : Std.U32) : Result (Std.U32 × Std.U32) := do
  ok (b, a)

theorem swap_spec (a b : U32) : swap a b = ok (b, a) := by
  rfl

• a &mut argument becomes an input, and its final value becomes an extra output
• sound because of ownership: while swap runs, no other code can touch *a or *b. in C any two pointers may alias, so C tools model memory explicitly instead

loops become recursive functions:

// 1 + 2 + ... + n
pub fn sum_to(n: u32) -> u32 {
    let mut s = 0;
    let mut i = 0;
    while i < n {
        i = i + 1;
        s = s + i;
    }
    s
}

def sum_to_loop (n s i : Std.U32) : Result Std.U32 := do
  if i < n
  then
    let i1 ← i + 1#u32
    let s1 ← s + i1
    sum_to_loop n s1 i1
  else ok s
partial_fixpoint

def sum_to (n : Std.U32) : Result Std.U32 :=
  sum_to_loop n 0#u32 0#u32

• variables the loop changes (s, i) become arguments. one iteration = one recursive call
• partial_fixpoint: Lean accepts the definition before anyone has shown the loop terminates

the loop lemma is the loop invariant:

theorem sum_to_loop_spec (n s i : U32)
    (hn : n.val ≤ 10000)             -- keeps s within 32 bits
    (hi : i.val ≤ n.val)             -- invariant
    (hs : s.val = triangle i.val) :  -- invariant
    sum_to_loop n s i ⦃ r => r.val = triangle n.val ⦄ := by   -- postcond
  unfold sum_to_loop
  split                              -- one goal per branch of the if
  · step*
    · -- no overflow in s + i1
      have h1 := triangle_formula i.val
      have h2 : i.val * (i.val + 1) ≤ 10000 * 10001 :=
        Nat.mul_le_mul (by omega) (by omega)
      scalar_tac
    · -- the invariant holds again
      rw [s1_post, hs, i1_post, triangle]
      omega
  · -- the loop exits: i = n
    have : i.val = n.val := by scalar_tac
    simp [hs, this]
termination_by n.val - i.val
decreasing_by scalar_decr_tac

• if the loop starts in a state where the invariant holds, it finishes without overflow and the result satisfies the postcond
• proved by induction on remaining iterations n−i: for the recursive call, step* applies the lemma being proved (= induction hypothesis)
• overflow bound uses triangle_formula: 2s = i(i+1) ≤ 10000*10001
• termination_by supplies the ranking function (≈ decreases)

goals left after step* are the familiar obligations (lec 3):

Verus vs. Lean on the same loop (both need spec, loop invariant, ranking function):