search

hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
194 stars 20 forks source link

`hax_lib::attributes`: impls: `requires` clause not available in `ensures` #784

Open W95Psp opened 3 months ago

W95Psp commented 3 months ago

Consider the following, where forall x. p x ==> q x.

#[hax_lib::attributes]
impl MyTrait for ... {
   #[requires(p x)]
   #[ensures(|result| ... /\ q x)]
   fn f(x: ...) { ... }
}

This will not result in F that typechecks, because the F precondition and postcondition of f is represented as a dedicated method in the typelcass MyTrait. We need to "add a precondition to the postcondition": the postcondition should require the precondition.

github-actions[bot] commented 1 month ago

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

W95Psp commented 1 month ago

Just like https://github.com/hacspec/hax/issues/789, this issue makes requires/ensures painful on traits, let's keep it open.