From 2d938116b92196a67a7134e2d98b8b09c98a13c6 Mon Sep 17 00:00:00 2001 From: Noah Schell Date: Tue, 2 Dec 2025 22:44:03 -0600 Subject: [PATCH 1/5] parity --- parity.dfy | 12 ++++++++++++ proofs/parity.dfy | 6 ++++++ 2 files changed, 18 insertions(+) create mode 100644 parity.dfy create mode 100644 proofs/parity.dfy diff --git a/parity.dfy b/parity.dfy new file mode 100644 index 0000000..14948d9 --- /dev/null +++ b/parity.dfy @@ -0,0 +1,12 @@ +predicate {:induction false} isEven(n: nat) +{ + if n == 0 then true + else if n == 1 then false + else isEven(n - 2) +} + +method {:induction false} ParityTest(x: nat, y: nat) { + assert (isEven(x) || isEven(y)) ==> isEven(x * y) by { + ParityProof(x, y); + } +} \ No newline at end of file diff --git a/proofs/parity.dfy b/proofs/parity.dfy new file mode 100644 index 0000000..c2fdaae --- /dev/null +++ b/proofs/parity.dfy @@ -0,0 +1,6 @@ +lemma {:induction false} ParityProof(x: nat, y: nat) + ensures (isEven(x) || isEven(y)) ==> isEven(x * y) +{ + +} + From b2990fc09705da636c345c341add584976aea18d Mon Sep 17 00:00:00 2001 From: Noah Schell <144622777+nSchell4@users.noreply.github.com> Date: Tue, 2 Dec 2025 23:30:16 -0600 Subject: [PATCH 2/5] move parity.dfy to testcases/parity.dfy --- parity.dfy => testcases/parity.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename parity.dfy => testcases/parity.dfy (99%) diff --git a/parity.dfy b/testcases/parity.dfy similarity index 99% rename from parity.dfy rename to testcases/parity.dfy index 14948d9..95c8bf2 100644 --- a/parity.dfy +++ b/testcases/parity.dfy @@ -9,4 +9,4 @@ method {:induction false} ParityTest(x: nat, y: nat) { assert (isEven(x) || isEven(y)) ==> isEven(x * y) by { ParityProof(x, y); } -} \ No newline at end of file +} From 04bdb1cb0a1075f618ba91c4d4505b3846b54040 Mon Sep 17 00:00:00 2001 From: Noah Schell <144622777+nSchell4@users.noreply.github.com> Date: Wed, 3 Dec 2025 13:27:28 -0600 Subject: [PATCH 3/5] move isEven condition to requires --- proofs/parity.dfy | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/proofs/parity.dfy b/proofs/parity.dfy index c2fdaae..eeede3f 100644 --- a/proofs/parity.dfy +++ b/proofs/parity.dfy @@ -1,5 +1,6 @@ lemma {:induction false} ParityProof(x: nat, y: nat) - ensures (isEven(x) || isEven(y)) ==> isEven(x * y) + requires isEven(x) || isEven(y) + ensures isEven(x * y) { } From ef9d8bf6b4b8e031e07bad3ededa6f4fbd481efe Mon Sep 17 00:00:00 2001 From: Noah Schell <144622777+nSchell4@users.noreply.github.com> Date: Thu, 4 Dec 2025 10:43:57 -0600 Subject: [PATCH 4/5] Moved isEven condition to requires statement in test file --- testcases/parity.dfy | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/testcases/parity.dfy b/testcases/parity.dfy index 95c8bf2..51acfec 100644 --- a/testcases/parity.dfy +++ b/testcases/parity.dfy @@ -5,8 +5,10 @@ predicate {:induction false} isEven(n: nat) else isEven(n - 2) } -method {:induction false} ParityTest(x: nat, y: nat) { - assert (isEven(x) || isEven(y)) ==> isEven(x * y) by { +method {:induction false} ParityTest(x: nat, y: nat) + requires isEven(x) || isEven(y) +{ + assert isEven(x * y) by { ParityProof(x, y); } } From 4c1becc7291f521e0fe45925b27d0678ae95ba71 Mon Sep 17 00:00:00 2001 From: Noah Schell <144622777+nSchell4@users.noreply.github.com> Date: Thu, 4 Dec 2025 10:49:44 -0600 Subject: [PATCH 5/5] add a decreases clause in proof file --- proofs/parity.dfy | 1 + 1 file changed, 1 insertion(+) diff --git a/proofs/parity.dfy b/proofs/parity.dfy index eeede3f..22b2ca6 100644 --- a/proofs/parity.dfy +++ b/proofs/parity.dfy @@ -1,6 +1,7 @@ lemma {:induction false} ParityProof(x: nat, y: nat) requires isEven(x) || isEven(y) ensures isEven(x * y) + decreases x + y { }