rightfully fails because [:consume-all] removes the strong prefix property of its parser. But right now, EverParse fails with F* Error 19, i.e. a Z3 failure to prove that field a above with [:consume-all] has the strong prefix property. While expected, this is not palatable to the user.
In fact, as designed in #116, [:consume-all] is meant to be used only as the last field of a struct. Thus, I believe this should be checked syntactically (or, at worst, at the level of the 3D AST) and EverParse should reject uses of [:consume-all] for struct fields other than the last one, with a suitable error message.
Reported by @Smfakhoury
The following 3D specification:
rightfully fails because
[:consume-all]removes the strong prefix property of its parser. But right now, EverParse fails with F* Error 19, i.e. a Z3 failure to prove that fieldaabove with[:consume-all]has the strong prefix property. While expected, this is not palatable to the user.In fact, as designed in #116,
[:consume-all]is meant to be used only as the last field of a struct. Thus, I believe this should be checked syntactically (or, at worst, at the level of the 3D AST) and EverParse should reject uses of[:consume-all]for struct fields other than the last one, with a suitable error message.