Skip to content

Commit

Permalink
Add more identifiers for saturated solinas
Browse files Browse the repository at this point in the history 
For #1609

Co-authored-by: Andres Erbsen <andres-github@andres.systems>
  • Loading branch information
@JasonGross @andres-erbsen
JasonGross and andres-erbsen committed Dec 7, 2023
1 parent 612f675 commit 9d120d3
Show file tree
Hide file tree
Showing 8 changed files with 239 additions and 51 deletions.
39 changes: 26 additions & 13 deletions src/AbstractInterpretation/ZRange.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -536,13 +536,17 @@ Module Compilers.
| ident.Nat_pred as idc
=> option_map (ident.interp idc)
| ident.Z_of_nat as idc
=> option_map (fun n => r[Z.of_nat n~>Z.of_nat n]%zrange)
| ident.Z_pos as idc
=> option_map (fun n => r[ident.interp idc n~>ident.interp idc n]%zrange)
| ident.Z_to_nat as idc
| ident.Z_to_pos as idc
=> fun v => v <- to_literal v; Some (ident.interp idc v)
| ident.List_length _
=> option_map (@List.length _)
| ident.value_barrier
=> fun x => x
| ident.Pos_mul as idc
| ident.Pos_add as idc
| ident.Nat_max as idc
| ident.Nat_mul as idc
| ident.Nat_add as idc
Expand Down Expand Up @@ -675,18 +679,20 @@ Module Compilers.
n
| None => ZRange.type.base.option.None
end
| ident.nat_rect_arrow _ _
| ident.eager_nat_rect_arrow _ _
=> fun O_case S_case n v
=> match n with
| ident.nat_rect_arrow _ _ as idc
| ident.eager_nat_rect_arrow _ _ as idc
| ident.nat_rect_fbb_b _ _ _ as idc
| ident.nat_rect_fbb_b_b _ _ _ _ as idc
=> fun O_case S_case n
=> let t := ((fun t (idc : ident (_ -> _ -> _ -> t)) => t) _ idc) in
match n return type.option.interp t with
| Some n
=> nat_rect
_
O_case
(fun n' rec => S_case (Some n') rec)
n
v
| None => ZRange.type.base.option.None
| None => ZRange.type.option.None
end
| ident.list_rect _ _
| ident.eager_list_rect _ _
Expand All @@ -700,18 +706,23 @@ Module Compilers.
ls
| None => ZRange.type.base.option.None
end
| ident.list_rect_arrow _ _ _
| ident.eager_list_rect_arrow _ _ _
=> fun N C ls v
=> match ls with
| ident.list_rect_arrow _ _ _ as idc
| ident.eager_list_rect_arrow _ _ _ as idc
| ident.list_rect_fbb_b _ _ _ _ as idc
| ident.list_rect_fbb_b_b _ _ _ _ _ as idc
| ident.list_rect_fbb_b_b_b _ _ _ _ _ _ as idc
| ident.list_rect_fbb_b_b_b_b _ _ _ _ _ _ _ as idc
| ident.list_rect_fbb_b_b_b_b_b _ _ _ _ _ _ _ _ as idc
=> fun N C ls
=> let t := ((fun t (idc : ident (_ -> _ -> _ -> t)) => t) _ idc) in
match ls return type.option.interp t with
| Some ls
=> list_rect
_
N
(fun x xs rec => C x (Some xs) rec)
ls
v
| None => ZRange.type.base.option.None
| None => ZRange.type.option.None
end
| ident.list_case _ _
=> fun N C ls
Expand Down Expand Up @@ -763,6 +774,8 @@ Module Compilers.
| 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_abs as idc
=> fun x => x <- x; Some (ZRange.two_corners_and_zero (ident.interp idc) x)
| ident.Z_max as idc
| ident.Z_min as idc
| ident.Z_add as idc
Expand Down
13 changes: 11 additions & 2 deletions src/AbstractInterpretation/ZRangeCommonProofs.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ Require Import Crypto.Util.NatUtil.
Require Import Crypto.Util.ZUtil.Morphisms.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.Tactics.DoWithHyp.
Require Import Crypto.AbstractInterpretation.ZRange.

Module Compilers.
Expand Down Expand Up @@ -36,14 +37,21 @@ Module Compilers.
| progress inversion_option
| discriminate
| solve [ eauto ]
| apply (@list_rect_Proper_gen _ ((_ -> _) -> _ -> _ -> _ -> _ -> _) ((eq ==> eq) ==> eq ==> eq ==> eq ==> eq ==> eq)%signature)
| apply (@list_rect_Proper_gen _ ((_ -> _) -> _ -> _ -> _ -> _) ((eq ==> eq) ==> eq ==> eq ==> eq ==> eq)%signature)
| apply (@list_rect_Proper_gen _ ((_ -> _) -> _ -> _ -> _) ((eq ==> eq) ==> eq ==> eq ==> eq)%signature)
| apply (@list_rect_Proper_gen _ ((_ -> _) -> _ -> _) ((eq ==> eq) ==> eq ==> eq)%signature)
| apply (@list_rect_Proper_gen _ ((_ -> _) -> _) ((eq ==> eq) ==> eq)%signature)
| apply (@nat_rect_Proper_nondep_gen ((_ -> _) -> _ -> _) ((eq ==> eq) ==> eq ==> eq)%signature)
| apply (@nat_rect_Proper_nondep_gen ((_ -> _) -> _) ((eq ==> eq) ==> eq)%signature)
| apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature)
| apply NatUtil.nat_rect_Proper_nondep
| apply ListUtil.list_rect_Proper
| apply ListUtil.list_rect_arrow_Proper
| apply ListUtil.list_case_Proper
| apply ListUtil.pointwise_map
| apply ListUtil.fold_right_Proper
| apply ListUtil.update_nth_Proper
| apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature)
| cbn; apply (f_equal (@Some _))
| progress cbn [ZRange.ident.option.interp]
| progress cbv [zrange_rect]
Expand All @@ -54,7 +62,8 @@ Module Compilers.
| [ H : forall x y, x = y -> _ |- _ ] => specialize (fun x => H x x eq_refl)
| [ H : forall x, ?f x = ?g x, H1 : ?f ?y = _, H2 : ?g ?y = _ |- _ ]
=> specialize (H y); rewrite H1, H2 in H
end ].
end
| do_with_exactly_one_hyp ltac:(fun H => apply H; clear H) ].
Qed.
End interp_related.
End option.
Expand Down
82 changes: 52 additions & 30 deletions src/AbstractInterpretation/ZRangeProofs.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -436,7 +436,7 @@ Module Compilers.
| break_innermost_match_step
| break_innermost_match_hyps_step
| progress cbn [id
ZRange.type.base.option.is_bounded_by is_bounded_by_bool ZRange.type.base.is_bounded_by lower upper fst snd projT1 projT2 bool_eq base.interp base.base_interp Crypto.Util.Option.bind fold_andb_map negb ZRange.ident.option.to_literal ZRange.type.base.option.None fst snd ZRange.type.base.option.interp ZRange.type.base.interp List.combine List.In base.interp_beq base.base_interp_beq base.base_interp] in *
ZRange.type.base.option.is_bounded_by is_bounded_by_bool ZRange.type.base.is_bounded_by lower upper fst snd projT1 projT2 bool_eq base.interp base.base_interp Crypto.Util.Option.bind fold_andb_map negb ZRange.ident.option.to_literal ZRange.type.base.option.None fst snd ZRange.type.base.option.interp ZRange.type.base.interp List.combine List.In base.interp_beq base.base_interp_beq base.base_interp ZRange.type.option.None] in *
| progress ident.fancy.cbv_fancy_in_all
| progress destruct_head'_bool
| solve [ auto with nocore ]
Expand Down Expand Up @@ -482,16 +482,43 @@ Module Compilers.
| [ |- and _ _ ] => apply conj
end
| progress cbv [bool_eq Bool.eqb option_map List.nth_default Definitions.Z.bneg is_bounded_by_bool zrange_beq] in *
| let rec do_rect_head lhs rhs k :=
lazymatch lhs with
| nat_rect ?P ?O ?S ?n
=> lazymatch rhs with
| nat_rect ?P' ?O' ?S' n
=> is_var n;
k ();
induction n; cbn [nat_rect];
generalize dependent (nat_rect P O S); generalize dependent (nat_rect P' O' S');
intros
end
| list_rect ?P ?N ?C ?ls
=> lazymatch rhs with
| list_rect ?P' ?N' ?C' ?ls'
=> lazymatch goal with
| [ H : length ls = length ls' |- _ ]
=> is_var ls; is_var ls'; k ();
let IH := fresh "IH" in
(revert dependent ls'; induction ls as [|? ls IH]; intros [|? ls']; intros; cbn [list_rect length] in * );
[
| exfalso; discriminate | exfalso; discriminate
| specialize (IH ls');
generalize dependent (list_rect P N C); generalize dependent (list_rect P' N' C') ];
intros
end
end
| ?f ?x
=> lazymatch rhs with
| ?g ?y
=> is_var x; is_var y;
do_rect_head f g ltac:(fun _ => k (); revert dependent x; try revert dependent y)
end
end in
lazymatch goal with
| [ |- ?R ?lhs ?rhs = true ] => do_rect_head lhs rhs ltac:(fun _ => idtac)
end
| match goal with
| [ |- ?R (nat_rect ?P ?O ?S ?n) (nat_rect ?P' ?O' ?S' ?n) = true ]
=> is_var n; induction n; cbn [nat_rect];
generalize dependent (nat_rect P O S); generalize dependent (nat_rect P' O' S');
intros
| [ |- ?R (nat_rect ?P ?O ?S ?n ?x) (nat_rect ?P' ?O' ?S' ?n ?y) = true ]
=> is_var n; is_var x; is_var y;
revert dependent x; revert dependent y; induction n; cbn [nat_rect];
generalize dependent (nat_rect P O S); generalize dependent (nat_rect P' O' S');
intros
| [ H : length ?ls = length ?ls' |- ?R (List.fold_right ?f ?x ?ls) (List.fold_right ?f' ?x' ?ls') = true ]
=> is_var ls; is_var ls';
let IH := fresh "IH" in
Expand All @@ -510,25 +537,6 @@ Module Compilers.
| specialize (IH ls');
generalize dependent (List.fold_right f x); generalize dependent (List.fold_right f' x') ];
intros
| [ H : length ?ls = length ?ls' |- ?R (list_rect ?P ?N ?C ?ls) (list_rect ?P' ?N' ?C' ?ls') = true ]
=> is_var ls; is_var ls';
let IH := fresh "IH" in
revert dependent ls'; induction ls as [|? ls IH]; intros [|? ls']; intros; cbn [list_rect length] in *;
[
| exfalso; discriminate | exfalso; discriminate
| specialize (IH ls');
generalize dependent (list_rect P N C); generalize dependent (list_rect P' N' C') ];
intros
| [ H : length ?ls = length ?ls' |- ?R (list_rect ?P ?N ?C ?ls ?x) (list_rect ?P' ?N' ?C' ?ls' ?y) = true ]
=> is_var ls; is_var ls'; is_var x; is_var y;
revert dependent y; try revert dependent x;
let IH := fresh "IH" in
revert dependent ls'; induction ls as [|? ls IH]; intros [|? ls']; intros; cbn [list_rect length] in *;
[
| exfalso; discriminate | exfalso; discriminate
| specialize (IH ls');
generalize dependent (list_rect P N C); generalize dependent (list_rect P' N' C') ];
intros
| [ H : forall a b, ?R a b = true -> ?R' (?f a) (?g b) = true |- ?R' (?f _) (?g _) = true ] => apply H; clear H
| [ H : forall a b, ?R a b = true -> forall c d, ?R' c d = true -> ?R'' (?f a c) (?g b d) = true |- ?R'' (?f _ _) (?g _ _) = true ]
=> apply H; clear H
Expand All @@ -550,7 +558,8 @@ Module Compilers.
=> 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 ].
end
| do_with_hyp' ltac:(fun H => apply H; clear H; now non_arith_t) ].

Local Lemma mul_by_halves_bounds x y n :
(0 <= x < 2^ (n / 2))%Z ->
Expand Down Expand Up @@ -723,6 +732,15 @@ Module Compilers.
all: change (@list_rect_arrow_nodep) with (fun A P Q => @list_rect A (fun _ => P -> Q)).
all: change (@Thunked.list_case) with (fun A P PNil => @list_case A (fun _ => P) (PNil Datatypes.tt)) in *.
all: change (@Thunked.option_rect) with (fun A P PS PN => @option_rect A (fun _ => P) PS (PN Datatypes.tt)) in *.
all: cbv [
nat_rect_fbb_b
nat_rect_fbb_b_b
list_rect_fbb_b
list_rect_fbb_b_b
list_rect_fbb_b_b_b
list_rect_fbb_b_b_b_b
list_rect_fbb_b_b_b_b_b
] in *.
all: cbv [respectful_hetero option_map option_rect zrange_rect list_case].
all: intros.
all: destruct_head_hnf' prod.
Expand Down Expand Up @@ -786,6 +804,9 @@ Module Compilers.
| [ Hx : is_bounded_by_bool _ ?x = true
|- is_bounded_by_bool _ (ZRange.two_corners ?f ?x) = true ]
=> apply (fun pf => @ZRange.monotoneb_two_corners_gen f pf x _ Hx); intros; auto with zarith
| [ Hx : is_bounded_by_bool _ ?x = true
|- is_bounded_by_bool _ (ZRange.two_corners_and_zero ?f ?x) = true ]
=> apply (fun pf1 pf2 => @ZRange.monotoneb_two_corners_and_zero_gen f pf1 pf2 x _ Hx); intros; auto with zarith
| [ |- is_bounded_by_bool (if _ then _ else _) (ZRange.four_corners _ _ _) = true ]
=> apply ZRange.is_bounded_by_bool_Proper_if_bool_union_dep; intros; Z.ltb_to_lt
| [ _ : is_bounded_by_bool ?x1 ?r1 = true,
Expand Down Expand Up @@ -817,6 +838,7 @@ Module Compilers.
end
| intros; mul_by_halves_t ].
all: try solve [ non_arith_t; Z.ltb_to_lt; reflexivity ].
all: try solve [ non_arith_t; try match goal with |- ?x = true => destruct x eqn:? end; reflect_hyps; subst; nia ].
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 () .. ].
Expand Down
Loading

0 comments on commit 9d120d3

Please sign in to comment.