Some class parameters are incorrectly passed #719
Comments
|
Thanks for fixing this, Lucas. |
|
I will reopen this issue because hax mainstream seems to produce the same kind of error for different modules in libcrux-ml-kem For example here the parameter of |
|
The old problems seem to be fixed with this PR #738 but now I got implicit parameters that are supposed to be passed explicitly, here's an example |
|
The previous comment was false alert. However, even with PR #738 I can still instances of this bug. |
This PR separates method generic args and trait generic args of the
`call` nodes of THIR expressions.
Consider the following example:
```rust
trait MyTrait<TraitType> {
fn meth<MethType>(...) {...}
}
fn example_call<TraitType, SelfType: MyTrait<TraitType>>(x: SelfType) {
x.meth::<String>(...)
}
```
Before this commit, the call `x.meth::<String>` produced a `Call` node
whose field `generic_args` was `[SelfType, TraitType, String]`.
Now, that `Call` node has a trait-specific generic arguments field
`[SelfType, TraitType]` and a method/function-specific generic
arguments field `[String].`
This commit does no change to the engine, that will be for a
subsequent PR.
This PR is related to #719.
This PR separates method generic args and trait generic args of the
`call` nodes of THIR expressions.
Consider the following example:
```rust
trait MyTrait<TraitType> {
fn meth<MethType>(...) {...}
}
fn example_call<TraitType, SelfType: MyTrait<TraitType>>(x: SelfType) {
x.meth::<String>(...)
}
```
Before this commit, the call `x.meth::<String>` produced a `Call` node
whose field `generic_args` was `[SelfType, TraitType, String]`.
Now, that `Call` node has a trait-specific generic arguments field
`[SelfType, TraitType]` and a method/function-specific generic
arguments field `[String].`
This commit does no change to the engine, that will be for a
subsequent PR.
This PR is related to #719.
This PR separates method generic args and trait generic args of the
`call` nodes of THIR expressions.
Consider the following example:
```rust
trait MyTrait<TraitType> {
fn meth<MethType>(...) {...}
}
fn example_call<TraitType, SelfType: MyTrait<TraitType>>(x: SelfType) {
x.meth::<String>(...)
}
```
Before this commit, the call `x.meth::<String>` produced a `Call` node
whose field `generic_args` was `[SelfType, TraitType, String]`.
Now, that `Call` node has a trait-specific generic arguments field
`[SelfType, TraitType]` and a method/function-specific generic
arguments field `[String].`
This commit does no change to the engine, that will be for a
subsequent PR.
This PR is related to #719.
|
Update: I almost fixed it, but got distracted with other things, I will finish that tomorrow morning. |
In some extracted F* files in
libcrux-ml-kem, arguments for classes are passed as explicit parameters. For example,v_Kvariable here is supposed to be ghost parameter https://github.com/cryspen/libcrux/blob/dev/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst#L89It's fixed manually in
dev_ml_kem_laxbranch https://github.com/cryspen/libcrux/blob/dev_ml_kem_lax/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst#L89The text was updated successfully, but these errors were encountered: