search

adampetcher / fcf

Foundational Cryptography Framework for machine-checked proofs of cryptography.
Other
48 stars 23 forks source link

adapt to coq/coq/17132 #41

Closed andres-erbsen closed 1 year ago

andres-erbsen commented 1 year ago

The lognat change isn't strictly required but IMO it's an improvement (N.size_nat is there to define gcd).

andrew-appel commented 1 year ago

Unfortunately, this PR is not backward-compatible to Coq 8.16.1. The problem is in Blist.v, with Nat.Div0.mod_mul_r (which doesn't exist in 8.16.1). Can you use the following proof instead?

Lemma bvToNat_natToBv : forall n k,
  bvToNat (natToBv n k) = k mod (2 ^ n).
Proof.
  induction n; cbn [bvToNat natToBv]; trivial; intros.
  cbn [Nat.pow]; rewrite Nat.mod_mul_r by (try apply Nat.pow_nonzero; lia).
  setoid_rewrite Nat.bit0_mod.
  f_equal.
  rewrite IHn, Nat.div2_div, Nat.double_twice; trivial.
Qed.
andrew-appel commented 1 year ago

testing this fix in #43 for Coq 8.17 compatibility