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

Engine: F*: fix #677 by always extracting implicit types #679

Merged
merged 6 commits into from
May 22, 2024
Merged

Engine: F*: fix #677 by always extracting implicit types #679

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
1c9aa5b
feat(engine/fstar): add `mk_app`
W95Psp May 16, 2024
e65d678
feat(engine/fstar): extract implicit types
W95Psp May 16, 2024
59ea525
chore(tests): extract implicit types: refresh snapshots
W95Psp May 16, 2024
fe76cd4
fix(proof-libs): fix implicits
W95Psp May 21, 2024
bd532c1
fix(examples): bump an rlimit
W95Psp May 22, 2024
ecc3a12
chore(example): refresh extractions
W95Psp May 22, 2024
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
1 change: 1 addition & 0 deletions engine/backends/fstar/fstar_ast.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,7 @@ let mk_e_abs args body =
let mk_e_app base args =
AST.mkApp base (List.map ~f:(fun arg -> (arg, AST.Nothing)) args) dummyRange

let mk_app base args = AST.mkApp base args dummyRange
let unit = term AST.(Const Const_unit)

let tc_solve =
Expand Down
17 changes: 10 additions & 7 deletions engine/backends/fstar/fstar_backend.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -450,14 +450,17 @@ struct
@@ "pexpr: expected a integer, found the following non-digit \
chars: '" ^ s ^ "'");
F.AST.Const (F.Const.Const_int (s, None)) |> F.term
| App { f; args; generic_args } ->
let const_generics =
List.filter_map
~f:(function GConst e -> Some e | _ -> None)
generic_args
| App { f; args; generic_args; bounds_impls = _; impl = _ } ->
let generic_args =
generic_args
|> List.filter ~f:(function GType (TArrow _) -> false | _ -> true)
|> List.map ~f:(function
| GConst const -> (pexpr const, F.AST.Nothing)
| GLifetime _ -> .
| GType ty -> (pty e.span ty, F.AST.Hash))
in
let args = const_generics @ args in
F.mk_e_app (pexpr f) @@ List.map ~f:pexpr args
let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in
F.mk_app (pexpr f) (generic_args @ args)
| If { cond; then_; else_ } ->
F.term
@@ F.AST.If
Expand Down
10 changes: 6 additions & 4 deletions test-harness/src/snapshots/toolchain__attributes into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -172,9 +172,8 @@ let t_NoE =
x:
Alloc.String.t_String
{ let _, out:(Core.Str.Iter.t_Chars & bool) =
Core.Iter.Traits.Iterator.f_any (Core.Str.impl__str__chars (Core.Ops.Deref.f_deref x
<:
string)
Core.Iter.Traits.Iterator.f_any #Core.Str.Iter.t_Chars
(Core.Str.impl__str__chars (Core.Ops.Deref.f_deref #Alloc.String.t_String x <: string)
<:
Core.Str.Iter.t_Chars)
(fun ch ->
Expand All @@ -184,7 +183,10 @@ let t_NoE =
~.out }

let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_BoundedU8 1uy 23uy =
(Hax_lib.f_get x <: u8) +! (Hax_lib.f_get y <: u8) <: t_BoundedU8 1uy 23uy
(Hax_lib.f_get #(t_BoundedU8 12uy 15uy) x <: u8) +!
(Hax_lib.f_get #(t_BoundedU8 10uy 11uy) y <: u8)
<:
t_BoundedU8 1uy 23uy

let double (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
x +! x <: t_Even
Expand Down
16 changes: 9 additions & 7 deletions test-harness/src/snapshots/toolchain__generics into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ let dup
(#v_T: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T)
(x: v_T)
: (v_T & v_T) = Core.Clone.f_clone x, Core.Clone.f_clone x <: (v_T & v_T)
: (v_T & v_T) = Core.Clone.f_clone #v_T x, Core.Clone.f_clone #v_T x <: (v_T & v_T)

let f (v_N x: usize) : usize = (v_N +! v_N <: usize) +! x

Expand All @@ -79,8 +79,10 @@ let g
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Convert.t_Into v_T (t_Array usize v_N))
(arr: v_T)
: usize =
(Core.Option.impl__unwrap_or (Core.Iter.Traits.Iterator.f_max (Core.Iter.Traits.Collect.f_into_iter
(Core.Convert.f_into arr <: t_Array usize v_N)
(Core.Option.impl__unwrap_or #usize
(Core.Iter.Traits.Iterator.f_max #(Core.Array.Iter.t_IntoIter usize v_N)
(Core.Iter.Traits.Collect.f_into_iter #(t_Array usize v_N)
(Core.Convert.f_into #v_T #(t_Array usize v_N) arr <: t_Array usize v_N)
<:
Core.Array.Iter.t_IntoIter usize v_N)
<:
Expand All @@ -92,6 +94,7 @@ let g

let call_g (_: Prims.unit) : usize =
(g (sz 3)
#(t_Array usize (sz 3))
(let list = [sz 42; sz 3; sz 49] in
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
Rust_primitives.Hax.array_of_list 3 list)
Expand All @@ -102,10 +105,9 @@ let call_g (_: Prims.unit) : usize =
let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
let acc:usize = v_LEN +! sz 9 in
let acc:usize =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = v_LEN
}
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
usize)
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_LEN }
<:
Core.Ops.Range.t_Range usize)
<:
Expand Down
2 changes: 1 addition & 1 deletion test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () }

/// Entrypoint
let main (_: Prims.unit) : Prims.unit =
let _:Prims.unit = main_a (Foo <: t_Foo) in
let _:Prims.unit = main_a #t_Foo (Foo <: t_Foo) in
let _:Prims.unit = main_b () in
let _:Prims.unit = main_c () in
()
Expand Down
98 changes: 62 additions & 36 deletions test-harness/src/snapshots/toolchain__loops into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ info:
stderr: true
stdout: true
include_flag: ~
backend_options: ~
---
exit = 0
stderr = '''
Expand All @@ -39,11 +40,14 @@ let bool_returning (x: u8) : bool = x <. 10uy
let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
let acc:usize = sz 0 in
let chunks:Core.Slice.Iter.t_ChunksExact usize =
Core.Slice.impl__chunks_exact (Core.Ops.Deref.f_deref arr <: t_Slice usize) v_CHUNK_LEN
Core.Slice.impl__chunks_exact #usize
(Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize)
v_CHUNK_LEN
in
let acc:usize =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Clone.f_clone chunks

Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_ChunksExact
usize)
(Core.Clone.f_clone #(Core.Slice.Iter.t_ChunksExact usize) chunks
<:
Core.Slice.Iter.t_ChunksExact usize)
<:
Expand All @@ -54,7 +58,8 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
let chunk:t_Slice usize = chunk in
let mean:usize = sz 0 in
let mean:usize =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter chunk
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize)
chunk
<:
Core.Slice.Iter.t_Iter usize)
mean
Expand All @@ -67,10 +72,8 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
acc)
in
let acc:usize =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.Iter.impl_87__remainder
chunks
<:
t_Slice usize)
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize)
(Core.Slice.Iter.impl_87__remainder #usize chunks <: t_Slice usize)
<:
Core.Slice.Iter.t_Iter usize)
acc
Expand All @@ -84,7 +87,10 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
let composed_range (n: usize) : usize =
let acc:usize = sz 0 in
let acc:usize =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_chain
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Chain.t_Chain
(Core.Ops.Range.t_Range usize) (Core.Ops.Range.t_Range usize))
(Core.Iter.Traits.Iterator.f_chain #(Core.Ops.Range.t_Range usize)
#(Core.Ops.Range.t_Range usize)
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
<:
Core.Ops.Range.t_Range usize)
Expand All @@ -111,8 +117,14 @@ let composed_range (n: usize) : usize =
let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
let acc:usize = sz 0 in
let acc:usize =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
(Core.Slice.impl__chunks (Core.Ops.Deref.f_deref arr <: t_Slice usize) (sz 4)
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
(Core.Slice.Iter.t_Chunks usize))
(Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Chunks usize)
(Core.Slice.impl__chunks #usize
(Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
<:
t_Slice usize)
(sz 4)
<:
Core.Slice.Iter.t_Chunks usize)
<:
Expand All @@ -123,8 +135,10 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
(fun acc temp_1_ ->
let acc:usize = acc in
let i, chunk:(usize & t_Slice usize) = temp_1_ in
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
(Core.Slice.impl__iter chunk <: Core.Slice.Iter.t_Iter usize)
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
(Core.Slice.Iter.t_Iter usize))
(Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Iter usize)
(Core.Slice.impl__iter #usize chunk <: Core.Slice.Iter.t_Iter usize)
<:
Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter usize))
<:
Expand All @@ -141,12 +155,9 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =

let f (_: Prims.unit) : u8 =
let acc:u8 = 0uy in
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = 1uy;
Core.Ops.Range.f_end = 10uy
}
<:
Core.Ops.Range.t_Range u8)
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range u8
)
({ Core.Ops.Range.f_start = 1uy; Core.Ops.Range.f_end = 10uy } <: Core.Ops.Range.t_Range u8)
<:
Core.Ops.Range.t_Range u8)
acc
Expand All @@ -160,8 +171,10 @@ let f (_: Prims.unit) : u8 =
let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
let acc:usize = sz 0 in
let acc:usize =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.impl__iter (Core.Ops.Deref.f_deref
arr
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter
usize)
(Core.Slice.impl__iter #usize
(Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
<:
t_Slice usize)
<:
Expand All @@ -179,8 +192,10 @@ let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
let acc:usize = sz 0 in
let acc:usize =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.impl__iter (Core.Ops.Deref.f_deref
arr
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter
usize)
(Core.Slice.impl__iter #usize
(Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
<:
t_Slice usize)
<:
Expand All @@ -191,7 +206,9 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
(fun acc item ->
let acc:usize = acc in
let item:usize = item in
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_rev
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev
(Core.Ops.Range.t_Range usize))
(Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize)
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = item }
<:
Core.Ops.Range.t_Range usize)
Expand All @@ -204,8 +221,15 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
let acc:usize = acc in
let i:usize = i in
let acc:usize = acc +! sz 1 in
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_zip
(Core.Slice.impl__iter (Core.Ops.Deref.f_deref arr <: t_Slice usize)
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Zip.t_Zip
(Core.Slice.Iter.t_Iter usize) (Core.Ops.Range.t_Range usize))
(Core.Iter.Traits.Iterator.f_zip #(Core.Slice.Iter.t_Iter usize)
#(Core.Ops.Range.t_Range usize)
(Core.Slice.impl__iter #usize
(Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global)
arr
<:
t_Slice usize)
<:
Core.Slice.Iter.t_Iter usize)
({ Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = i }
Expand All @@ -230,7 +254,9 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize =
let acc:usize = sz 0 in
let acc:usize =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter arr
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Alloc.Vec.t_Vec
(usize & usize) Alloc.Alloc.t_Global)
arr
<:
Alloc.Vec.Into_iter.t_IntoIter (usize & usize) Alloc.Alloc.t_Global)
acc
Expand All @@ -244,10 +270,9 @@ let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize
let range1 (_: Prims.unit) : usize =
let acc:usize = sz 0 in
let acc:usize =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = sz 15
}
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
usize)
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 15 }
<:
Core.Ops.Range.t_Range usize)
<:
Expand All @@ -263,10 +288,9 @@ let range1 (_: Prims.unit) : usize =
let range2 (n: usize) : usize =
let acc:usize = sz 0 in
let acc:usize =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = n +! sz 10 <: usize
}
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
usize)
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n +! sz 10 <: usize }
<:
Core.Ops.Range.t_Range usize)
<:
Expand All @@ -282,7 +306,9 @@ let range2 (n: usize) : usize =
let rev_range (n: usize) : usize =
let acc:usize = sz 0 in
let acc:usize =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_rev
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev
(Core.Ops.Range.t_Range usize))
(Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize)
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
<:
Core.Ops.Range.t_Range usize)
Expand Down
Loading
Loading