-
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Types.v
120 lines (108 loc) · 4.05 KB
/
Types.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
From Coq Require Vector.
From Coq Require Import NArith String.
Open Scope N_scope.
Open Scope type_scope.
(* https://http2.github.io/http2-spec/index.html#rfc.section.5.1.1 *)
Definition StreamId := N.
(* https://http2.github.io/http2-spec/index.html#rfc.section.5.3.2 *)
Definition Weight := N.
(* https://http2.github.io/http2-spec/index.html#rfc.section.6.2 *)
Definition HeaderBlockFragment := string.
(* https://http2.github.io/http2-spec/index.html#rfc.section.6.3 *)
Inductive Priority :=
{ exclusive : bool;
streamDependency : StreamId;
weight : Weight
}.
(* https://http2.github.io/http2-spec/index.html#rfc.section.6.5 *)
Definition SettingValue := N.
Inductive SettingKeyId :=
SettingHeaderTableSize
| SettingEnablePush
| SettingMaxConcurrentStreams
| SettingInitialWindowSize
| SettingMaxFrameSize
| SettingMaxHeaderBlockSize.
Definition Setting := SettingValue * SettingKeyId.
(* https://http2.github.io/http2-spec/index.html#rfc.section.6.9 *)
Definition WindowSize := N.
(* https://http2.github.io/http2-spec/index.html#rfc.section.7 *)
Definition ErrorCode := N.
Inductive ErrorCodeId :=
NoError (* 0x0 *)
| ProtocolError (* 0x1 *)
| InternalError (* 0x2 *)
| FlowControlError (* 0x3 *)
| SettingsTimeout (* 0x4 *)
| StreamClosed (* 0x5 *)
| FrameSizeError (* 0x6 *)
| RefusedStream (* 0x7 *)
| Cancel (* 0x8 *)
| CompressionError (* 0x9 *)
| ConnectError (* 0xa *)
| EnhanceYourCalm (* 0xb *)
| InadequateSecurity (* 0xc *)
| HTTP11Required (* 0xd *)
| UnknownErrorCode : ErrorCode -> ErrorCodeId.
Definition fromErrorCodeId (e:ErrorCodeId) : ErrorCode :=
match e with
| NoError => 0x0
| ProtocolError => 0x1
| InternalError => 0x2
| FlowControlError => 0x3
| SettingsTimeout => 0x4
| StreamClosed => 0x5
| FrameSizeError => 0x6
| RefusedStream => 0x7
| Cancel => 0x8
| CompressionError => 0x9
| ConnectError => 0xa
| EnhanceYourCalm => 0xb
| InadequateSecurity => 0xc
| HTTP11Required => 0xd
| (UnknownErrorCode w) => w
end.
Definition toErrorCodeId (e:ErrorCode) : ErrorCodeId :=
match e with
| 0x0 => NoError
| 0x1 => ProtocolError
| 0x2 => InternalError
| 0x3 => FlowControlError
| 0x4 => SettingsTimeout
| 0x5 => StreamClosed
| 0x6 => FrameSizeError
| 0x7 => RefusedStream
| 0x8 => Cancel
| 0x9 => CompressionError
| 0xa => ConnectError
| 0xb => EnhanceYourCalm
| 0xc => InadequateSecurity
| 0xd => HTTP11Required
| w => UnknownErrorCode w
end.
(* https://http2.github.io/http2-spec/index.html#rfc.section.4.1 *)
Definition FrameFlags := Vector.t bool 8.
Inductive FrameHeader :=
{ payloadLength : nat;
flags : FrameFlags;
streamId : StreamId
}.
(* https://http2.github.io/http2-spec/index.html#rfc.section.6 *)
Definition FrameType := N.
Inductive FramePayload : FrameType -> Type :=
DataFrame : string -> FramePayload 0
| HeadersFrame : option Priority -> HeaderBlockFragment -> FramePayload 1
| PriorityFrame : Priority -> FramePayload 2
| RSTStreamFrame : ErrorCodeId -> FramePayload 3
| SettingsFrame : list Setting -> FramePayload 4
| PushPromiseFrame : StreamId -> HeaderBlockFragment -> FramePayload 5
| PingFrame : string -> FramePayload 6
| GoAwayFrame : StreamId -> ErrorCodeId -> string -> FramePayload 7
| WindowUpdateFrame : WindowSize -> FramePayload 8
| ContinuationFrame : HeaderBlockFragment -> FramePayload 9
| UnknownFrame type : string -> FramePayload type.
Inductive Frame :=
{ frameHeader : FrameHeader;
frameType : FrameType;
framePayload : FramePayload frameType
}.