Skip to content

tests: add property based testing using TypeScript oracles#488

Draft
christoph-dfinity wants to merge 6 commits intomainfrom
cursor/ts-pbt-queue-oracle
Draft

tests: add property based testing using TypeScript oracles#488
christoph-dfinity wants to merge 6 commits intomainfrom
cursor/ts-pbt-queue-oracle

Conversation

@christoph-dfinity
Copy link
Copy Markdown
Contributor

Summary

Adds a TypeScript property-based testing harness (fast-check) with a minimal array-backed OracleDeque reference, model-based command tests for deque operations, and a first cross-language check: a fixed trace is emitted to test/oracleReplay/QueueReplayFixture.mo and replayed in Motoko against pure/Queue.

Changes

  • TS: fast-check model/command tests; generate:oracle-fixture wired into test:ts
  • Motoko: Queue.oracleReplay.test.mo asserts final queue state matches the oracle fixture
  • Misc: Minor List.mo style fixes from the same branch

Test plan

  • npm test

Made with Cursor

- OracleDeque reference and model-based command tests under test/ts/pbt; run via test:ts

- Add fast-check devDependency

- List.mo: let vs var and semicolon style fixes

Made-with: Cursor
- Emit QueueReplayFixture.mo from queueOracleTrace; replay test vs pure/Queue

- Wire generate:oracle-fixture into test:ts

Made-with: Cursor
@github-actions
Copy link
Copy Markdown

Benchmark Results

bench/ArrayBuilding.bench.mo $({\color{green}-0.18\%})$

Large known-size array building

Compares performance of different data structures for building arrays of known size.

Instructions: ${\color{green}-0.13\%}$
Heap: ${\color{gray}0\%}$
Stable Memory: ${\color{gray}0\%}$
Garbage Collection: ${\color{green}-0.05\%}$

Instructions

1000 100000 1000000
List 542_175 $({\color{green}-1.11\%})$ 47_994_641 $({\color{green}-0.68\%})$ 475_069_688 $({\color{green}-0.65\%})$
Buffer 342_033 $({\color{red}+0.01\%})$ 33_903_445 $({\color{red}+0.00\%})$ 339_003_651 $({\color{red}+0.00\%})$
pure/List 302_163 $({\color{red}+0.01\%})$ 30_003_600 $({\color{red}+0.00\%})$ 300_055_973 $({\color{red}+0.00\%})$
VarArray ?T 180_546 $({\color{red}+0.01\%})$ 17_802_958 $({\color{red}+0.00\%})$ 178_003_164 $({\color{green}-0.00\%})$
VarArray T 160_841 $({\color{red}+0.02\%})$ 15_803_253 $({\color{red}+0.00\%})$ 158_003_459 $({\color{red}+0.00\%})$
Array (baseline) 42_715 $({\color{red}+0.05\%})$ 4_003_127 $({\color{red}+0.00\%})$ 40_003_333 $({\color{green}-0.00\%})$

Heap

1000 100000 1000000
List 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$
Buffer 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$
pure/List 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$
VarArray ?T 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$
VarArray T 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$
Array (baseline) 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$

Garbage Collection

1000 100000 1000000
List 9.96 KiB $({\color{green}-0.97\%})$ 797.46 KiB $({\color{green}-0.01\%})$ 7.67 MiB $({\color{green}-0.00\%})$
Buffer 8.71 KiB $({\color{gray}0\%})$ 782.15 KiB $({\color{gray}0\%})$ 7.63 MiB $({\color{gray}0\%})$
pure/List 19.95 KiB $({\color{gray}0\%})$ 1.91 MiB $({\color{gray}0\%})$ 19.07 MiB $({\color{gray}0\%})$
VarArray ?T 8.24 KiB $({\color{gray}0\%})$ 781.68 KiB $({\color{gray}0\%})$ 7.63 MiB $({\color{gray}0\%})$
VarArray T 8.23 KiB $({\color{gray}0\%})$ 781.67 KiB $({\color{gray}0\%})$ 7.63 MiB $({\color{gray}0\%})$
Array (baseline) 4.3 KiB $({\color{gray}0\%})$ 391.02 KiB $({\color{gray}0\%})$ 3.82 MiB $({\color{gray}0\%})$
No previous results found "/home/runner/work/motoko-core/motoko-core/.bench/Base64.bench.json"
bench/Base64.bench.mo $({\color{gray}0\%})$

Base64

Compare zero bytes vs mixed bytes encoding to Base64

Instructions: ${\color{gray}0\%}$
Heap: ${\color{gray}0\%}$
Stable Memory: ${\color{gray}0\%}$
Garbage Collection: ${\color{gray}0\%}$

Instructions

zero bytes mixed bytes
1 948 948
10 3_242 3_242
100 22_742 22_742
1000 217_742 217_742
10000 2_168_137 2_167_783

Heap

zero bytes mixed bytes
1 272 B 272 B
10 272 B 272 B
100 272 B 272 B
1000 272 B 272 B
10000 272 B 272 B

Garbage Collection

zero bytes mixed bytes
1 344 B 344 B
10 496 B 496 B
100 1.77 KiB 1.77 KiB
1000 14.66 KiB 14.66 KiB
10000 143.57 KiB 143.57 KiB
bench/FromIters.bench.mo $({\color{red}+0.05\%})$

Benchmarking the fromIter functions

Columns describe the number of elements in the input iter.

Instructions: ${\color{red}+0.05\%}$
Heap: ${\color{gray}0\%}$
Stable Memory: ${\color{gray}0\%}$
Garbage Collection: ${\color{gray}0\%}$

Instructions

100 10_000 100_000
Array.fromIter 48_828 $({\color{red}+0.13\%})$ 4_712_089 $({\color{red}+0.00\%})$ 47_103_197 $({\color{red}+0.00\%})$
List.fromIter 31_762 $({\color{red}+0.20\%})$ 3_061_605 $({\color{red}+0.00\%})$ 30_603_615 $({\color{red}+0.00\%})$
List.fromIter . Iter.reverse 50_359 $({\color{red}+0.12\%})$ 4_832_625 $({\color{red}+0.00\%})$ 48_305_537 $({\color{red}+0.00\%})$

Heap

100 10_000 100_000
Array.fromIter 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$
List.fromIter 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$
List.fromIter . Iter.reverse 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$

Garbage Collection

100 10_000 100_000
Array.fromIter 2.76 KiB $({\color{gray}0\%})$ 234.79 KiB $({\color{gray}0\%})$ 2.29 MiB $({\color{gray}0\%})$
List.fromIter 3.51 KiB $({\color{gray}0\%})$ 312.88 KiB $({\color{gray}0\%})$ 3.05 MiB $({\color{gray}0\%})$
List.fromIter . Iter.reverse 5.11 KiB $({\color{gray}0\%})$ 469.17 KiB $({\color{gray}0\%})$ 4.58 MiB $({\color{gray}0\%})$
bench/ListBufferNewArray.bench.mo $({\color{green}-4.07\%})$

List vs. Buffer for creating known-size arrays

Performance comparison between List and Buffer for creating a new array.

Instructions: ${\color{red}+0.12\%}$
Heap: ${\color{gray}0\%}$
Stable Memory: ${\color{gray}0\%}$
Garbage Collection: ${\color{green}-4.19\%}$

Instructions

0 (baseline) 1 5 10 100 (for loop)
List 1_431 $({\color{green}-7.50\%})$ 2_751 $({\color{green}-5.66\%})$ 8_731 $({\color{green}-3.48\%})$ 13_524 $({\color{green}-3.04\%})$ 73_224 $({\color{green}-1.80\%})$
pure/List 1_311 $({\color{red}+5.13\%})$ 1_419 $({\color{red}+4.72\%})$ 2_503 $({\color{red}+2.62\%})$ 3_863 $({\color{red}+1.63\%})$ 31_928 $({\color{red}+0.19\%})$
Buffer 2_183 $({\color{red}+3.02\%})$ 2_335 $({\color{red}+2.82\%})$ 3_582 $({\color{red}+1.82\%})$ 5_147 $({\color{red}+1.22\%})$ 36_700 $({\color{red}+0.16\%})$

Heap

0 (baseline) 1 5 10 100 (for loop)
List 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$
pure/List 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$
Buffer 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$

Garbage Collection

0 (baseline) 1 5 10 100 (for loop)
List 476 B $({\color{green}-17.36\%})$ 516 B $({\color{green}-16.23\%})$ 676 B $({\color{green}-12.89\%})$ 784 B $({\color{green}-11.31\%})$ 1.84 KiB $({\color{green}-5.05\%})$
pure/List 360 B $({\color{gray}0\%})$ 380 B $({\color{gray}0\%})$ 460 B $({\color{gray}0\%})$ 560 B $({\color{gray}0\%})$ 2.3 KiB $({\color{gray}0\%})$
Buffer 856 B $({\color{gray}0\%})$ 864 B $({\color{gray}0\%})$ 896 B $({\color{gray}0\%})$ 936 B $({\color{gray}0\%})$ 1.62 KiB $({\color{gray}0\%})$
bench/PriorityQueues.bench.mo $({\color{green}-2.68\%})$

Different priority queue implementations

_Compare the performance of the following priority queue implementations:

  • PriorityQueue: Binary heap implementation over List.
  • PriorityQueueSet: Wrapper over Set<(T, Nat)>._

Instructions: ${\color{green}-2.70\%}$
Heap: ${\color{gray}0\%}$
Stable Memory: ${\color{gray}0\%}$
Garbage Collection: ${\color{red}+0.02\%}$

Instructions

A) PriorityQueue B) PriorityQueueSet
1.) 100000 operations (push:pop = 1:1) 568_913_162 $({\color{green}-4.79\%})$ 522_729_679 $({\color{green}-0.00\%})$
2.) 100000 operations (push:pop = 2:1) 707_495_283 $({\color{green}-4.77\%})$ 809_692_987 $({\color{green}-0.00\%})$
3.) 100000 operations (push:pop = 10:1) 336_409_806 $({\color{green}-6.01\%})$ 873_180_969 $({\color{green}-0.00\%})$
4.) 100000 operations (only push) 176_983_018 $({\color{green}-8.02\%})$ 886_824_651 $({\color{green}-0.00\%})$
5.) 50000 pushes, then 50000 pops 745_226_761 $({\color{green}-4.04\%})$ 961_778_074 $({\color{red}+0.00\%})$
6.) 50000 pushes, then 25000 "pop;push"es 504_254_251 $({\color{green}-4.76\%})$ 922_136_355 $({\color{green}-0.00\%})$

Heap

A) PriorityQueue B) PriorityQueueSet
1.) 100000 operations (push:pop = 1:1) 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$
2.) 100000 operations (push:pop = 2:1) 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$
3.) 100000 operations (push:pop = 10:1) 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$
4.) 100000 operations (only push) 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$
5.) 50000 pushes, then 50000 pops 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$
6.) 50000 pushes, then 25000 "pop;push"es 272 B $({\color{gray}0\%})$ 272 B $({\color{gray}0\%})$

Garbage Collection

A) PriorityQueue B) PriorityQueueSet
1.) 100000 operations (push:pop = 1:1) 15.07 MiB $({\color{red}+0.24\%})$ 17.43 MiB $({\color{gray}0\%})$
2.) 100000 operations (push:pop = 2:1) 19.73 MiB $({\color{gray}0\%})$ 19.32 MiB $({\color{gray}0\%})$
3.) 100000 operations (push:pop = 10:1) 8.67 MiB $({\color{gray}0\%})$ 12.64 MiB $({\color{gray}0\%})$
4.) 100000 operations (only push) 3.87 MiB $({\color{gray}0\%})$ 9.96 MiB $({\color{gray}0\%})$
5.) 50000 pushes, then 50000 pops 22.03 MiB $({\color{red}+0.02\%})$ 26.2 MiB $({\color{gray}0\%})$
6.) 50000 pushes, then 25000 "pop;push"es 14.22 MiB $({\color{gray}0\%})$ 18.44 MiB $({\color{gray}0\%})$
bench/PureListStackSafety.bench.mo $({\color{red}+0.00\%})$

List Stack safety

Check stack-safety of the following pure/List-related functions.

Instructions: ${\color{red}+0.00\%}$
Heap: ${\color{gray}0\%}$
Stable Memory: ${\color{gray}0\%}$
Garbage Collection: ${\color{gray}0\%}$

Instructions

pure/List.split 24_602_588 $({\color{red}+0.00\%})$
pure/List.all 7_901_078 $({\color{red}+0.00\%})$
pure/List.any 8_001_454 $({\color{red}+0.00\%})$
pure/List.map 23_103_831 $({\color{red}+0.00\%})$
pure/List.filter 21_104_252 $({\color{red}+0.00\%})$
pure/List.filterMap 27_404_804 $({\color{red}+0.00\%})$
pure/List.partition 21_305_058 $({\color{red}+0.00\%})$
pure/List.join 33_105_390 $({\color{red}+0.00\%})$
pure/List.flatten 24_805_731 $({\color{red}+0.00\%})$
pure/List.take 24_605_728 $({\color{red}+0.00\%})$
pure/List.drop 9_904_183 $({\color{red}+0.00\%})$
pure/List.foldRight 19_105_832 $({\color{red}+0.00\%})$
pure/List.merge 31_808_648 $({\color{red}+0.00\%})$
pure/List.chunks 51_510_408 $({\color{red}+0.00\%})$
pure/Queue 142_662_569 $({\color{red}+0.00\%})$

Heap

pure/List.split 272 B $({\color{gray}0\%})$
pure/List.all 272 B $({\color{gray}0\%})$
pure/List.any 272 B $({\color{gray}0\%})$
pure/List.map 272 B $({\color{gray}0\%})$
pure/List.filter 272 B $({\color{gray}0\%})$
pure/List.filterMap 272 B $({\color{gray}0\%})$
pure/List.partition 272 B $({\color{gray}0\%})$
pure/List.join 272 B $({\color{gray}0\%})$
pure/List.flatten 272 B $({\color{gray}0\%})$
pure/List.take 272 B $({\color{gray}0\%})$
pure/List.drop 272 B $({\color{gray}0\%})$
pure/List.foldRight 272 B $({\color{gray}0\%})$
pure/List.merge 272 B $({\color{gray}0\%})$
pure/List.chunks 272 B $({\color{gray}0\%})$
pure/Queue 272 B $({\color{gray}0\%})$

Garbage Collection

pure/List.split 3.05 MiB $({\color{gray}0\%})$
pure/List.all 328 B $({\color{gray}0\%})$
pure/List.any 328 B $({\color{gray}0\%})$
pure/List.map 3.05 MiB $({\color{gray}0\%})$
pure/List.filter 3.05 MiB $({\color{gray}0\%})$
pure/List.filterMap 3.05 MiB $({\color{gray}0\%})$
pure/List.partition 3.05 MiB $({\color{gray}0\%})$
pure/List.join 3.05 MiB $({\color{gray}0\%})$
pure/List.flatten 3.05 MiB $({\color{gray}0\%})$
pure/List.take 3.05 MiB $({\color{gray}0\%})$
pure/List.drop 328 B $({\color{gray}0\%})$
pure/List.foldRight 1.53 MiB $({\color{gray}0\%})$
pure/List.merge 4.58 MiB $({\color{gray}0\%})$
pure/List.chunks 7.63 MiB $({\color{gray}0\%})$
pure/Queue 18.31 MiB $({\color{gray}0\%})$
bench/Queues.bench.mo $({\color{red}+0.87\%})$

Different queue implementations

Compare the performance of the following queue implementations:

  • pure/Queue: The default immutable double-ended queue implementation.
    • Pros: Good amortized performance, meaning that the average cost of operations is low O(1).
    • Cons: In worst case, an operation can take O(size) time rebuilding the queue as demonstrated in the Pop front 2 elements scenario.
  • pure/RealTimeQueue
    • Pros: Every operation is guaranteed to take at most O(1) time and space.
    • Cons: Poor amortized performance: Instruction cost is on average 3x for pop and 8x for push compared to pure/Queue.
  • mutable Queue
    • Pros: Also O(1) guarantees with a lower constant factor than pure/RealTimeQueue. Amortized performance is comparable to pure/Queue.
    • Cons: It is mutable and cannot be used in shared types (not shareable).

Instructions: ${\color{red}+0.87\%}$
Heap: ${\color{gray}0\%}$
Stable Memory: ${\color{gray}0\%}$
Garbage Collection: ${\color{gray}0\%}$

Instructions

pure/Queue pure/RealTimeQueue mutable Queue
Initialize with 2 elements 3_156 $({\color{red}+2.07\%})$ 2_368 $({\color{red}+2.78\%})$ 3_104 $({\color{red}+2.11\%})$
Push 500 elements 90_777 $({\color{red}+0.07\%})$ 744_283 $({\color{red}+0.01\%})$ 219_389 $({\color{red}+0.05\%})$
Pop front 2 elements 87_030 $({\color{red}+0.07\%})$ 4_510 $({\color{red}+1.44\%})$ 3_911 $({\color{red}+1.66\%})$
Pop 150 front&back 92_159 $({\color{red}+0.07\%})$ 304_972 $({\color{red}+0.02\%})$ 124_645 $({\color{red}+0.05\%})$

Heap

pure/Queue pure/RealTimeQueue mutable Queue
Initialize with 2 elements 324 B $({\color{gray}0\%})$ 300 B $({\color{gray}0\%})$ 352 B $({\color{gray}0\%})$
Push 500 elements 8.08 KiB $({\color{gray}0\%})$ 8.17 KiB $({\color{gray}0\%})$ 19.8 KiB $({\color{gray}0\%})$
Pop front 2 elements 240 B $({\color{gray}0\%})$ 240 B $({\color{gray}0\%})$ 192 B $({\color{gray}0\%})$
Pop 150 front&back -4.42 KiB $({\color{gray}0\%})$ -492 B $({\color{gray}0\%})$ -11.45 KiB $({\color{gray}0\%})$

Garbage Collection

pure/Queue pure/RealTimeQueue mutable Queue
Initialize with 2 elements 508 B $({\color{gray}0\%})$ 444 B $({\color{gray}0\%})$ 456 B $({\color{gray}0\%})$
Push 500 elements 10.1 KiB $({\color{gray}0\%})$ 137.84 KiB $({\color{gray}0\%})$ 344 B $({\color{gray}0\%})$
Pop front 2 elements 12.19 KiB $({\color{gray}0\%})$ 528 B $({\color{gray}0\%})$ 424 B $({\color{gray}0\%})$
Pop 150 front&back 15.61 KiB $({\color{gray}0\%})$ 49.66 KiB $({\color{gray}0\%})$ 12.1 KiB $({\color{gray}0\%})$
No previous results found "/home/runner/work/motoko-core/motoko-core/.bench/Sort.bench.json"
bench/Sort.bench.mo $({\color{gray}0\%})$

Sort

VarArray.sortInPlace profiling

Instructions: ${\color{gray}0\%}$
Heap: ${\color{gray}0\%}$
Stable Memory: ${\color{gray}0\%}$
Garbage Collection: ${\color{gray}0\%}$

Instructions

100 1000 10000 12000 100000 1000000
old-sort 205_485 2_681_849 35_810_354 43_067_857 442_387_583 5_046_582_633
new-sort 72_494 1_123_252 16_084_259 19_445_631 201_432_959 2_423_397_137

Heap

100 1000 10000 12000 100000 1000000
old-sort 272 B 272 B 272 B 272 B 272 B 308 B
new-sort 272 B 272 B 272 B 272 B 272 B 308 B

Garbage Collection

100 1000 10000 12000 100000 1000000
old-sort 736 B 4.23 KiB 39.39 KiB 47.2 KiB 390.95 KiB 3.82 MiB
new-sort 536 B 2.28 KiB 19.86 KiB 23.77 KiB 195.64 KiB 1.91 MiB

Note: Renamed benchmarks cannot be compared. Refer to the current baseline for manual comparison.

- Emit gitignored test/generated/QueueOracleFixtures.mo; replay all in Motoko

- Filter commands like modelRun; decode ops via toString for cloned commands

- test:mops runs generate:oracle-fixtures first; remove single committed fixture

Made-with: Cursor
- Format List.mo and Queue.oracleReplay.test.mo

- Add Next changelog entry for oracle replay tests (#488)

Made-with: Cursor
- fast-check add/remove/get vs OracleNatTextMap; 100 generated fixtures

- Map.oracleReplay.test.mo; chain map emitter in generate:oracle-fixtures
- emitOracleFixtures orchestrator; CLI --seed or env; stderr repro hint

- Optional ORACLE_PBT_SEED for TS fast-check; update replay test comments
@christoph-dfinity christoph-dfinity changed the title Property-based oracle testing: TypeScript fast-check + Motoko queue replay tests: add property based testing using TypeScript oracles Apr 15, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant