diff options
author | Jade Philipoom <jadep@google.com> | 2018-04-20 10:20:05 +0200 |
---|---|---|
committer | jadephilipoom <jade.philipoom@gmail.com> | 2018-04-30 04:20:04 -0400 |
commit | 3411d5d537c88ab134245f1d475046a6a13836b7 (patch) | |
tree | 0c786feb3e24451e935ac918df8d03bcd9bf7b13 /src/Experiments | |
parent | c95a7ed3892bed4e86500a5a7339181ce2b6d00c (diff) |
Fix bounds analysis for saturated ops and remove unneeded comment
Diffstat (limited to 'src/Experiments')
-rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 34 |
1 files changed, 13 insertions, 21 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 98d445e6e..a4604ce39 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -4762,7 +4762,9 @@ Module Compilers. | Some x, Some y => type.option.Some (t:=(type.Z*type.Z)%ctype) - (ZRange.split_bounds (ZRange.four_corners BinInt.Z.sub x y) split_at) + (let b := ZRange.split_bounds (ZRange.four_corners BinInt.Z.sub x y) split_at in + (* N.B. sub_get_borrow returns - ((x - y) / split_at) as the borrow, so we need to negate *) + (fst b, ZRange.opp (snd b))) | Some _, None | None, Some _ | None, None => type.option.None end | ident.Z_sub_with_get_borrow_concrete split_at @@ -4771,9 +4773,9 @@ Module Compilers. | Some x, Some y, Some z => type.option.Some (t:=(type.Z*type.Z)%ctype) - (ZRange.split_bounds - (ZRange.eight_corners (fun x y z => (x - y - z)%Z) x y z) - split_at) + (let b := ZRange.split_bounds (ZRange.eight_corners (fun x y z => (x - y - z)%Z) x y z) split_at in + (* N.B. sub_get_borrow returns - ((x - y) / split_at) as the borrow, so we need to negate *) + (fst b, ZRange.opp (snd b))) | _, _, _ => type.option.None end | ident.Z_zselect @@ -8290,19 +8292,6 @@ Module Barrett256. Definition M := (2^256-2^224+2^192+2^96-1). Definition machine_wordsize := 256. - (* TODO : why does this not bounds check? - Let F := Some r[0 ~> 115792089237316195423570985008687907853269984665640564039457584007913129639935]%zrange. - Eval vm_compute in ( - partial.bounds.expr.extract' (fun t : type => id) - (λ x : partial.data (type.type_primitive type.Z * type.type_primitive type.Z), - ident.Z.cast2 - (r[0 ~> 115792089237316195423570985008687907853269984665640564039457584007913129639935]%zrange, - r[0 ~> 1]%zrange)%core @@ - (ident.Z.add_get_carry_concrete - 115792089237316195423570985008687907853269984665640564039457584007913129639936 @@ - (ident.Z.cast r[0 ~> 115792089237316195423570985008687907853269984665640564039457584007913129639935] @@ - (ident.fst @@ (Var x)), ident.primitive (t:=type.Z) 26959946667150639793205513449348445388433292963828203772348655992835 @@ TT ))) (F, F)). - *) Derive barrett_red256 SuchThat (BarrettReduction.rbarrett_red_correctT M machine_wordsize barrett_red256) As barrett_red256_correct. @@ -8314,6 +8303,7 @@ 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 *) (* 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 @@ -8356,8 +8346,8 @@ barrett_red256 = fun var : type -> Type => λ x : var (type.type_primitive type. expr_let x37 := ADDC_256 (x36₂, x27, x30) in expr_let x38 := ADD_256 (x33, x36₁) in expr_let x39 := ADDC_256 (x38₂, x32, x37₁) in - expr_let x40 := ADD_256 (Z.opp @@ (fst @@ x38), x₁) in - expr_let x41 := ADDC_256 (x40₂, Z.opp @@ (fst @@ x39), x₂) in + expr_let x40 := Z.add_get_carry_concrete 115792089237316195423570985008687907853269984665640564039457584007913129639936 @@ (Z.opp @@ (fst @@ x38), x₁) in + expr_let x41 := Z.add_with_get_carry_concrete 115792089237316195423570985008687907853269984665640564039457584007913129639936 @@ (x40₂, Z.opp @@ (fst @@ x39), x₂) in expr_let x42 := SELL (x41₁, 0, 115792089210356248762697446949407573530086143415290314195533631308867097853951) in expr_let x43 := Z.cast uint256 @@ (fst @@ SUB_256 (x40₁, x42)) in ADDM (x43, 0, 115792089210356248762697446949407573530086143415290314195533631308867097853951) @@ -8744,8 +8734,10 @@ c.Add256($x36, $x34, $x35); c.Addc256($x37, $x36_hi, $x27, $x30); c.Add256($x38, $x33, $x36_lo); c.Addc256($x39, $x38_hi, $x32, $x37_lo); -c.Add256($x40, Z.opp @@ $x38_lo, $x_lo); -c.Addc256($x41, $x40_hi, Z.opp @@ $x39_lo, $x_hi); +expr_let x40 := Z.add_get_carry_concrete 115792089237316195423570985008687907853269984665640564039457584007913129639936 @@ + (Z.opp @@ $x38_lo, $x_lo) in +expr_let x41 := Z.add_with_get_carry_concrete 115792089237316195423570985008687907853269984665640564039457584007913129639936 @@ + ($x40_hi, Z.opp @@ $x39_lo, $x_hi) in c.Sell($x42, $x41_lo, RegZero, RegMod); c.Sub($x43, $x40_lo, $x42); c.AddM($ret, $x43, RegZero, RegMod); |