bitsum: try removing positivity constraint on `key_size`

[tahina-pro]

https://github.com/project-everest/everparse/blob/452f1fedecf5c3413095787480ac3f1c7680e715/src/lowparse/LowParse.Spec.BitSum.fst#L21

Thank you @nikswamy for pointing this out. For now I will leave it as is, for the sake of merging your changes into master, CI permitting. Later I will separately investigate whether I can remove that restriction on key_size, and if not, I will update the comment accordingly.

Originally posted by @tahina-pro in https://github.com/project-everest/everparse/pull/38#discussion_r556969221

[tahina-pro]

I hope this constraint can be lifted thanks to FStarLang/FStar#2205, which should allow me to correctly perform structural recursion on bitsum_t