VDD: Boundary-Only Spec to Verified Solution

This tutorial shows a VDD flow where a bodyless abstract spec is used as a temporary proof interface, and then refined into a concrete implementation that the verifier checks. We call the step of adding bodies refining. For the language rules behind this pattern, see pure functions and abstract functions.

1) Start with a declaration-only spec

We only write ensures clauses and leave the body out. The declaration is an assumption while it is abstract, so it belongs in the VDD scaffolding phase. The real proof happens when we refine it with a body.

Source: snippets/equation_system_body_sat_decl.mo

module {
  public pure abstract func conditionalBounds(x : Int) : Int
    ensures x == 5 ==> result > 10;
    ensures x == 8 ==> result < 5;
    ensures x == 12 ==> result > 14;
    ensures x == 14 ==> result < 5;
    ensures x == 16 ==> result > 18;
    ensures (x == 5 or x == 12 or x == 16) ==> result % 2 == 1;
    ensures (x == 8 or x == 14) ==> result % 2 == 0;
    ensures (x == 5 or x == 12 or x == 16) ==> result * result > x * x;
    ensures (x == 8 or x == 14) ==> result * result <= 16;
}

Check the declaration with --check or --viper. If it type-checks, callers can be written against the interface while the implementation is still open.

Here are the denied ranges at each x-value (the function must avoid these segments):

2) Refine into a concrete solution

One way to satisfy pointwise constraints is to build a Lagrange interpolation polynomial that hits specific values at x = 5, 8, 12, 14, 16. An AI (or a CAS) can propose the coefficients, and the verifier confirms the refinement.

Source: snippets/equation_system_body_sat.mo

module {
  public func conditionalBounds(x : Int) : Int
    ensures x == 5 ==> result > 10;
    ensures x == 8 ==> result < 5;
    ensures x == 12 ==> result > 14;
    ensures x == 14 ==> result < 5;
    ensures x == 16 ==> result > 18;
    ensures (x == 5 or x == 12 or x == 16) ==> result % 2 == 1;
    ensures (x == 8 or x == 14) ==> result % 2 == 0;
    ensures (x == 5 or x == 12 or x == 16) ==> result * result > x * x;
    ensures (x == 8 or x == 14) ==> result * result <= 16;
  {
    let term1 = 11 * (x - 8) * (x - 12) * (x - 14) * (x - 16) / 2079;
    let term2 = 15 * (x - 5) * (x - 8) * (x - 14) * (x - 16) / 224;
    let term3 = 19 * (x - 5) * (x - 8) * (x - 12) * (x - 14) / 704;
    term1 + term2 + term3
  };
}

Verify the implementation, then visualize it against the denied ranges. The important shift is that the contracts stop being only an assumed interface: the body is now responsible for every ensures clause.