Conversation
jschneider-bensch
left a comment
jschneider-bensch
left a comment
There was a problem hiding this comment.
Can you say more about the inconvenience of cfg(hax) when using Rust specs?
| v (Seq.index ${_lhs0}.f_elements i) + v (Seq.index ${rhs}.f_elements i))" | ||
| ); | ||
| hax_lib::fstar!( | ||
| r#"reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) (Spec.Utils.is_i16b_array_opaque)"# |
There was a problem hiding this comment.
Is this related to the introduction of opaque predicates? Does it mean while the higher-level modules will have less F* annotations, we will need to reveal_opaque in the lower-levels?
There was a problem hiding this comment.
Yes, the observation is that the verification of higher-level modules was taking an unnecessarily long time because the underlying math was not opaque, even if the math itself is not needed for the proof. So we make it opaque at (or near) the trait boundary, so modules above can be verified quickly and the modules below will need to reveal these predicates when needed.
libcrux-ml-kem/src/invert_ntt.rs
Outdated
There was a problem hiding this comment.
The spec functions return hax_lib::Prop instead of bool, which means you use .and here as the connective. That could be cumbersome in case there are a larger number of preconditions that have to be .anded together. Would it be possible to implement e.g. BitAnd for Prop to be able to & two of them. (The short-circuiting && is sadly not overloadable.)
There was a problem hiding this comment.
Yes, that would be a good feature upgrade. For now, I am trying to live within the constraints of the current hax-lib until libcrux is upgraded to latest hax.
libcrux-ml-kem/src/invert_ntt.rs
Outdated
There was a problem hiding this comment.
This invariant is much more readable (to me)! Any reason to use the fstar_prop_expr! instead of (*zeta_i == _zeta_i_init - round * 4).to_prop()?
There was a problem hiding this comment.
no good reason, we should change to your version (earlier, I may have been trying to avoid to_prop but it was not a good reason).
| (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ sz i ])))"# | ||
| hax_lib::fstar_prop_expr!(r#"v $zeta_i == v $_zeta_i_init - v $round * 4"#).and( | ||
| hax_lib::forall(|i: usize| { | ||
| if i < 16 { |
There was a problem hiding this comment.
Maybe there could be a convenience macro for loop invariants like this, e.g. pivot!(array, round, prop_lower_equal, prop_higher) that states prop_lower_equal for array[i] with i in 0..=round and prop_higher for i in (round + 1).. array.len().
There was a problem hiding this comment.
sure, yes, once we have a bunch of annotations like these, we can try to find common patterns. (Copilot is already able to suggest these patterns to me now.)
| #[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning")] | ||
| #[hax_lib::requires( | ||
| spec::is_bounded_poly(3328, re).and( | ||
| match layer { |
There was a problem hiding this comment.
It's neat to be able to use a match here, but it could also be written in terms of layer, i.e. *zeta_i == (1 << (8 - layer)) (keeping the boundedness condition for layer). Does it make a difference for the proofs?
There was a problem hiding this comment.
I don't like using shifts in specs. Maybe you mean pow2(8 - layer) which may be nicer if that is what the NIST spec says e.g.
I undid that, it basically needs a few more |
2 participants
This PR does a few things:
We should discuss this style and stabilize it before going further.
One design point is the use of
cfg(hax)for specs.I was doing that uniformly before, but it is inconvenient when we start using Rust annotations more uniformly.
But maybe now the code is less cluttered, we don't mind having hax enabled everywhere? Dunno.
So some discussion is needed around how and whether to use conditional flags.