emit: let an inline-Pulse postcondition determine the result

src/pass/emit.rs

@@ -7250,6 +7250,18 @@ impl<'a> Emitter<'a> {
                 Self::mentions_return(a) || Self::mentions_return(b) || Self::mentions_return(c)
             }
             ExprT::FnCall(_, args) => args.iter().any(|a| Self::mentions_return(a)),
+            // A spec written in Pulse can only reach `return` through an
+            // antiquotation, so the verbatim tokens around them cannot
+            // reintroduce it. Looking inside is what lets a clause that fixes
+            // the result to a Pulse-level function of the arguments --
+            // `_ensures(return == (_Bool)_inline_pulse(f $(A) $(B)))`, which is
+            // the only way to say "this predicate decides that" -- still be
+            // emitted as `rewrites_to` rather than a plain equality.
+            ExprT::InlinePulse(code, _) => code.tokens.iter().any(|tok| match tok {
+                InlinePulseToken::RValueAntiquot { expr, .. }
+                | InlinePulseToken::LValueAntiquot { expr, .. } => Self::mentions_return(expr),
+                _ => false,
+            }),
             _ => true,
         }
     }
@@ -7578,6 +7590,9 @@ impl<'a> Emitter<'a> {
     }
 
     fn emit_fn_decl(&mut self, env: &Env, decl: &FnDecl) -> Doc {
+        if decl.is_pure {
+            return self.emit_pure_fn_decl(env, decl);
+        }
         self.emit_fn_sig(env, decl)
             .nest(2)
             .append(Doc::hardline())
@@ -7887,7 +7902,43 @@ impl<'a> Emitter<'a> {
 
     fn emit_pure_fn(&mut self, env: &Env, decl: &FnDecl, body: &Stmts) -> Doc {
         let env = &mut env.clone();
+        let (params, ty_doc) = self.emit_pure_fn_sig(env, decl);
+        let body_doc = self.emit_pure_body(env, body);
+        mk_let_rec(
+            decl.is_rec,
+            self.emit_name(Name::Fn(decl.name.val.clone())),
+            &params,
+            ty_doc,
+            body_doc,
+        )
+    }
+
+    /// A `_pure` function without a body is an external pure operation. It is
+    /// assumed rather than stubbed out as a state-passing `fn`, so that it can
+    /// be applied inside the pre- and postconditions of the functions that call
+    /// it. A stubbed `fn` cannot: Pulse rejects a stateful application in a
+    /// specification.
+    fn emit_pure_fn_decl(&mut self, env: &Env, decl: &FnDecl) -> Doc {
+        let env = &mut env.clone();
+        let (params, ty_doc) = self.emit_pure_fn_sig(env, decl);
+        (Doc::text("assume val")
+            .append(Doc::line())
+            .append(self.emit_name(Name::Fn(decl.name.val.clone()))))
+        .append(
+            Doc::concat(params.iter().map(|arg| Doc::line().append(arg.clone())))
+                .append(Doc::line().append(":"))
+                .nest(2),
+        )
+        .group()
+        .append(Doc::line().append(ty_doc))
+        .nest(2)
+        .group()
+    }
 
+    /// Shared signature elaboration for the two pure forms: the parameter list
+    /// and the result type, including the `Pure` effect wrapper when the
+    /// declaration carries a contract.
+    fn emit_pure_fn_sig(&mut self, env: &mut Env, decl: &FnDecl) -> (Vec<Doc>, Doc) {
         let mut params = vec![];
 
         // Emit ghost arguments as implicit erased parameters
@@ -7946,8 +7997,6 @@ impl<'a> Emitter<'a> {
             .map(|e| self.emit_pure_prop(env, e))
             .collect();
 
-        let body_doc = self.emit_pure_body(env, body);
-
         let has_specs = !requires_props.is_empty() || !ensures_props.is_empty();
 
         let ty_doc = if has_specs || (decl.is_rec && decl.decreases.is_some()) {
@@ -7991,14 +8040,7 @@ impl<'a> Emitter<'a> {
             ret_type_doc
         };
 
-        let body = mk_let_rec(
-            decl.is_rec,
-            self.emit_name(Name::Fn(decl.name.val.clone())),
-            &params,
-            ty_doc,
-            body_doc,
-        );
-        body
+        (params, ty_doc)
     }
 
     fn emit_let_decl(&mut self, env: &Env, let_decl: &LetDecl) -> Doc {

test/ensures_determines_result/Makefile

@@ -0,0 +1 @@
+../_templates/Makefile

test/ensures_determines_result/ensures_determines_result.c

@@ -0,0 +1,53 @@
+// A postcondition that fixes the result to a Pulse-level function of the
+// arguments -- `_ensures(return == (_Bool)_inline_pulse(f $(A) $(B)))` -- is
+// emitted as Pulse's `rewrites_to`, the same as when the right-hand side is a
+// plain C expression.
+//
+// That is not cosmetic. Pulse's impure-spec elaborator, which is what turns an
+// `_assert` over a stateful call into a proposition, looks for exactly a
+// `rewrites_to` in the callee's postcondition; an ordinary equality leaves it
+// with nothing to name the result by, and the assertion does not elaborate at
+// all. So `screen` below is the regression: it only translates if `agree`'s
+// contract determines its result.
+
+#include "pal.h"
+
+#include <stdint.h>
+
+// An external pure operation, assumed as a pure F* value. It stands for the
+// vocabulary predicate a real contract would name.
+_pure _Bool
+agrees(uint32_t A, uint32_t B);
+
+// Decides `agrees`.
+_Bool
+agree(uint32_t A, uint32_t B)
+    _ensures(return == (_Bool)_inline_pulse(Func_agrees.func_agrees $(A) $(B)));
+
+// Requires it, in the shape of a routine that asserts its precondition fatally
+// rather than returning a verdict.
+uint32_t
+combine(uint32_t A, uint32_t B)
+    _requires((_Bool)_inline_pulse(Func_agrees.func_agrees $(A) $(B)));
+
+// The impure-spec use: asserting a stateful call needs the call's result to be
+// nameable as a pure term.
+uint32_t
+checked_combine(uint32_t A, uint32_t B)
+    _requires((_Bool)_inline_pulse(Func_agrees.func_agrees $(A) $(B)))
+{
+    _assert(agree(A, B));
+    return combine(A, B);
+}
+
+// And the caller that discharges the assertion by screening first.
+uint32_t
+screen(uint32_t A, uint32_t B)
+{
+    if (!agree(A, B))
+    {
+        return 0;
+    }
+
+    return checked_combine(A, B);
+}

test/ensures_determines_result/fstar.fst.config.json

@@ -0,0 +1 @@
+../_templates/fstar.fst.config.json

test/ensures_determines_result/pal.config.json

@@ -0,0 +1 @@
+../_templates/pal.config.json

test/ensures_determines_result/pal.h

@@ -0,0 +1 @@
+../pal.h

test/pure_external_contract/Makefile

@@ -0,0 +1 @@
+../_templates/Makefile

test/pure_external_contract/fstar.fst.config.json

@@ -0,0 +1 @@
+../_templates/fstar.fst.config.json

test/pure_external_contract/pal.config.json

@@ -0,0 +1 @@
+../_templates/pal.config.json

test/pure_external_contract/pal.h

@@ -0,0 +1 @@
+../pal.h

test/pure_external_contract/pure_external_contract.c

@@ -0,0 +1,43 @@
+// A `_pure` function without a body is an external pure operation. It is
+// assumed as a pure F* value, so it can be named in the contracts of the
+// functions that call it. A checked-arithmetic routine is the motivating case:
+// its result is only meaningful when its status says it did not overflow, and
+// that status is classified by another external pure operation.
+
+#include "pal.h"
+
+#include <stdint.h>
+
+_pure _Bool
+failed(int Status);
+
+// Declared once without a contract, as an external header would provide it,
+// and again with the contract that header documents. Clang merges the two, so
+// the contract applies without the first declaration having to change.
+int
+checked_add(uint32_t A, uint32_t B, _out uint32_t* Result);
+
+// `*Result >= A` is unsigned wraparound saying the true sum fits: adding B
+// wraps exactly when the mathematical sum leaves the 32-bit range.
+int
+checked_add(uint32_t A, uint32_t B, _out uint32_t* Result)
+    _ensures(failed(return) || (*Result == A + B && *Result >= A));
+
+// Provable only from the contract above: on the path the status accepts, the
+// result is the exact mathematical sum rather than a wrapped one.
+uint32_t
+saturating_add(uint32_t X, uint32_t Y)
+    _ensures(_inline_pulse(
+        pure (FStar.UInt32.v $(return) <= FStar.UInt32.v $(X) + FStar.UInt32.v $(Y))))
+{
+    uint32_t sum = 0;
+    int status;
+
+    status = checked_add(X, Y, &sum);
+    if (failed(status))
+    {
+        sum = 0;
+    }
+
+    return sum;
+}