blob: f01773f369d221bf4cf98f8ea4501aa6aa4493cb (
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
|
(.using
[library
[lux (.except)
[abstract
[functor (.only Functor)]
[apply (.only Apply)]
[monad (.only Monad)]]
[type
[primitive (.except)]]]])
(primitive: .public (Policy brand value label)
value
(type: .public (Can_Upgrade brand label value)
(-> value (Policy brand value label)))
(type: .public (Can_Downgrade brand label value)
(-> (Policy brand value label) value))
(type: .public (Privilege brand label)
(Record
[#can_upgrade (Can_Upgrade brand label)
#can_downgrade (Can_Downgrade brand label)]))
(type: .public (Delegation brand from to)
(All (_ value)
(-> (Policy brand value from)
(Policy brand value to))))
(def: .public (delegation downgrade upgrade)
(All (_ brand from to)
(-> (Can_Downgrade brand from) (Can_Upgrade brand to)
(Delegation brand from to)))
(|>> downgrade upgrade))
(type: .public (Context brand scope label)
(-> (Privilege brand label)
(scope label)))
(def: privilege
Privilege
[#can_upgrade (|>> abstraction)
#can_downgrade (|>> representation)])
(def: .public (with_policy context)
(All (_ brand scope)
(Ex (_ label)
(-> (Context brand scope label)
(scope label))))
(context ..privilege))
(def: (of_policy constructor)
(-> Type Type)
(type (All (_ brand label)
(constructor (All (_ value) (Policy brand value label))))))
(implementation: .public functor
(~ (..of_policy Functor))
(def: (each f fa)
(|> fa representation f abstraction)))
(implementation: .public apply
(~ (..of_policy Apply))
(def: functor ..functor)
(def: (on fa ff)
(abstraction ((representation ff) (representation fa)))))
(implementation: .public monad
(~ (..of_policy Monad))
(def: functor ..functor)
(def: in (|>> abstraction))
(def: conjoint (|>> representation)))
)
(template [<brand> <value> <upgrade> <downgrade>]
[(primitive: .public <brand>
Any
(type: .public <value>
(Policy <brand>))
(type: .public <upgrade>
(Can_Upgrade <brand>))
(type: .public <downgrade>
(Can_Downgrade <brand>))
)]
[Privacy Private Can_Conceal Can_Reveal]
[Safety Safe Can_Trust Can_Distrust]
)
|
