Length of frames

[favonia]

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

[liyishuai]

Does Coq have a bounded integer library? I'm a bit reluctant to depend on external packages.

[lastland]

One way to encode bounded integers in Coq is using subset types {n: nat | n < ... }. Then by using Program Definition, etc., you can reuse most of the functions provided by nat, with obligations to prove that if the result is also a bounded integer, it is within the bound.

However, many people would suggest reconsidering the options before using that because reasoning about dependent types (for example, when doing unification, etc.) in Coq can be painful...

[liyishuai]

Also, considering that SETTINGS_MAX_FRAME_SIZE can go up to 16M, we should use binary numbers rather than nat in most cases.

[favonia]

I think that Sigma type encoding {nat | ...} should work, even if not the best solution.

Re: 16M: maybe we can also define 16K and 16M to be some large enough unknown constants.

[liyishuai]

SETTINGS_MAX_FRAME_SIZE varies during runtime. Is this a reason against limiting the frame size at type level? A frame cannot be guaranteed to be valid at compile time at all.

[favonia]

Well, our client or server can always fix the bound to exactly 16384, the default value.

[lastland]

If we treat SETTINGS_MAX_FRAME_SIZE as an opaque value, it should not matter how big it is, right? Or am I missing something?

[lastland]

But anyway, I do not have a strong opinion on this. If you decided to use the binary format N, remember to check out peano_ind...

[favonia]

If we treat SETTINGS_MAX_FRAME_SIZE as an opaque value, it should not matter how big it is, right? Or am I missing something?

I believe that is the case. We only have to make sure proper bound-checking is enforced with respect to some "reasonable" constants.

[liyishuai]

This value can be modified by SETTINGS frames. I don't think it's proper to make it opaque.
I'm somehow ambitious to make this library general enough to reason about all implementations rather than ours.

[lastland]

You will want to say something like, for all values we can give to the settings, some properties hold. And reasoning about the setting should not rely on it being a particular value. Therefore, the values of settings remain abstract all the time and there is no concrete number that we need to worry about.

I am not suggesting to keep using nat though, I just don't think this should be the reason behind the decision.

[lastland]

And although I have heard a lot of arguments against using sigma types, I would actually be interested to see how they would play out here...

[liyishuai]

You will want to say something like, for all values we can give to the settings, some properties hold.

To be concrete, what would a running checker look like?

[liyishuai]

I think 16M is a reasonable constant limit here. The static bound-checking tells if the frame can be valid in any context, and the runtime checking decides whether this frame is valid under current context.