blob: 9a1d8a20b4fc6b35711ea3ed03abdf4953fc9c46 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.ZUtil.Definitions.
Require Import Crypto.Util.ZUtil.Hints.PullPush.
Local Open Scope Z_scope.
Module Z.
Lemma rshi_correct : forall s a b n, 0 <= n -> s <> 0 ->
Z.rshi s a b n = ((b + a * s) / 2 ^ n) mod s.
Proof.
cbv [Z.rshi]; intros. pose proof (Z.log2_nonneg s).
break_match;
repeat match goal with
| H : _ = s |- _ => rewrite H
| _ => rewrite Z.land_ones by auto with zarith
| _ => progress autorewrite with Zshift_to_pow push_Zpow
| _ => reflexivity
end.
Qed.
End Z.
|
