From 78d0ae6b83639363d6faa923bea57083ac97cd1b Mon Sep 17 00:00:00 2001 From: John Lu Date: Sat, 11 Jul 2026 11:30:40 -0400 Subject: [PATCH 1/3] Add SeaHorn proof Verifies an imperative C leftpad with SeaHorn. The harness checks all three properties for nondeterministic inputs. Co-Authored-By: Claude Fable 5 --- seahorn/leftpad.c | 75 +++++++++++++++++++++++++++++++++++++++++++++++ seahorn/readme.md | 72 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 147 insertions(+) create mode 100644 seahorn/leftpad.c create mode 100644 seahorn/readme.md diff --git a/seahorn/leftpad.c b/seahorn/leftpad.c new file mode 100644 index 0000000..95e15c0 --- /dev/null +++ b/seahorn/leftpad.c @@ -0,0 +1,75 @@ +/* Leftpad, proved with SeaHorn: https://seahorn.github.io/ + * + * Verify with: sea pf leftpad.c + * "unsat" means the verification conditions are unsatisfiable, + * i.e. no execution can violate an assertion: leftpad is correct. + */ +#include "seahorn/seahorn.h" +#include + +/* External functions with no definition are treated by SeaHorn as + * returning an arbitrary (nondeterministic) value. */ +extern int nd_int(void); +extern char nd_char(void); + +static int max(int a, int b) { return a > b ? a : b; } + +/* The code under verification. Pads string `s` of length `len` on the + * left with `c` up to length `n`, writing into `out`. Returns the + * number of characters written. */ +int leftpad(char c, int n, const char *s, int len, char *out) { + int pad = n - len; + if (pad < 0) + pad = 0; + for (int i = 0; i < pad; ++i) + out[i] = c; + for (int i = 0; i < len; ++i) + out[pad + i] = s[i]; + return pad + len; +} + +/* The verification harness. Every value is arbitrary, so proving the + * assertions here proves them for ALL inputs. */ +int main(void) { + char c = nd_char(); + int n = nd_int(); + int len = nd_int(); + assume(len >= 0); /* a string's length is non-negative */ + + int expected = max(n, len); + int pad = expected - len; + + /* Specs 2 and 3 are universally quantified over positions, so we + * check them at an arbitrary symbolic index j. Since j is arbitrary, + * proving the assertion proves it for every position at once. We + * pick j *before* the loops run, so that the loop invariants Spacer + * must infer only concern the single cell out[j] and stay + * quantifier-free. j is only constrained to be non-negative: the + * guards below decide whether it falls in the prefix, the suffix, + * or (when j >= expected) outside the output, where there is + * nothing to assert. Additionally assuming j < expected (i.e. + * assume(j >= 0 && j < expected)) would make the combined + * assumption unsatisfiable when expected == 0, silently pruning + * those inputs and leaving Spec 1 unverified for them. */ + int j = nd_int(); + assume(j >= 0); + + /* An arbitrary string: `len` nondeterministic characters. */ + char *s = malloc(len); + for (int i = 0; i < len; ++i) + s[i] = nd_char(); + char *out = malloc(expected); + + int outlen = leftpad(c, n, s, len, out); + + /* Spec 1: the length of the output is max(n, len). */ + sassert(outlen == expected); + if (j < pad) + /* Spec 2: the prefix is padding characters, and nothing else. */ + sassert(out[j] == c); + else if (j < expected) + /* Spec 3: the suffix is the original string. */ + sassert(out[j] == s[j - pad]); + + return 0; +} diff --git a/seahorn/readme.md b/seahorn/readme.md new file mode 100644 index 0000000..cd5d196 --- /dev/null +++ b/seahorn/readme.md @@ -0,0 +1,72 @@ +# [SeaHorn](https://seahorn.github.io/) + +## About SeaHorn + +SeaHorn is an automated verification framework for LLVM-based +languages. It takes a C program with assertions, compiles it to LLVM +bitcode, translates the bitcode into Constrained Horn Clauses (CHCs), +and hands those to the [Spacer](https://spacer.bitbucket.io/) solver +built into Z3. Spacer searches for an inductive invariant that proves +every assertion, or for a concrete execution that violates one. + +The proof here, `leftpad.c`, contains no loop invariants, lemmas, or +proof hints, only the implementation and the specification (as +assertions); the invariants needed to prove the loops correct are +inferred by the solver. The +[Dafny](../dafny/Leftpad.dfy) and [Frama-C](../frama-c/leftpad.c) +proofs verify similar imperative code but annotate their loops with +explicit invariants; the [smtlib](../smtlib/leftpad.smt) and +[z3py](../z3py/leftpad.py) proofs are equally automatic but prove a +declarative definition of leftpad rather than loop code. The trade-off +for the automation is less control: if the solver diverges, you cannot +supply the missing invariant annotation; you have to reshape the +problem instead. + +## About the proof + +The code under verification is an ordinary imperative `leftpad`: two +loops writing into an output buffer. The proof lives in `main`, a +verification harness in which every input (the pad character, the +target length, the string contents and its length) is nondeterministic, +so proving the assertions proves them for all inputs. There are no +upper bounds on the string length or the padding. + +The three properties of leftpad are checked as follows: + +1. The length of the output is `max(n, len(str))`: asserted directly + on the length returned by `leftpad`. + +2 & 3. The prefix is all padding and the suffix is the original + string. These properties are universally quantified over every + position of the output. Instead of a quantified assertion, the + harness picks a + single symbolic index `j`, constrained only to be non-negative, and + asserts the property at `out[j]` whenever `j` falls inside the + output. Since `j` is arbitrary, SeaHorn must prove the assertion + for every value of `j`, which is the universally quantified + property. This keeps the invariants Spacer needs quantifier-free. + +The only assumption on the inputs is `len >= 0`, which says the input +string has a non-negative length. + +One caveat: SeaHorn's default encoding models signed integer +arithmetic as exact mathematical arithmetic, so this proof does not +account for overflow of `n - len`. + +## Running it + +With [Docker](https://hub.docker.com/r/seahorn/seahorn-llvm14): + +``` +docker run -v $(pwd):/host -it seahorn/seahorn-llvm14:nightly \ + sea pf /host/leftpad.c +``` + +SeaHorn prints `unsat`, meaning the verification conditions are +unsatisfiable: no execution of `leftpad` can violate the specification. + +## About me + +I'm [John Lu](https://johnlyu2.github.io/), a PhD student at +UWaterloo. My research interests are at the intersection of formal +methods and machine learning. From 88891b939e434dd8dfb46f0fa61d0a3044110b1f Mon Sep 17 00:00:00 2001 From: John Lu Date: Sat, 11 Jul 2026 15:37:46 -0400 Subject: [PATCH 2/3] Use memhavoc for arbitary input string --- seahorn/leftpad.c | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/seahorn/leftpad.c b/seahorn/leftpad.c index 95e15c0..659f1b4 100644 --- a/seahorn/leftpad.c +++ b/seahorn/leftpad.c @@ -12,6 +12,10 @@ extern int nd_int(void); extern char nd_char(void); +/* SeaHorn built-in: marks `size` bytes at `ptr` as holding arbitrary + * values. */ +extern void memhavoc(void *ptr, size_t size); + static int max(int a, int b) { return a > b ? a : b; } /* The code under verification. Pads string `s` of length `len` on the @@ -56,8 +60,7 @@ int main(void) { /* An arbitrary string: `len` nondeterministic characters. */ char *s = malloc(len); - for (int i = 0; i < len; ++i) - s[i] = nd_char(); + memhavoc(s, len); char *out = malloc(expected); int outlen = leftpad(c, n, s, len, out); From 949a151d2c82058fdb5e2b5919cfeff35332beda Mon Sep 17 00:00:00 2001 From: John Lu Date: Sat, 11 Jul 2026 15:38:05 -0400 Subject: [PATCH 3/3] Add --rm to docker command in readme --- seahorn/readme.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/seahorn/readme.md b/seahorn/readme.md index cd5d196..78e8cd4 100644 --- a/seahorn/readme.md +++ b/seahorn/readme.md @@ -58,7 +58,7 @@ account for overflow of `n - len`. With [Docker](https://hub.docker.com/r/seahorn/seahorn-llvm14): ``` -docker run -v $(pwd):/host -it seahorn/seahorn-llvm14:nightly \ +docker run --rm -v $(pwd):/host -it seahorn/seahorn-llvm14:nightly \ sea pf /host/leftpad.c ```