diff options
| author |  Jade Philipoom <jadep@google.com> | 2018-04-27 10:35:48 +0200 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2018-04-30 04:20:04 -0400 |
| commit | c1e78a56f5f86f27257c8f79766ceaa9dab18faa (patch) | |
| tree | bc972579a37d17158d6a586f49d39ec02ccc6ae4 /src/Experiments/SimplyTypedArithmetic.v | |
| parent | 3411d5d537c88ab134245f1d475046a6a13836b7 (diff) | |
fix comment
Diffstat (limited to 'src/Experiments/SimplyTypedArithmetic.v')
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 3 |
1 files changed, 2 insertions, 1 deletions
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 |