blob: 560f89199059956ed69ca4e5a9aed724c28875a1 (
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
|
Require Import Crypto.Util.ZRange.
Require Import Crypto.Util.Sum.
Require Import Crypto.Util.LetIn.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Experiments.NewPipeline.Language.
Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation.
Local Open Scope Z_scope.
Module Compilers.
Export Language.Compilers.
Export UnderLets.Compilers.
Export AbstractInterpretation.Compilers.
Import invert_expr.
Import defaults.
Axiom admit_pf : False.
Local Notation admit := (match admit_pf with end).
Theorem CheckedPartialEvaluateWithBounds_Correct
(relax_zrange : zrange -> option zrange)
(Hrelax : forall r r' z, is_tighter_than_bool z r = true
-> relax_zrange r = Some r'
-> is_tighter_than_bool z r' = true)
{t} (E : Expr t)
(b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
(b_out : ZRange.type.base.option.interp (type.final_codomain t))
rv (Hrv : CheckedPartialEvaluateWithBounds relax_zrange E b_in b_out = inl rv)
: forall arg
(Harg : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg = true),
ZRange.type.base.option.is_bounded_by b_out (type.app_curried (Interp rv) arg) = true
/\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg
= type.app_curried (Interp E) arg.
Proof.
cbv [CheckedPartialEvaluateWithBounds CheckPartialEvaluateWithBounds Let_In] in *;
break_innermost_match_hyps; inversion_sum; subst.
intros arg Harg.
split.
{ eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ].
revert Harg.
exact admit. (* boundedness *) }
{ exact admit. (* correctness of interp *) }
Qed.
End Compilers.
|
