diff options
Diffstat (limited to 'src/Compilers/Z/Syntax.v')
| -rw-r--r-- | src/Compilers/Z/Syntax.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Compilers/Z/Syntax.v b/src/Compilers/Z/Syntax.v index 754b3fb5a..7d0c84421 100644 --- a/src/Compilers/Z/Syntax.v +++ b/src/Compilers/Z/Syntax.v @@ -6,6 +6,7 @@ Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.TypeUtil. Require Import Crypto.Util.FixedWordSizes. Require Import Crypto.Util.Option. +Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.NatUtil. (* for nat_beq for equality schemes *) Export Syntax.Notations. @@ -26,6 +27,9 @@ Inductive op : flat_type base_type -> flat_type base_type -> Type := | Land T1 T2 Tout : op (Tbase T1 * Tbase T2) (Tbase Tout) | Lor T1 T2 Tout : op (Tbase T1 * Tbase T2) (Tbase Tout) | Opp T Tout : op (Tbase T) (Tbase Tout) +| Zselect T1 T2 T3 Tout : op (Tbase T1 * Tbase T2 * Tbase T3) (Tbase Tout) +| AddWithCarry T1 T2 T3 Tout : op (Tbase T1 * Tbase T2 * Tbase T3) (Tbase Tout) +| AddWithGetCarry (bitwidth : Z) T1 T2 T3 Tout1 Tout2 : op (Tbase T1 * Tbase T2 * Tbase T3) (Tbase Tout1 * Tbase Tout2) . Definition interp_base_type (v : base_type) : Type := @@ -78,6 +82,9 @@ Definition Zinterp_op src dst (f : op src dst) | Land _ _ _ => fun xy => Z.land (fst xy) (snd xy) | Lor _ _ _ => fun xy => Z.lor (fst xy) (snd xy) | Opp _ _ => fun x => Z.opp x + | Zselect _ _ _ _ => fun ctf => let '(c, t, f) := eta3 ctf in Z.zselect c t f + | AddWithCarry _ _ _ _ => fun cxy => let '(c, x, y) := eta3 cxy in Z.add_with_carry c x y + | AddWithGetCarry bitwidth _ _ _ _ _ => fun cxy => let '(c, x, y) := eta3 cxy in Z.add_with_get_carry bitwidth c x y end%Z. Definition interp_op src dst (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst |