From c1e78a56f5f86f27257c8f79766ceaa9dab18faa Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Fri, 27 Apr 2018 10:35:48 +0200 Subject: fix comment --- src/Experiments/SimplyTypedArithmetic.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/Experiments/SimplyTypedArithmetic.v') diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index a4604ce39..a6eda9643 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -8303,7 +8303,8 @@ Module Barrett256. Print barrett_red256. (* TODO: the ADD/ADDC instructions containing Z.opp should be translated to SUB/SUBB in partial evaluation *) - (* TODO: it is suspicious that this bounds-checks, given that the carries from the above-mentioned ADD/ADDC instructions could be negative *) + (* Note: the aforementioned ADD/ADDC instructions currently *do* fail to bounds-check, although the pipeline doesn't give an error. + This is why their results are not cast (because the carry has range [-1~>0]). *) (* barrett_red256 = fun var : type -> Type => λ x : var (type.type_primitive type.Z * type.type_primitive type.Z)%ctype, expr_let x0 := SELM (x₂, 0, 26959946667150639793205513449348445388433292963828203772348655992835) in -- cgit v1.2.3