blob: cd9a966dacd0dfdd07446025690571a52d9adc06 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
(.using
[library
[lux (.except)
["_" test (.only Test)]
[abstract
[monad (.only do)]
[\\specification
[functor
["$[0]" contravariant]]]]
[data
["[0]" bit (.open: "[1]#[0]" equivalence)]]
[math
["[0]" random]
[number
["[0]" nat]]]]]
[\\library
["[0]" / (.only Hash)
[//
[equivalence (.only Equivalence)]]]])
(def: .public test
Test
(do random.monad
[leftN random.nat
rightN random.nat
.let [hash (is (Equivalence (/.Hash Nat))
(implementation
(def: (= (open "left#[0]") (open "right#[0]"))
(and (bit#= (left#= (left#hash leftN) (left#hash leftN))
(right#= (right#hash leftN) (right#hash leftN)))
(bit#= (left#= (left#hash rightN) (left#hash rightN))
(right#= (right#hash rightN) (right#hash rightN)))
(bit#= (left#= (left#hash leftN) (left#hash rightN))
(right#= (right#hash leftN) (right#hash rightN)))))))]]
(<| (_.covering /._)
(all _.and
(_.for [/.functor]
($contravariant.spec hash nat.hash /.functor))
))))
|
