From bbd4c70afe3ae31e96d59abee97e24fe06aaee97 Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 11 Nov 2016 16:06:42 -0500 Subject: Define word version of conditional subtraction --- src/ModularArithmetic/ModularBaseSystemWord.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 src/ModularArithmetic/ModularBaseSystemWord.v (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ModularBaseSystemWord.v b/src/ModularArithmetic/ModularBaseSystemWord.v new file mode 100644 index 000000000..9283bfb30 --- /dev/null +++ b/src/ModularArithmetic/ModularBaseSystemWord.v @@ -0,0 +1,23 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Notations. +Require Import Bedrock.Word. +Local Open Scope Z_scope. + +Section conditional_subtract_modulus. + Context {int_width num_limbs : nat}. + Local Notation limb := (word int_width). + Local Notation digits := (tuple limb num_limbs). + Local Notation zero := (natToWord int_width 0). + Local Notation one := (natToWord int_width 1). + Local Notation "u [ i ]" := (nth_default zero u i). + Context (modulus : digits). + Context (ge_modulusW : digits -> limb) (negW : limb -> limb). + + Definition conditional_subtract_modulusW (us : digits) := + (* [and_term] is all ones if us' is full, so the subtractions subtract q overall. + Otherwise, it's all zeroes, and the subtractions do nothing. *) + map2 (fun x y => wminus x y) us (map (wand (negW (ge_modulusW us))) modulus). + +End conditional_subtract_modulus. \ No newline at end of file -- cgit v1.2.3