-
Notifications
You must be signed in to change notification settings - Fork 56
/
SeqNum.v
75 lines (63 loc) · 2.56 KB
/
SeqNum.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
Require Import Verdi.Verdi.
Set Implicit Arguments.
Section SeqNum.
Context {orig_base_params : BaseParams}.
Context {orig_multi_params : MultiParams orig_base_params}.
Record seq_num_data := mkseq_num_data { tdNum : nat;
tdSeen : list (name * list nat);
tdData : data }.
Record seq_num_msg := mkseq_num_msg { tmNum : nat; tmMsg : msg }.
Definition seq_num_msg_eq_dec (x y : seq_num_msg) : {x = y} + {x <> y}.
decide equality.
apply msg_eq_dec.
decide equality.
Defined.
Fixpoint processPackets (seq_num : nat) (packets : list (name * msg)) : nat * list (name * seq_num_msg) :=
match packets with
| [] => (seq_num, [])
| p :: ps => let (n', pkts) := processPackets seq_num ps in
(S n', (fst p, mkseq_num_msg n' (snd p)) :: pkts)
end.
Definition seq_num_init_handlers (n : name) :=
mkseq_num_data 0 [] (init_handlers n).
Definition seq_num_net_handlers (dst : name) (src : name) (m : seq_num_msg) (state : seq_num_data) :
list output * seq_num_data * list (name * seq_num_msg) :=
let seen_src := assoc_default name_eq_dec (tdSeen state) src [] in
if member (tmNum m) seen_src then
([], state, [])
else
let '(out, data', pkts) := net_handlers dst src (tmMsg m) (tdData state) in
let (n', tpkts) := processPackets (tdNum state) pkts in
(out, mkseq_num_data n' (assoc_set name_eq_dec (tdSeen state) src (tmNum m :: seen_src)) data', tpkts).
Definition seq_num_input_handlers
(h : name)
(inp : input)
(state : seq_num_data) :
(list output) * seq_num_data * list (name * seq_num_msg) :=
let '(out, data', pkts) := input_handlers h inp (tdData state) in
let (n', tpkts) := processPackets (tdNum state) pkts in
(out, mkseq_num_data n' (tdSeen state) data', tpkts).
Instance base_params : BaseParams :=
{
data := seq_num_data ;
input := input ;
output := output
}.
Instance multi_params : MultiParams _ :=
{
name := name ;
msg := seq_num_msg ;
msg_eq_dec := seq_num_msg_eq_dec ;
name_eq_dec := name_eq_dec ;
nodes := nodes ;
all_names_nodes := all_names_nodes;
no_dup_nodes := no_dup_nodes;
init_handlers := seq_num_init_handlers;
net_handlers := seq_num_net_handlers;
input_handlers := seq_num_input_handlers
}.
End SeqNum.
#[global]
Hint Extern 5 (@BaseParams) => apply base_params : typeclass_instances.
#[global]
Hint Extern 5 (@MultiParams _) => apply multi_params : typeclass_instances.