liyishuai / coq-http2 Goto Github PK

Is there a reason not to use bounded integers for the lengths?

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?

As mentioned in #1, dependent types makes Coq reasoning painful.
I started with the following definition for FramePayload:

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.

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.

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.

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...

What is the meaning of zeroFrameType and nonZeroFramType and why is WindowUpdateType in neither?