val parse_vldata_payload_size (sz: integer_size)
    : Pure nat (requires True) (ensures (fun y -> y == pow2 (FStar.Mul.op_Star 8 sz) - 1))
let parse_vldata_payload_size
  (sz: integer_size)
: Pure nat
  (requires True)
  (ensures (fun y -> y == pow2 (FStar.Mul.op_Star 8 sz) - 1 ))
= match sz with
  | 1 -> 255
  | 2 -> 65535
  | 3 -> 16777215
  | 4 -> 4294967295
val parse_vldata_payload_size (sz: integer_size)
    : Pure nat (requires True) (ensures (fun y -> y == pow2 (FStar.Mul.op_Star 8 sz) - 1))
let parse_vldata_payload_size (sz: integer_size)
    : Pure nat (requires True) (ensures (fun y -> y == pow2 (FStar.Mul.op_Star 8 sz) - 1)) =
match sz with
| 1 -> 255
| 2 -> 65535
| 3 -> 16777215
| 4 -> 4294967295
LowParse.Spec.VLData.fsti.checked
prims.fst.checked LowParse.Spec.FLData.fst.checked LowParse.Spec.AllIntegers.fst.checked LowParse.Math.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked
LowParse.Spec.VLData.fsti
LowParse.Spec.BoundedInt.integer_size Prims.nat Prims.l_True Prims.eq2 Prims.int Prims.op_Subtraction Prims.pow2 FStar.Mul.op_Star
module LowParse.Spec.VLData
include LowParse.Spec.FLData
include LowParse.Spec.AllIntegers // for bounded_integer, in_bounds, etc.

module Seq = FStar.Seq
module U32 = FStar.UInt32
module M = LowParse.Math

#reset-options "--z3rlimit 64 --max_fuel 64 --max_ifuel 64 --z3refresh --z3cliopt smt.arith.nl=false"

let parse_vldata_payload_size
  (sz: integer_size)
: Pure nat
  (requires True)
val parse_vldata_payload_size (sz: integer_size)
    : Pure nat (requires True) (ensures (fun y -> y == pow2 (FStar.Mul.op_Star 8 sz) - 1))
sz: LowParse.Spec.BoundedInt.integer_size -> Prims.Pure Prims.nat