blob: f66f74921ee63af940da3ad0ad4b03bab3cd8085 (
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
|
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.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.
Lemma MapCastCorrect
{round_up}
{t} (e : Expr base_type op 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),
Interp (@Bounds.interp_op) e input_bounds = b
/\ Bounds.is_bounded_by b (Interp interp_op e v)
/\ cast_back_flat_const (Interp interp_op e' v') = (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.
|
