Comments (12)
y1ca1
commented on August 23, 2024
Ok, this is a much cleaner repro:
use vstd::prelude::*;
verus! {
pub trait Bar {
type U<'a>;
}
pub trait Foo<S> where
S: for<'a> Bar<U<'a> = Self::T<'a>>,
{
type T<'a>;
}
fn main();
} // verus!from verus.
Chris-Hawblitzel
commented on August 23, 2024
Can you try the lifetime-for branch?
from verus.
y1ca1
commented on August 23, 2024
Thanks for the fix! I tried the branch and found some other issues:
The original code now verifies:
use vstd::prelude::*;
verus! {
pub trait Bar {
type U<'a>;
}
pub trait Foo<S> where
S: for<'a> Bar<U<'a> = Self::T<'a>>,
{
type T<'a>;
}
fn main();
} // verus!❯ verus foo.rs
verification results:: 1 verified, 0 errorsBut if we add an associated function to the trait Foo that refers to the associated type, some peculiar error messages show up:
use vstd::prelude::*;
verus! {
pub trait Bar {
type U<'a>;
}
pub trait Foo<S>
where
S: for<'a> Bar<U<'a> = Self::T<'a>>,
{
type T<'a>;
fn foo<'a>(&self, s: &'a [u8]) -> (res: Result<Self::T<'a>, ()>); // errs Verus
// fn foo_<'a>(&self, o: Self::T<'a>); // also errs
}
fn main();
} // verus!❯ verus foo.rs
error: lifetime name `'a29_a` shadows a lifetime name that is already in scope
--> foo.rs:17:12
|
17 | fn foo<'a>(&self, s: &'a [u8]) -> (res: Result<Self::T<'a>, ()>);
| ^^^^^^
18 | // fn foo_<'a>(&self, o: Self::T<'a>);
| ^^^^^^
error: lifetime name `'a29_a` shadows a lifetime name that is already in scope
--> foo.rs:17:12
|
17 | fn foo<'a>(&self, s: &'a [u8]) -> (res: Result<Self::T<'a>, ()>);
| ^^^^^^
...
22 | fn main();
| _________^
23 | | } // verus!
| |___^
error: trait takes 0 lifetime arguments but 1 lifetime argument was supplied
--> foo.rs:23:7
|
1 | | use vstd::prelude::*;
| |_
...
23| } // verus!
| _______^
error: missing generics for associated type `T25_Bar::A24_U`
--> <crate attribute>:1:10
|
1 | allow(internal_features)
| ^^^^^
error: trait takes 0 lifetime arguments but 1 lifetime argument was supplied
error: missing generics for associated type `T25_Bar::A24_U`
error: binding for associated type `A24_U` references lifetime `'a29_a`, which does not appear in the trait input types
error: aborting due to 7 previous errors
note: This error was found in Verus pass: ownership checking of tracked code
error: aborting due to 8 previous errors
P.S. The code type-checks in Rust.
from verus.
Chris-Hawblitzel
commented on August 23, 2024
Can you try now?
from verus.
y1ca1
commented on August 23, 2024
Thanks again for the fix! However, I found another peculiar error reported and likely a bug:
use vstd::prelude::*;
verus! {
trait Bar<S>: View {
type T;
}
trait Foo {
type U<'a>;
}
struct S<F>(F);
impl<F> View for S<F> where F: Foo, for <'a>F::U<'a>: View {
type V = S<F>;
spec fn view(&self) -> Self::V;
}
fn main();
} // verus!❯ verus src/main.rs
error: use of undeclared lifetime name `'b38_a`
--> /Users/yicai/Research/with-B.P./repos/verus/source/vstd/seq.rs:31:18
|
31 | pub struct Seq<A> {
| ^
error: aborting due to 1 previous error
note: This error was found in Verus pass: ownership checking of tracked code
error: aborting due to 2 previous errors
However, when removing the seemingly unrelated code (the trait Bar):
use vstd::prelude::*;
verus! {
trait Foo {
type U<'a>;
}
struct S<F>(F);
impl<F> View for S<F> where F: Foo, for <'a>F::U<'a>: View {
type V = S<F>;
spec fn view(&self) -> Self::V;
}
fn main();
} // verus!Or using a custom View trait for the unrelated code:
trait MyView {
type V;
spec fn view(&self) -> Self::V;
}
trait Bar<S>: MyView {
type T;
}
...❯ verus src/main.rs
verification results:: 1 verified, 0 errorsOr replacing the impl View with a blank impl:
use vstd::prelude::*;
verus! {
trait Bar<S>: View {
type T;
}
trait Foo {
type U<'a>;
}
struct S<F>(F);
impl<F> S<F> where F: Foo, for <'a>F::U<'a>: View {
}
fn main();
} // verus!❯ verus src/main.rs
verification results:: 1 verified, 0 errorsMaybe something to do with the vstd View trait?
from verus.
Chris-Hawblitzel
commented on August 23, 2024
Can you try again now?
from verus.
y1ca1
commented on August 23, 2024
Thanks! Here is a new bug:
use vstd::prelude::*;
verus! {
trait TT {
type A<'a>;
fn f<'a>(s: Self::A<'a>);
}
struct Foo<M>(M);
impl<M> Foo<M> where
for<'a> M: TT<A<'a> = &'a [u8]>,
{
fn foo<'a>(&self, s: &'a [u8])
{
M::f(s)
}
}
fn main();
} // verus!❯ verus src/main.rs
error: mismatched types
--> src/main.rs:18:14
|
18 | M::f(s)
| ^
error: aborting due to 1 previous error
note: This error was found in Verus pass: ownership checking of tracked code
error: aborting due to 2 previous errorsThe above code type-checks in Rust.
Plus FWIW, changing the function to spec makes Verus panic:
use vstd::prelude::*;
verus! {
trait TT {
type A<'a>;
spec fn f<'a>(s: Self::A<'a>);
}
struct Foo<M>(M);
impl<M> Foo<M> where
for<'a> M: TT<A<'a> = &'a [u8]>,
{
spec fn foo<'a>(&self, s: &'a [u8])
{
M::f(s)
}
}
fn main();
} // verus!❯ verus src/main.rs
thread '<unnamed>' panicked at rust_verify/src/verifier.rs:522:17:
internal error: ill-typed AIR code: error 'error 'in equality, left expression has type tuple%0. and right expression has different type Poly' in expression '(= (main!impl&%0.foo.? M&. M& self! s!) (main!TT.f.? M&. M& s!))'' in ex
pression '(=>
(fuel_bool fuel%main!impl&%0.foo.)
(forall ((M&. Dcr) (M& Type) (self! Poly) (s! Poly)) (!
(= (main!impl&%0.foo.? M&. M& self! s!) (main!TT.f.? M&. M& s!))
:pattern ((main!impl&%0.foo.? M&. M& self! s!))
:qid internal_main!impl&__0.foo.?_definition
:skolemid skolem_internal_main!impl&__0.foo.?_definition
)))'
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread '<unnamed>' panicked at rust_verify/src/verifier.rs:1949:29:
worker thread panickedFinally, a proof fn is good:
use vstd::prelude::*;
verus! {
trait TT {
type A<'a>;
proof fn f<'a>(s: Self::A<'a>);
}
struct Foo<M>(M);
impl<M> Foo<M> where
for<'a> M: TT<A<'a> = &'a [u8]>,
{
proof fn foo<'a>(&self, s: &'a [u8])
{
M::f(s)
}
}
fn main();
} // verus!❯ verus src/main.rs
verification results:: 2 verified, 0 errorsfrom verus.
Chris-Hawblitzel
commented on August 23, 2024
I put the spec fn foo issue in #1108 . The other issue should be fixed. Can you try it now?
from verus.
y1ca1
commented on August 23, 2024
Thanks! I played with it and found another interesting bug:
use vstd::prelude::*;
verus!{
trait Foo
{
type R<'a>;
fn foo<'a>(&self, s: &'a [u8]) -> Self::R<'a>;
}
trait Bar<Other>
where
Self: Foo,
Other: Foo,
{
fn bar(&self, other: &Other);
}
impl<U1, U2, V1, V2> Bar<Pair<U2, V2>> for Pair<U1, V1>
where
U1: Foo,
U2: for<'a> Foo<R<'a> = ()>,
V1: Foo,
V2: Foo,
{
fn bar(&self, c: &Pair<U2, V2>) {
}
}
struct Pair<S, T>(S, T);
impl<S, T> Foo for Pair<S, T>
where
S: Foo,
T: Foo,
{
type R<'a> = T::R<'a>;
fn foo<'a>(&self, s: &'a [u8]) -> Self::R<'a> {
self.1.foo(s)
}
}
}
fn main() {}❯ verus src/main.rs
error: mismatched types
--> src/main.rs:37:39
|
37 | fn foo<'a>(&self, s: &'a [u8]) -> Self::R<'a> {
| ^^^^^^^^^^^
38 | self.1.foo(s)
| ^^^^^^
error: aborting due to 1 previous error
note: This error was found in Verus pass: ownership checking of tracked code
error: aborting due to 2 previous errorsThe type error disappears If we move struct Pair<S, T>(S, T); above impl Bar for Pair:
...
struct Pair<S, T>(S, T);
impl<U1, U2, V1, V2> Bar<Pair<U2, V2>> for Pair<U1, V1>
where
U1: Foo,
U2: for<'a> Foo<R<'a> = ()>,
V1: Foo,
V2: Foo,
{
fn bar(&self, c: &Pair<U2, V2>) {
}
}
...❯ verus src/main.rs
verification results:: 2 verified, 0 errorsfrom verus.
Chris-Hawblitzel
commented on August 23, 2024
Ok, try now.
from verus.
y1ca1
commented on August 23, 2024
Ok, try now.
Thanks! Will try it when I get a chance.
from verus.
y1ca1
commented on August 23, 2024
All works!!
Thanks to the series of fixes, I migrated our codebase from using trait generic lifetime (trait Trait<'a>) to the more expressive and fine-grained generic associated type (GAT). Can't thank you enough!
from verus.
Related Issues (20)
- match if-guard wrong semantics with or-patterns
- Pruning on load prunes away lemmas that have been broadcast-used
- Add support for disabling overflow checks
- Panic with expand-errors + overflow checks HOT 1
- Broadcast use shouldn't unconditionally reach a function to prevent it to be pruned
- Expand-errors blames incorrect conjunct HOT 1
- has_type issue with TypX::Primitive
- Verus panic when checking termination on a `Seq` of recursive enums HOT 2
- About heap restriction in PPtr HOT 3
- Panic with opaque associated function
- Verus fails to verify sum additivity for Seq<i32> HOT 1
- wrongly reporting signature mismatch for external_fn_specification HOT 1
- Definitions of functions mentioned in trait requires/ensures are not always visible to implementations of that trait HOT 3
- Array verification regression HOT 5
- vargo doesn't respect RUSTFLAGS
- Generated SMT axioms about trait implementations with associated type projections have triggers that aren't general enough HOT 4
- Panic with `reveal_strlit("")` and `String::from_str("")`
- Using `PhantomData` will cause an unnecessary inaccessible fields error HOT 3
- lifetime-generate doesn't handle auto-derefs for receiver
- left shift operation without a explicit type is not verified HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from verus.