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.

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

EverParse+Pulse: Verified parsing and serialization with separation logic #155

Open
wants to merge 112 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
112 commits
Select commit Hold shift + click to select a range
638269a
pts_to_serialized, validator, jumper, peek, CPS reader, read
tahina-pro Jul 3, 2024
9777ccf
WIP LowParse.Pulse.Combinators
tahina-pro Jul 8, 2024
573761d
integer readers
tahina-pro Jul 8, 2024
b084439
validate, jump int
tahina-pro Jul 8, 2024
de8c900
switch to CPS validators
tahina-pro Jul 8, 2024
2e9bf08
synth, filter
tahina-pro Jul 9, 2024
cf0534c
validate_nonempty
tahina-pro Jul 9, 2024
7209ceb
validate_nondep_then
tahina-pro Jul 9, 2024
cbf928e
common validate_dtuple2 and nondep_then
tahina-pro Jul 9, 2024
6352265
split_dtuple2, simplified split_nondep_then
tahina-pro Jul 9, 2024
53d8e8b
jump_nondep_then, jump_dtuple2
tahina-pro Jul 9, 2024
4fd8c75
validate_and_read
tahina-pro Jul 9, 2024
ad30058
validate_filter -> validate_and_read_filter
tahina-pro Jul 9, 2024
dc5e56b
validate_dtuple2 with validate_and_read tag, remove validate_nondep_then
tahina-pro Jul 9, 2024
fd887c5
restore validate_nondep_then
tahina-pro Jul 9, 2024
cb95617
validate_and_read_dtuple2
tahina-pro Jul 9, 2024
14f5bac
read_synth, read_filter
tahina-pro Jul 10, 2024
b44c18b
validate_and_read_synth
tahina-pro Jul 10, 2024
9383b8c
bitsum
tahina-pro Jul 10, 2024
4b29d00
validate_and_read integers; ret, empty; etc.
tahina-pro Jul 11, 2024
944b32d
ifthenelse_jumper, jump_ret, jump_empty
tahina-pro Jul 11, 2024
769d3b1
some extraction fixes: avoid pure lets in F* assemblies, replace reco…
tahina-pro Jul 11, 2024
376403d
mark more combinators inline_for_extraction
tahina-pro Jul 11, 2024
9d360cb
Karamel chokes on tuples. Use a custom slice_pair type instead
tahina-pro Jul 12, 2024
92f6343
Karamel chokes on local ghost functions, hoist them instead (mainly f…
tahina-pro Jul 12, 2024
5e76a3f
slice_pair moved to Pulse
tahina-pro Jul 12, 2024
39a4638
read then pure cont
tahina-pro Jul 12, 2024
f9a36f3
read with pure continuation
tahina-pro Jul 12, 2024
b5f83df
pure_read_ext, empty, dtuple, ifthenelse
tahina-pro Jul 12, 2024
ff928b0
properly normalize integer readers
tahina-pro Jul 12, 2024
5d088a0
replace CPS reader with pure_reader
tahina-pro Jul 13, 2024
cf0a5ba
restore validate_and_read_intro, jump_dtuple2, with leaf_reader this …
tahina-pro Jul 13, 2024
626d975
revert to non-CPS validators; jumpers with offsets instead of sizes
tahina-pro Jul 15, 2024
f85e1c0
eta-expand validate_synth because of the pure bind
tahina-pro Jul 15, 2024
0238383
ifthenelse_validator
tahina-pro Jul 16, 2024
fc169dd
bound offset on validator failure
tahina-pro Jul 16, 2024
d75f3b6
jump_vclist; dtuple2, nondep_then, nlist accessors
tahina-pro Jul 17, 2024
4c57be3
pts_to_serialized_nlist_1, pts_to_serialized_length, etc.
tahina-pro Jul 18, 2024
a8eb400
Util: stick -> trade
tahina-pro Jul 19, 2024
6dee4b9
move all trade lemmas to Pulse.Lib.Trade.Util
tahina-pro Jul 19, 2024
65945cb
LowParse.Pulse: stick -> trade
tahina-pro Jul 19, 2024
e93bb12
LowParse.Pulse: remove now implicit arguments to trade operations
tahina-pro Jul 19, 2024
709bf3b
LowParse.Pulse: stick -> trade in names
tahina-pro Jul 19, 2024
e1ff2c4
LowParse.Pulse: vprop -> slprop
tahina-pro Jul 19, 2024
1dc81c2
WIP write
tahina-pro Jul 22, 2024
f922d50
WIP ghost parsers
tahina-pro Jul 23, 2024
50ebfeb
convert LowParse.Pulse back to ghost parsers, serializers (WIP impl_p…
tahina-pro Jul 23, 2024
bd2955d
WIP serialize
tahina-pro Jul 25, 2024
a723657
writer, size lenses
tahina-pro Jul 25, 2024
0e7e174
compute_remaining_size_constant_size
tahina-pro Jul 26, 2024
6986044
fuse Write into Base
tahina-pro Jul 26, 2024
26891a1
compose writing lenses, write ints
tahina-pro Jul 26, 2024
caea2d3
WIP l2r_write_dtuple2
tahina-pro Jul 30, 2024
6d47866
write dtuple2, nondep_then
tahina-pro Jul 30, 2024
6b86b7a
l2r_write_synth
tahina-pro Aug 1, 2024
eca27ba
l2r_write_filter
tahina-pro Aug 1, 2024
5917d64
l2r_leaf_writer_ext
tahina-pro Aug 1, 2024
05e9b22
l2r_leaf_write_filter
tahina-pro Aug 2, 2024
8ca9313
WHY WHY WHY are lambdas no longer usable in slprops?
tahina-pro Aug 22, 2024
59e59a0
lowparse: remove LowParse.Pulse.Util
tahina-pro Sep 6, 2024
24f2db9
WIP more l2r_writer combinators
tahina-pro Sep 27, 2024
88251c3
serialization combinators with reverse handling of vmatch
tahina-pro Oct 1, 2024
4d569ba
l2r_writer_ifthenelse
tahina-pro Oct 1, 2024
a3ba19f
serialize seqbytes by copy
tahina-pro Oct 1, 2024
deb455c
extensionality with explicit type equality in vmatch
tahina-pro Oct 1, 2024
ef51cfd
vmatch should act on low-level data bundled with perm
tahina-pro Oct 2, 2024
bc979a7
WIP l2r_write_nlist_as_array
tahina-pro Oct 4, 2024
a03661d
l2r_write_nlist_as_array
tahina-pro Oct 4, 2024
e771aa9
nlist_match_array: make varray partial
tahina-pro Oct 4, 2024
7dd28f6
move nlist_match_array_intro to LowParse.Pulse.VCList
tahina-pro Oct 4, 2024
19ea2f5
nlist_sorted
tahina-pro Oct 9, 2024
a74cccc
l2r_leaf_writer_ifthenelse
tahina-pro Oct 10, 2024
c9e131f
test extraction of CBOR serializer
tahina-pro Oct 10, 2024
430fac5
write_header
tahina-pro Oct 10, 2024
ac651f1
adjust proofs to new official Pulse slices
tahina-pro Oct 11, 2024
da4929e
move lemmas to LowParse.Pulse
tahina-pro Oct 15, 2024
4caa9b9
WIP serialize tagged
tahina-pro Oct 16, 2024
6bd6456
compute_remaining_size combinators
tahina-pro Oct 16, 2024
1c6683f
extract the validator, the parser and the serializer
tahina-pro Oct 16, 2024
367716a
towards sharing of Makefiles
tahina-pro Oct 25, 2024
9a15bae
ignore response files
tahina-pro Oct 25, 2024
1b08afc
recover build of lowparse/pulse
tahina-pro Oct 25, 2024
9b78c60
use --ext context_pruning with new Makefiles
tahina-pro Oct 25, 2024
2c3edcc
CI: install pulse, build lowparse/pulse
tahina-pro Oct 25, 2024
2ae077b
also install Pulse to build the binary package (even though it's not …
tahina-pro Oct 26, 2024
bfeaa30
fix standalone CI
tahina-pro Oct 28, 2024
3593766
(TEMP) use FStarLang/pulse#247
tahina-pro Oct 29, 2024
28f4e3b
remove slice_pair
tahina-pro Oct 29, 2024
848ec7a
Revert "(TEMP) use FStarLang/pulse#247"
tahina-pro Oct 30, 2024
7f0579b
Merge branch 'master' of github.com:project-everest/everparse into _t…
tahina-pro Dec 5, 2024
650078a
serilize vclist from a slice
tahina-pro Nov 9, 2024
dfbe4f5
pts_to_serialized_ext_trade_gen, validate_filter_gen, pts_to_serializ…
tahina-pro Nov 13, 2024
540a89e
ghost_split, join dtuple2, nondep_then, associativity, rewrite under …
tahina-pro Nov 15, 2024
f376ae0
pts_to_serialized_ext_nondep_then_left, nlist_hd_tl_nondep_then_left
tahina-pro Nov 18, 2024
7b0eb19
use the shared Makefiles for LowParse
tahina-pro Oct 26, 2024
5e27207
Merge branch 'master' into _taramana_pulse
tahina-pro Dec 21, 2024
65398bd
skip CI dependency build for binary package
tahina-pro Dec 22, 2024
f3ae96b
missing packages for standalone build
tahina-pro Dec 22, 2024
61e673b
CI: bootstrap F*
tahina-pro Jan 2, 2025
2a41fcb
Pulse no longer follows FHS, need to use its `out/` subdirectory
tahina-pro Jan 2, 2025
af1a606
Merge branch 'master' of github.com:project-everest/everparse into ta…
tahina-pro Jan 14, 2025
db4cc1c
pulse.Makefile: Simplify
mtzguido Jan 8, 2025
f394a53
with @mtzguido: fstar.exe: no longer use FSTAR_HOME
tahina-pro Jan 14, 2025
5e572ee
with @mtzguido: Use karamel's -fstar option to make sure we respect F…
tahina-pro Jan 14, 2025
ffe2ad0
common.Makefile: no longer use FSTAR_HOME
tahina-pro Jan 14, 2025
9a45eaf
install Pulse as part of the new CI
tahina-pro Jan 14, 2025
39a0cc8
Merge branch 'master' of github.com:project-everest/everparse into _t…
tahina-pro Jan 26, 2025
99e1321
pts_to_serialized_copy
tahina-pro Jan 26, 2025
47cb3b7
pts_to_serialized_share, gather
tahina-pro Jan 28, 2025
1712fb6
Merge branch 'master' into _taramana_pulse
tahina-pro Feb 1, 2025
379ff8a
backport #170
tahina-pro Feb 26, 2025
8055951
Merge branch 'master' of github.com:project-everest/everparse into _t…
tahina-pro Feb 26, 2025
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
Prev Previous commit
Next Next commit
read with pure continuation
tahina-pro committed Oct 25, 2024
commit f9a36f30266c5e911dd81577075958609e2a3800
54 changes: 54 additions & 0 deletions src/lowparse/pulse/LowParse.Pulse.Base.fst
Original file line number Diff line number Diff line change
@@ -676,6 +676,60 @@ let reader_of_leaf_reader
: reader s
= reader_of_leaf_reader' r

inline_for_extraction
let pure_reader
(#t: Type0)
(#k: parser_kind)
(#p: parser k t)
(s: serializer p)
: Tot Type
= (input: slice byte) ->
(#pm: perm) ->
(#v: Ghost.erased t) ->
(t': Type0) ->
(f: ((x: t { x == Ghost.reveal v }) -> Tot t')) ->
stt t' (pts_to_serialized s input #pm v) (fun x' -> pts_to_serialized s input #pm v ** pure (x' == f v))

inline_for_extraction
```pulse
fn pure_read
(#t: Type0)
(#k: parser_kind)
(#p: parser k t)
(#s: serializer p)
(r: pure_reader s)
(input: slice byte)
(#pm: perm)
(#v: Ghost.erased t)
requires (pts_to_serialized s input #pm v)
returns v' : t
ensures (pts_to_serialized s input #pm v' ** pure (Ghost.reveal v == v'))
{
r input #pm #v t id
}
```

inline_for_extraction
```pulse
fn pure_reader_of_leaf_reader
(#t: Type0)
(#k: parser_kind)
(#p: parser k t)
(#s: serializer p)
(r: leaf_reader s)
: pure_reader #t #k #p s
=
(input: slice byte)
(#pm: perm)
(#v: Ghost.erased t)
(t': Type0)
(f: _)
{
let x = r input #pm #v;
f x
}
```

inline_for_extraction
let validate_and_read (#t: Type0) (#k: parser_kind) (p: parser k t) : Tot Type =
(input: slice byte) ->
33 changes: 33 additions & 0 deletions src/lowparse/pulse/LowParse.Pulse.BitSum.fst
Original file line number Diff line number Diff line change
@@ -122,3 +122,36 @@ let read_bitsum'
stt_cps_ifthenelse
(read_bitsum'_cont b)
)

inline_for_extraction
let pure_read_synth_cont_ifthenelse
(#t: Type0)
(x: Ghost.erased t)
: Tot (if_combinator_weak (pure_read_synth_cont_t #t x))
= fun cond iftrue iffalse t' g' -> if cond then iftrue () t' g' else iffalse () t' g'

inline_for_extraction
let pure_read_bitsum'
(#t: eqtype)
(#tot: pos)
(#cl: uint_t tot t)
(#b: bitsum' cl tot)
(d: destr_bitsum'_t b)
(#k: parser_kind)
(#p: parser k t)
(#s: serializer p)
(r: pure_reader s)
: Tot (pure_reader (tot_serialize_bitsum' b s))
= pure_read_synth
(pure_read_filter
r
(filter_bitsum' b)
)
(synth_bitsum'_injective b; synth_bitsum' b)
(synth_bitsum'_recip_inverse b; synth_bitsum'_recip b)
(
d
(pure_read_synth_cont_t #(bitsum'_type b))
(pure_read_synth_cont_ifthenelse #(bitsum'_type b))
(pure_read_synth_cont_init)
)
91 changes: 85 additions & 6 deletions src/lowparse/pulse/LowParse.Pulse.Combinators.fst
Original file line number Diff line number Diff line change
@@ -359,6 +359,58 @@ let read_synth'
: Tot (reader (tot_serialize_synth p1 f2 s1 f1 ()))
= read_synth r f2 f1 (fun x -> intro_stt_cps (f2 x))

inline_for_extraction
let pure_read_synth_cont_t
(#t: Type0)
(x: t)
= (t': Type0) -> (g': ((y: t { y == x }) -> t')) -> (y': t' { y' == g' x })

inline_for_extraction
let pure_read_synth_cont
(#t1 #t2: Type0)
(f2: (t1 -> Tot t2))
(f2': ((x: t1) -> pure_read_synth_cont_t (f2 x)))
(x1: Ghost.erased t1)
(t': Type0)
(g: ((x2: t2 { x2 == f2 x1 }) -> Tot t'))
(x1': t1 { x1' == Ghost.reveal x1 })
: Tot t'
= f2' x1' t' g

inline_for_extraction
```pulse
fn pure_read_synth
(#k1: parser_kind) (#t1: Type0) (#p1: parser k1 t1) (#s1: serializer p1) (r: pure_reader s1)
(#t2: Type0) (f2: (t1 -> Tot t2) { synth_injective f2 }) (f1: (t2 -> Tot t1) { synth_inverse f2 f1 })
(f2': ((x: t1) -> pure_read_synth_cont_t (f2 x)))
: pure_reader #t2 #k1 #(tot_parse_synth p1 f2) (tot_serialize_synth p1 f2 s1 f1 ())
= (input: slice byte)
(#pm: _)
(#v: _)
(t': Type0)
(g: _)
{
pts_to_serialized_synth_l2r_stick s1 f2 f1 input;
let res = r input #pm #(f1 v) t' (pure_read_synth_cont f2 f2' (f1 v) t' g);
elim_stick _ _;
res
}
```

inline_for_extraction
let pure_read_synth_cont_init
(#t: Type0)
(x: t)
: Tot (pure_read_synth_cont_t #t x)
= fun t' g' -> g' x

inline_for_extraction
let pure_read_synth'
(#k1: parser_kind) (#t1: Type0) (#p1: parser k1 t1) (#s1: serializer p1) (r: pure_reader s1)
(#t2: Type0) (f2: (t1 -> Tot t2) { synth_injective f2 }) (f1: (t2 -> Tot t1) { synth_inverse f2 f1 })
: pure_reader #t2 #k1 #(tot_parse_synth p1 f2) (tot_serialize_synth p1 f2 s1 f1 ())
= pure_read_synth r f2 f1 (fun x -> pure_read_synth_cont_init (f2 x))

inline_for_extraction
```pulse
fn validate_and_read_synth_cont_cont
@@ -570,14 +622,12 @@ fn pts_to_serialized_filter_intro
(f: (t -> bool))
(input: slice byte)
(#pm: perm)
(#v: Ghost.erased t)
(#v: t)
requires (pts_to_serialized s input #pm v ** pure (f v == true))
ensures exists* (v': parse_filter_refine f) . pts_to_serialized (tot_serialize_filter s f) input #pm v' ** pure ((v' <: t) == Ghost.reveal v)
ensures exists* (v': parse_filter_refine f) . pts_to_serialized (tot_serialize_filter s f) input #pm v' ** pure ((v' <: t) == v)
{
unfold (pts_to_serialized s input #pm v);
let sq: squash (f v == true) = ();
let v' : Ghost.erased (parse_filter_refine f) = Ghost.hide (parse_filter_refine_intro #t f (Ghost.reveal v) sq);
fold (pts_to_serialized (tot_serialize_filter s f) input #pm v');
fold (pts_to_serialized (tot_serialize_filter s f) input #pm v);
}
```

@@ -591,7 +641,7 @@ fn pts_to_serialized_filter_elim
(f: (t -> bool))
(input: slice byte)
(#pm: perm)
(#v: Ghost.erased (parse_filter_refine f))
(#v: parse_filter_refine f)
requires (pts_to_serialized (tot_serialize_filter s f) input #pm v)
ensures pts_to_serialized s input #pm v
{
@@ -618,6 +668,35 @@ fn read_filter
}
```

inline_for_extraction
let pure_read_filter_cont
(#t: Type0)
(f: t -> bool)
(v: Ghost.erased (parse_filter_refine f))
(t': Type0)
(g: (x: parse_filter_refine f { x == Ghost.reveal v }) -> t')
(x: t { x == Ghost.reveal #t (Ghost.hide #t (Ghost.reveal v)) })
: Tot t'
= g x

inline_for_extraction
```pulse
fn pure_read_filter
(#k1: parser_kind) (#t1: Type0) (#p1: parser k1 t1) (#s1: serializer p1) (r: pure_reader s1) (f: (t1 -> bool))
: pure_reader #(parse_filter_refine f) #(parse_filter_kind k1) #(tot_parse_filter p1 f) (tot_serialize_filter s1 f)
= (input: slice byte)
(#pm: _)
(#v: _)
(t': Type0)
(g: _)
{
pts_to_serialized_filter_elim s1 f input;
let res = r input #pm #(Ghost.hide (Ghost.reveal v)) t' (pure_read_filter_cont f v t' g);
pts_to_serialized_filter_intro s1 f input;
res
}
```

let pair_of_dtuple2
(#t1 #t2: Type)
(x: dtuple2 t1 (fun _ -> t2))