Proof libs: `%` is modeled as an euclidian remainder while it's just a remainder

[W95Psp]

Basically, (-4 % 8) is 4 in F* but -4 in Rust.

/// Typechecks in F*.
/// If you click `Share` and `Open in Rust playground`, then `Run`, you'll observe this panics.
fn main() {
    assert!((-4 % 8) == 4);
}

Open this code snippet in the playground

[github-actions[bot]]

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]

This is still very much relevant. It's a trivial fix, the real job here is to make sure this doesn't break anything.

[clementblaudeau]

I've noticed it while working on the Lean backend, where % has the same semantic as Rust. This breaks the spec of Barrett for instance :

#[hax_lib::fstar::options("--z3rlimit 100")]
#[hax::requires((i64::from(value) >= -BARRETT_R && i64::from(value) <= BARRETT_R))]
#[hax::ensures(|result| result > -FIELD_MODULUS && result < FIELD_MODULUS &&
                   result % FIELD_MODULUS == value % FIELD_MODULUS)]
pub fn barrett_reduce(value: FieldElement) -> FieldElement {

as result % FIELD_MODULUS can be negative, while value % FIELD_MODULUS is not

[github-actions[bot]]

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.