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

add a trigger on domain equality for extensional equality axiom for maps #714

Closed
wants to merge 2 commits into from
Closed

add a trigger on domain equality for extensional equality axiom for maps #714

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d5abab1
allow #![trigger f(x)] on ensures (of broadcast_forall) functions
utaal Jul 26, 2023
d4e407b
add a trigger on domain equality for extensional equality axiom for maps
utaal Jul 26, 2023
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 dependencies/syn/src/gen/clone.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions dependencies/syn/src/gen/debug.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion dependencies/syn/src/gen/eq.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions dependencies/syn/src/gen/fold.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions dependencies/syn/src/gen/hash.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

3 changes: 3 additions & 0 deletions dependencies/syn/src/gen/visit.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

3 changes: 3 additions & 0 deletions dependencies/syn/src/gen/visit_mut.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

7 changes: 6 additions & 1 deletion dependencies/syn/src/verus.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,7 @@ ast_struct! {

ast_struct! {
pub struct Ensures {
pub attrs: Vec<Attribute>,
pub token: Token![ensures],
pub exprs: Specification,
}
Expand Down Expand Up @@ -428,8 +429,12 @@ pub mod parsing {
#[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
impl Parse for Ensures {
fn parse(input: ParseStream) -> Result<Self> {
let mut attrs = Vec::new();
let token = input.parse()?;
attr::parsing::parse_inner(input, &mut attrs)?;
Ok(Ensures {
token: input.parse()?,
attrs,
token,
exprs: input.parse()?,
})
}
Expand Down
5 changes: 5 additions & 0 deletions dependencies/syn/syn.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -846,6 +846,11 @@
"any": []
},
"fields": {
"attrs": {
"vec": {
"syn": "Attribute"
}
},
"token": {
"token": "Ensures"
},
Expand Down
3 changes: 3 additions & 0 deletions dependencies/syn/tests/debug/gen.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

213 changes: 134 additions & 79 deletions source/builtin_macros/src/syntax.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -315,23 +315,62 @@ impl Visitor {
));
}
}
if let Some(Ensures { token, mut exprs }) = ensures {
if let Some(Ensures { attrs, token, mut exprs }) = ensures {
if exprs.exprs.len() > 0 {
for expr in exprs.exprs.iter_mut() {
self.visit_expr_mut(expr);
}
if let Some((p, ty)) = ret_pat {
stmts.push(Stmt::Semi(
Expr::Verbatim(
quote_spanned!(token.span => ::builtin::ensures(|#p: #ty| [#exprs])),
),
Semi { spans: [token.span] },
));
} else {
stmts.push(Stmt::Semi(
Expr::Verbatim(quote_spanned!(token.span => ::builtin::ensures([#exprs]))),
Semi { spans: [token.span] },
));
let cont = match self.extract_quant_triggers(attrs, token.span) {
Ok(
found @ (ExtractQuantTriggersFound::Auto
| ExtractQuantTriggersFound::Triggers(..)),
) => {
if exprs.exprs.len() != 1 {
let err = "when using #![trigger f(x)], only one ensures is allowed";
let expr =
Expr::Verbatim(quote_spanned!(token.span => compile_error!(#err)));
stmts.push(Stmt::Semi(expr, Semi { spans: [token.span] }));
false
} else {
let e = take_expr(&mut exprs.exprs[0]);
match found {
ExtractQuantTriggersFound::Auto => {
exprs.exprs[0] = Expr::Verbatim(
quote_spanned!(exprs.exprs[0].span() => #[verus::internal(auto_trigger)] (#e)),
);
}
ExtractQuantTriggersFound::Triggers(tuple) => {
exprs.exprs[0] = Expr::Verbatim(
quote_spanned!(exprs.exprs[0].span() => ::builtin::with_triggers(#tuple, #e)),
);
}
ExtractQuantTriggersFound::None => unreachable!(),
}
true
}
}
Ok(ExtractQuantTriggersFound::None) => true,
Err(err_expr) => {
exprs.exprs[0] = err_expr;
false
}
};
if cont {
if let Some((p, ty)) = ret_pat {
stmts.push(Stmt::Semi(
Expr::Verbatim(
quote_spanned!(token.span => ::builtin::ensures(|#p: #ty| [#exprs])),
),
Semi { spans: [token.span] },
));
} else {
stmts.push(Stmt::Semi(
Expr::Verbatim(
quote_spanned!(token.span => ::builtin::ensures([#exprs])),
),
Semi { spans: [token.span] },
));
}
}
}
}
Expand Down Expand Up @@ -956,7 +995,7 @@ impl Visitor {
_ => panic!("expected closure for quantifier"),
};

match extract_quant_triggers(inner_attrs, span) {
match self.extract_quant_triggers(inner_attrs, span) {
Ok(ExtractQuantTriggersFound::Auto) => match &mut *arg {
Expr::Closure(closure) => {
let body = take_expr(&mut closure.body);
Expand Down Expand Up @@ -1028,8 +1067,12 @@ impl Visitor {
stmts.push(stmt_with_semi!(token.span => ::builtin::invariant_ensures([#exprs])));
}
}
if let Some(Ensures { token, mut exprs }) = ensures {
if exprs.exprs.len() > 0 {
if let Some(Ensures { token, mut exprs, attrs }) = ensures {
if attrs.len() > 0 {
let err = "outer attributes only allowed on function's ensures";
let expr = Expr::Verbatim(quote_spanned!(token.span => compile_error!(#err)));
stmts.push(Stmt::Semi(expr, Semi { spans: [token.span] }));
} else if exprs.exprs.len() > 0 {
for expr in exprs.exprs.iter_mut() {
self.visit_expr_mut(expr);
}
Expand All @@ -1049,66 +1092,70 @@ impl Visitor {
}
self.inside_ghost -= 1;
}
}

enum ExtractQuantTriggersFound {
Auto,
Triggers(ExprTuple),
None,
}
fn extract_quant_triggers(
&mut self,
inner_attrs: Vec<Attribute>,
span: Span,
) -> Result<ExtractQuantTriggersFound, Expr> {
let mut triggers: Vec<Expr> = Vec::new();
for attr in inner_attrs {
let trigger: syn_verus::Result<syn_verus::Specification> =
syn_verus::parse2(attr.tokens.clone());
let path_segments_str =
attr.path.segments.iter().map(|x| x.ident.to_string()).collect::<Vec<_>>();
let ident_str = match &path_segments_str[..] {
[attr_name] => Some(attr_name),
_ => None,
};
match (trigger, ident_str) {
(Ok(trigger), Some(id)) if id == &"auto" && trigger.exprs.len() == 0 => {
return Ok(ExtractQuantTriggersFound::Auto);
}
(Ok(trigger), Some(id)) if id == &"trigger" => {
let mut exprs = trigger.exprs;
for expr in exprs.iter_mut() {
self.visit_expr_mut(expr);
}
let tuple = ExprTuple { attrs: vec![], paren_token: Paren(span), elems: exprs };
triggers.push(Expr::Tuple(tuple));
}
(Err(err), _) => {
let span = attr.span();
let err = err.to_string();

fn extract_quant_triggers(
inner_attrs: Vec<Attribute>,
span: Span,
) -> Result<ExtractQuantTriggersFound, Expr> {
let mut triggers: Vec<Expr> = Vec::new();
for attr in inner_attrs {
let trigger: syn_verus::Result<syn_verus::Specification> =
syn_verus::parse2(attr.tokens.clone());
let path_segments_str =
attr.path.segments.iter().map(|x| x.ident.to_string()).collect::<Vec<_>>();
let ident_str = match &path_segments_str[..] {
[attr_name] => Some(attr_name),
_ => None,
};
match (trigger, ident_str) {
(Ok(trigger), Some(id)) if id == &"auto" && trigger.exprs.len() == 0 => {
return Ok(ExtractQuantTriggersFound::Auto);
}
(Ok(trigger), Some(id)) if id == &"trigger" => {
let tuple =
ExprTuple { attrs: vec![], paren_token: Paren(span), elems: trigger.exprs };
triggers.push(Expr::Tuple(tuple));
return Err(Expr::Verbatim(quote_spanned!(span => compile_error!(#err))));
}
_ => {
let span = attr.span();
return Err(Expr::Verbatim(
quote_spanned!(span => compile_error!("expected trigger")),
));
}
}
(Err(err), _) => {
let span = attr.span();
let err = err.to_string();
}

return Err(Expr::Verbatim(quote_spanned!(span => compile_error!(#err))));
}
_ => {
let span = attr.span();
return Err(Expr::Verbatim(
quote_spanned!(span => compile_error!("expected trigger")),
));
Ok(if triggers.len() > 0 {
let mut elems = Punctuated::new();
for elem in triggers {
elems.push(elem);
elems.push_punct(Token![,](span));
}
}
ExtractQuantTriggersFound::Triggers(ExprTuple {
attrs: vec![],
paren_token: Paren(span),
elems,
})
} else {
ExtractQuantTriggersFound::None
})
}
}

Ok(if triggers.len() > 0 {
let mut elems = Punctuated::new();
for elem in triggers {
elems.push(elem);
elems.push_punct(Token![,](span));
}
ExtractQuantTriggersFound::Triggers(ExprTuple {
attrs: vec![],
paren_token: Paren(span),
elems,
})
} else {
ExtractQuantTriggersFound::None
})
enum ExtractQuantTriggersFound {
Auto,
Triggers(ExprTuple),
None,
}

impl VisitMut for Visitor {
Expand Down Expand Up @@ -1661,7 +1708,7 @@ impl VisitMut for Visitor {
Expr::AssertForall(assert) => {
let span = assert.assert_token.span;
let mut arg = assert.expr;
match extract_quant_triggers(assert.attrs, span) {
match self.extract_quant_triggers(assert.attrs, span) {
Ok(ExtractQuantTriggersFound::Auto) => {
arg = Box::new(Expr::Verbatim(
quote_spanned!(arg.span() => #[verus::internal(auto_trigger)] #arg),
Expand Down Expand Up @@ -1731,16 +1778,24 @@ impl VisitMut for Visitor {
stmts.push(stmt_with_semi!(
token.span => ::builtin::requires([#exprs])));
}
if let Some(Ensures { token, mut exprs }) = ensures {
for expr in exprs.exprs.iter_mut() {
self.visit_expr_mut(expr);
}
if let Some((p, ty)) = ret_pat {
stmts.push(stmt_with_semi!(
token.span => ::builtin::ensures(|#p: #ty| [#exprs])));
if let Some(Ensures { token, mut exprs, attrs }) = ensures {
if attrs.len() > 0 {
let err = "outer attributes only allowed on function's ensures";
let expr = Expr::Verbatim(
quote_spanned!(token.span => compile_error!(#err)),
);
stmts.push(Stmt::Semi(expr, Semi { spans: [token.span] }));
} else {
stmts.push(stmt_with_semi!(
token.span => ::builtin::ensures([#exprs])));
for expr in exprs.exprs.iter_mut() {
self.visit_expr_mut(expr);
}
if let Some((p, ty)) = ret_pat {
stmts.push(stmt_with_semi!(
token.span => ::builtin::ensures(|#p: #ty| [#exprs])));
} else {
stmts.push(stmt_with_semi!(
token.span => ::builtin::ensures([#exprs])));
}
}
}
self.inside_ghost -= 1;
Expand Down
4 changes: 3 additions & 1 deletion source/pervasive/map.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -393,7 +393,9 @@ pub proof fn axiom_map_remove_different<K, V>(m: Map<K, V>, key1: K, key2: K)
#[verifier(broadcast_forall)]
pub proof fn axiom_map_ext_equal<K, V>(m1: Map<K, V>, m2: Map<K, V>)
ensures
#[trigger] (m1 =~= m2) <==> {
#![trigger (m1 =~= m2)]
#![trigger (m1.dom() =~= m2.dom())]
(m1 =~= m2) <==> {
&&& m1.dom() =~= m2.dom()
&&& forall|k: K| #![auto] m1.dom().contains(k) ==> m1[k] == m2[k]
},
Expand Down
Loading
Loading