Module OldInequalities

Function ge


pub  fn ge
[
$S,
@D,
N : Nat
]
(   x : uint[N] $S @D,
   y : uint[N] $S @D,
   bw : uint[18446744073709551616] $pre @public
) 
-> bool[N] $S @D

where

  Field[N]

Test if the number in the first argument is greater than or equal to the number in the second argument. The third argument provides a common length of the binary representation that is used if the numbers are in $post @prover.

Function ge’


pub  fn ge’
[
$S,
@D,
N : Nat
]
(   x : list[bool[N] $S @D] $pre @public,
   y : list[bool[N] $S @D] $pre @public,
   bw : uint[18446744073709551616] $pre @public
) 
-> bool[N] $S @D

where

  Field[N]

Test if the number with little-endian binary representation in the first argument is greater than or equal to the number with little-endian binary representation in the second argument. The third argument provides the common length of the representations (the actual lists can be longer but the remaining parts are not read).

Function gt


pub  fn gt
[
$S,
@D,
N : Nat
]
(   x : uint[N] $S @D,
   y : uint[N] $S @D,
   bw : uint[18446744073709551616] $pre @public
) 
-> bool[N] $S @D

where

  Field[N]

Test if the number in the first argument is greater than the number in the second argument. The third argument provides a common length of the binary representation that is used if the numbers are in $post @prover.

Function gt’


pub  fn gt’
[
$S,
@D,
N : Nat
]
(   x : list[bool[N] $S @D] $pre @public,
   y : list[bool[N] $S @D] $pre @public,
   bw : uint[18446744073709551616] $pre @public
) 
-> bool[N] $S @D

where

  Field[N]

Test if the number with little-endian binary representation in the first argument is greater than the number with little-endian binary representation in the second argument. The third argument provides the common length of the representations (the actual lists can be longer but the remaining parts are not read).

Function le


pub  fn le
[
$S,
@D,
N : Nat
]
(   x : uint[N] $S @D,
   y : uint[N] $S @D,
   bw : uint[18446744073709551616] $pre @public
) 
-> bool[N] $S @D

where

  Field[N]

Test if the number in the first argument is less than or equal to the number in the second argument. The third argument provides a common length of the binary representation that is used if the numbers are in $post @prover.

Function le’


pub  fn le’
[
$S,
@D,
N : Nat
]
(   x : list[bool[N] $S @D] $pre @public,
   y : list[bool[N] $S @D] $pre @public,
   bw : uint[18446744073709551616] $pre @public
) 
-> bool[N] $S @D

where

  Field[N]

Test if the number with little-endian binary representation in the first argument is less than or equal to the number with little-endian binary representation in the second argument. The third argument provides the common length of the representations (the actual lists can be longer but the remaining parts are not read).

Function less_than


pub  fn less_than
[
$S,
@D,
N : Nat
]
(   xb : list[bool[N] $S @D] $pre @public,
   yb : list[bool[N] $S @D] $pre @public,
   bw : uint[18446744073709551616] $pre @public
) 
-> bool[N] $S @D

where

  Field[N]

Test if the number with little-endian binary representation in the first argument is less than the number with little-endian binary representation in the second argument. The third argument provides the common length of the representations (the actual lists can be longer but the remaining parts are not read).

Function lt


unchecked eff * -> * -> * -> * ! <$S>

pub  fn lt
[
$S,
@D,
N : Nat
]
(   x : uint[N] $S @D,
   y : uint[N] $S @D,
   bw : uint[18446744073709551616] $pre @public
) 
-> bool[N] $S @D

where

  Field[N]

Test if the number in the first argument is less than the number in the second argument. The third argument provides a common length of the binary representation that is used if the numbers are in $post @prover.

Function lt’


pub  fn lt’
[
$S,
@D,
N : Nat
]
(   x : list[bool[N] $S @D] $pre @public,
   y : list[bool[N] $S @D] $pre @public,
   bw : uint[18446744073709551616] $pre @public
) 
-> bool[N] $S @D

where

  Field[N]

Test if the number with little-endian binary representation in the first argument is less than the number with little-endian binary representation in the second argument. The third argument provides the common length of the representations (the actual lists can be longer but the remaining parts are not read). Synonym of less_than.