Add SeaHorn proof

seahorn/leftpad.c

@@ -0,0 +1,78 @@
+/* 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 <stdlib.h>
+
+/* 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);
+
+/* 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
+ * 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);
+  memhavoc(s, len);
+  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;
+}

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 --rm -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.