blob: 0137ba9ae70d8b57b1ed51f73f1e707ca0f48e5a (
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
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
(.using
[library
[lux (.except)
["_" test (.only Test)]
["[0]" type (.open: "[1]#[0]" equivalence)]
[abstract
[monad (.only do)]
["[0]" predicate]
[\\specification
["$[0]" equivalence]
["$[0]" order]
["$[0]" monoid]
["$[0]" codec]]]
[control
["[0]" try]
["[0]" exception]]
[data
["[0]" product]
["[0]" bit (.open: "[1]#[0]" equivalence)]]
[math
["[0]" random (.only Random)]
[number
["i" int]]]]]
["$[0]" //
["[1]" modulus]]
[\\library
["[0]" / (.only)
["/[1]" //
["[1]" modulus]]]])
(def: .public (random modulus)
(All (_ %) (-> (//.Modulus %) (Random (/.Mod %))))
(# random.monad each
(/.modular modulus)
random.int))
(def: .public test
Test
(<| (_.covering /._)
(_.for [/.Mod])
(do random.monad
[param##% ($//.random +1,000,000)
param (..random param##%)
subject##% (random.only (predicate.and (|>> //.divisor (i.> +2))
(|>> (//.= param##%) not))
($//.random +1,000,000))
subject (..random subject##%)
another (..random subject##%)]
(`` (all _.and
(_.for [/.equivalence /.=]
($equivalence.spec /.equivalence (..random subject##%)))
(_.for [/.order /.<]
($order.spec /.order (..random subject##%)))
(~~ (template [<composite> <monoid>]
[(_.for [<monoid> <composite>]
($monoid.spec /.equivalence (<monoid> subject##%) (..random subject##%)))]
[/.+ /.addition]
[/.* /.multiplication]
))
(_.for [/.codec]
($codec.spec /.equivalence (/.codec subject##%) (..random subject##%)))
(_.coverage [/.incorrect_modulus]
(case (|> param
(# (/.codec param##%) encoded)
(# (/.codec subject##%) decoded))
{try.#Failure error}
(exception.match? /.incorrect_modulus error)
{try.#Success _}
false))
(_.coverage [/.modulus]
(and (type#= (type_of (/.modulus subject))
(type_of (/.modulus subject)))
(not (type#= (type_of (/.modulus subject))
(type_of (/.modulus param))))))
(_.coverage [/.modular /.value]
(/.= subject
(/.modular (/.modulus subject) (/.value subject))))
(_.coverage [/.>]
(bit#= (/.> another subject)
(/.< subject another)))
(_.coverage [/.<= /.>=]
(bit#= (/.<= another subject)
(/.>= subject another)))
(_.coverage [/.-]
(let [zero (/.modular (/.modulus subject) +0)]
(and (/.= zero
(/.- subject subject))
(/.= subject
(/.- zero subject)))))
(_.coverage [/.inverse]
(let [one (/.modular (/.modulus subject) +1)
co_prime? (i.co_prime? (//.divisor (/.modulus subject))
(/.value subject))]
(case (/.inverse subject)
{.#Some subject^-1}
(and co_prime?
(|> subject
(/.* subject^-1)
(/.= one)))
{.#None}
(not co_prime?))))
(_.coverage [/.adapter]
(<| (try.else false)
(do try.monad
[copy##% (//.modulus (//.divisor subject##%))
adapt (/.adapter subject##% copy##%)]
(in (|> subject
/.value
(/.modular copy##%)
adapt
(/.= subject))))))
(_.coverage [/.moduli_are_not_equal]
(case (/.adapter subject##% param##%)
{try.#Failure error}
(exception.match? /.moduli_are_not_equal error)
{try.#Success _}
false))
)))))
|
