emit: let an inline-Pulse postcondition determine the result - #247
Draft
nikswamy wants to merge 3 commits into
Draft
emit: let an inline-Pulse postcondition determine the result#247nikswamy wants to merge 3 commits into
nikswamy wants to merge 3 commits into
Conversation
A `_pure` function with a body is emitted as an F* `let`, but a `_pure` function without one fell through to the ordinary external-declaration path and became a state-passing `fn` with an unreachable body. That made external pure operations unusable in specifications: Pulse rejects a stateful application in a pre- or postcondition with "cannot use ... in impure spec". Emit them as `assume val` instead, sharing the signature elaboration with the defined case so both forms agree on parameters, the `Pure` effect wrapper, and contract placement. Call sites already emit a plain application, so nothing about calling such a function changes. This is what lets a checked-arithmetic routine be given the contract its header documents. Its result is only meaningful when its status says it did not overflow, and that status is classified by another external pure operation, so the postcondition has to name one external pure function to say anything about the result of another. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit cddb926)
…33-inline-pulse-ensures
`_ensures(return == E)` is emitted as Pulse's `rewrites_to` when `E` does not
mention the result, which is what lets the prover substitute for the result
rather than carry an equation about it. The test for "does `E` mention the
result" answered conservatively -- `true` -- for any expression form it did not
recognise, and an inline-Pulse fragment was one of those. So a clause of the
shape
_ensures(return == (_Bool)_inline_pulse(f $(A) $(B)))
was emitted as a plain equality instead.
That is the only way to say "this function decides that predicate", and it has
a consequence beyond the prover's convenience: the impure-spec elaborator,
which is what turns an assertion over a stateful call into a proposition, looks
for exactly a `rewrites_to` in the callee's postcondition. Without one it has
no term to name the result by, and an `_assert` over such a call fails to
elaborate with "cannot find rewrites_to in post".
An inline-Pulse fragment can only reach the result through an antiquotation, so
looking inside its antiquotations is both sufficient and precise; the verbatim
tokens around them cannot reintroduce it.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d
(cherry picked from commit 7ddb7ed)
Contributor
|
!diff |
Generated F* output diffEffect of this pull request on the F* code SummaryFull diff: full diff artifact Diffdiff --git base/c_assert/Func_pal_c_assert_enabled.fst head/c_assert/Func_pal_c_assert_enabled.fst
index ad5d080..218c7b8 100644
--- base/c_assert/Func_pal_c_assert_enabled.fst
+++ head/c_assert/Func_pal_c_assert_enabled.fst
@@ -3,6 +3,4 @@ open Pulse
open Pulse.Lib.C
#lang-pulse
-divergent fn func_pal_c_assert_enabled ()
- returns return_1 : bool
-{ assume pure False; unreachable () }
\ No newline at end of file
+assume val func_pal_c_assert_enabled () : bool
\ No newline at end of file
diff --git base/containing_record/Func_pal_c_assert_enabled.fst head/containing_record/Func_pal_c_assert_enabled.fst
index ad5d080..218c7b8 100644
--- base/containing_record/Func_pal_c_assert_enabled.fst
+++ head/containing_record/Func_pal_c_assert_enabled.fst
@@ -3,6 +3,4 @@ open Pulse
open Pulse.Lib.C
#lang-pulse
-divergent fn func_pal_c_assert_enabled ()
- returns return_1 : bool
-{ assume pure False; unreachable () }
\ No newline at end of file
+assume val func_pal_c_assert_enabled () : bool
\ No newline at end of file
diff --git base/dpe/Func_compare.fst head/dpe/Func_compare.fst
index acf7f02..29abe4a 100644
--- base/dpe/Func_compare.fst
+++ head/dpe/Func_compare.fst
@@ -12,7 +12,7 @@ divergent fn func_compare
preserves (array_pts_to_full var_a1 'p_a1_0 'val_a1_0)
preserves (array_pts_to_full var_a2 'p_a2_0 'val_a2_0)
returns return_1 : bool
- ensures (with_pure (return_1 = (Seq.equal (array_value_of var_a1) (array_value_of var_a2))))
+ ensures (rewrites_to return_1 ((Seq.equal (array_value_of var_a1) (array_value_of var_a2))))
{
let mut var_len = var_len;
let mut var_a1 = var_a1;
diff --git base/dpe/Func_compare.fsti head/dpe/Func_compare.fsti
index a15560d..8db351a 100644
--- base/dpe/Func_compare.fsti
+++ head/dpe/Func_compare.fsti
@@ -12,4 +12,4 @@ requires (with_pure ((reveal (length_of var_a2)) = (SizeT.v var_len)))
preserves (array_pts_to_full var_a1 'p_a1_0 'val_a1_0)
preserves (array_pts_to_full var_a2 'p_a2_0 'val_a2_0)
returns return_1 : bool
-ensures (with_pure (return_1 = (Seq.equal (array_value_of var_a1) (array_value_of var_a2))))
\ No newline at end of file
+ensures (rewrites_to return_1 ((Seq.equal (array_value_of var_a1) (array_value_of var_a2))))
\ No newline at end of file
diff --git head/ensures_determines_result/Func_agree.fst head/ensures_determines_result/Func_agree.fst
new file mode 100644
index 0000000..7f905de
--- /dev/null
+++ head/ensures_determines_result/Func_agree.fst
@@ -0,0 +1,13 @@
+module Func_agree
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_agree (var_a: Typedef_uint32_t.ty_uint32_t) (var_b: Typedef_uint32_t.ty_uint32_t)
+ requires ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
+ requires ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
+ returns return_1 : bool
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
+ ensures (rewrites_to return_1 ((Func_agrees.func_agrees var_a var_b)))
+{ assume pure False; unreachable () }
\ No newline at end of file
diff --git head/ensures_determines_result/Func_agrees.fst head/ensures_determines_result/Func_agrees.fst
new file mode 100644
index 0000000..613b059
--- /dev/null
+++ head/ensures_determines_result/Func_agrees.fst
@@ -0,0 +1,7 @@
+module Func_agrees
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+assume val func_agrees (var_a: Typedef_uint32_t.ty_uint32_t) (var_b: Typedef_uint32_t.ty_uint32_t) :
+ bool
\ No newline at end of file
diff --git head/ensures_determines_result/Func_checked_combine.fst head/ensures_determines_result/Func_checked_combine.fst
new file mode 100644
index 0000000..0238ba3
--- /dev/null
+++ head/ensures_determines_result/Func_checked_combine.fst
@@ -0,0 +1,21 @@
+module Func_checked_combine
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_checked_combine
+ (var_a: Typedef_uint32_t.ty_uint32_t)
+ (var_b: Typedef_uint32_t.ty_uint32_t)
+ requires ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
+ requires ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
+ requires (with_pure (Func_agrees.func_agrees var_a var_b))
+ returns return_1 : Typedef_uint32_t.ty_uint32_t
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
+{
+ let mut var_a = var_a;
+ let mut var_b = var_b;
+ assert (with_pure (Func_agree.func_agree (!var_a) (!var_b)));
+ return (Func_combine.func_combine (!var_a) (!var_b));
+}
\ No newline at end of file
diff --git head/ensures_determines_result/Func_checked_combine.fsti head/ensures_determines_result/Func_checked_combine.fsti
new file mode 100644
index 0000000..7d11f38
--- /dev/null
+++ head/ensures_determines_result/Func_checked_combine.fsti
@@ -0,0 +1,15 @@
+module Func_checked_combine
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_checked_combine
+ (var_a: Typedef_uint32_t.ty_uint32_t)
+ (var_b: Typedef_uint32_t.ty_uint32_t)
+requires ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
+requires ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
+requires (with_pure (Func_agrees.func_agrees var_a var_b))
+returns return_1 : Typedef_uint32_t.ty_uint32_t
+ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
+ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
+ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/ensures_determines_result/Func_combine.fst head/ensures_determines_result/Func_combine.fst
new file mode 100644
index 0000000..5b3a8e3
--- /dev/null
+++ head/ensures_determines_result/Func_combine.fst
@@ -0,0 +1,16 @@
+module Func_combine
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_combine
+ (var_a: Typedef_uint32_t.ty_uint32_t)
+ (var_b: Typedef_uint32_t.ty_uint32_t)
+ requires ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
+ requires ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
+ requires (with_pure (Func_agrees.func_agrees var_a var_b))
+ returns return_1 : Typedef_uint32_t.ty_uint32_t
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
+{ assume pure False; unreachable () }
\ No newline at end of file
diff --git head/ensures_determines_result/Func_screen.fst head/ensures_determines_result/Func_screen.fst
new file mode 100644
index 0000000..ff0ed68
--- /dev/null
+++ head/ensures_determines_result/Func_screen.fst
@@ -0,0 +1,20 @@
+module Func_screen
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_screen (var_a: Typedef_uint32_t.ty_uint32_t) (var_b: Typedef_uint32_t.ty_uint32_t)
+ requires ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
+ requires ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
+ returns return_1 : Typedef_uint32_t.ty_uint32_t
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
+{
+ let mut var_a = var_a;
+ let mut var_b = var_b;
+ if ((not (Func_agree.func_agree (!var_a) (!var_b)))) {
+ return (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ } else {};
+ return (Func_checked_combine.func_checked_combine (!var_a) (!var_b));
+}
\ No newline at end of file
diff --git head/ensures_determines_result/Func_screen.fsti head/ensures_determines_result/Func_screen.fsti
new file mode 100644
index 0000000..2eacc64
--- /dev/null
+++ head/ensures_determines_result/Func_screen.fsti
@@ -0,0 +1,12 @@
+module Func_screen
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_screen (var_a: Typedef_uint32_t.ty_uint32_t) (var_b: Typedef_uint32_t.ty_uint32_t)
+requires ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
+requires ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
+returns return_1 : Typedef_uint32_t.ty_uint32_t
+ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
+ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
+ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/ensures_determines_result/TranslationErrors.fst head/ensures_determines_result/TranslationErrors.fst
new file mode 100644
index 0000000..bf62561
--- /dev/null
+++ head/ensures_determines_result/TranslationErrors.fst
@@ -0,0 +1 @@
+module TranslationErrors
diff --git head/ensures_determines_result/Typedef___uint32_t.fst head/ensures_determines_result/Typedef___uint32_t.fst
new file mode 100644
index 0000000..b9a5b44
--- /dev/null
+++ head/ensures_determines_result/Typedef___uint32_t.fst
@@ -0,0 +1,13 @@
+module Typedef___uint32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty___uint32_t : Type = UInt32.t
+[@@pulse_eager_unfold] let predicate ty___uint32_t__pred ([@@@mkey] this: ty___uint32_t) (p: perm) =
+ emp
+[@@pulse_eager_unfold] let predicate ty___uint32_t__uninit_pred ([@@@mkey] this: ty___uint32_t) =
+ emp
+instance has_zero_default_ty___uint32_t : (has_zero_default ty___uint32_t) =
+ { zero_default = (UInt32.uint_to_t 0) }
\ No newline at end of file
diff --git head/ensures_determines_result/Typedef_uint32_t.fst head/ensures_determines_result/Typedef_uint32_t.fst
new file mode 100644
index 0000000..aa0f488
--- /dev/null
+++ head/ensures_determines_result/Typedef_uint32_t.fst
@@ -0,0 +1,13 @@
+module Typedef_uint32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_uint32_t : Type = Typedef___uint32_t.ty___uint32_t
+[@@pulse_eager_unfold] let predicate ty_uint32_t__pred ([@@@mkey] this: ty_uint32_t) (p: perm) =
+ ((Typedef___uint32_t.ty___uint32_t__pred this p))
+[@@pulse_eager_unfold] let predicate ty_uint32_t__uninit_pred ([@@@mkey] this: ty_uint32_t) =
+ ((Typedef___uint32_t.ty___uint32_t__uninit_pred this))
+instance has_zero_default_ty_uint32_t : (has_zero_default ty_uint32_t) =
+ { zero_default = zero_default }
\ No newline at end of file
diff --git head/ensures_determines_result/diagnostics.json head/ensures_determines_result/diagnostics.json
new file mode 100644
index 0000000..9e26dfe
--- /dev/null
+++ head/ensures_determines_result/diagnostics.json
@@ -0,0 +1 @@
+{}
\ No newline at end of file
diff --git base/if_ensures/Func_pal_c_assert_enabled.fst head/if_ensures/Func_pal_c_assert_enabled.fst
index ad5d080..218c7b8 100644
--- base/if_ensures/Func_pal_c_assert_enabled.fst
+++ head/if_ensures/Func_pal_c_assert_enabled.fst
@@ -3,6 +3,4 @@ open Pulse
open Pulse.Lib.C
#lang-pulse
-divergent fn func_pal_c_assert_enabled ()
- returns return_1 : bool
-{ assume pure False; unreachable () }
\ No newline at end of file
+assume val func_pal_c_assert_enabled () : bool
\ No newline at end of file
diff --git head/pure_external_contract/Func_checked_add.fst head/pure_external_contract/Func_checked_add.fst
new file mode 100644
index 0000000..d44fbda
--- /dev/null
+++ head/pure_external_contract/Func_checked_add.fst
@@ -0,0 +1,25 @@
+module Func_checked_add
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_checked_add
+ (var_a: Typedef_uint32_t.ty_uint32_t)
+ (var_b: Typedef_uint32_t.ty_uint32_t)
+ (var_result: (ref Typedef_uint32_t.ty_uint32_t))
+ requires ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
+ requires ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
+ requires ((Pulse.Lib.Reference.pts_to_uninit var_result))
+ returns return_1 : Int32.t
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
+ ensures
+ exists* (val_result_0: Typedef_uint32_t.ty_uint32_t).
+ ((Pulse.Lib.Reference.pts_to var_result #1.0R val_result_0) **
+ (Typedef_uint32_t.ty_uint32_t__pred (!var_result) 1.0R))
+ ensures
+ (with_pure
+ ((Func_failed.func_failed return_1) ||
+ (((!var_result) = (var_a `Pulse.Lib.C.UInt32.add_wrap` var_b)) &&
+ (var_a `UInt32.lte` (!var_result)))))
+{ assume pure False; unreachable () }
\ No newline at end of file
diff --git head/pure_external_contract/Func_failed.fst head/pure_external_contract/Func_failed.fst
new file mode 100644
index 0000000..9a8eaf4
--- /dev/null
+++ head/pure_external_contract/Func_failed.fst
@@ -0,0 +1,6 @@
+module Func_failed
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+assume val func_failed (var_status: Int32.t) : bool
\ No newline at end of file
diff --git head/pure_external_contract/Func_saturating_add.fst head/pure_external_contract/Func_saturating_add.fst
new file mode 100644
index 0000000..01160fb
--- /dev/null
+++ head/pure_external_contract/Func_saturating_add.fst
@@ -0,0 +1,27 @@
+module Func_saturating_add
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_saturating_add
+ (var_x: Typedef_uint32_t.ty_uint32_t)
+ (var_y: Typedef_uint32_t.ty_uint32_t)
+ requires ((Typedef_uint32_t.ty_uint32_t__pred var_x 1.0R))
+ requires ((Typedef_uint32_t.ty_uint32_t__pred var_y 1.0R))
+ returns return_1 : Typedef_uint32_t.ty_uint32_t
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred var_x 1.0R))
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred var_y 1.0R))
+ ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
+ ensures (pure (FStar.UInt32.v return_1 <= FStar.UInt32.v var_x + FStar.UInt32.v var_y))
+{
+ let mut var_x = var_x;
+ let mut var_y = var_y;
+ let mut var_sum : Typedef_uint32_t.ty_uint32_t;
+ var_sum := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ let mut var_status_1 : Int32.t;
+ var_status_1 := (Func_checked_add.func_checked_add (!var_x) (!var_y) var_sum);
+ if ((Func_failed.func_failed (!var_status_1))) {
+ var_sum := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ } else {};
+ return (!var_sum);
+}
\ No newline at end of file
diff --git head/pure_external_contract/Func_saturating_add.fsti head/pure_external_contract/Func_saturating_add.fsti
new file mode 100644
index 0000000..93c8b38
--- /dev/null
+++ head/pure_external_contract/Func_saturating_add.fsti
@@ -0,0 +1,15 @@
+module Func_saturating_add
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_saturating_add
+ (var_x: Typedef_uint32_t.ty_uint32_t)
+ (var_y: Typedef_uint32_t.ty_uint32_t)
+requires ((Typedef_uint32_t.ty_uint32_t__pred var_x 1.0R))
+requires ((Typedef_uint32_t.ty_uint32_t__pred var_y 1.0R))
+returns return_1 : Typedef_uint32_t.ty_uint32_t
+ensures ((Typedef_uint32_t.ty_uint32_t__pred var_x 1.0R))
+ensures ((Typedef_uint32_t.ty_uint32_t__pred var_y 1.0R))
+ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
+ensures (pure (FStar.UInt32.v return_1 <= FStar.UInt32.v var_x + FStar.UInt32.v var_y))
\ No newline at end of file
diff --git head/pure_external_contract/TranslationErrors.fst head/pure_external_contract/TranslationErrors.fst
new file mode 100644
index 0000000..bf62561
--- /dev/null
+++ head/pure_external_contract/TranslationErrors.fst
@@ -0,0 +1 @@
+module TranslationErrors
diff --git head/pure_external_contract/Typedef___uint32_t.fst head/pure_external_contract/Typedef___uint32_t.fst
new file mode 100644
index 0000000..b9a5b44
--- /dev/null
+++ head/pure_external_contract/Typedef___uint32_t.fst
@@ -0,0 +1,13 @@
+module Typedef___uint32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty___uint32_t : Type = UInt32.t
+[@@pulse_eager_unfold] let predicate ty___uint32_t__pred ([@@@mkey] this: ty___uint32_t) (p: perm) =
+ emp
+[@@pulse_eager_unfold] let predicate ty___uint32_t__uninit_pred ([@@@mkey] this: ty___uint32_t) =
+ emp
+instance has_zero_default_ty___uint32_t : (has_zero_default ty___uint32_t) =
+ { zero_default = (UInt32.uint_to_t 0) }
\ No newline at end of file
diff --git head/pure_external_contract/Typedef_uint32_t.fst head/pure_external_contract/Typedef_uint32_t.fst
new file mode 100644
index 0000000..aa0f488
--- /dev/null
+++ head/pure_external_contract/Typedef_uint32_t.fst
@@ -0,0 +1,13 @@
+module Typedef_uint32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_uint32_t : Type = Typedef___uint32_t.ty___uint32_t
+[@@pulse_eager_unfold] let predicate ty_uint32_t__pred ([@@@mkey] this: ty_uint32_t) (p: perm) =
+ ((Typedef___uint32_t.ty___uint32_t__pred this p))
+[@@pulse_eager_unfold] let predicate ty_uint32_t__uninit_pred ([@@@mkey] this: ty_uint32_t) =
+ ((Typedef___uint32_t.ty___uint32_t__uninit_pred this))
+instance has_zero_default_ty_uint32_t : (has_zero_default ty_uint32_t) =
+ { zero_default = zero_default }
\ No newline at end of file
diff --git head/pure_external_contract/diagnostics.json head/pure_external_contract/diagnostics.json
new file mode 100644
index 0000000..9e26dfe
--- /dev/null
+++ head/pure_external_contract/diagnostics.json
@@ -0,0 +1 @@
+{}
\ No newline at end of file
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part of the upstreaming of
nswamy/pal-c-project-integration(PR33 of 35 PRs) — seePR_PLAN.mdon that branch for the whole plan and the dependency graph.Base:
nswamy/pal-pr26-rewrites-to— a stacked PR. It depends onnswamy/pal-pr26-rewrites-to,nswamy/pal-pr06-pure-external-decls, so only the commits listed below are its own; it will be retargeted atmainonce its parents land.Extends PR26's "does
Emention the result" test to look inside an inline-Pulse fragment'santiquotations, which is both sufficient and precise — that is the only way an inline
fragment can reach the result. It is also the only way to say "this function decides that
predicate", which the impure-spec elaborator needs a
rewrites_tofor. The fixture calls a_pureexternal declaration, hence PR06.Commits
Testing
Verified:
make rust lib,test/check-template.sh,cargo fmt --check,clang-format --dry-run --Werror, and F* verification oftest/compound_literal_member,test/ensures_determines_result,test/nullable_out,test/nullable_out_struct,test/pure_external_contract,test/rvalue_member,test/rvalue_member_branch.