blob: b8e268b1cc3426567ce9e3dbaa3f44b75a6a3dea (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Language.
Require Import Crypto.LanguageWf.
Require Import Crypto.Util.ZRange.
Require Import Crypto.RewriterAllTactics.
Require Import Crypto.RewriterRulesProofs.
Module Compilers.
Import Language.Compilers.
Import Language.Compilers.defaults.
Import LanguageWf.Compilers.
Import RewriterAllTactics.Compilers.RewriteRules.GoalType.
Import RewriterAllTactics.Compilers.RewriteRules.Tactic.
Module Import RewriteRules.
Section __.
Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z)
(value_range flag_range : zrange)
(Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
(Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)).
Definition VerifiedRewriterToFancyWithCasts : VerifiedRewriter.
Proof using All. make_rewriter false (@fancy_with_casts_rewrite_rules_proofs invert_low invert_high value_range flag_range Hlow Hhigh). Defined.
Definition RewriteToFancyWithCasts {t} : Expr t -> Expr t.
Proof using invert_low invert_high value_range flag_range.
let v := (eval hnf in (@Rewrite VerifiedRewriterToFancyWithCasts t)) in exact v.
Defined.
Lemma Wf_RewriteToFancyWithCasts {t} e (Hwf : Wf e) : Wf (@RewriteToFancyWithCasts t e).
Proof using All. now apply VerifiedRewriterToFancyWithCasts. Qed.
Lemma Interp_gen_RewriteToFancyWithCasts {cast_outside_of_range t} e (Hwf : Wf e)
: expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteToFancyWithCasts t e)
== expr.Interp (@ident.gen_interp cast_outside_of_range) e.
Proof using All. now apply VerifiedRewriterToFancyWithCasts. Qed.
Lemma Interp_RewriteToFancyWithCasts {t} e (Hwf : Wf e) : Interp (@RewriteToFancyWithCasts t e) == Interp e.
Proof using All. apply Interp_gen_RewriteToFancyWithCasts; assumption. Qed.
End __.
End RewriteRules.
Module Export Hints.
Hint Resolve Wf_RewriteToFancyWithCasts : wf.
Hint Rewrite @Interp_gen_RewriteToFancyWithCasts @Interp_RewriteToFancyWithCasts : interp.
End Hints.
End Compilers.
|