blob: 1217cd7211a2a2ee157583bbbfc9d40ca4151161 (
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
48
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Wf.
Require Import Crypto.Compilers.SmartMap.
Require Import Crypto.Compilers.Relations.
Require Import Crypto.Compilers.Z.MapCastByDeBruijnInterp.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.Z.Syntax.Util.
Require Import Crypto.Compilers.Z.InterpSideConditions.
Require Import Crypto.Compilers.Z.Bounds.Interpretation.
Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.IsBoundedBy.
Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.PullCast.
Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn.
Require Import Crypto.Util.PointedProp.
Lemma MapCastCorrect
{round_up}
{t} (e : Expr t)
(Hwf : Wf e)
(input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
: forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e'))
v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v)
(Hside : to_prop (InterpSideConditions e v)),
Compilers.Syntax.Interp (@Bounds.interp_op) e input_bounds = b
/\ Bounds.is_bounded_by b (Compilers.Syntax.Interp interp_op e v)
/\ cast_back_flat_const (Compilers.Syntax.Interp interp_op e' v') = (Compilers.Syntax.Interp interp_op e v).
Proof.
apply MapCastCorrect; auto.
{ apply is_bounded_by_interp_op. }
{ apply pull_cast_genericize_op, is_bounded_by_interp_op. }
Qed.
Lemma MapCastCorrect_eq
{round_up}
{t} (e : Expr t)
{evb ev}
(Hwf : Wf e)
(input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
: forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e'))
v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v)
(Hside : to_prop (InterpSideConditions e v))
(Hevb : evb = Compilers.Syntax.Interp (@Bounds.interp_op) e input_bounds)
(Hev : ev = Compilers.Syntax.Interp interp_op e v),
evb = b
/\ Bounds.is_bounded_by b ev
/\ cast_back_flat_const (Compilers.Syntax.Interp interp_op e' v') = ev.
Proof.
intros; subst; apply MapCastCorrect; auto.
Qed.
|
