Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

More fine-grained bounds analysis #1769

Merged
merged 1 commit into from
Dec 5, 2023
Merged

More fine-grained bounds analysis #1769

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 32 additions & 8 deletions src/AbstractInterpretation/ZRange.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -282,6 +282,29 @@ Module Compilers.
Lemma interp_beq_lb {t x y} : x = y -> @interp_beq t t x y = true.
Proof. apply reflect_to_beq; exact _. Qed.

Fixpoint union {t} : interp t -> interp t -> interp t
:= match t return interp t -> interp t -> interp t with
| base.type.type_base base.type.Z => Option.map2 ZRange.union
| base.type.type_base _ as t
| base.type.unit as t
=> fun x y
=> if @interp_beq t t x y
then x
else None
| base.type.prod A B => fun '(a, b) '(a', b') =>
(@union A a a', @union B b b')
| base.type.list A => fun la lb => Option.bind2 la lb (fun la lb =>
if Nat.eqb (length la) (length lb)
then Datatypes.Some (List.map (uncurry (@union A)) (List.combine la lb))
else Datatypes.None)
| base.type.option A => fun oa ob => Option.bind2 oa ob (fun l r =>
match l, r return option (option (interp A)) with
| Datatypes.Some l, Datatypes.Some r => Datatypes.Some (Datatypes.Some (union l r))
| Datatypes.None, Datatypes.None => Datatypes.Some Datatypes.None
| _, _ => Datatypes.None
end)
end.

Fixpoint is_bounded_by {t} : interp t -> binterp t -> bool
:= match t with
| base.type.type_base base.type.Z as t
Expand Down Expand Up @@ -573,12 +596,6 @@ Module Compilers.
| None => None
end
| ident.Z_eqb as idc
| ident.Z_leb as idc
| ident.Z_ltb as idc
| ident.Z_geb as idc
| ident.Z_gtb as idc
| ident.Z_max as idc
| ident.Z_min as idc
| ident.Z_pow as idc
| ident.Z_lxor as idc
| ident.Z_modulo as idc
Expand Down Expand Up @@ -623,13 +640,13 @@ Module Compilers.
=> fun t f b
=> match b with
| Some b => if b then t tt else f tt
| None => ZRange.type.base.option.None
| None => type.base.option.union (t tt) (f tt)
end
| ident.bool_rect_nodep _
=> fun t f b
=> match b with
| Some b => if b then t else f
| None => ZRange.type.base.option.None
| None => type.base.option.union t f
end
| ident.option_rect _ _
=> fun s n o
Expand Down Expand Up @@ -737,10 +754,17 @@ Module Compilers.
| ident.List_app _
=> fun ls1 ls2 => ls1 <- ls1; ls2 <- ls2; Some (List.app ls1 ls2)
| ident.List_rev _ => option_map (@List.rev _)
| ident.Z_leb as idc
| ident.Z_ltb as idc
| ident.Z_geb as idc
| ident.Z_gtb as idc
=> fun x y => x <- x; y <- y; ZRange.ToConstant.four_corners Bool.eqb (ident.interp idc) x y
| ident.Z_opp as idc
| ident.Z_log2 as idc
| ident.Z_log2_up as idc
=> fun x => x <- x; Some (ZRange.two_corners (ident.interp idc) x)
| ident.Z_max as idc
| ident.Z_min as idc
| ident.Z_add as idc
| ident.Z_mul as idc
| ident.Z_sub as idc
Expand Down
67 changes: 67 additions & 0 deletions src/AbstractInterpretation/ZRangeProofs.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@ Require Import Crypto.Util.Tactics.SpecializeBy.
Require Import Crypto.Util.Tactics.SpecializeAllWays.
Require Import Crypto.Util.Tactics.Head.
Require Import Crypto.Util.Tactics.PrintGoal.
Require Import Crypto.Util.Tactics.DoWithHyp.
Require Import Crypto.Language.PreExtra.
Require Import Crypto.CastLemmas.
Require Import Crypto.AbstractInterpretation.ZRange.
Expand All @@ -58,6 +59,61 @@ Module Compilers.
Module option.
Lemma is_bounded_by_None t v : ZRange.type.base.option.is_bounded_by (@ZRange.type.base.option.None t) v = true.
Proof. induction t; cbn; cbv [andb]; break_innermost_match; eauto. Qed.

Lemma tighter_than_union t (rx ry : ZRange.type.base.option.interp t) :
ZRange.type.base.option.is_tighter_than rx (ZRange.type.base.option.union rx ry) = true /\
ZRange.type.base.option.is_tighter_than ry (ZRange.type.base.option.union rx ry) = true.
Proof.
induction t; [destruct t|..]; destruct rx, ry;
cbn [
ZRange.type.base.interp
ZRange.type.base.option.interp
ZRange.type.base.option.is_tighter_than
ZRange.type.base.is_tighter_than
ZRange.type.base.option.union
Option.map2
Option.bind2
] in *; auto 2.
all: fold (@ZRange.type.base.option.interp) in *.
all: break_innermost_match; reflect_hyps; inversion_option; subst; auto 2.
all: split_and.
all: cbn [option_beq].
all: rewrite ?Bool.andb_true_iff; auto.
all: try now split; first [ apply ZRange.is_tighter_than_bool_union_l | apply ZRange.is_tighter_than_bool_union_r ].
all: do 2 try (match goal with
| [ |- context[?x = true] ]
=> lazymatch x with true => fail | false => fail | _ => idtac end;
destruct x eqn:?; progress reflect_hyps
end;
cbn [ZRange.type.base.option.None] in *;
auto 2; subst; try congruence).
{ rewrite 2 fold_andb_map_map.
rewrite 2 fold_andb_map_iff.
rewrite List.combine_length.
do_with_hyp' ltac:(fun H => rewrite H).
rewrite Nat.min_id.
repeat split; intros *; destruct_head'_prod; cbn [uncurry fst snd].
all: rewrite In_nth_error_iff.
all: intros [n H']; revert H'.
all: rewrite !nth_error_combine.
all: break_innermost_match; intros; inversion_option; inversion_pair; subst; auto. }
Qed.

Lemma is_bounded_by_union_l t (rx ry : ZRange.type.base.option.interp t) x :
ZRange.type.base.option.is_bounded_by rx x = true ->
ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union rx ry) x = true.
Proof.
eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; try eassumption;
eapply tighter_than_union.
Qed.

Lemma is_bounded_by_union_r t (rx ry : ZRange.type.base.option.interp t) y :
ZRange.type.base.option.is_bounded_by ry y = true ->
ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union rx ry) y = true.
Proof.
eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; try eassumption;
eapply tighter_than_union.
Qed.
End option.
End base.

Expand Down Expand Up @@ -484,6 +540,16 @@ Module Compilers.
| [ H : (forall a b, ?R0 a b = true -> forall c d, ?R1 c d = true -> forall e f, (forall g h, ?R3 g h = true -> ?R4 (e g) (f h) = true) -> forall i j, ?R5 i j = true -> ?R6 (?F _ _ _ _) (?G _ _ _ _) = true)
|- ?R6 (?F _ _ _ _) (?G _ _ _ _) = true ]
=> apply H; clear H
end
| match goal with
| [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.Thunked.bool_rect _ _ _ true) = true ]
=> apply ZRange.type.base.option.is_bounded_by_union_l
| [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.Thunked.bool_rect _ _ _ false) = true ]
=> apply ZRange.type.base.option.is_bounded_by_union_r
| [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.bool_rect_nodep _ _ true) = true ]
=> apply ZRange.type.base.option.is_bounded_by_union_l
| [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.bool_rect_nodep _ _ false) = true ]
=> apply ZRange.type.base.option.is_bounded_by_union_r
end ].

Local Lemma mul_by_halves_bounds x y n :
Expand Down Expand Up @@ -751,6 +817,7 @@ Module Compilers.
end
| intros; mul_by_halves_t ].
all: try solve [ non_arith_t; Z.ltb_to_lt; reflexivity ].
all: try solve [ cbv [ZRange.ToConstant.four_corners ZRange.ToConstant.Option.four_corners ZRange.ToConstant.Option.apply_to_range ZRange.ToConstant.Option.two_corners ZRange.ToConstant.Option.union option_beq Bool.eqb] in *; non_arith_t; Z.ltb_to_lt; lia ].
(** For command-line debugging, we display goals that should not remain *)
all: [ > idtac "WARNING: Remaining goal:"; print_context_and_goal () .. ].
Qed.
Expand Down
Loading