From 99d876590c271351fe4d3d53cc1b4b6ab4876b06 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Fri, 15 Aug 2025 15:19:57 -0700 Subject: [PATCH 1/4] auto commit --- StandardLibrary/test/TestMutableMap.dfy | 75 +++++++++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 StandardLibrary/test/TestMutableMap.dfy diff --git a/StandardLibrary/test/TestMutableMap.dfy b/StandardLibrary/test/TestMutableMap.dfy new file mode 100644 index 000000000..f3601ef27 --- /dev/null +++ b/StandardLibrary/test/TestMutableMap.dfy @@ -0,0 +1,75 @@ +include "../../libraries/src/MutableMap/MutableMap.dfy" +include "../../StandardLibrary/src/Index.dfy" + +module TestMutableMap { + import opened DafnyLibraries + import opened StandardLibrary.UInt + + method {:test} TestPerformanceBaseline() + { + var testMap := new MutableMap(); + var iterations := 100; + + var i := 0; + while i < iterations { + testMap.Put(i, i); + i := i + 1; + } + + expect testMap.Size() == iterations; + + i := 0; + while i < iterations { + expect testMap.HasKey(i); + i := i + 1; + } + + i := 0; + while i < iterations { + expect testMap.HasKey(i); + expect testMap.Select(i) == i; + i := i + 1; + } + + i := 0; + while i < iterations { + testMap.Remove(i); + i := i + 1; + } + + expect testMap.Size() == 0; + } + + method {:test} TestPerformanceScaling() + { + TestMapOperations(10); + TestMapOperations(100); + TestMapOperations(1000); + } + + method TestMapOperations(size: int) + requires size > 0 + { + var testMap := new MutableMap(); + + var i := 0; + while i < size { + testMap.Put(i, i); + i := i + 1; + } + + expect testMap.Size() == size; + + var tempI; + while i < size { + tempI := testMap.Select(i); + expect i == tempI; + i := i + 1; + } + + while i < size { + testMap.Remove(i); + expect !testMap.HasKey(i); + } + } +} From 90aeba6cfd9fd54197afe6db514bc610afedb7f9 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Fri, 15 Aug 2025 15:46:12 -0700 Subject: [PATCH 2/4] auto commit --- StandardLibrary/test/TestMutableMap.dfy | 46 +++++++------------------ 1 file changed, 12 insertions(+), 34 deletions(-) diff --git a/StandardLibrary/test/TestMutableMap.dfy b/StandardLibrary/test/TestMutableMap.dfy index f3601ef27..b87ac3bbd 100644 --- a/StandardLibrary/test/TestMutableMap.dfy +++ b/StandardLibrary/test/TestMutableMap.dfy @@ -4,47 +4,25 @@ include "../../StandardLibrary/src/Index.dfy" module TestMutableMap { import opened DafnyLibraries import opened StandardLibrary.UInt + import Time - method {:test} TestPerformanceBaseline() + method {:test} TestPerformanceScaling() { - var testMap := new MutableMap(); - var iterations := 100; - + var sizes := [10, 1000000000, 100000000000000000]; var i := 0; - while i < iterations { - testMap.Put(i, i); - i := i + 1; + while i < |sizes| { + TestForEachSize(sizes[i]); + i := i + 1; } - - expect testMap.Size() == iterations; - - i := 0; - while i < iterations { - expect testMap.HasKey(i); - i := i + 1; - } - - i := 0; - while i < iterations { - expect testMap.HasKey(i); - expect testMap.Select(i) == i; - i := i + 1; - } - - i := 0; - while i < iterations { - testMap.Remove(i); - i := i + 1; - } - - expect testMap.Size() == 0; } - method {:test} TestPerformanceScaling() + method TestForEachSize(size: int) + requires size > 0 { - TestMapOperations(10); - TestMapOperations(100); - TestMapOperations(1000); + var time1 := Time.GetAbsoluteTime(); + TestMapOperations(size); + print "Time taken for " , size , " items \n"; + Time.PrintTimeSince(time1); } method TestMapOperations(size: int) From 4cc2f48b3691da88e2dd3dc91f2b6112446533a2 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Fri, 15 Aug 2025 15:48:10 -0700 Subject: [PATCH 3/4] auto commit --- StandardLibrary/test/TestMutableMap.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/StandardLibrary/test/TestMutableMap.dfy b/StandardLibrary/test/TestMutableMap.dfy index b87ac3bbd..5952929af 100644 --- a/StandardLibrary/test/TestMutableMap.dfy +++ b/StandardLibrary/test/TestMutableMap.dfy @@ -8,7 +8,7 @@ module TestMutableMap { method {:test} TestPerformanceScaling() { - var sizes := [10, 1000000000, 100000000000000000]; + var sizes := [1, 10, 10000, 100000, 1000000, 1000000000, 100000000000000000]; var i := 0; while i < |sizes| { TestForEachSize(sizes[i]); From 02fbfd46c7f7cea89b27326943bfcb9eb245baba Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Sun, 17 Aug 2025 18:06:26 -0700 Subject: [PATCH 4/4] auto commit --- StandardLibrary/test/TestMutableMap.dfy | 65 ++++++++++++++++--------- 1 file changed, 43 insertions(+), 22 deletions(-) diff --git a/StandardLibrary/test/TestMutableMap.dfy b/StandardLibrary/test/TestMutableMap.dfy index 5952929af..67c6dca74 100644 --- a/StandardLibrary/test/TestMutableMap.dfy +++ b/StandardLibrary/test/TestMutableMap.dfy @@ -26,28 +26,49 @@ module TestMutableMap { } method TestMapOperations(size: int) - requires size > 0 + requires size > 0 +{ + // Explicitly parametrize with , int> + var testMap := new MutableMap((k: seq, v: int) => true, true); + var i := 0; + while i < size { + // Convert int -> seq (just an example: single-byte sequence) + var key := IntToBytes(i); + testMap.Put(key, i); + i := i + 1; + } + expect testMap.Size() == size; + // Reset loop + i := 0; + while i < size { + var key := IntToBytes(i); + var tempI := testMap.Select(key); + expect i == tempI; + i := i + 1; + } + i := 0; + while i < size { + var key := IntToBytes(i); + testMap.Remove(key); + expect !testMap.HasKey(key); + i := i + 1; + } +} +method IntToBytes(x: int) returns (bytes: seq) + requires x >= 0 + ensures |bytes| > 0 +{ + var result := []; + var n := x; + while n > 0 + decreases n { - var testMap := new MutableMap(); - - var i := 0; - while i < size { - testMap.Put(i, i); - i := i + 1; - } - - expect testMap.Size() == size; - - var tempI; - while i < size { - tempI := testMap.Select(i); - expect i == tempI; - i := i + 1; - } - - while i < size { - testMap.Remove(i); - expect !testMap.HasKey(i); - } + result := [(n % 256) as uint8] + result; + n := n / 256; + } + if |result| == 0 { + result := [(0) as uint8]; } + bytes := result; +} }