Skip to content

Allow proof blocks inside proof fn (fixes #2061) #2249

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

Open
nitrotap wants to merge 1 commit into
base: main
Choose a base branch
from
+159 −17
Open

Allow proof blocks inside proof fn (fixes #2061) #2249

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
45 changes: 37 additions & 8 deletions source/builtin_macros/src/syntax.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,8 +77,11 @@ pub(crate) struct Visitor {
pub(crate) erase_ghost: EraseGhost,
// TODO: this should always be true
use_spec_traits: bool,
// inside_ghost > 0 means we're currently visiting ghost code
// inside_ghost > 0 means we're currently visiting ghost code (spec or proof)
inside_ghost: u32,
// inside_spec > 0 means we're currently visiting spec code (not proof)
// This is used to distinguish spec fn from proof fn for proof block handling
inside_spec: u32,
// inside_type > 0 means we're currently visiting a type
inside_type: u32,
// inside_external_code > 0 means we're currently visiting an external or external_body body
Expand Down Expand Up @@ -1021,25 +1024,33 @@ impl Visitor {
_ => (vec![], vec![]),
};

let (inside_ghost, mode_attrs): (u32, Vec<Attribute>) = match &sig.mode {
FnMode::Default => (0, vec![]),
FnMode::Spec(token) => (1, vec![mk_verus_attr(token.spec_token.span, quote! { spec })]),
// inside_ghost: 1 for spec/proof functions (ghost code)
// inside_spec: 1 for spec functions only (needed for proof block handling)
let (inside_ghost, inside_spec, mode_attrs): (u32, u32, Vec<Attribute>) = match &sig.mode {
FnMode::Default => (0, 0, vec![]),
FnMode::Spec(token) => {
(1, 1, vec![mk_verus_attr(token.spec_token.span, quote! { spec })])
}
FnMode::SpecChecked(token) => (
1,
1,
vec![mk_verus_attr(
token.spec_token.span,
quote_spanned! { token.spec_token.span => spec(checked) },
)],
),
FnMode::Proof(token) => {
(1, vec![mk_verus_attr(token.proof_token.span, quote! { proof })])
(1, 0, vec![mk_verus_attr(token.proof_token.span, quote! { proof })])
}
FnMode::ProofAxiom(token) => {
(1, vec![mk_verus_attr(token.axiom_token.span, quote! { proof })])
(1, 0, vec![mk_verus_attr(token.axiom_token.span, quote! { proof })])
}
FnMode::Exec(token) => {
(0, 0, vec![mk_verus_attr(token.exec_token.span, quote! { exec })])
}
FnMode::Exec(token) => (0, vec![mk_verus_attr(token.exec_token.span, quote! { exec })]),
};
self.inside_ghost = inside_ghost;
self.inside_spec = inside_spec;

let prover = self.take_ghost(&mut sig.spec.prover);
let prover_attr = prover.as_ref().map(|verus_syn::Prover { id: prover_ident, .. }| {
Expand Down Expand Up @@ -3070,6 +3081,7 @@ impl Visitor {
self.inside_ghost -= 1;

let is_inside_ghost = self.inside_ghost > 0;
let is_inside_spec = self.inside_spec > 0;

if let Expr::Call(call) = expr {
let (_, is_tracked) = mode_block;
Expand Down Expand Up @@ -3101,7 +3113,10 @@ impl Visitor {
((false, _), Expr::Block(..)) => {
// proof { ... }
let inner = take_expr(&mut *unary.expr);
let e = if is_inside_ghost {
// Use is_inside_spec (not is_inside_ghost) to distinguish spec fn from proof fn.
// In spec fn, proof blocks are used for termination checking (proof_in_spec).
// In proof fn or exec fn, proof blocks are treated as regular proof_block.
let e = if is_inside_spec {
quote_spanned!(span => #[verifier::proof_in_spec] /* vattr */ #inner)
} else {
quote_spanned!(span => #[verifier::proof_block] /* vattr */ #inner)
Expand Down Expand Up @@ -4831,6 +4846,7 @@ pub(crate) fn rewrite_items_inner(
erase_ghost,
use_spec_traits,
inside_ghost: 0,
inside_spec: 0,
inside_type: 0,
inside_external_code: 0,
inside_const: false,
Expand All @@ -4842,6 +4858,7 @@ pub(crate) fn rewrite_items_inner(
for mut item in &mut *items {
visitor.visit_item_mut(&mut item);
visitor.inside_ghost = 0;
visitor.inside_spec = 0;
visitor.inside_const = false;
visitor.inside_arith = InsideArith::None;
}
Expand All @@ -4866,6 +4883,7 @@ pub(crate) fn rewrite_impl_items(
erase_ghost,
use_spec_traits,
inside_ghost: 0,
inside_spec: 0,
inside_type: 0,
inside_external_code: 0,
inside_const: false,
Expand All @@ -4877,6 +4895,7 @@ pub(crate) fn rewrite_impl_items(
for mut item in &mut items.items {
visitor.visit_impl_item_mut(&mut item);
visitor.inside_ghost = 0;
visitor.inside_spec = 0;
visitor.inside_const = false;
visitor.inside_arith = InsideArith::None;
}
Expand All @@ -4899,6 +4918,7 @@ pub(crate) fn rewrite_expr(
erase_ghost,
use_spec_traits: true,
inside_ghost: if inside_ghost { 1 } else { 0 },
inside_spec: 0,
inside_type: 0,
inside_external_code: 0,
inside_const: false,
Expand Down Expand Up @@ -4930,6 +4950,7 @@ pub(crate) fn rewrite_proof_decl(
erase_ghost,
use_spec_traits: true,
inside_ghost: 0,
inside_spec: 0,
inside_type: 0,
inside_external_code: 0,
inside_const: false,
Expand Down Expand Up @@ -4983,6 +5004,7 @@ pub(crate) fn rewrite_expr_node(erase_ghost: EraseGhost, inside_ghost: bool, exp
erase_ghost,
use_spec_traits: true,
inside_ghost: if inside_ghost { 1 } else { 0 },
inside_spec: 0,
inside_type: 0,
inside_external_code: 0,
inside_const: false,
Expand Down Expand Up @@ -5172,6 +5194,7 @@ pub(crate) fn sig_specs_attr(
erase_ghost,
use_spec_traits: true,
inside_ghost: 1,
inside_spec: 0,
inside_type: 0,
inside_external_code: 0,
inside_const: false,
Expand Down Expand Up @@ -5210,6 +5233,7 @@ pub(crate) fn while_loop_spec_attr(
erase_ghost,
use_spec_traits: true,
inside_ghost: 1,
inside_spec: 0,
inside_type: 0,
inside_external_code: 0,
inside_const: false,
Expand Down Expand Up @@ -5242,6 +5266,7 @@ pub(crate) fn for_loop_spec_attr(
erase_ghost,
use_spec_traits: true,
inside_ghost: 1,
inside_spec: 0,
inside_type: 0,
inside_external_code: 0,
inside_const: false,
Expand Down Expand Up @@ -5300,6 +5325,7 @@ pub(crate) fn proof_block(
erase_ghost,
use_spec_traits: true,
inside_ghost: 1,
inside_spec: 0,
inside_type: 0,
inside_external_code: 0,
inside_const: false,
Expand All @@ -5324,6 +5350,7 @@ pub(crate) fn proof_macro_exprs(
erase_ghost,
use_spec_traits: true,
inside_ghost: if inside_ghost { 1 } else { 0 },
inside_spec: 0,
inside_type: 0,
inside_external_code: 0,
inside_const: false,
Expand Down Expand Up @@ -5353,6 +5380,7 @@ pub(crate) fn inv_macro_exprs(
erase_ghost,
use_spec_traits: true,
inside_ghost: 0,
inside_spec: 0,
inside_type: 0,
inside_external_code: 0,
inside_const: false,
Expand Down Expand Up @@ -5388,6 +5416,7 @@ pub(crate) fn proof_macro_explicit_exprs(
erase_ghost,
use_spec_traits: true,
inside_ghost: if inside_ghost { 1 } else { 0 },
inside_spec: 0,
inside_type: 0,
inside_external_code: 0,
inside_const: false,
Expand Down
123 changes: 116 additions & 7 deletions source/rust_verify_test/tests/proof_in_spec.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -262,8 +262,9 @@ test_verify_one_file! {
} => Err(err) => assert_vir_error_msg(err, "proof blocks inside spec code is currently supported only for")
}

// proof blocks inside proof fn are now allowed (redundant but harmless)
test_verify_one_file! {
#[test] non_spec_fn_not_yet_supported verus_code! {
#[test] proof_block_in_proof_fn_allowed verus_code! {
proof fn f(i: int) {
let x: int = {
proof {
Expand All @@ -272,7 +273,7 @@ test_verify_one_file! {
3
};
}
} => Err(err) => assert_vir_error_msg(err, "proof blocks inside spec code is currently supported only for")
} => Ok(())
}

test_verify_one_file! {
Expand All @@ -288,8 +289,9 @@ test_verify_one_file! {
} => Err(err) => assert_vir_error_msg(err, "return is not allowed inside spec")
}

// assignment inside proof block in proof fn is now allowed
test_verify_one_file! {
#[test] assign_not_allowed verus_code! {
#[test] assign_in_proof_block_in_proof_fn verus_code! {
proof fn f(i: int) {
let mut b = false;
let x: int = {
Expand All @@ -299,7 +301,7 @@ test_verify_one_file! {
3
};
}
} => Err(err) => assert_vir_error_msg(err, "proof blocks inside spec code is currently supported only for")
} => Ok(())
}

test_verify_one_file! {
Expand All @@ -322,20 +324,20 @@ test_verify_one_file! {
} => Err(err) => assert_vir_error_msg(err, "expression has mode spec, expected mode proof")
}

// tracked variables inside proof block in proof fn is now allowed
test_verify_one_file! {
#[test] tracked_not_allowed2 verus_code! {
#[test] tracked_in_proof_block_in_proof_fn verus_code! {
proof fn h(tracked i: int) {
}
proof fn f(tracked i: int) {
let x: int = {
proof {
h(i);
h(i);
}
3
};
}
} => Err(err) => assert_vir_error_msg(err, "proof blocks inside spec code is currently supported only for")
} => Ok(())
}

test_verify_one_file! {
Expand Down Expand Up @@ -487,3 +489,110 @@ test_verify_one_file! {
}
} => Ok(())
}

// ============================================================================
// Tests for issue #2061: proof blocks inside proof fn should be allowed
// https://github.com/verus-lang/verus/issues/2061
// ============================================================================

// Basic case from the issue: proof { } directly in proof fn body
test_verify_one_file! {
#[test] issue_2061_basic verus_code! {
proof fn foo() {
proof { }
}
} => Ok(())
}

// proof block with assertion in proof fn
test_verify_one_file! {
#[test] issue_2061_with_assert verus_code! {
proof fn foo() {
proof {
assert(1 + 1 == 2);
}
}
} => Ok(())
}

// proof block with failing assertion in proof fn
test_verify_one_file! {
#[test] issue_2061_with_failing_assert verus_code! {
proof fn foo() {
proof {
assert(false); // FAILS
}
}
} => Err(err) => assert_one_fails(err)
}

// nested proof blocks in proof fn
test_verify_one_file! {
#[test] issue_2061_nested verus_code! {
proof fn foo() {
proof {
proof {
assert(true);
}
}
}
} => Ok(())
}

// proof block in proof fn with local variable
test_verify_one_file! {
#[test] issue_2061_with_local verus_code! {
proof fn foo() {
let x: int = 5;
proof {
assert(x == 5);
}
}
} => Ok(())
}

// proof block in proof fn inside expression
test_verify_one_file! {
#[test] issue_2061_in_expression verus_code! {
proof fn foo() -> int {
let result: int = {
proof {
assert(true);
}
42
};
result
}
} => Ok(())
}

// Verify spec fn with decreases still works (regression test)
test_verify_one_file! {
#[test] issue_2061_spec_fn_still_works verus_code! {
spec fn factorial(n: nat) -> nat
decreases n
{
if n == 0 {
1
} else {
proof {
// This proof block in spec fn with decreases should still work
assert(n > 0);
}
n * factorial((n - 1) as nat)
}
}
} => Ok(())
}

// Ensure proof blocks in spec fn WITHOUT decreases still error
test_verify_one_file! {
#[test] issue_2061_spec_fn_no_decreases_still_errors verus_code! {
spec fn f(i: int) -> int {
proof {
assert(true);
}
3
}
} => Err(err) => assert_vir_error_msg(err, "proof blocks inside spec code is currently supported only for")
}
8 changes: 6 additions & 2 deletions source/vir/src/modes.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2913,8 +2913,12 @@ fn check_expr(
}
Ghost::Ghost
}
(_, false, false) => {
return Err(error(&expr.span, "already in proof mode"));
(Ghost::Ghost, false, false) => {
// Already in proof/spec mode - proof block is redundant but allowed
if !is_unit(&e1.typ) {
return Err(error(&expr.span, "proof block must have type ()"));
}
Ghost::Ghost
}
(Ghost::Exec, false, true) => {
return Err(error(
Expand Down
Loading