This repository has been archived by the owner on Oct 10, 2022. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 1
/
http_2.rflx
254 lines (244 loc) · 11.6 KB
/
http_2.rflx
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
package HTTP_2 is
type Payload_Length is mod 2 ** 24;
type Frame_Type is
(DATA => 0,
HEADERS => 1,
PRIORITY => 2,
RST_STREAM => 3,
SETTINGS => 4,
PUSH_PROMISE => 5,
PING => 6,
GOAWAY => 7,
WINDOW_UPDATE => 8,
CONTINUATION => 9)
with Size => 8;
type Settings_Identifier is
(HEADER_TABLE_SIZE => 16#01#,
ENABLE_PUSH => 16#02#,
MAX_CONCURRENT_STREAMS => 16#03#,
INITIAL_WINDOW_SIZE => 16#04#,
MAX_FRAME_SIZE => 16#05#,
MAX_HEADER_LIST_SIZE => 16#06#)
with Size => 16;
type Settings_Value_Generic is mod 2 ** 32;
type Settings_Value_Enable_Push is range 0 .. 1 with Size => 32;
type Settings_Value_Initial_Window_Size is range 0 .. 2 ** 31 - 1 with Size => 32;
type Settings_Value_Max_Frame_Size is range 2 ** 14 .. 2 ** 24 - 1 with Size => 32;
type Zero_Bit is range 0 .. 0 with Size => 1;
type Stream_ID is mod 2 ** 31;
type Weight is mod 2 ** 8;
type Error_Code is
(NO_ERROR => 16#00#,
PROTOCOL_ERROR => 16#01#,
INTERNAL_ERROR => 16#02#,
FLOW_CONTROL_ERROR => 16#03#,
TIMEOUT => 16#04#,
STREAM_CLOSED => 16#05#,
FRAME_SIZE_ERROR => 16#06#,
REFUSED_STREAM => 16#07#,
CANCEL => 16#08#,
COMPRESSION_ERROR => 16#09#,
CONNECT_ERROR => 16#0A#,
ENHANCE_YOUR_CALM => 16#0B#,
INADEQUATE_SECURITY => 16#0C#,
HTTP_1_1_REQUIRED => 16#0D#)
with Size => 32;
type Window_Size_Increment is range 1 .. 2 ** 31 - 1 with Size => 31;
type Pad_Length is mod 2 ** 8;
type Settings_Parameter is
message
Settings_Identifier : Settings_Identifier
then Settings_Value_Enable_Push
if Settings_Identifier = ENABLE_PUSH
then Settings_Value_Initial_Window_Size
if Settings_Identifier = INITIAL_WINDOW_SIZE
then Settings_Value_Max_Frame_Size
if Settings_Identifier = MAX_FRAME_SIZE
then Settings_Value_Generic
if Settings_Identifier = HEADER_TABLE_SIZE
or Settings_Identifier = MAX_CONCURRENT_STREAMS
or Settings_Identifier = MAX_HEADER_LIST_SIZE;
Settings_Value_Enable_Push : Settings_Value_Enable_Push
then null;
Settings_Value_Initial_Window_Size : Settings_Value_Initial_Window_Size
then null;
Settings_Value_Max_Frame_Size : Settings_Value_Max_Frame_Size
then null;
Settings_Value_Generic : Settings_Value_Generic;
end message;
type Settings_Parameters is sequence of Settings_Parameter;
type Frame is
message
Payload_Length : Payload_Length;
Frame_Type : Frame_Type;
Flag_Bit_7_Unused : Zero_Bit;
Flag_Bit_6_Unused : Zero_Bit;
Flag_Priority : Boolean
then Flag_Bit_4_Unused
if (Frame_Type = HEADERS
or ((Frame_Type = DATA
or Frame_Type = SETTINGS
or Frame_Type = PING
or Frame_Type = GOAWAY
or Frame_Type = RST_STREAM
or Frame_Type = WINDOW_UPDATE
or Frame_Type = PRIORITY
or Frame_Type = PUSH_PROMISE
or Frame_Type = CONTINUATION
) and Flag_Priority = False));
Flag_Bit_4_Unused : Zero_Bit;
Flag_Padded : Boolean
then Flag_End_Headers
if (Frame_Type = DATA
or Frame_Type = HEADERS
or Frame_Type = PUSH_PROMISE
or ((Frame_Type = SETTINGS
or Frame_Type = PING
or Frame_Type = CONTINUATION
or Frame_Type = GOAWAY
or Frame_Type = RST_STREAM
or Frame_Type = WINDOW_UPDATE
or Frame_Type = PRIORITY
) and Flag_Padded = False));
Flag_End_Headers : Boolean
then Flag_Bit_1_Unused
if (Frame_Type = HEADERS
or Frame_Type = PUSH_PROMISE
or Frame_Type = CONTINUATION
or ((Frame_Type = DATA
or Frame_Type = SETTINGS
or Frame_Type = PING
or Frame_Type = GOAWAY
or Frame_Type = RST_STREAM
or Frame_Type = WINDOW_UPDATE
or Frame_Type = PRIORITY
) and Flag_End_Headers = False));
Flag_Bit_1_Unused : Zero_Bit;
Flag_End_Stream_ACK : Boolean
then Reserved_Bit_1
if ((Frame_Type = SETTINGS and Payload_Length mod 6 = 0)
or (Frame_Type = PING and Payload_Length = 8)
or Frame_Type = DATA
or Frame_Type = HEADERS
or ((Frame_Type = PUSH_PROMISE
or Frame_Type = CONTINUATION
or Frame_Type = GOAWAY
or Frame_Type = RST_STREAM
or (Frame_Type = WINDOW_UPDATE and Payload_Length = 4)
or (Frame_Type = PRIORITY and Payload_Length = 5)
) and Flag_End_Stream_ACK = False));
Reserved_Bit_1 : Zero_Bit;
Stream_Identifier : Stream_ID
then Pad_Length
if (Frame_Type = DATA or Frame_Type = HEADERS or Frame_Type = PUSH_PROMISE) and Flag_Padded = True
then Application_Data
with Size => Payload_Length * 8
if Frame_Type = DATA and Flag_Padded = False
then Exclusive_Flag
if Frame_Type = HEADERS and Flag_Priority = True and Flag_Padded = False
then Header_Block_Fragment
with Size => Payload_Length * 8
if (Frame_Type = HEADERS and Flag_Priority = False and Flag_Padded = False) or Frame_Type = CONTINUATION
then Exclusive_Flag
if Frame_Type = PRIORITY
then Error_Code
if Frame_Type = RST_STREAM
then Settings_Parameters
with Size => Payload_Length * 8
if Frame_Type = SETTINGS
then Application_Data
with Size => 64
if Frame_Type = PING and Stream_Identifier = 0
then Reserved_Bit_2
if (Frame_Type = GOAWAY and Stream_Identifier = 0)
or Frame_Type = WINDOW_UPDATE
or (Frame_Type = PUSH_PROMISE and Flag_Padded = False);
Settings_Parameters : Settings_Parameters
then null
-- https://github.com/Componolit/RecordFlux/issues/554
if Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First);
Pad_Length : Pad_Length
then Application_Data
with Size => (Payload_Length - Pad_Length) * 8 - Pad_Length'Size
if Frame_Type = DATA and Payload_Length >= Pad_Length * 8 + Pad_Length'Size
then Exclusive_Flag
if Frame_Type = HEADERS and Flag_Priority = True
then Header_Block_Fragment
with Size => Payload_Length * 8
if Frame_Type = HEADERS and Flag_Priority = False
then Reserved_Bit_2
if Frame_Type = PUSH_PROMISE;
Reserved_Bit_2 : Zero_Bit
then Promised_Stream_ID
if Frame_Type = PUSH_PROMISE
then Last_Stream_ID
if Frame_Type = GOAWAY
then Window_Size_Increment
if Frame_Type = WINDOW_UPDATE;
Promised_Stream_ID : Stream_ID
then Header_Block_Fragment
with Size => (Payload_Length - Pad_Length) * 8 - (Promised_Stream_ID'Last - Pad_Length'First + 1)
if Flag_Padded = True
and Payload_Length >= Pad_Length + (Promised_Stream_ID'Last - Pad_Length'First + 1) / 8
then Header_Block_Fragment
with Size => Payload_Length * 8 - (Promised_Stream_ID'Last - Reserved_Bit_2'First + 1)
if Flag_Padded = False
and Payload_Length >= (Promised_Stream_ID'Last - Reserved_Bit_2'First + 1) / 8;
Last_Stream_ID : Stream_ID
then Error_Code;
Exclusive_Flag : Boolean;
Stream_Dependency : Stream_ID;
Weight : Weight
then Header_Block_Fragment
with Size => (Payload_Length - Pad_Length) * 8 - (Weight'Last - Pad_Length'First + 1)
if Frame_Type = HEADERS and Flag_Padded = True
and Payload_Length >= Pad_Length + (Weight'Last - Pad_Length'First + 1) / 8
then Header_Block_Fragment
with Size => Payload_Length * 8 - (Weight'Last - Exclusive_Flag'First + 1)
if Frame_Type = HEADERS
and Flag_Padded = False and Payload_Length >= (Weight'Last - Exclusive_Flag'First + 1) / 8
then null
if Frame_Type = PRIORITY
-- https://github.com/Componolit/RecordFlux/issues/554
and Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First);
Header_Block_Fragment : Opaque
then Padding
if (Frame_Type = HEADERS or Frame_Type = PUSH_PROMISE) and Flag_Padded = True
then null
if (Frame_Type = CONTINUATION
or ((Frame_Type = PUSH_PROMISE or Frame_Type = HEADERS) and Flag_Padded = False))
-- https://github.com/Componolit/RecordFlux/issues/554
and Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First);
Application_Data : Opaque
then Padding
if Frame_Type = DATA and Flag_Padded = True
then null
if ((Frame_Type = DATA and Flag_Padded = False) or Frame_Type = PING)
-- https://github.com/Componolit/RecordFlux/issues/554
and Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First);
Padding : Opaque
with Size => Pad_Length * 8;
Error_Code : Error_Code
then null
if Frame_Type = RST_STREAM
-- https://github.com/Componolit/RecordFlux/issues/554
and Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First)
then null
if Frame_Type = GOAWAY
and Payload_Length * 8 = (Error_Code'Size + Last_Stream_ID'Size + Reserved_Bit_2'Size)
-- https://github.com/Componolit/RecordFlux/issues/554
and Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First)
then Additional_Debug_Data
with Size => (Payload_Length * 8 - (Error_Code'Size + Last_Stream_ID'Size + Reserved_Bit_2'Size))
if Frame_Type = GOAWAY
and Payload_Length * 8 > (Error_Code'Size + Last_Stream_ID'Size + Reserved_Bit_2'Size);
Additional_Debug_Data : Opaque
then null
-- https://github.com/Componolit/RecordFlux/issues/554
if Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First);
Window_Size_Increment : Window_Size_Increment
then null
-- https://github.com/Componolit/RecordFlux/issues/554
if Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First);
end message;
end HTTP_2;