Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fully specify integer parsers #130

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Fully specify integer parsers #130

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 22 additions & 7 deletions src/lowparse/LowParse.Spec.BoundedInt.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand All @@ -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)
Expand All @@ -160,15 +175,17 @@ 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))
= (fun (x: bounded_integer sz) ->
E.n_to_le sz (U32.v x)
)

#push-options "--z3rlimit 16"

let serialize_bounded_integer_le_correct
(sz: integer_size)
: Lemma
Expand All @@ -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;
Expand Down
22 changes: 22 additions & 0 deletions src/lowparse/LowParse.Spec.BoundedInt.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down
12 changes: 6 additions & 6 deletions src/lowparse/LowParse.Spec.Int.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Loading