-
Notifications
You must be signed in to change notification settings - Fork 19
/
TraceGens.v
486 lines (444 loc) · 22.1 KB
/
TraceGens.v
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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
(*
The ChainTrace datatype is defined as a ChainedList of ChainStates and ChainSteps.
This file defines a generator combinator, gChain, for the ChainBuilder type.
From this, a generator/arbitrary instance for the ChainTrace type is derived automatically.
This file also contains checker combinator over ChainBuilders/ChainTraces,
like forAllChainTrace, reachableFrom_chaintrace, and pre_post_assertion.
*)
Global Set Warnings "-extraction-logical-axiom".
From QuickChick Require Import QuickChick. Import QcNotation.
From ConCert Require Import Blockchain.
From ConCert Require Import Serializable.
From ConCert Require Import BoundedN.
From ConCert Require Import ResultMonad.
From ConCert Require Import ChainedList.
From ConCert.Execution.QCTests Require Import TestUtils ChainPrinters .
From ExtLib.Structures Require Import Monads.
Import MonadNotation. Open Scope monad_scope.
From Coq Require Import ZArith.
From Coq Require Import List.
Import BoundedN.Stdpp.
Import ListNotations.
Section TraceGens.
Context {ChainBuilder : ChainBuilderType}.
Context `{Show ChainBuilder}.
Context `{Show ChainState}.
(* Deconstructs a ChainTrace to a list of blockheaders list of the minimum information
needed to reconstruct a ChainTrace, that being a list of block headers and
chain_state_queues from each step_block *)
Fixpoint trace_blocks {from to} (trace : ChainTrace from to) : list (BlockHeader * list Action) :=
match trace with
| snoc trace' (Blockchain.step_block _ _ header _ _ _ _ as step) =>
trace_blocks trace' ++ [(header, chain_state_queue (snd (chainstep_states step)))]
| snoc trace' _ => trace_blocks trace'
| clnil => []
end.
(* Reconstructs list of block information (blockheaders and queues) to a ChainBuilder.
It trims any empty blocks that can be removed without invalidating execution of
the remaining actions.
Also removes any actions that cannot be executed *)
Fixpoint build_chain_builder (init_cb : ChainBuilder) blocks : result ChainBuilder AddBlockError :=
(* Instead of using the original header we need override height and finalized_height
since the blockchain requires that the height always grows by one and if we trim and keep the
height in the original header then the height would increase by two *)
let new_header header :=
{| block_height := S (chain_height init_cb);
block_slot := header.(block_slot);
block_finalized_height := finalized_height init_cb;
block_creator := header.(block_creator);
block_reward := header.(block_reward); |} in
(* Remove any actions that are no longer valid due to earlier actions
that could have been removed by the shrinker *)
let try_remove_invalid_acts header acts blocks :=
let valid_acts := fold_left (fun acts act =>
match builder_add_block init_cb (new_header header) (acts ++ [act]) with
| Ok cb => acts ++ [act]
| Err error => acts
end ) acts [] in
match builder_add_block init_cb (new_header header) valid_acts with (* TODO: also try to trim block here if valid_acts is empty *)
| Ok cb => build_chain_builder cb blocks
| Err error => Err error
end in
let build_block header acts blocks :=
match builder_add_block init_cb (new_header header) acts with
| Ok cb => build_chain_builder cb blocks
| Err error => try_remove_invalid_acts header acts blocks
end in
(* Attempt to trim block *)
let try_trim header blocks :=
let trimmed_result := build_chain_builder init_cb blocks in
match trimmed_result with
| Ok cb => Ok cb
| Err error => build_block header [] blocks
end in
match blocks with
| [] => Ok init_cb
| (header, []) :: xs => try_trim header xs
| (header, acts) :: xs => build_block header acts xs
end.
(* Reconstructs a list of ChainBuilders *)
Fixpoint rebuild_chains (shrunk_chains : list (list (BlockHeader * list Action))) init_cb : list ChainBuilder :=
match shrunk_chains with
| [] => []
| block :: blocks =>
match build_chain_builder init_cb block with
| Ok cb => cb :: rebuild_chains blocks init_cb
| Err error => rebuild_chains blocks init_cb
end
end.
(* Alternative version of ordinary list shrinker that does not attempt to shrink list elements *)
Fixpoint shrinkListAux_ {A} (l : list A) : list (list A) :=
match l with
| [] => []
| x :: xs => xs :: map (fun xs' : list A => x :: xs') (shrinkListAux_ xs)
end.
(* Shrink list of blocks by trying all combinations of removing one action *)
Fixpoint shrinkChainBuilderAux (blocks : list (BlockHeader * list Action)) : list (list (BlockHeader * list Action)) :=
match blocks with
| [] => []
| block :: blocks' =>
let '(header, acts) := block in
let acts_shrunk := shrinkListAux_ acts in
let block_shrunk := map (fun acts => (header, acts)) acts_shrunk in
(map (fun block' => block' :: blocks') block_shrunk) ++
map (fun xs => block :: xs) (shrinkChainBuilderAux blocks')
end.
(* Shrinker for ChainBuilders, it will only try to shrink the blocks and their action queues,
it will not attempt to shrink parameters of any actions *)
Instance shrinkChainBuilder : Shrink ChainBuilder :=
{
shrink cb :=
let cb_blocks := trace_blocks cb.(builder_trace) in
let shrunk_blocks := shrinkChainBuilderAux cb_blocks in
rebuild_chains shrunk_blocks builder_initial
}.
(* Adds a block with 50 money as reward. This will be used for all testing. *)
Definition add_block (chain : ChainBuilder) acts : result ChainBuilder AddBlockError :=
let header :=
{| block_height := S (chain_height chain);
block_slot := S (current_slot chain);
block_finalized_height := finalized_height chain;
block_creator := creator;
block_reward := 50; |} in
builder_add_block chain header acts.
Definition gAdd_block (cb : ChainBuilder)
(gActOptFromChainSized : Environment -> nat -> GOpt Action)
(act_depth : nat)
(max_acts_per_block : nat)
: G (result ChainBuilder AddBlockError) :=
acts <- optToVector max_acts_per_block (gActOptFromChainSized cb act_depth) ;;
returnGen (add_block cb acts).
(* Given a function from nat to a generator, try the generator on decreasing number until one returns Ok *)
Fixpoint try_decreasing {T E} (default : E) (n : nat) (g : nat -> G (result T E)) : G (result T E) :=
match n with
| 0 => returnGen (Err default)
| S n' =>
ma <- (g n) ;;
match ma with
| Err e => try_decreasing default n' g
| Ok r => returnGen (Ok r)
end
end.
Definition gChain (init_lc : ChainBuilder)
(gActOptFromChainSized : Environment -> nat -> GOpt Action)
(max_length : nat)
(act_depth : nat)
(max_acts_per_block : nat)
: G ChainBuilder :=
let gAdd_block' lc max_acts := gAdd_block lc gActOptFromChainSized act_depth max_acts in
let default_error := action_evaluation_depth_exceeded in (* Not ideal approach, but it suffices for now *)
let try_twice g := backtrack_result default_error [(1, g);(1, g)] in
let try_decreasing g := try_decreasing default_error max_acts_per_block (fun n => try_twice (g n)) in
(* Try decreasing max_acts_per_block, this is needed in some cases since there might be blocks
where it is not possible to generate max_acts_per_block number of valid actions *)
let fix rec n (lc : ChainBuilder) : G ChainBuilder :=
match n with
| 0 => returnGen lc
| S n => lc' <- try_decreasing (gAdd_block' lc) ;; (* heuristic: try twice for more expected robustness *)
match lc' with
| Ok lc' => rec n lc'
(* if no new chain could be generated without error, return the old chain *)
| err => returnGen lc
end
end in
rec max_length init_lc.
(* Generator that generates blocks of invalid actions.
It will return a ChainBuilder and a list of actions that will
cause an error if the actions are added as a new block to the ChainBuilder *)
Definition gInvalidAction
(init_lc : ChainBuilder)
(gActOptFromChainSized : Environment -> nat -> GOpt Action)
(max_length : nat)
(act_depth : nat)
(max_acts_per_block : nat)
: G (ChainBuilder * list Action) :=
let fix rec n (lc : ChainBuilder) : G (ChainBuilder * list Action) :=
match n with
| 0 => returnGen (lc, []) (* max_length was reached without any errors *)
| S n =>
acts <- optToVector max_acts_per_block (gActOptFromChainSized lc act_depth) ;;
match (TraceGens.add_block lc acts) with
| Ok lc' => rec n lc'
(* If no new chain could be generated without error, return the trace and action list *)
| err => returnGen (lc, acts)
end
end in
rec max_length init_lc.
Definition get_reachable {to} : ChainTrace empty_state to -> reachable to := fun t => inhabits t.
Definition gReachableFromTrace {to} (gtrace : G (ChainTrace empty_state to)) : G (reachable to) :=
bindGen gtrace (fun trace =>
returnGen (get_reachable trace)).
Global Instance shrinkReachable : Shrink {to : ChainState | reachable to} :=
{|
shrink a := [a]
|}.
Global Instance genReachableSized `{GenSized ChainBuilder} : GenSized {to | reachable to}.
Proof.
constructor.
intros H2.
apply H1 in H2.
apply (bindGen H2).
intros cb.
remember (builder_trace cb) as trace.
apply returnGen.
eapply exist.
apply get_reachable.
apply trace.
Defined.
Global Instance shrinkChainTraceSig : Shrink {to : ChainState & ChainTrace empty_state to} :=
{|
shrink a := [a]
|}.
Global Instance genChainTraceSigSized `{GenSized ChainBuilder} : GenSized {to : ChainState & ChainTrace empty_state to}.
Proof.
constructor.
intros n.
apply H1 in n.
apply (bindGen n).
intros cb.
remember (builder_trace cb) as trace.
apply returnGen.
eapply existT.
eauto.
Defined.
(* Checker combinators on ChainBuilder *)
Definition forAllChainBuilder {prop : Type}
`{Checkable prop}
(maxLength : nat)
(init_lc : ChainBuilder)
(gTrace : ChainBuilder -> nat -> G ChainBuilder)
(pf : ChainBuilder -> prop)
: Checker :=
forAllShrink (gTrace init_lc maxLength)
shrink (fun cb => checker (pf cb)).
(* Gathers all ChainStates from a ChainTrace in a list, appearing in order. *)
(* Currently not tail-call optimized. Can be improved if needed. *)
Fixpoint trace_states {from to} (trace : ChainTrace from to) : list ChainState :=
match trace with
| snoc trace' step => trace_states trace' ++ [snd (chainstep_states step)]
| clnil => []
end.
(* Variant that only gathers ChainStates of step_block steps in the trace. *)
Fixpoint trace_states_step_block {from to} (trace : ChainTrace from to) : list ChainState :=
match trace with
| snoc trace' (Blockchain.step_block _ _ _ _ _ _ _ as step) =>
trace_states_step_block trace' ++ [snd (chainstep_states step)]
| snoc trace' _ => trace_states_step_block trace'
| clnil => []
end.
(* Gather execution information for each step_action in a ChainTrace *)
Fixpoint trace_states_step_action {from to} (trace : ChainTrace from to) : list (Action * list Action * ChainState * ChainState) :=
match trace with
| snoc trace' (Blockchain.step_action _ _ act _ new_acts _ _ _ as step) =>
let '(from, to) := chainstep_states step in
trace_states_step_action trace' ++ [(act, new_acts, from, to)]
| snoc trace' _ => trace_states_step_action trace'
| clnil => []
end.
(* Asserts that a ChainState property holds for all step_block ChainStates in a ChainTrace *)
Definition ChainTrace_ChainTraceProp {prop : Type}
{from to}
`{Checkable prop}
(trace : ChainTrace from to)
(pf : ChainState -> prop)
: Checker :=
let printOnFail (cs : ChainState) : Checker := whenFail (show cs) (checker (pf cs)) in
let trace_list := trace_states_step_block trace in
discard_empty trace_list (conjoin_map printOnFail).
(* -------------------- Checker combinators on traces -------------------- *)
(* Asserts that a ChainState property holds on all ChainStates in a ChainTrace *)
Definition forAllChainState {prop : Type}
`{Checkable prop}
(maxLength : nat)
(init_lc : ChainBuilder)
(gTrace : ChainBuilder -> nat -> G ChainBuilder)
(pf : ChainState -> prop)
: Checker :=
let printOnFail (cs : ChainState) : Checker := whenFail (show cs) (checker (pf cs)) in
forAllShrink (gTrace init_lc maxLength) shrink
(fun cb => discard_empty (trace_states cb.(builder_trace)) (conjoin_map printOnFail)).
(* Asserts that a ChainState property holds on all step_block ChainStates in a ChainTrace *)
Definition forAllBlocks {prop : Type}
`{Checkable prop}
(maxLength : nat)
(init_lc : ChainBuilder)
(gTrace : ChainBuilder -> nat -> G ChainBuilder)
(pf : ChainState -> prop)
: Checker :=
forAllShrink (gTrace init_lc maxLength) shrink
(fun cb => ChainTrace_ChainTraceProp cb.(builder_trace) pf).
(* Checker combinators on ChainTrace, asserting holds a property on
each pair of succeeding ChainStates in the trace. *)
Definition forAllChainStatePairs {prop : Type}
`{Checkable prop}
(maxLength : nat)
(init_lc : ChainBuilder)
(gTrace : ChainBuilder -> nat -> G ChainBuilder)
(pf : ChainState -> ChainState -> prop)
: Checker :=
(* helper function folding over the trace*)
let last_cstate {from to} (trace : ChainTrace from to) := to in
let fix all_statepairs {from to : ChainState} (trace : ChainTrace from to) prev_bstate : Checker :=
match trace with
| snoc trace' step =>
match step with
| Blockchain.step_block _ _ _ _ _ _ _ =>
(* next_bstate has acts, bstate_before_step_block has no acts *)
let '(bstate_before_step_block, next_bstate) := chainstep_states step in
conjoin [(checker (pf next_bstate prev_bstate)); all_statepairs trace' bstate_before_step_block]
| _ => all_statepairs trace' prev_bstate
end
| clnil => checker true
end in
forAllShrink (gTrace init_lc maxLength) shrink
(fun cb => all_statepairs cb.(builder_trace) (last_cstate cb.(builder_trace))).
(* Asserts that property holds on all action evaluations *)
Definition forAllActionExecution {prop : Type}
`{Checkable prop}
(maxLength : nat)
(init_lc : ChainBuilder)
(gTrace : ChainBuilder -> nat -> G ChainBuilder)
(pf : Action -> list Action -> ChainState -> ChainState -> prop)
: Checker :=
let printOnFail x : Checker :=
let '(action, new_acts, cs_from, cs_to) := x in
whenFail (show cs_from) (checker (pf action new_acts cs_from cs_to)) in
let trace_list cb := trace_states_step_action cb.(builder_trace) in
forAllShrink (gTrace init_lc maxLength) shrink
(fun cb => discard_empty (trace_list cb) (conjoin_map printOnFail)).
(* Asserts that a boolean predicate holds for at least one ChainState in the given ChainTrace *)
Definition existsb_chaintrace {from to}
(pf : ChainState -> bool)
(trace : ChainTrace from to) : bool :=
existsb pf (trace_states trace).
(* Asserts that a ChainState satisfying a given predicate is reachable from the given trace generator. *)
Definition reachableFromSized_chaintrace
(maxLength : nat)
(init_lc : ChainBuilder)
(gTrace : ChainBuilder -> nat -> G ChainBuilder )
(pf : ChainState -> bool)
: Checker :=
existsP (gTrace init_lc maxLength) (fun cb =>
existsb_chaintrace pf cb.(builder_trace)).
Definition reachableFrom_chaintrace init_lc gTrace pf : Checker :=
sized (fun n => reachableFromSized_chaintrace n init_lc gTrace pf).
(* This property states that if there is a reachable chainstate satisfying the reachable_prop predicate,
then all succeeding chainstates must satisfy implied_prop *)
Definition reachableFrom_implies_chaintracePropSized
{A prop : Type}
`{Checkable prop}
(maxLength : nat)
(init_cb : ChainBuilder)
(gTrace : ChainBuilder -> nat -> G ChainBuilder)
(reachable_prop : ChainState -> option A)
(implied_prop : A -> list ChainState -> list ChainState -> prop)
: Checker :=
forAllShrink (gTrace init_cb maxLength) shrink
(fun cb =>
let trace := cb.(builder_trace) in
let reachable_prop_bool := isSome o reachable_prop in
let tracelist := trace_states_step_block trace in
match split_at_first_satisfying reachable_prop_bool tracelist with
| Some ((x::xs) as pre, post) =>
(* last_step is the element satisfying reachable_prop_bool *)
let last_step := (List.last pre x) in
isSomeCheck (reachable_prop last_step)
(fun a =>
(* assert that implied_prop holds on the post trace *)
implied_prop a pre post
)
| _ => false ==> true
end).
Open Scope string_scope.
(* if pre tests true, then post tests true, for all tested execution traces *)
Definition pre_post_assertion {Setup Msg State prop : Type}
`{Checkable prop}
`{Serializable Msg}
`{Serializable State}
`{Serializable Setup}
`{Show Msg}
(maxLength : nat)
(init_chain : ChainBuilder)
(gTrace : ChainBuilder -> nat -> G ChainBuilder)
(c : Contract Setup Msg State)
(caddr : Address)
(pre : State -> Msg -> bool)
(post : Chain -> ContractCallContext -> State -> Msg -> option (State * list ActionBody) -> prop) : Checker :=
let action_bodies actions := map (fun act => act.(act_body)) actions in
let post_helper env cctx post_cstate new_acts cstate msg : Checker :=
whenFail ("On Msg: " ++ show msg)
(checker (post env.(env_chain) cctx cstate msg (Some (post_cstate, action_bodies new_acts)))) in
let stepProp (act : Action) (new_acts : list Action) (cs_from : ChainState) (cs_to : ChainState) :=
let env_from : Environment := cs_from.(chain_state_env) in
let env_to : Environment := cs_to.(chain_state_env) in
let amount :=
match act.(act_body) with
| act_call _ amount _ => amount
| _ => 0%Z
end in
let new_balance :=
if (act.(act_from) =? caddr)%address then
env_from.(env_account_balances) caddr
else
(env_from.(env_account_balances) caddr + amount)%Z in
let cctx := build_ctx act.(act_from) caddr new_balance amount in
match act.(act_body) with
| act_call to _ ser_msg =>
if address_eqb to caddr
then
match @deserialize Msg _ ser_msg with
| Some msg =>
match get_contract_state State env_from caddr with
| Some cstate_from =>
if pre cstate_from msg
then
match get_contract_state State env_to caddr with
| Some cstate_to => (post_helper env_from cctx cstate_to new_acts cstate_from msg)
| None => checker true
end
else checker true (* TODO: should be discarded!*)
| None => checker true
end
| None => checker true
end
else checker true
| _ => checker true
end in
forAllActionExecution maxLength init_chain gTrace stepProp.
(* For any ChainState in a ChainTrace if pf tests true on all previous ChainStates in the
ChainTrace then implied_prop tests true, for all tested execution traces*)
Definition forAllChainState_implication {prop : Type}
`{Checkable prop}
(maxLength : nat)
(init_lc : ChainBuilder)
(gTrace : ChainBuilder -> nat -> G ChainBuilder)
(pf : ChainState -> bool)
(implied_prop : ChainState -> prop)
: Checker :=
let printOnFail (cs : ChainState) : Checker := whenFail (show cs) (checker (implied_prop cs)) in
let map_implication (states : list ChainState) : list Checker :=
snd (fold_left (fun '(b, checkers) state =>
(b && (pf state), (implication b (printOnFail state)) :: checkers)) states (true, [])) in
forAllShrink (gTrace init_lc maxLength) shrink
(fun cb => conjoin (map_implication (trace_states cb.(builder_trace)))).
End TraceGens.