diff --git a/src/lowparse/LowParse.Spec.BoundedInt.fst b/src/lowparse/LowParse.Spec.BoundedInt.fst
index b8602daf8..a971b1b61 100644
--- a/src/lowparse/LowParse.Spec.BoundedInt.fst
+++ b/src/lowparse/LowParse.Spec.BoundedInt.fst
@@ -25,7 +25,20 @@ let bounded_integer_prop_equiv
   assert_norm (pow2 24 == 16777216);
   assert_norm (pow2 32 == 4294967296)
 
-#push-options "--z3rlimit 16"
+let bounded_integer_prop_equiv_smtpat i u
+: Lemma
+  (bounded_integer_prop i u <==> U32.v u < pow2 (8 * i))
+  [SMTPat (bounded_integer_prop i u)]
+=
+  bounded_integer_prop_equiv i u
+
+let bounded_integer_compat_smtpat (i: integer_size) u
+: Lemma
+  (requires bounded_integer_prop i u)
+  (ensures pow2 (8 * i) <= pow2 32 /\ pow2 32 == 4294967296)
+  [SMTPat (bounded_integer_prop i u)]
+=
+  M.pow2_le_compat 32 (8 `FStar.Mul.op_Star` i)
 
 let decode_bounded_integer
   (i: integer_size)
@@ -129,8 +142,6 @@ let bounded_integer_of_le_injective'
     E.le_to_n_inj b1 b2
   end else ()
 
-#pop-options
-
 let bounded_integer_of_le_injective
   (i: integer_size)
 : Lemma
@@ -152,6 +163,10 @@ let synth_u16_le_injective : squash (synth_injective synth_u16_le) = ()
 
 let parse_u16_le = parse_bounded_integer_le 2 `parse_synth` synth_u16_le
 
+let parse_u16_le_spec b =
+  parse_synth_eq (parse_bounded_integer_le 2) synth_u16_le b;
+  E.lemma_le_to_n_is_bounded (Seq.slice b 0 2)
+
 inline_for_extraction
 let synth_u32_le
   (x: bounded_integer 4)
@@ -160,6 +175,10 @@ let synth_u32_le
 
 let parse_u32_le = parse_bounded_integer_le 4 `parse_synth` synth_u32_le
 
+let parse_u32_le_spec b =
+  parse_synth_eq (parse_bounded_integer_le 4) synth_u32_le b;
+  E.lemma_le_to_n_is_bounded (Seq.slice b 0 4)
+
 let serialize_bounded_integer_le'
   (sz: integer_size)
 : Tot (bare_serializer (bounded_integer sz))
@@ -167,8 +186,6 @@ let serialize_bounded_integer_le'
     E.n_to_le sz (U32.v x)
   )
 
-#push-options "--z3rlimit 16"
-
 let serialize_bounded_integer_le_correct
   (sz: integer_size)
 : Lemma
@@ -185,8 +202,6 @@ let serialize_bounded_integer_le_correct
   in
   Classical.forall_intro prf
 
-#pop-options
-
 let serialize_bounded_integer_le
 sz
 = serialize_bounded_integer_le_correct sz;
diff --git a/src/lowparse/LowParse.Spec.BoundedInt.fsti b/src/lowparse/LowParse.Spec.BoundedInt.fsti
index d9652d69e..8916cadca 100644
--- a/src/lowparse/LowParse.Spec.BoundedInt.fsti
+++ b/src/lowparse/LowParse.Spec.BoundedInt.fsti
@@ -77,8 +77,30 @@ val parse_bounded_integer_le
 
 val parse_u16_le : parser parse_u16_kind U16.t
 
+val parse_u16_le_spec
+  (b: bytes)
+: Lemma
+  (requires (Seq.length b >= 2))
+  (ensures (
+    let pp = parse parse_u16_le b in
+    Some? pp /\ (
+    let (Some (v, consumed)) = pp in
+    U16.v v == E.le_to_n (Seq.slice b 0 2) /\ consumed == 2
+  )))
+
 val parse_u32_le : parser parse_u32_kind U32.t
 
+val parse_u32_le_spec
+  (b: bytes)
+: Lemma
+  (requires (Seq.length b >= 4))
+  (ensures (
+    let pp = parse parse_u32_le b in
+    Some? pp /\ (
+    let (Some (v, consumed)) = pp in
+    U32.v v == E.le_to_n (Seq.slice b 0 4) /\ consumed == 4
+  )))
+
 val serialize_bounded_integer_le
   (sz: integer_size)
 : Tot (serializer (parse_bounded_integer_le sz))
diff --git a/src/lowparse/LowParse.Spec.Int.fsti b/src/lowparse/LowParse.Spec.Int.fsti
index bf68d5c60..c82c70ade 100644
--- a/src/lowparse/LowParse.Spec.Int.fsti
+++ b/src/lowparse/LowParse.Spec.Int.fsti
@@ -23,7 +23,7 @@ val parse_u8_spec
     let pp = parse parse_u8 b in
     Some? pp /\ (
     let (Some (v, consumed)) = pp in
-    U8.v v == E.be_to_n (Seq.slice b 0 1)
+    U8.v v == E.be_to_n (Seq.slice b 0 1) /\ consumed == 1
   )))
 
 val parse_u8_spec'
@@ -34,7 +34,7 @@ val parse_u8_spec'
     let pp = parse parse_u8 b in
     Some? pp /\ (
     let (Some (v, consumed)) = pp in
-    v == Seq.index b 0
+    v == Seq.index b 0 /\ consumed == 1
   )))
 
 val serialize_u8 : serializer parse_u8
@@ -66,7 +66,7 @@ val parse_u16_spec
     let pp = parse parse_u16 b in
     Some? pp /\ (
     let (Some (v, consumed)) = pp in
-    U16.v v == E.be_to_n (Seq.slice b 0 2)
+    U16.v v == E.be_to_n (Seq.slice b 0 2) /\ consumed == 2
   )))
 
 val serialize_u16 : serializer parse_u16
@@ -85,7 +85,7 @@ val parse_u32_spec
     let pp = parse parse_u32 b in
     Some? pp /\ (
     let (Some (v, consumed)) = pp in
-    U32.v v == E.be_to_n (Seq.slice b 0 4)
+    U32.v v == E.be_to_n (Seq.slice b 0 4) /\ consumed == 4
   )))
 
 val serialize_u32 : serializer parse_u32
@@ -104,7 +104,7 @@ val parse_u64_spec
     let pp = parse parse_u64 b in
     Some? pp /\ (
     let (Some (v, consumed)) = pp in
-    U64.v v == E.be_to_n (Seq.slice b 0 8)
+    U64.v v == E.be_to_n (Seq.slice b 0 8) /\ consumed == 8
   )))
 
 val serialize_u64 : serializer parse_u64
@@ -119,7 +119,7 @@ val parse_u64_le_spec
     let pp = parse parse_u64_le b in
     Some? pp /\ (
     let (Some (v, consumed)) = pp in
-    U64.v v == E.le_to_n (Seq.slice b 0 8)
+    U64.v v == E.le_to_n (Seq.slice b 0 8) /\ consumed == 8
   )))
 
 val serialize_u64_le : serializer parse_u64_le