Merge branch 'dafny-lang:main' into main

Makefile

@@ -13,11 +13,13 @@ check:
  assets/src/test-generation/verify.sh
  assets/src/insertion-sort/verify.sh
  assets/src/proof-dependencies/verify.sh
+ assets/src/brittleness/verify.sh
 
 generate:
  node builders/verification-compelling-verify.js --regenerate _includes/verification-compelling-intro.html
  python3 builders/madoko-gen.py insertion-sort --check
  python3 builders/madoko-gen.py proof-dependencies --check
+ python3 builders/madoko-gen.py brittleness --check
 
 watch-compelling:
  node builders/verification-compelling-verify.js --watch _includes/verification-compelling-intro.html

_posts/2023-12-01-avoiding-verification-brittleness.markdown

@@ -0,0 +1,8 @@
+---
+layout: post
+title: "Avoiding verification brittleness in Dafny"
+author: Aaron Tomb and Jean-Baptiste Tristan
+date: 2023-12-01 11:00:00 -0500
+---
+
+{% include brittleness.html %}

assets/src/brittleness/RationalAdd.dfy

@@ -0,0 +1,96 @@
+module Rat {
+
+ ghost predicate Rational(x: real) {
+ exists n: int, m: int :: m > 0 && x == (n as real) / (m as real)
+ }
+
+ type rat = x: real | Rational(x) witness (0 as real / 1 as real)
+
+}
+
+module M1 { import opened Rat
+
+ ghost function add(x: rat, y: rat): rat
+ requires Rational(x)
+ requires Rational(y)
+ ensures Rational(add(x,y)) // Comment -> postcondition not verified
+ ensures add(x, y) == x + y
+ {
+ var n1: int, m1: int :| m1 > 0 && x == (n1 as real) / (m1 as real);
+ var n2: int, m2: int :| m2 > 0 && y == (n2 as real) / (m2 as real);
+ //var r1 := x + y; // Uncomment -> postcondition not verified
+ var r: rat := ((n1 * m2 + n2 * m1) as real) / ((m1 * m2) as real);
+ assert Rational(r);
+ //assert r == x + y; // Uncomment -> much higher resource use
+ r
+ }
+}
+
+module M2 { import opened Rat
+
+ ghost function add2(x: rat, y: rat): rat
+ requires Rational(x)
+ requires Rational(y)
+ // ensures Rational(add2(x,y)) // Uncomment -> higher resource use with 3.13, failure with 4.3
+ ensures add2(x, y) == x + y
+ {
+ var x1: int, x2: int :| x2 > 0 && x == (x1 as real) / (x2 as real);
+ var y1: int, y2: int :| y2 > 0 && y == (y1 as real) / (y2 as real);
+ var r: real := x + y;
+ var final_d: int := x2 * y2;
+ // var r1 := x + y; // Uncomment -> higher resource use with 3.13, failure with 4.3
+ assert (x1 as real) / (x2 as real) == ((x1 * y2) as real) / ((x2 * y2) as real);
+ assert r == (((x1 * y2) + (y1 * x2)) as real) / (final_d as real);
+ // assert Rational(r); // Uncomment -> higher resource use with 3.13, failure with 4.3
+ // assert r == x + y; // Uncomment -> higher resource use with 3.13, failure with 4.3
+ r
+ }
+
+}
+
+module M3 { import opened Rat
+
+ lemma AddStep1(x1: int, x2: int, y1: int, y2: int)
+ requires x2 > 0
+ requires y2 > 0
+ ensures (x1 as real) / (x2 as real) == ((x1 * y2) as real) / ((x2 * y2) as real)
+ {}
+
+ lemma AddStep2(r: real, x:real, y: real, x1: int, x2: int, y1: int, y2: int)
+ requires x2 > 0
+ requires x == (x1 as real) / (x2 as real)
+ requires y2 > 0
+ requires y == (y1 as real) / (y2 as real)
+ requires r == x + y
+ ensures r == (((x1 * y2) + (y1 * x2)) as real) / ((x2 * y2) as real)
+ {}
+
+ lemma AddStep3(r: real, x:real, y: real, x1: int, x2: int, y1: int, y2: int)
+ requires x2 > 0
+ requires x == (x1 as real) / (x2 as real)
+ requires y2 > 0
+ requires y == (y1 as real) / (y2 as real)
+ requires r == x + y
+ requires (x1 as real) / (x2 as real) == ((x1 * y2) as real) / ((x2 * y2) as real)
+ requires r == (((x1 * y2) + (y1 * x2)) as real) / ((x2 * y2) as real)
+ ensures Rational(r)
+ {}
+
+ ghost function add3(x: rat, y: rat): rat
+ requires Rational(x)
+ requires Rational(y)
+ //ensures Rational(add3(x, y)) // Fine
+ ensures add3(x, y) == x + y
+ {
+ var x1: int, x2: int :| x2 > 0 && x == (x1 as real) / (x2 as real);
+ var y1: int, y2: int :| y2 > 0 && y == (y1 as real) / (y2 as real);
+ var r: real := x + y;
+ // var r1 := x + y; // Fine
+ AddStep1(x1,x2,y1,y2);
+ AddStep2(r,x,y,x1,x2,y1,y2);
+ AddStep3(r,x,y,x1,x2,y1,y2); // Higher resource use if left out, even without postcondition
+ // assert r == x + y; // Fine
+ r
+ }
+
+}

assets/src/brittleness/RationalAdd.dfy.expect

@@ -0,0 +1,17 @@
+ |
+4 | exists n: int, m: int :: m > 0 && x == (n as real) / (m as real)
+ | ^^^^^^
+
+RationalAdd.dfy(4,4): Warning: /!\ No terms found to trigger on.
+RationalAdd.dfy(13,17): Error: a postcondition could not be proved on this return path
+ |
+13 | ghost function add(x: rat, y: rat): rat
+ | ^^^
+
+RationalAdd.dfy(17,12): Related location: this is the postcondition that could not be proved
+ |
+17 | ensures add(x, y) == x + y
+ | ^^^^^^^^^^^^^^^^^^
+
+
+Dafny program verifier finished with 10 verified, 1 error

assets/src/brittleness/TriangleSum.dfy

@@ -0,0 +1,79 @@
+module A1 {
+
+ ghost function TriangleSum(n: nat): nat
+
+ lemma TriangleSumBase()
+ ensures TriangleSum(0) == 0
+
+ lemma TriangleSumRec()
+ ensures forall n: nat :: n > 0 ==> TriangleSum(n) == n + TriangleSum(n - 1)
+
+}
+
+module A2 refines A1 {
+
+ lemma Proof1(n: nat)
+ ensures TriangleSum(n) == (n * (n + 1)) / 2
+ {
+ TriangleSumBase();
+ TriangleSumRec();
+ if n > 0 {
+ Proof1(n - 1);
+ }
+ }
+
+}
+
+module A3 refines A1 {
+
+ lemma Proof2(n: nat)
+ ensures TriangleSum(n) == (n * (n + 1)) / 2
+ {
+ if n == 0 {
+ TriangleSumBase();
+ } else {
+ assert TriangleSum(n) == n + TriangleSum(n - 1) by {
+ TriangleSumRec();
+ }
+ Proof2(n - 1);
+ }
+ }
+
+}
+
+module A4 refines A1 {
+
+ lemma Proof3(n: nat)
+ ensures TriangleSum(n) == (n * (n + 1)) / 2
+ {
+ TriangleSumBase();
+ TriangleSumRec();
+ if n == 0 {
+ } else {
+ assert TriangleSum(n) == n + TriangleSum(n - 1);
+ Proof3(n - 1);
+ }
+ }
+
+}
+
+module A5 refines A1 {
+
+ lemma TriangleSumRecExplicit(n: nat)
+ requires n > 0
+ ensures TriangleSum(n) == n + TriangleSum(n - 1)
+
+ lemma Proof4(n: nat)
+ ensures TriangleSum(n) == (n * (n + 1)) / 2
+ {
+ if n == 0 {
+ TriangleSumBase();
+ } else {
+ assert TriangleSum(n) == n + TriangleSum(n - 1) by {
+ TriangleSumRecExplicit(n);
+ }
+ Proof4(n - 1);
+ }
+ }
+
+}

assets/src/brittleness/verify.sh

@@ -0,0 +1,19 @@
+#!/bin/bash
+
+set -e
+
+if command -v dafny > /dev/null 2>&1
+then
+ echo 
+ echo "*** Verification of the brittleness blog post"
+else
+ echo "Verification requires dafny to be installed"
+ exit 1
+fi
+
+cd "$(dirname "$0")"
+
+(dafny verify RationalAdd.dfy > RationalAdd.dfy.out) || true
+diff RationalAdd.dfy.out RationalAdd.dfy.expect
+rm -f RationalAdd.dfy.out
+dafny verify TriangleSum.dfy

assets/src/cracking-the-coding-interview-permutations/permutations.dfy

@@ -0,0 +1,156 @@
+/* Definitions */
+
+predicate IsPermutationOf<T(==)>(p: seq<T>, s: seq<T>) {
+ multiset(p) == multiset(s)
+}
+
+ghost function AllPermutationsOf<T(!new)>(s: seq<T>): iset<seq<T>> {
+ iset p | IsPermutationOf(p, s)
+}
+
+function CalculateAllPermutationsOf<T(==)>(s: seq<T>): set<seq<T>> {
+ if |s| == 0 then
+ {s}
+ else
+ set p, i | p in CalculateAllPermutationsOf(s[1..]) && 0 <= i <= |p| :: InsertAt(p, s[0], i)
+}
+
+function InsertAt<T>(s: seq<T>, x: T, i: nat): seq<T>
+ requires i <= |s|
+{
+ s[..i] + [x] + s[i..]
+}
+
+function DeleteAt<T>(s: seq<T>, i: nat): seq<T>
+ requires i < |s|
+{
+ s[..i] + s[i+1..]
+}
+
+function FirstOccurrence<T(==)>(p: seq<T>, x: T): (i: nat)
+ requires x in multiset(p)
+ ensures i < |p|
+ ensures p[i] == x
+{
+ if p[0] == x then
+ 0
+ else
+ FirstOccurrence(p[1..], x) + 1
+}
+
+/* Lemmas */
+
+lemma Correctness<T(!new)>(s: seq<T>)
+ ensures (iset p | p in CalculateAllPermutationsOf(s)) == AllPermutationsOf(s)
+{
+ assert (iset p | p in CalculateAllPermutationsOf(s)) == AllPermutationsOf(s) by {
+ assert forall p :: p in CalculateAllPermutationsOf(s) <==> p in AllPermutationsOf(s) by {
+ forall p
+ ensures p in CalculateAllPermutationsOf(s) <==> p in AllPermutationsOf(s) 
+ {
+ CorrectnessImplicationOne(s, p);
+ CorrectnessImplicationTwo(s, p);
+ }
+ }
+ }
+}
+
+lemma CorrectnessImplicationOne<T(!new)>(s: seq<T>, p: seq<T>)
+ ensures p in CalculateAllPermutationsOf(s) ==> p in AllPermutationsOf(s)
+{
+ if |s| == 0 {
+ // induction base, no proof hints needed
+ } else {
+ // induction step
+ if p in CalculateAllPermutationsOf(s) {
+ assert p in AllPermutationsOf(s) by {
+ assert IsPermutationOf(p, s) by {
+ var p', i :| p' in CalculateAllPermutationsOf(s[1..]) && 0 <= i <= |p'| && p == InsertAt(p', s[0], i);
+ calc == {
+ multiset(p);
+ multiset(InsertAt(p', s[0], i));
+ { MultisetAfterInsertAt(p', s[0], i); }
+ multiset([s[0]]) + multiset(p');
+ { CorrectnessImplicationOne(s[1..], p'); } // induction hypothesis
+ multiset([s[0]]) + multiset(s[1..]);
+ multiset([s[0]] + s[1..]);
+ { assert [s[0]] + s[1..] == s; }
+ multiset(s);
+ }
+ }
+ }
+ }
+ }
+}
+
+lemma CorrectnessImplicationTwo<T(!new)>(s: seq<T>, p: seq<T>)
+ ensures p in CalculateAllPermutationsOf(s) <== p in AllPermutationsOf(s)
+{
+ if |s| == 0 {
+ // induction base, no proof hints needed
+ } else {
+ // induction step
+ if p in AllPermutationsOf(s) {
+ assert p in CalculateAllPermutationsOf(s) by {
+ var i := FirstOccurrence(p, s[0]);
+ var p' := DeleteAt(p, i);
+ assert p' in CalculateAllPermutationsOf(s[1..]) by {
+ assert p' in AllPermutationsOf(s[1..]) by {
+ PermutationBeforeAndAfterDeletionAt(p, s, i, 0);
+ }
+ CorrectnessImplicationTwo(s[1..], p'); // induction hypothesis
+ }
+ assert p == InsertAt(p', s[0], i) by {
+ InsertAfterDeleteAt(p, i);
+ }
+ }
+ }
+ }
+}
+
+lemma MultisetAfterInsertAt<T>(s: seq<T>, x: T, i: nat)
+ requires i <= |s|
+ ensures multiset(InsertAt(s, x, i)) == multiset([x]) + multiset(s)
+{
+ calc == {
+ multiset(InsertAt(s, x, i));
+ multiset(s[..i] + [x] + s[i..]);
+ multiset(s[..i]) + multiset([x]) + multiset(s[i..]);
+ multiset([x]) + multiset(s[..i]) + multiset(s[i..]);
+ multiset([x]) + multiset(s[..i] + s[i..]);
+ { assert s[..i] + s[i..] == s; }
+ multiset([x]) + multiset(s);
+ }
+}
+
+lemma PermutationBeforeAndAfterDeletionAt<T>(p: seq<T>, s: seq<T>, i: nat, j: nat)
+ requires IsPermutationOf(p, s)
+ requires i < |p|
+ requires j < |s|
+ requires p[i] == s[j]
+ ensures IsPermutationOf(DeleteAt(p, i), DeleteAt(s, j))
+{
+ assert IsPermutationOf(DeleteAt(p, i), DeleteAt(s, j)) by {
+ calc == {
+ multiset(DeleteAt(p, i));
+ multiset(p[..i] + p[i+1..]);
+ multiset(p[..i]) + multiset(p[i+1..]);
+ multiset(p[..i]) + multiset([p[i]]) + multiset(p[i+1..]) - multiset([p[i]]);
+ multiset(p[..i] + [p[i]] + p[i+1..]) - multiset([p[i]]);
+ { assert p[..i] + [p[i]] + p[i+1..] == p; }
+ multiset(p) - multiset([p[i]]);
+ multiset(s) - multiset([s[j]]);
+ { assert s[..j] + [s[j]] + s[j+1..] == s; }
+ multiset(s[..j] + [s[j]] + s[j+1..]) - multiset([s[j]]);
+ multiset(s[..j]) + multiset([s[j]]) + multiset(s[j+1..]) - multiset([s[j]]);
+ multiset(s[..j]) + multiset(s[j+1..]);
+ multiset(s[..j] + s[j+1..]);
+ multiset(DeleteAt(s, j));
+ }
+ }
+}
+
+lemma InsertAfterDeleteAt<T>(s: seq<T>, i: nat)
+ requires i < |s|
+ ensures s == InsertAt(DeleteAt(s, i), s[i], i)
+{}