blob: 0103342f41ac2c0e02029de79f3f55909f5ad14a (
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
49
50
51
52
53
54
55
56
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Wf.
Require Import Crypto.Compilers.SmartMap.
Require Import Crypto.Compilers.Relations.
Require Import Crypto.Compilers.MapCastByDeBruijnInterp.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.Z.Syntax.Util.
Require Import Crypto.Compilers.Z.MapCastByDeBruijn.
Require Import Crypto.Compilers.Z.InterpSideConditions.
Require Import Crypto.Util.PointedProp.
Section language.
Context {interp_base_type_bounds : base_type -> Type}
(interp_op_bounds : forall src dst, op src dst -> interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst)
(pick_typeb : forall t, interp_base_type_bounds t -> base_type).
Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v).
Context (cast_op : forall t tR (opc : op t tR) args_bs,
op (pick_type args_bs) (pick_type (interp_op_bounds t tR opc args_bs)))
(cast_backb: forall t b, interp_base_type (pick_typeb t b) -> interp_base_type t).
Let cast_back : forall t b, interp_flat_type interp_base_type (pick_type b) -> interp_flat_type interp_base_type t
:= fun t b => SmartFlatTypeMapUnInterp cast_backb.
Context (inboundsb : forall t, interp_base_type_bounds t -> interp_base_type t -> Prop).
Let inbounds : forall t, interp_flat_type interp_base_type_bounds t -> interp_flat_type interp_base_type t -> Prop
:= fun t => interp_flat_type_rel_pointwise inboundsb (t:=t).
Context (interp_op_bounds_correct
: forall t tR opc bs
(v : interp_flat_type interp_base_type t)
(H : inbounds t bs v)
(Hside : to_prop (interped_op_side_conditions opc v)),
inbounds tR (interp_op_bounds t tR opc bs) (interp_op t tR opc v))
(pull_cast_back
: forall t tR opc bs
(v : interp_flat_type interp_base_type (pick_type bs))
(H : inbounds t bs (cast_back t bs v))
(Hside : to_prop (interped_op_side_conditions opc (cast_back t bs v))),
interp_op t tR opc (cast_back t bs v)
=
cast_back _ _ (interp_op _ _ (cast_op _ _ opc bs) v)).
Local Notation MapCast
:= (@MapCast interp_base_type_bounds interp_op_bounds pick_typeb cast_op).
Lemma MapCastCorrect
{t} (e : Expr t)
(Hwf : Wf e)
(input_bounds : interp_flat_type interp_base_type_bounds (domain t))
: forall {b} e' (He':MapCast e input_bounds = Some (existT _ b e'))
v v' (Hv : @inbounds _ input_bounds v /\ cast_back _ _ v' = v)
(Hside : to_prop (InterpSideConditions e v)),
Compilers.Syntax.Interp interp_op_bounds e input_bounds = b
/\ @inbounds _ b (Compilers.Syntax.Interp interp_op e v)
/\ cast_back _ _ (Compilers.Syntax.Interp interp_op e' v') = (Compilers.Syntax.Interp interp_op e v).
Proof using Type*.
apply MapCastCorrect; auto using internal_base_type_dec_lb.
Qed.
End language.
|
