Add Tower of Hanoi + Simple Arithmetic Tests #182

Sarthak-Dayal · 2025-12-04T01:06:59Z

Adds a test case + proof stub for a tower of Hanoi implementation with helper lemmas for my version of the proof. Note that this does not check whether all disks end on the right peg, simply for ease of implementing the proofs.
Adds a test case + proof stub for a simple addition implementation

Copilot

Pull request overview

This PR adds two new test cases with proof stubs for Dafny verification: a bubble sort implementation and a sum formula proof. The bubble sort includes helper lemmas to establish correctness properties such as length preservation, multiset preservation, and sorted order guarantees.

Adds bubble sort test case with functions for single-pass and multi-pass sorting
Adds sum formula test case comparing recursive and closed-form implementations
Includes comprehensive proof stubs with helper lemmas for establishing sorting properties

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 1 comment.

File	Description
testcases/sum_formula.dfy	Defines recursive sum function, closed-form formula, and test lemma
testcases/bubble_sort.dfy	Implements bubble sort with BubblePass and Sort functions, includes test method
proofs/sum_formula.dfy	Provides proof stub for sum formula equivalence
proofs/bubble_sort.dfy	Defines main correctness lemma and helper lemmas for sorting properties

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

testcases/bubble_sort.dfy

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Copilot

Pull request overview

Copilot reviewed 4 out of 4 changed files in this pull request and generated 5 comments.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2025-12-04T01:14:45Z

proofs/sum_formula.dfy

@@ -0,0 +1,5 @@
+lemma {:induction false} proof(n: nat)


The lemma name proof is too generic and doesn't follow the naming convention used by most other test cases in this repository. Consider using a more descriptive PascalCase name like SumEqualsFormulaProof to match the pattern used in other files (e.g., AddAllProof, ExpPositiveProof, PrimeDivisorLemma).

Suggested change

lemma {:induction false} proof(n: nat)

lemma {:induction false} SumEqualsFormulaProof(n: nat)

Copilot · 2025-12-04T01:14:45Z

proofs/bubble_sort.dfy

+lemma {:induction false} sorting_correctness(s: seq<int>)
+    ensures |Sort(s)| == |s| &&
+            forall i: int, j: int :: 0 <= i < j < |Sort(s)| ==> Sort(s)[i] <= Sort(s)[j]
+    decreases |s|
+{
+
+}
+
+lemma {:induction false} bubble_pass_preserves_length(s: seq<int>)
+    ensures |BubblePass(s)| == |s|
+    decreases |s|
+{
+
+}
+
+lemma {:induction false} sort_helper_preserves_length(s: seq<int>, n: int)
+    requires 0 <= n
+    ensures |SortHelper(s, n)| == |s|
+    decreases n
+{
+
+}
+
+lemma {:induction false} bubble_pass_preserves_multiset(s: seq<int>)
+    ensures (forall x :: x in multiset(s) ==> x in multiset(BubblePass(s))) &&
+            (forall x :: x in multiset(BubblePass(s)) ==> x in multiset(s))
+    decreases |s|
+{
+
+}
+
+lemma {:induction false} bubble_pass_elements_from_original(s: seq<int>, i: int)
+    requires 0 <= i < |BubblePass(s)|
+    ensures BubblePass(s)[i] in multiset(s)
+{
+
+}
+
+lemma {:induction false} element_in_multiset_bounded_by_max(s: seq<int>, elem: int)
+    requires elem in multiset(s)
+    requires forall i :: 0 <= i < |s| - 1 ==> s[i] <= s[|s| - 1]
+    ensures elem <= s[|s| - 1]
+{
+
+}
+
+lemma {:induction false} bubble_pass_moves_max_to_end(s: seq<int>)
+    requires |s| > 0
+    ensures forall i :: 0 <= i < |BubblePass(s)| - 1 ==> BubblePass(s)[i] <= BubblePass(s)[|BubblePass(s)| - 1]
+    decreases |s|
+{
+
+}
+
+lemma {:induction false} bubble_pass_preserves_max_at_end(s: seq<int>)
+    requires |s| > 0
+    requires forall i :: 0 <= i < |s| - 1 ==> s[i] <= s[|s| - 1]
+    ensures BubblePass(s)[|BubblePass(s)| - 1] == s[|s| - 1]
+    decreases |s|
+{
+
+}
+
+lemma {:induction false} bubble_pass_prefix_when_max_at_end(s: seq<int>)
+    requires |s| > 1
+    requires forall i :: 0 <= i < |s| - 1 ==> s[i] <= s[|s| - 1]
+    ensures BubblePass(s)[..|BubblePass(s)|-1] == BubblePass(s[..|s|-1])
+    decreases |s|
+{
+
+}
+
+lemma {:induction false} sort_helper_produces_sorted_sequence(s: seq<int>, n: int)
+    requires 0 <= n
+    requires n >= |s|
+    ensures forall i: int, j: int :: 0 <= i < j < |SortHelper(s, n)| ==> SortHelper(s, n)[i] <= SortHelper(s, n)[j]
+    decreases n, |s|
+{
+
+}
+
+lemma {:induction false} sort_helper_decomposes_with_max(s: seq<int>, n: int)
+    requires 0 <= n
+    requires |s| > 0
+    requires forall i :: 0 <= i < |s| - 1 ==> s[i] <= s[|s| - 1]
+    ensures SortHelper(s, n) == SortHelper(s[..|s|-1], n) + [s[|s| - 1]]
+    decreases n
+{
+
+}
+
+lemma {:induction false} sort_helper_preserves_upper_bound(s: seq<int>, n: int, bound: int)
+    requires 0 <= n
+    requires forall i :: 0 <= i < |s| ==> s[i] <= bound
+    ensures forall i :: 0 <= i < |SortHelper(s, n)| ==> SortHelper(s, n)[i] <= bound
+    decreases n
+{
+
+}
+


The lemma names in this file use snake_case (e.g., sorting_correctness, bubble_pass_preserves_length), which is inconsistent with the PascalCase naming convention used for lemmas throughout the rest of the repository (e.g., AddAllProof, ExpPositiveProof, PrimeDivisorLemma). Consider renaming to use PascalCase for consistency.

Copilot · 2025-12-04T01:14:45Z

testcases/bubble_sort.dfy

+ghost function {:induction false} SortHelper(s: seq<int>, n: int): seq<int>
+    decreases n
+{
+    if n <= 0 then s // sorted


The comment // sorted is misleading. When n <= 0, the function simply returns the sequence s unchanged, which is not necessarily sorted. A more accurate comment would be // base case: no more passes or // assume sorted after |s| passes.

Suggested change

if n <= 0 then s // sorted

if n <= 0 then s // base case: no more passes

testcases/sum_formula.dfy

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Copilot

Pull request overview

Copilot reviewed 4 out of 4 changed files in this pull request and generated 2 comments.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

proofs/bubble_sort.dfy

SatvikDuddukuru · 2025-12-04T01:23:07Z

The code looks good overall. The sum test is a good basic example, and the bubble sort test seems to make sense as well, but I have not tried working through filling out the stubs. Just to make copilot happy, maybe use Pascal case. The content itself looks good.

zsa296 · 2025-12-04T03:03:08Z

Bubble sort is already a private TC, and as such, I do not believe it would be a valid public TC.

AmeyaPurao · 2025-12-04T03:17:38Z

Bubble sort is already a private TC, and as such, I do not believe it would be a valid public TC.

I agree on this. I'm not sure on the exact intended distinction but these better scoped for a private case.

Sarthak-Dayal · 2025-12-04T04:26:23Z

Shoot thanks for letting me know, I did not realize it was already a private TC

Copilot

Pull request overview

Copilot reviewed 4 out of 4 changed files in this pull request and generated 10 comments.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

testcases/sum_formula.dfy

proofs/hanoi_towers.dfy

testcases/sum_formula.dfy

testcases/hanoi_towers.dfy

testcases/sum_formula.dfy

testcases/hanoi_towers.dfy

testcases/sum_formula.dfy

testcases/hanoi_towers.dfy

add tests

73a6f5b

Copilot AI review requested due to automatic review settings December 4, 2025 01:07

Copilot started reviewing on behalf of Sarthak-Dayal December 4, 2025 01:07 View session

Copilot finished reviewing on behalf of Sarthak-Dayal December 4, 2025 01:09

Copilot AI reviewed Dec 4, 2025

View reviewed changes

testcases/bubble_sort.dfy Outdated Show resolved Hide resolved

Update testcases/bubble_sort.dfy

4c7a8bf

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Copilot AI review requested due to automatic review settings December 4, 2025 01:10

Copilot started reviewing on behalf of Sarthak-Dayal December 4, 2025 01:10 View session

Copilot finished reviewing on behalf of Sarthak-Dayal December 4, 2025 01:13

Copilot AI reviewed Dec 4, 2025

View reviewed changes

Update testcases/sum_formula.dfy

e781d80

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Copilot AI review requested due to automatic review settings December 4, 2025 01:16

Update testcases/sum_formula.dfy

7a51180

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Copilot started reviewing on behalf of Sarthak-Dayal December 4, 2025 01:16 View session

Copilot finished reviewing on behalf of Sarthak-Dayal December 4, 2025 01:19

Copilot AI reviewed Dec 4, 2025

View reviewed changes

proofs/bubble_sort.dfy Outdated Show resolved Hide resolved

proofs/bubble_sort.dfy Outdated Show resolved Hide resolved

Sarthak-Dayal added 4 commits December 3, 2025 23:29

add tower of hanoi testcase

43ab03c

remove bubble sort

b584f6e

add hanoi towers tc

cda6da4

remove old tc

52f1454

Sarthak-Dayal changed the title ~~Add Bubble Sort + Simple Arithmetic Tests~~ Add Tower of Hanoi + Simple Arithmetic Tests Dec 4, 2025

remove bubble sort tc

5aab11d

Copilot AI review requested due to automatic review settings December 4, 2025 05:57

Copilot started reviewing on behalf of Sarthak-Dayal December 4, 2025 05:57 View session

Sarthak-Dayal requested a review from SatvikDuddukuru December 4, 2025 05:59

Copilot finished reviewing on behalf of Sarthak-Dayal December 4, 2025 06:00

Copilot AI reviewed Dec 4, 2025

View reviewed changes

	lemma {:induction false} proof(n: nat)
	lemma {:induction false} SumEqualsFormulaProof(n: nat)

	if n <= 0 then s // sorted
	if n <= 0 then s // base case: no more passes

Add Tower of Hanoi + Simple Arithmetic Tests #182

Are you sure you want to change the base?

Add Tower of Hanoi + Simple Arithmetic Tests #182

Uh oh!

Conversation

Sarthak-Dayal commented Dec 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Copilot AI Dec 4, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 4, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 4, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Uh oh!

SatvikDuddukuru commented Dec 4, 2025

Uh oh!

zsa296 commented Dec 4, 2025

Uh oh!

AmeyaPurao commented Dec 4, 2025

Uh oh!

Sarthak-Dayal commented Dec 4, 2025

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Sarthak-Dayal commented Dec 4, 2025 •

edited

Loading