plausible/Test/KeyValueStoreExample/TestKeyValueStoreCheckerGenerators.lean at chamelean/main · codyroux/plausible · GitHub

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
/-
Copyright (c) 2026 AWS. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: AWS
-/
import Test.KeyValueStoreExample.KeyValueStore
import Plausible.Arbitrary
import Plausible.DeriveArbitrary
import Plausible.Chamelean.ArbitrarySizedSuchThat
import Plausible.Chamelean.DeriveChecker
import Plausible.Chamelean.DeriveConstrainedProducer
import Plausible.Chamelean.EnumeratorCombinators
import Plausible.Chamelean.GeneratorCombinators
import Plausible.Attr

open Plausible
open KeyValueStore

-- Suppress warnings for unused variables in derived generators/checkers
set_option linter.unusedVariables false

-- Suppress warnings for redundant pattern-match cases in derived generators/checkers
set_option match.ignoreUnusedAlts true

/-- We override the default `Arbitrary` for `String`s so that we only produce strings of length 1
    where the string is a single letter from `A` to `I` -/
instance instKeyValueStoreArbitraryString : Arbitrary String where
  arbitrary := GeneratorCombinators.elementsWithDefault "A" ["A", "B", "C", "D", "E", "F", "G", "H", "I"]

---------------------------------------------------------------------------------------------------------------------------------------
-- Derived Checkers & Generators (everything below in this file is automatically generated by Chamelean)
---------------------------------------------------------------------------------------------------------------------------------------


#guard_msgs(drop info, drop warning) in
derive_generator (fun k s2 => ∃ (s1 : List (String × String)), KeyValueStore.RemoveKV k s1 s2)

#guard_msgs(drop info, drop warning) in
derive_generator (fun ka s1a => ∃ (s2a : List (String × String)), KeyValueStore.RemoveKV ka s1a s2a)

#guard_msgs(drop info, drop warning) in
derive_generator (fun k v s2 => ∃ (s1 : List (String × String)), KeyValueStore.AddKV k v s1 s2)

#guard_msgs(drop info, drop warning) in
derive_generator (fun k v s1 => ∃ (s2 : List (String × String)), KeyValueStore.AddKV k v s1 s2)

#guard_msgs(drop info, drop warning) in
derive_generator (fun k x_1 s2 => ∃ (v : String), KeyValueStore.AddKV k v x_1 s2)

#guard_msgs(drop info, drop warning) in
derive_checker (fun s kv => KeyValueStore.LookupKV s kv)

#guard_msgs(drop info, drop warning) in
derive_generator (fun kv => ∃ (s1 : List (String × String)), KeyValueStore.LookupKV s1 kv)

#guard_msgs(drop info, drop warning) in
derive_checker (fun k2 v s_1 s2 => KeyValueStore.AddKV k2 v s_1 s2)

#guard_msgs(drop info) in
derive_checker (fun k s s2 => RemoveKV k s s2)

#guard_msgs(drop info, drop warning) in
derive_generator (fun x => ∃ (s : List (String × String)), KeyValueStore.EvalStateApiCall s x)

#guard_msgs(drop info, drop warning) in
derive_generator (fun s => ∃ (kv : StateResult × String × Nat × String), KeyValueStore.LookupKV s kv)

#guard_msgs(drop info, drop warning) in
derive_generator (fun s => ∃ (nb : Nat × List (String × String)), KeyValueStore.GetBucket s nb)

#guard_msgs(drop info, drop warning) in
derive_generator (fun v x_1 s2 => ∃ (k : _), KeyValueStore.AddKV k v x_1 s2)

#guard_msgs(drop info, drop warning) in
derive_generator (fun x => ∃ (foo : StateAPICall × StateResult × List (String × String)), KeyValueStore.EvalStateApiCall x foo)

#guard_msgs(drop info, drop warning) in
derive_generator (fun s => ∃ (crns : APICall × Result × (Nat × List (Nat × List (String × String)))), KeyValueStore.EvalApiCall s crns)

#guard_msgs(drop info, drop warning) in
derive_generator (fun s => ∃ (o : List (APICall × Result) × (Nat × List (Nat × List (String × String)))), KeyValueStore.EvalApiCalls s o)


/- Uncommenting the following line results in random sequences of API Calls, such as:

```lean
([(KeyValueStore.APICall.CreateBucket, KeyValueStore.Result.Created 0),
  (KeyValueStore.APICall.CreateBucket, KeyValueStore.Result.Created 1),
  (KeyValueStore.APICall.DeleteBucket 0, KeyValueStore.Result.Removed),
  (KeyValueStore.APICall.DeleteBucket 1, KeyValueStore.Result.Removed),
  (KeyValueStore.APICall.CreateBucket, KeyValueStore.Result.Created 2),
  (KeyValueStore.APICall.DeleteBucket 2, KeyValueStore.Result.Removed),
  (KeyValueStore.APICall.CreateBucket, KeyValueStore.Result.Created 3),
  (KeyValueStore.APICall.DeleteBucket 3, KeyValueStore.Result.Removed),
  (KeyValueStore.APICall.CreateBucket, KeyValueStore.Result.Created 4),
  (KeyValueStore.APICall.CreateBucket, KeyValueStore.Result.Created 5),
  (KeyValueStore.APICall.DeleteBucket 4, KeyValueStore.Result.Removed),
  (KeyValueStore.APICall.CreateBucket, KeyValueStore.Result.Created 6),
  (KeyValueStore.APICall.DeleteBucket 5, KeyValueStore.Result.Removed),
  (KeyValueStore.APICall.CreateBucket, KeyValueStore.Result.Created 7),
  (KeyValueStore.APICall.DeleteBucket 6, KeyValueStore.Result.Removed),
  (KeyValueStore.APICall.OpBucket 7 (KeyValueStore.StateAPICall.Get "B" none),
   KeyValueStore.Result.OpResult (KeyValueStore.StateResult.NoSuchKeyFailure)),
  (KeyValueStore.APICall.DeleteBucket 7, KeyValueStore.Result.Removed),
  (KeyValueStore.APICall.CreateBucket, KeyValueStore.Result.Created 8),
  (KeyValueStore.APICall.OpBucket 8 (KeyValueStore.StateAPICall.KeyExists "E"),
   KeyValueStore.Result.OpResult (KeyValueStore.StateResult.NoSuchKeyResult))],
 9,
 [(8, [])])
```

-/
#guard_msgs(drop info) in
#eval Gen.run (ArbitrarySizedSuchThat.arbitrarySizedST (fun crs => KeyValueStore.EvalApiCalls (0, []) crs) 20) 20