diff options
10 files changed, 185 insertions, 181 deletions
diff --git a/src/Compilers/Z/CNotations.v b/src/Compilers/Z/CNotations.v index 0c4838fdf..7262951b2 100644 --- a/src/Compilers/Z/CNotations.v +++ b/src/Compilers/Z/CNotations.v @@ -63,6 +63,8 @@ Reserved Notation "'mulx_u32ℤ' ( a , b )" (format "'mulx_u32ℤ' ( a , b )"). Reserved Notation "'mulx_u64ℤ' ( a , b )" (format "'mulx_u64ℤ' ( a , b )"). Reserved Notation "'mulx_u128ℤ' ( a , b )" (format "'mulx_u128ℤ' ( a , b )"). +Reserved Notation "'cmovznz' ( v , a , b )" (format "'cmovznz' ( v , a , b )"). +Reserved Notation "'cmovznzℤ' ( v , a , b )" (format "'cmovznzℤ' ( v , a , b )"). (* python: << #!/usr/bin/env python @@ -134,6 +136,8 @@ Reserved Notation "'mulx_u32ℤ' ( a , b )" (format "'mulx_u32ℤ' ( a , b )"). Reserved Notation "'mulx_u64ℤ' ( a , b )" (format "'mulx_u64ℤ' ( a , b )"). Reserved Notation "'mulx_u128ℤ' ( a , b )" (format "'mulx_u128ℤ' ( a , b )"). +Reserved Notation "'cmovznz' ( v , a , b )" (format "'cmovznz' ( v , a , b )"). +Reserved Notation "'cmovznzℤ' ( v , a , b )" (format "'cmovznzℤ' ( v , a , b )"). (""" + r"""* python: <<""") @@ -263,8 +267,8 @@ for v0 in (False, True): tes = ('v' if not v0 else '(Var v)') lhs = ('x' if not v1 else '(Var x)') rhs = ('y' if not v2 else '(Var y)') - print('Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair %s %s) %s)).' % (tes, lhs, rhs)) - print('Notation "v == 0 ?ℤ x : y" := (Op (Zselect _ _ _ TZ) (Pair (Pair %s %s) %s)).' % (tes, lhs, rhs)) + print('Notation "\'cmovznz\' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair %s %s) %s)).' % (tes, lhs, rhs)) + print('Notation "\'cmovznzℤ\' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair %s %s) %s)).' % (tes, lhs, rhs)) for lgwordsz in range(0, len(types)): for v0 in (False, True): for v1 in (False, True): @@ -272,8 +276,8 @@ for lgwordsz in range(0, len(types)): tes = ('v' if not v0 else '(Var v)') lhs = ('x' if not v1 else '(Var x)') rhs = ('y' if not v2 else '(Var y)') - print('Notation "\'(%s)\' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord %d)) (Pair (Pair %s %s) %s)) (at level 40, x at level 10, y at level 10).' % (types[lgwordsz], lgwordsz, tes, lhs, rhs)) - print('Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord %d) (TWord %d) (TWord %d)) (Pair (Pair %s %s) %s)).' % (lgwordsz, lgwordsz, lgwordsz, tes, lhs, rhs)) + print('Notation "\'(%s)\' \'cmovznz\' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord %d)) (Pair (Pair %s %s) %s)) (format "\'(%s)\' \'cmovznz\' ( v , x , y )").' % (types[lgwordsz], lgwordsz, tes, lhs, rhs, types[lgwordsz])) + print('Notation "\'cmovznz\' ( v , x , y )" := (Op (Zselect _ (TWord %d) (TWord %d) (TWord %d)) (Pair (Pair %s %s) %s)).' % (lgwordsz, lgwordsz, lgwordsz, tes, lhs, rhs)) for opn, op in (('addcarryx', 'AddWithGetCarry'), ('subborrow', 'SubWithGetBorrow')): for wordsz in (32, 64, 128, 51): lgwordsz = log2_up(wordsz) @@ -1690,166 +1694,166 @@ Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) ( Notation "x >> y" := (Op (Shr (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)). Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 30). Notation "x >> y" := (Op (Shr (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))). -Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair v x) y)). -Notation "v == 0 ?ℤ x : y" := (Op (Zselect _ _ _ TZ) (Pair (Pair v x) y)). -Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair v x) (Var y))). -Notation "v == 0 ?ℤ x : y" := (Op (Zselect _ _ _ TZ) (Pair (Pair v x) (Var y))). -Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair v (Var x)) y)). -Notation "v == 0 ?ℤ x : y" := (Op (Zselect _ _ _ TZ) (Pair (Pair v (Var x)) y)). -Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair v (Var x)) (Var y))). -Notation "v == 0 ?ℤ x : y" := (Op (Zselect _ _ _ TZ) (Pair (Pair v (Var x)) (Var y))). -Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) x) y)). -Notation "v == 0 ?ℤ x : y" := (Op (Zselect _ _ _ TZ) (Pair (Pair (Var v) x) y)). -Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) x) (Var y))). -Notation "v == 0 ?ℤ x : y" := (Op (Zselect _ _ _ TZ) (Pair (Pair (Var v) x) (Var y))). -Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) (Var x)) y)). -Notation "v == 0 ?ℤ x : y" := (Op (Zselect _ _ _ TZ) (Pair (Pair (Var v) (Var x)) y)). -Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "v == 0 ?ℤ x : y" := (Op (Zselect _ _ _ TZ) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v x) y)). -Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v x) (Var y))). -Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v (Var x)) y)). -Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) x) y)). -Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v x) y)). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v x) (Var y))). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v (Var x)) y)). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) x) y)). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v x) y)). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v x) (Var y))). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v (Var x)) y)). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) x) y)). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v x) y)). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v x) (Var y))). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v (Var x)) y)). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) x) y)). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v x) y)). -Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v x) (Var y))). -Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v (Var x)) y)). -Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) x) y)). -Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v x) y)). -Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v x) (Var y))). -Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v (Var x)) y)). -Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) x) y)). -Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v x) y)). -Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v x) (Var y))). -Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v (Var x)) y)). -Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) x) y)). -Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v x) y)). -Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v x) (Var y))). -Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v (Var x)) y)). -Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) x) y)). -Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) (Var x)) (Var y))). -Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v x) y)). -Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v x) (Var y))). -Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v (Var x)) y)). -Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v (Var x)) (Var y))). -Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) x) y)). -Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) x) (Var y))). -Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) (Var x)) y)). -Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). -Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair v x) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair v x) y)). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair v x) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair v x) (Var y))). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair v (Var x)) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair v (Var x)) y)). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair v (Var x)) (Var y))). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) x) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair (Var v) x) y)). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair (Var v) x) (Var y))). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair (Var v) (Var x)) y)). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'cmovznzℤ' ( v , x , y )" := (Op (Zselect _ _ _ TZ) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v x) y)) (format "'(bool)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v x) y)). +Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v x) (Var y))) (format "'(bool)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v x) (Var y))). +Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v (Var x)) y)) (format "'(bool)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v (Var x)) y)). +Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v (Var x)) (Var y))) (format "'(bool)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) x) y)) (format "'(bool)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) x) y)). +Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) x) (Var y))) (format "'(bool)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) (Var x)) y)) (format "'(bool)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(bool)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(bool)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v x) y)). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v x) (Var y))). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v (Var x)) y)). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) x) y)). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v x) y)). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v x) (Var y))). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v (Var x)) y)). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) x) y)). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v x) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v x) y)). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v x) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v x) (Var y))). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v (Var x)) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v (Var x)) y)). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) x) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) x) y)). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint8_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint8_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v x) y)) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v x) y)). +Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v x) (Var y))) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v x) (Var y))). +Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v (Var x)) y)) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v (Var x)) y)). +Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) x) y)) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) x) y)). +Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint16_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint16_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v x) y)) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v x) y)). +Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v x) (Var y))) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v x) (Var y))). +Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v (Var x)) y)) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v (Var x)) y)). +Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) x) y)) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) x) y)). +Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint32_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint32_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v x) y)) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v x) y)). +Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v x) (Var y))) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v x) (Var y))). +Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v (Var x)) y)) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v (Var x)) y)). +Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) x) y)) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) x) y)). +Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint64_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint64_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v x) y)) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v x) y)). +Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v x) (Var y))) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v x) (Var y))). +Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v (Var x)) y)) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v (Var x)) y)). +Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) x) y)) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) x) y)). +Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint128_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint128_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v x) y)) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v x) y)). +Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v x) (Var y))) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v x) (Var y))). +Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v (Var x)) y)) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v (Var x)) y)). +Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v (Var x)) (Var y))) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) x) y)) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) x) y)). +Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) x) (Var y))) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) (Var x)) y)) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint256_t)' 'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) (Var x)) (Var y))) (format "'(uint256_t)' 'cmovznz' ( v , x , y )"). +Notation "'cmovznz' ( v , x , y )" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) (Var x)) (Var y))). Notation "'addcarryx_u32' ( c , a , b )" := (Op (AddWithGetCarry 32 (TWord 0) (TWord 5) (TWord 5) (TWord 5) (TWord 0)) (Pair (Pair c a) b)). Notation "'addcarryx_u32' ( c , a , b )" := (Op (AddWithGetCarry 32 (TWord 0) (TWord 0) (TWord 5) (TWord 5) (TWord 0)) (Pair (Pair c a) b)). Notation "'addcarryx_u32' ( c , a , b )" := (Op (AddWithGetCarry 32 (TWord 0) (TWord 5) (TWord 0) (TWord 5) (TWord 0)) (Pair (Pair c a) b)). diff --git a/src/Specific/IntegrationTestFreezeDisplay.log b/src/Specific/IntegrationTestFreezeDisplay.log index 471c997c7..9cf04d26f 100644 --- a/src/Specific/IntegrationTestFreezeDisplay.log +++ b/src/Specific/IntegrationTestFreezeDisplay.log @@ -7,7 +7,7 @@ Interp-η uint64_t x16, uint8_t x17 = subborrow_u51(x14, x6, 0x7ffffffffffff); uint64_t x19, uint8_t x20 = subborrow_u51(x17, x8, 0x7ffffffffffff); uint64_t x22, uint8_t x23 = subborrow_u51(x20, x7, 0x7ffffffffffff); - uint64_t x24 = (uint64_t) (x23 == 0 ? 0x0 : 0xffffffffffffffffL); + uint64_t x24 = (uint64_t)cmovznz(x23, 0x0, 0xffffffffffffffffL); uint64_t x25 = x24 & 0x7ffffffffffed; uint64_t x27, uint8_t x28 = addcarryx_u51(0x0, x10, x25); uint64_t x29 = x24 & 0x7ffffffffffff; diff --git a/src/Specific/IntegrationTestMontgomeryP256_128Display.log b/src/Specific/IntegrationTestMontgomeryP256_128Display.log index 5a9182d47..260a1ff5a 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128Display.log +++ b/src/Specific/IntegrationTestMontgomeryP256_128Display.log @@ -33,8 +33,8 @@ Interp-η uint128_t x91, uint8_t x92 = subborrow_u128(0x0, x84, 0xffffffffffffffffffffffffL); uint128_t x94, uint8_t x95 = subborrow_u128(x92, x87, 0xffffffff000000010000000000000000L); uint128_t _, uint8_t x98 = subborrow_u128(x95, x89, 0x0); - uint128_t x99 = x98 == 0 ? x94 : x87; - uint128_t x100 = x98 == 0 ? x91 : x84; + uint128_t x99 = cmovznz(x98, x94, x87); + uint128_t x100 = cmovznz(x98, x91, x84); return (x99, x100)) (x, x0)%core : word128 * word128 → word128 * word128 → ReturnType (uint128_t * uint128_t) diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.log b/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.log index 3c1716a73..ea6db527b 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.log +++ b/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.log @@ -7,8 +7,8 @@ Interp-η uint128_t x15, uint8_t x16 = subborrow_u128(0x0, x9, 0xffffffffffffffffffffffffL); uint128_t x18, uint8_t x19 = subborrow_u128(x16, x12, 0xffffffff000000010000000000000000L); uint128_t _, uint8_t x22 = subborrow_u128(x19, x13, 0x0); - uint128_t x23 = x22 == 0 ? x18 : x12; - uint128_t x24 = x22 == 0 ? x15 : x9; + uint128_t x23 = cmovznz(x22, x18, x12); + uint128_t x24 = cmovznz(x22, x15, x9); return (x23, x24)) (x, x0)%core : word128 * word128 → word128 * word128 → ReturnType (uint128_t * uint128_t) diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.log b/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.log index 94b63495c..76ead3f3d 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.log +++ b/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.log @@ -4,7 +4,7 @@ Interp-η λ '(x1, x2)%core, uint128_t x4, uint8_t x5 = subborrow_u128(0x0, 0x0, x2); uint128_t x7, uint8_t x8 = subborrow_u128(x5, 0x0, x1); - uint128_t x9 = (uint128_t) (x8 == 0 ? 0x0 : 0xffffffffffffffffffffffffffffffffL); + uint128_t x9 = (uint128_t)cmovznz(x8, 0x0, 0xffffffffffffffffffffffffffffffffL); uint128_t x10 = x9 & 0xffffffffffffffffffffffffL; uint128_t x12, uint8_t x13 = addcarryx_u128(0x0, x4, x10); uint128_t x14 = x9 & 0xffffffff000000010000000000000000L; diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.log b/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.log index 444680769..39885afbc 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.log +++ b/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.log @@ -4,7 +4,7 @@ Interp-η λ '(x4, x5, (x6, x7))%core, uint128_t x9, uint8_t x10 = subborrow_u128(0x0, x5, x7); uint128_t x12, uint8_t x13 = subborrow_u128(x10, x4, x6); - uint128_t x14 = (uint128_t) (x13 == 0 ? 0x0 : 0xffffffffffffffffffffffffffffffffL); + uint128_t x14 = (uint128_t)cmovznz(x13, 0x0, 0xffffffffffffffffffffffffffffffffL); uint128_t x15 = x14 & 0xffffffffffffffffffffffffL; uint128_t x17, uint8_t x18 = addcarryx_u128(0x0, x9, x15); uint128_t x19 = x14 & 0xffffffff000000010000000000000000L; diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256Display.log b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256Display.log index 1dc1b7ba3..982d44aaf 100644 --- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256Display.log +++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256Display.log @@ -105,10 +105,10 @@ Interp-η uint64_t x311, uint8_t x312 = subborrow_u64(x309, x298, 0x0); uint64_t x314, uint8_t x315 = subborrow_u64(x312, x301, 0xffffffff00000001L); uint64_t _, uint8_t x318 = subborrow_u64(x315, x303, 0x0); - uint64_t x319 = x318 == 0 ? x314 : x301; - uint64_t x320 = x318 == 0 ? x311 : x298; - uint64_t x321 = x318 == 0 ? x308 : x295; - uint64_t x322 = x318 == 0 ? x305 : x292; + uint64_t x319 = cmovznz(x318, x314, x301); + uint64_t x320 = cmovznz(x318, x311, x298); + uint64_t x321 = cmovznz(x318, x308, x295); + uint64_t x322 = cmovznz(x318, x305, x292); return (x319, x320, x321, x322)) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_AddDisplay.log b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_AddDisplay.log index e6498cf83..ba7a2f50d 100644 --- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_AddDisplay.log +++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_AddDisplay.log @@ -11,10 +11,10 @@ Interp-η uint64_t x35, uint8_t x36 = subborrow_u64(x33, x23, 0x0); uint64_t x38, uint8_t x39 = subborrow_u64(x36, x26, 0xffffffff00000001L); uint64_t _, uint8_t x42 = subborrow_u64(x39, x27, 0x0); - uint64_t x43 = x42 == 0 ? x38 : x26; - uint64_t x44 = x42 == 0 ? x35 : x23; - uint64_t x45 = x42 == 0 ? x32 : x20; - uint64_t x46 = x42 == 0 ? x29 : x17; + uint64_t x43 = cmovznz(x42, x38, x26); + uint64_t x44 = cmovznz(x42, x35, x23); + uint64_t x45 = cmovznz(x42, x32, x20); + uint64_t x46 = cmovznz(x42, x29, x17); return (x43, x44, x45, x46)) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_OppDisplay.log b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_OppDisplay.log index 891c0a611..211b2b863 100644 --- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_OppDisplay.log +++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_OppDisplay.log @@ -6,7 +6,7 @@ Interp-η uint64_t x11, uint8_t x12 = subborrow_u64(x9, 0x0, x4); uint64_t x14, uint8_t x15 = subborrow_u64(x12, 0x0, x6); uint64_t x17, uint8_t x18 = subborrow_u64(x15, 0x0, x5); - uint64_t x19 = (uint64_t) (x18 == 0 ? 0x0 : 0xffffffffffffffffL); + uint64_t x19 = (uint64_t)cmovznz(x18, 0x0, 0xffffffffffffffffL); uint64_t x20 = x19 & 0xffffffffffffffffL; uint64_t x22, uint8_t x23 = addcarryx_u64(0x0, x8, x20); uint64_t x24 = x19 & 0xffffffff; diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_SubDisplay.log b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_SubDisplay.log index fadb63620..eb4289fd2 100644 --- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_SubDisplay.log +++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_SubDisplay.log @@ -6,7 +6,7 @@ Interp-η uint64_t x20, uint8_t x21 = subborrow_u64(x18, x7, x13); uint64_t x23, uint8_t x24 = subborrow_u64(x21, x9, x15); uint64_t x26, uint8_t x27 = subborrow_u64(x24, x8, x14); - uint64_t x28 = (uint64_t) (x27 == 0 ? 0x0 : 0xffffffffffffffffL); + uint64_t x28 = (uint64_t)cmovznz(x27, 0x0, 0xffffffffffffffffL); uint64_t x29 = x28 & 0xffffffffffffffffL; uint64_t x31, uint8_t x32 = addcarryx_u64(0x0, x17, x29); uint64_t x33 = x28 & 0xffffffff; |