forked from Componolit/RecordFlux-specifications
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathhttp_2.rflx
242 lines (232 loc) · 11.2 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
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 array 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
if Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First); -- ISSUE: Componolit/RecordFlux#554
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 and Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First); -- ISSUE: Componolit/RecordFlux#554
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))
and Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First); -- ISSUE: Componolit/RecordFlux#554
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)
and Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First); -- ISSUE: Componolit/RecordFlux#554
Padding : Opaque
with Size => Pad_Length * 8;
Error_Code : Error_Code
then null
if Frame_Type = RST_STREAM and Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First) -- ISSUE: Componolit/RecordFlux#554
then null
if Frame_Type = GOAWAY
and Payload_Length * 8 = (Error_Code'Size + Last_Stream_ID'Size + Reserved_Bit_2'Size)
and Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First) -- ISSUE: Componolit/RecordFlux#554
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
if Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First); -- ISSUE: Componolit/RecordFlux#554
Window_Size_Increment : Window_Size_Increment
then null
if Message'Size = Payload_Length * 8 + (Stream_Identifier'Last + 1 - Payload_Length'First); -- ISSUE: Componolit/RecordFlux#554
end message;
end HTTP_2;