Problem on verifying code produced by QD

[Black-Kamous]

I tried to produce parsers and serializers for NDN TLV coding scheme, the bitcoin_varint is very similar to the variable length number used in NDN TLV, so I wrote a rfc file as follows:

struct {
  bitcoin_varint tlv_type;
  bitcoin_varint tlv_len;
  opaque tlv_value[tlv_len];
} MustBeFresh;

struct {
  bitcoin_varint tlv_type;
  bitcoin_varint tlv_len;
  opaque tlv_value[tlv_len];
} Nonce;

struct {
  bitcoin_varint tlv_type;
  bitcoin_varint tlv_len;
  opaque tlv_value[tlv_len];
} InterestLifeTime;

struct {
  bitcoin_varint tlv_type;
  bitcoin_varint tlv_len;
  opaque tlv_value[tlv_len];
} NameComponent;

struct {
  bitcoin_varint tlv_type;
  NameComponent nc<0..255:bitcoin_varint>;
} Name;

struct {
  Name name;
  MustBeFresh mbf;
  Nonce nonce;
  InterestLifeTime ilt;
} InterestValue;

struct {
  bitcoin_varint tlv_type;
  bitcoin_varint tlv_len;
  InterestValue iv[tlv_len];
} Interest;

An error occured while verifying Interest.fst

* Error 19 at Interest.fst(77,141-77,165):
  - Subtyping check failed
  - Expected type
      s2':
      LowParse.SLow.Base.serializer32 Interest_iv.interest_iv_serializer
        { LowParse.SLow.Combinators.serialize32_kind_precond LowParse.Spec.BCVLI.parse_bcvli_kind
            Interest_iv.interest_iv_parser_kind }
    got type LowParse.SLow.Base.serializer32 Interest_iv.interest_iv_serializer
  - The SMT solver could not prove the query.

The code where error appeared is as follows:

inline_for_extraction let interest'_serializer32 : LS.serializer32 interest'_serializer = (LS.serialize32_bcvli `LS.serialize32_nondep_then` interest_iv_serializer32)

I read about the code of serialize32_nondep_then, it requires the two serializers in its params should satisfy serialize32_kind_precond

let serialize32_kind_precond
  (k1 k2: parser_kind)
: GTot bool
= Some? k1.parser_kind_high &&
  Some? k2.parser_kind_high &&
  Some?.v k1.parser_kind_high + Some?.v k2.parser_kind_high < 4294967296

So I investigated the parser_kind of serialize32_bcvli and interest_iv_serializer32, as follows:

let parse_bcvli_kind = {
  parser_kind_low = 1;
  parser_kind_high = Some 5;
  parser_kind_subkind = Some ParserStrong;
  parser_kind_metadata = None;
}

inline_for_extraction noextract let interest_iv_parser_kind = LP.strong_parser_kind 9 4294967300 None

I think that's where the problem is: the two parser_kind_high above is 5 and 4294967300, 5+4294967300 exceeds 4294967296.

Any suggestions on how I should fix my rfc file or change something in LowParse code to make it right? Thanks a lot for helping! The QD log is attached below:

Writing parsers for type <mustBeFresh> to <./MustBeFresh.fst>...
LINFO<mustBeFresh@tlv_type>: vl=yes lenLen=0 minLen=1 maxLen=5 minCount=0 maxCount=0 meta=default
LINFO<mustBeFresh@tlv_value>: vl=yes lenLen=1 minLen=1 maxLen=4294967300 minCount=0 maxCount=0 meta=default
LINFO<mustBeFresh>: vl=no lenLen=0 minLen=2 maxLen=4294967305 minCount=0 maxCount=0 meta=default
Writing parsers for type <mustBeFresh_tlv_value> to <./MustBeFresh_tlv_value.fst>...
Writing parsers for type <nonce> to <./Nonce.fst>...
LINFO<nonce@tlv_type>: vl=yes lenLen=0 minLen=1 maxLen=5 minCount=0 maxCount=0 meta=default
LINFO<nonce@tlv_value>: vl=yes lenLen=1 minLen=1 maxLen=4294967300 minCount=0 maxCount=0 meta=default
LINFO<nonce>: vl=no lenLen=0 minLen=2 maxLen=4294967305 minCount=0 maxCount=0 meta=default
Writing parsers for type <nonce_tlv_value> to <./Nonce_tlv_value.fst>...
Writing parsers for type <interestLifeTime> to <./InterestLifeTime.fst>...
LINFO<interestLifeTime@tlv_type>: vl=yes lenLen=0 minLen=1 maxLen=5 minCount=0 maxCount=0 meta=default
LINFO<interestLifeTime@tlv_value>: vl=yes lenLen=1 minLen=1 maxLen=4294967300 minCount=0 maxCount=0 meta=default
LINFO<interestLifeTime>: vl=no lenLen=0 minLen=2 maxLen=4294967305 minCount=0 maxCount=0 meta=default
Writing parsers for type <interestLifeTime_tlv_value> to <./InterestLifeTime_tlv_value.fst>...
Writing parsers for type <nameComponent> to <./NameComponent.fst>...
LINFO<nameComponent@tlv_type>: vl=yes lenLen=0 minLen=1 maxLen=5 minCount=0 maxCount=0 meta=default
LINFO<nameComponent@tlv_value>: vl=yes lenLen=1 minLen=1 maxLen=4294967300 minCount=0 maxCount=0 meta=default
LINFO<nameComponent>: vl=no lenLen=0 minLen=2 maxLen=4294967305 minCount=0 maxCount=0 meta=default
Writing parsers for type <nameComponent_tlv_value> to <./NameComponent_tlv_value.fst>...
Writing parsers for type <name> to <./Name.fst>...
LINFO<name@tlv_type>: vl=yes lenLen=0 minLen=1 maxLen=5 minCount=0 maxCount=0 meta=default
LINFO<name@nc>: vl=yes lenLen=3 minLen=1 maxLen=258 minCount=0 maxCount=127 meta=default
LINFO<name>: vl=no lenLen=0 minLen=2 maxLen=263 minCount=0 maxCount=0 meta=default
Writing parsers for type <name_nc> to <./Name_nc.fst>...
Writing parsers for type <interestValue> to <./InterestValue.fst>...
LINFO<interestValue@name>: vl=no lenLen=0 minLen=2 maxLen=263 minCount=0 maxCount=0 meta=default
LINFO<interestValue@mbf>: vl=no lenLen=0 minLen=2 maxLen=4294967305 minCount=0 maxCount=0 meta=default
LINFO<interestValue@nonce>: vl=no lenLen=0 minLen=2 maxLen=4294967305 minCount=0 maxCount=0 meta=default
LINFO<interestValue@ilt>: vl=no lenLen=0 minLen=2 maxLen=4294967305 minCount=0 maxCount=0 meta=default
LINFO<interestValue>: vl=no lenLen=0 minLen=8 maxLen=12884902178 minCount=0 maxCount=0 meta=default
Writing parsers for type <interest> to <./Interest.fst>...
LINFO<interest@tlv_type>: vl=yes lenLen=0 minLen=1 maxLen=5 minCount=0 maxCount=0 meta=default
LINFO<interest@iv>: vl=yes lenLen=1 minLen=9 maxLen=4294967300 minCount=0 maxCount=0 meta=default
LINFO<interest>: vl=no lenLen=0 minLen=10 maxLen=4294967305 minCount=0 maxCount=0 meta=default
Writing parsers for type <interest_iv> to <./Interest_iv.fst>...

[tahina-pro]

Thanks for your question!

In fact, QuackyDucky is meant to be used with FStar.Bytes pure byte sequences (which are the results of serializer32 functions from LowParse.SLow) or LowStar.Buffer, the Low* model for C arrays. In both cases, indexing is limited to $[0..2^{32})$ only, which explains the preconditions on such combinators.

We are currently trying to alleviate such constraints by porting LowParse combinators to Pulse (cf. #155 ), where indexing is done on size_t with Karamel introducing C compile-time assertions for indexing beyond $2^{32}$, but so far we have not started porting QuackyDucky to use such combinators yet.

Hope it helps!

[tahina-pro]

Concretely, the construct that you used for the NameComponent field of Name should help you: I'd suggest to fuse the separate tlv_len field from MustBeFresh etc. into the corresponding value field with the <..> construct. Moreover, you will likely need to put bounds on such sizes, as you did for NameComponent.

[Black-Kamous]

Thank you for your help!

[Black-Kamous]

Thank you for your help!