From 8f58bfde3085f76a3e772e71ad3fdb53ed2c46e7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Sun, 6 Oct 2024 08:49:23 -0700
Subject: [PATCH 1/2] Enable --ext __unrefine everwhere (checker + lib +
examples)
---
Pulse.fst.config.json | 4 ++--
lib/pulse/Pulse.fst.config.json | 1 +
lib/pulse/core/Pulse.fst.config.json | 4 ++--
share/pulse/Makefile.include-base | 2 +-
share/pulse/examples/Pulse.fst.config.json | 4 ++--
src/checker/PulseChecker.fst.config.json | 4 ++--
6 files changed, 10 insertions(+), 9 deletions(-)
diff --git a/Pulse.fst.config.json b/Pulse.fst.config.json
index 78ae24736..d1a7cabf9 100644
--- a/Pulse.fst.config.json
+++ b/Pulse.fst.config.json
@@ -4,8 +4,8 @@
"--query_cache",
"--load_cmxs",
"pulse",
- "--ext",
- "context_pruning"
+ "--ext", "__unrefine",
+ "--ext", "context_pruning"
],
"include_dirs": [
"lib/pulse",
diff --git a/lib/pulse/Pulse.fst.config.json b/lib/pulse/Pulse.fst.config.json
index d37c87599..1ab8bd54c 100644
--- a/lib/pulse/Pulse.fst.config.json
+++ b/lib/pulse/Pulse.fst.config.json
@@ -3,6 +3,7 @@
"options": [
"--query_cache",
"--load_cmxs", "pulse",
+ "--ext", "__unrefine",
"--ext", "context_pruning"
],
"include_dirs": [
diff --git a/lib/pulse/core/Pulse.fst.config.json b/lib/pulse/core/Pulse.fst.config.json
index cf6a55f62..a1246cc1a 100644
--- a/lib/pulse/core/Pulse.fst.config.json
+++ b/lib/pulse/core/Pulse.fst.config.json
@@ -2,8 +2,8 @@
"fstar_exe": "fstar.exe",
"options": [
"--query_cache",
- "--ext",
- "context_pruning"
+ "--ext", "__unrefine",
+ "--ext", "context_pruning"
],
"include_dirs": [
]
diff --git a/share/pulse/Makefile.include-base b/share/pulse/Makefile.include-base
index bb8b6fa58..a12032d41 100644
--- a/share/pulse/Makefile.include-base
+++ b/share/pulse/Makefile.include-base
@@ -19,7 +19,7 @@ else
USE_HINTS:=
endif
-FSTAR_OPTIONS += $(USE_HINTS) --ext context_pruning
+FSTAR_OPTIONS += $(USE_HINTS) --ext context_pruning --ext __unrefine
# A place to put all build artifacts
ifneq (,$(OUTPUT_DIRECTORY))
diff --git a/share/pulse/examples/Pulse.fst.config.json b/share/pulse/examples/Pulse.fst.config.json
index 51f3a0063..7019c5279 100644
--- a/share/pulse/examples/Pulse.fst.config.json
+++ b/share/pulse/examples/Pulse.fst.config.json
@@ -8,8 +8,8 @@
"_output/cache",
"--warn_error",
"-249",
- "--ext",
- "context_pruning"
+ "--ext", "__unrefine",
+ "--ext", "context_pruning"
],
"include_dirs": [
"../../../lib/pulse",
diff --git a/src/checker/PulseChecker.fst.config.json b/src/checker/PulseChecker.fst.config.json
index a4a4dc6a1..c57f6d609 100644
--- a/src/checker/PulseChecker.fst.config.json
+++ b/src/checker/PulseChecker.fst.config.json
@@ -2,8 +2,8 @@
"fstar_exe": "fstar.exe",
"options": [
"--query_cache",
- "--ext",
- "context_pruning"
+ "--ext", "__unrefine",
+ "--ext", "context_pruning"
],
"include_dirs": [
]
From ced3f4ac69df1c66533a4b72c59c4b412f88bf87 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Sun, 6 Oct 2024 09:24:24 -0700
Subject: [PATCH 2/2] Fixes for --ext __unrefine, some annotations
---
lib/pulse/c/Pulse.C.Types.Scalar.fsti | 2 +-
lib/pulse/core/PulseCore.HeapExtension.fst | 2 +-
lib/pulse/core/PulseCore.MemoryAlt.fst | 4 ++--
lib/pulse/lib/Pulse.Lib.HashTable.Spec.fst | 12 ++++++++----
lib/pulse/lib/Pulse.Lib.HigherArray.fst | 3 +--
src/checker/Pulse.Checker.Prover.Match.Matchers.fst | 2 +-
src/checker/Pulse.Typing.Env.fst | 2 +-
7 files changed, 15 insertions(+), 12 deletions(-)
diff --git a/lib/pulse/c/Pulse.C.Types.Scalar.fsti b/lib/pulse/c/Pulse.C.Types.Scalar.fsti
index 3a62baebf..e4e4a88e2 100644
--- a/lib/pulse/c/Pulse.C.Types.Scalar.fsti
+++ b/lib/pulse/c/Pulse.C.Types.Scalar.fsti
@@ -134,7 +134,7 @@ let read_prf
p' == p
))
=
- let prf v0' p' : Lemma
+ let prf v0' (p':perm) : Lemma
(requires (mk_fraction (scalar t) (mk_scalar v0') p' == mk_fraction (scalar t) (mk_scalar v0) p))
(ensures (v0' == Ghost.reveal v0 /\ p' == Ghost.reveal p))
= mk_scalar_inj (Ghost.reveal v0) v0' p p'
diff --git a/lib/pulse/core/PulseCore.HeapExtension.fst b/lib/pulse/core/PulseCore.HeapExtension.fst
index f4d3fcd5f..2760c1029 100644
--- a/lib/pulse/core/PulseCore.HeapExtension.fst
+++ b/lib/pulse/core/PulseCore.HeapExtension.fst
@@ -1897,7 +1897,7 @@ let distinct_invariants_have_distinct_names
let invariant_name_identifies_invariant
(#h:heap_sig u#a)
(e:inames (extend h))
- (p q:ext_slprop h)
+ (p q:(extend h).slprop)
(i:iiref h)
(j:iiref h{ i == j } )
: ghost_action_except (extend h)
diff --git a/lib/pulse/core/PulseCore.MemoryAlt.fst b/lib/pulse/core/PulseCore.MemoryAlt.fst
index d0189b12b..67dc9bf1d 100644
--- a/lib/pulse/core/PulseCore.MemoryAlt.fst
+++ b/lib/pulse/core/PulseCore.MemoryAlt.fst
@@ -617,7 +617,7 @@ let distinct_invariants_have_distinct_names_alt
(q:slprop u#m { p =!= q })
(i j:iref)
: pst_ghost_action_except u#0 u#m
- (squash (~(eq2 #(E.iiref sig_1) (reveal_iref i) (reveal_iref j))))
+ (squash (reveal_iref i =!= reveal_iref j))
e
(inv i p `star` inv j q)
(fun _ -> inv i p `star` inv j q)
@@ -640,7 +640,7 @@ let distinct_invariants_have_distinct_names
(q:slprop u#m { p =!= q })
(i j:iref)
: pst_ghost_action_except u#0 u#m
- (squash (~(eq2 #iref i j)))
+ (squash (i =!= j))
e
(inv i p `star` inv j q)
(fun _ -> inv i p `star` inv j q)
diff --git a/lib/pulse/lib/Pulse.Lib.HashTable.Spec.fst b/lib/pulse/lib/Pulse.Lib.HashTable.Spec.fst
index 9ccf6a37e..5c164ce03 100644
--- a/lib/pulse/lib/Pulse.Lib.HashTable.Spec.fst
+++ b/lib/pulse/lib/Pulse.Lib.HashTable.Spec.fst
@@ -172,7 +172,8 @@ let repr_t_sz kt vt sz = r:repr_t kt vt { r.sz == sz}
let lemma_clean_upd_lookup_walk #kt #vt #sz
(spec1 spec2 : spec_t kt vt)
(repr1 repr2 : repr_t_sz kt vt sz)
- idx k v (k':_{k =!= k'})
+ (idx : nat{idx < repr1.sz})
+ k v (k':_{k =!= k'})
: Lemma (requires
repr_related repr1 repr2
/\ (forall i. i < repr1.sz /\ i <> idx ==> repr1 @@ i == repr2 @@ i)
@@ -206,7 +207,8 @@ let lemma_clean_upd_lookup_walk #kt #vt #sz
let lemma_used_upd_lookup_walk #kt #vt #sz
(spec1 spec2 : spec_t kt vt)
(repr1 repr2 : repr_t_sz kt vt sz)
- idx k (k':_{k =!= k'})
+ (idx : nat{idx < repr1.sz})
+ k (k':_{k =!= k'})
(v v' : vt)
: Lemma (requires
repr_related repr1 repr2
@@ -244,7 +246,8 @@ let lemma_used_upd_lookup_walk #kt #vt #sz
let lemma_del_lookup_walk #kt #vt #sz
(spec1 spec2 : spec_t kt vt)
(repr1 repr2 : repr_t_sz kt vt sz)
- upos k v (k':_{k =!= k'})
+ (upos : nat{upos < repr1.sz})
+ k v (k':_{k =!= k'})
: Lemma (requires
repr_related repr1 repr2 /\
(forall i. i < sz /\ i <> upos ==> repr1 @@ i == repr2 @@ i) /\
@@ -278,7 +281,8 @@ let lemma_del_lookup_walk #kt #vt #sz
let lemma_zombie_upd_lookup_walk #kt #vt #sz
(spec spec' : spec_t kt vt)
(repr repr' : repr_t_sz kt vt sz)
- idx k v (k':_{k =!= k'})
+ (idx : nat{idx < repr.sz})
+ k v (k':_{k =!= k'})
: Lemma (requires
repr_related repr repr'
/\ (forall i. i < sz /\ i <> idx ==> repr @@ i == repr' @@ i)
diff --git a/lib/pulse/lib/Pulse.Lib.HigherArray.fst b/lib/pulse/lib/Pulse.Lib.HigherArray.fst
index 1247c6e07..276d6faeb 100644
--- a/lib/pulse/lib/Pulse.Lib.HigherArray.fst
+++ b/lib/pulse/lib/Pulse.Lib.HigherArray.fst
@@ -538,7 +538,7 @@ fn pts_to_range_prop'
(#s: Seq.seq elt)
requires pts_to_range a i j #p s
ensures pts_to_range a i j #p s ** pure (
- (i <= j /\ j <= length a /\ Seq.length s == j - i)
+ (i <= j /\ j <= length a /\ eq2 #nat (Seq.length s) (j - i))
)
{
unfold pts_to_range a i j #p s;
@@ -550,7 +550,6 @@ ensures pts_to_range a i j #p s ** pure (
let pts_to_range_prop = pts_to_range_prop'
-
ghost
fn pts_to_range_intro'
(#elt: Type)
diff --git a/src/checker/Pulse.Checker.Prover.Match.Matchers.fst b/src/checker/Pulse.Checker.Prover.Match.Matchers.fst
index 80f308246..cb6b506eb 100644
--- a/src/checker/Pulse.Checker.Prover.Match.Matchers.fst
+++ b/src/checker/Pulse.Checker.Prover.Match.Matchers.fst
@@ -289,7 +289,7 @@ let head_is_uvar (uvs:env) (t:term) : T.Tac bool =
let hd, _ = T.collect_app t in
match T.inspect hd with
| T.Tv_Var v ->
- List.existsb (fun (x, _) -> x = v.uniq) (bindings uvs)
+ List.existsb (fun (x, _) -> (x <: var) = v.uniq) (bindings uvs)
| _ -> false
(**************** The actual matchers *)
diff --git a/src/checker/Pulse.Typing.Env.fst b/src/checker/Pulse.Typing.Env.fst
index c3fad92f1..d96c52a3a 100644
--- a/src/checker/Pulse.Typing.Env.fst
+++ b/src/checker/Pulse.Typing.Env.fst
@@ -158,7 +158,7 @@ let rec remove_binding_aux (g:env)
let m = Map.restrict (Set.complement (Set.singleton x)) (Map.upd g.m x tm_unknown) in
// we need uniqueness invariant in the representation
assume (forall (b:var & typ). List.Tot.memP b prefix <==> (List.Tot.memP b g.bs /\
- fst b =!= x));
+ fst b =!= (x <: var)));
let g' = {g with bs = prefix; names=prefix_names; m} in
assert (equal g (push_env (push_binding (mk_env (fstar_env g)) x ppname_default t) g'));
x, t, g'