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 b67170f commit d73f0b7
Show file tree
Hide file tree
Showing 8 changed files with 449 additions and 53 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 @@ -548,13 +548,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 @@ -687,18 +691,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 @@ -712,18 +718,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 @@ -775,6 +786,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
Loading

0 comments on commit d73f0b7

Please sign in to comment.