liyishuai / coq-http2 Goto Github PK
View Code? Open in Web Editor NEWLicense: MIT License
License: MIT License
Is there a reason not to use bounded integers for the lengths?
The network bytes are big-endian, whereas little-endian makes numeric conversion simpler and more reason-able. We should probably represent the fields in little-endian vectors, and only use big-endian when transforming them into strings.
All the numbers encoded in frames are fixed-length, and they are not much involved in arithmetic computations. Maybe we should instead represent them as vectors? which also alleviates the pain of reasoning about their bounds.
What is the meaning of zeroFrameType
and nonZeroFramType
and why is WindowUpdateType
in neither?
I'm stuck implementing the integer decoding in HPACK using a monadic parser. The pseudocode, decoding an integer I with an N bit prefix, is as follows:
decode I from the next N bits
if I < 2^N - 1, return I
else
M = 0
repeat
B = next octet
I = I + (B & 127) * 2^M
M = M + 7
while B & 128 == 128
return I
The important thing to note is that the function essentially recurses until a byte with the first bit set to 0 occurs. How can I reason that either this will happen, or the parser will run out of bytes to read?
Currently, I'd like to write the following:
Fixpoint decode_integer_h {m:Tycon} `{Monad m} `{MError HPACKError m}
`{MParser byte m} (M:N) : m N :=
a <- get_byte ;;
let B := (N_of_ascii a) in
let I := (BinNatDef.N.land B 127) * 2^M in
if N.land B 128 =? 128
then e <- decode_integer_h (M + 7) ;;
ret (I + e)
else ret I.
Definition decode_integer {m:Tycon} `{Monad m} `{MError HPACKError m}
`{MParser byte m} (prefix:N) (n:N) : m N :=
if prefix <? 2^n - 1 then ret prefix
else a <- decode_integer_h 0 ;;
ret (prefix + a).
But coq can't guess the decreasing argument for decode_integer_h.
Does anybody have any suggestions for testing HPACK beyond comparing to the spec by eye? The spec provides some examples that I had hoped to use but I found that the way they represent strings is strange.
Specifically, in this example, 0a corresponds to ".", while in ascii, it corresponds to a newline "\n". All of the examples (besides encoding integers) have cases like this, which means I can't simply copy and paste and then compare the output to the value.
They also provide the hex value, so I was thinking of instead copy and pasting and comparing the output value converted to a hex dump either in or outside coq, but I'm not sure that's worth the effort.
I was also thinking about testing (or better yet proving) some proposition relating the encoding and decoding (like that decoding an encoded header field representation is the identity) but I'm not sure what kind of real guarantees this gives.
Any idea how we can ensure coverage of the HTTP2 spec? Annotating each sentence with the line number in the source code where it is handled seems tedious but I'm not sure there's something better to do...
I'm currently doing some more testing on frame encoding and I found I'm unable to compute the functions completely, there just ends up being a complicated unsimplified term. I believe this to be because of the dependent types in the frame header encoding (which was added after I last tested the encoder), though I'm not completely sure. Is there some special way to run dependently typed functions?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.