aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification/lux/abstract/hash.lux
blob: 2b6aa5cd658363a84a7bc21a5b200e501bd7e82f (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
(.require
 [library
  [lux (.except)
   [abstract
    [monad (.only do)]
    [\\specification
     ["[0]S" equivalence]]]
   [math
    ["[0]" random (.only Random)]
    [number
     ["n" nat]]]
   [test
    ["_" property (.only Test)]]]]
 [\\library
  ["[0]" /]])

(def .public (spec (open "/#[0]") random)
  (All (_ a) (-> (/.Hash a) (Random a) Test))
  (do random.monad
    [parameter random
     subject random]
    (all _.and
         (_.for [/.equivalence]
                (equivalenceS.spec /#equivalence random))
         (_.coverage [/.Hash /.hash]
           (if (/#= parameter subject)
             (n.= (/#hash parameter) (/#hash subject))
             true))
         )))