Skip to content

Commit

Permalink
Add a test comparing the reference implemntations of foldl,
Browse files Browse the repository at this point in the history
`scanl` and `iterate` to their primitive implementations.
  • Loading branch information
robdockins committed Dec 7, 2021
1 parent 22af290 commit 928cc98
Show file tree
Hide file tree
Showing 3 changed files with 44 additions and 0 deletions.
12 changes: 12 additions & 0 deletions tests/regression/reference.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
import Cryptol::Reference as Ref

// NB, using subtraction here because is is not commutative or associative

property foldl_eq (z:Integer) (xs:[10]Integer) =
foldl (-) z xs == Ref::foldl (-) z xs

property scanl_eq (z:Integer) (xs:[10]Integer) =
scanl (-) z xs == Ref::scanl (-) z xs

property iterate_eq (z:Integer) (i:[8]) =
(iterate (\x -> x + 1) z)@i == (Ref::iterate (\x -> x + 1) z)@i
10 changes: 10 additions & 0 deletions tests/regression/reference.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
:l reference.cry

:set tests=1000
:check

:set prover=sbv-z3
:prove

:set prover=w4-z3
:prove
22 changes: 22 additions & 0 deletions tests/regression/reference.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
Loading module Cryptol
Loading module Cryptol
Loading module Cryptol::Reference
Loading module Main
property foldl_eq Using random testing.
Testing... Passed 1000 tests.
property scanl_eq Using random testing.
Testing... Passed 1000 tests.
property iterate_eq Using random testing.
Testing... Passed 1000 tests.
:prove foldl_eq
Q.E.D.
:prove scanl_eq
Q.E.D.
:prove iterate_eq
Q.E.D.
:prove foldl_eq
Q.E.D.
:prove scanl_eq
Q.E.D.
:prove iterate_eq
Q.E.D.

0 comments on commit 928cc98

Please sign in to comment.