Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Apt
Acre
Milawa
Smtlink
Abnf
Vwsim
Isar
Wp-gen
Dimacs-reader
Pfcs
Legacy-defrstobj
Aleobft
Proof-checker-array
Soft
Farray
Rp-rewriter
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
C
Java
Taspi
Bitcoin
Des
Ethereum
Sha-2
Yul
Zcash
Jubjub
Jubjub-abst
Jubjub-r-pointp
Jubjub-pointp
Jubjub-d
Jubjub-montgomery
Maybe-jubjub-pointp
Jubjub-point->u
Jubjub-q
Jubjub-point->v
Point-on-jubjub-p
Jubjub-rstar-pointp
Jubjub-add
Jubjub-r-properties
Not-jubjub-r-pointp-when-0-ordinate
Jubjub-r-doubling-injectivity
Point-0-m1
Not-jubjub-r-pointp-of-jubjub-r-point-with-neg-ordinate
Not-jubjub-r-pointp-when-lower-order
Jubjub-r-doubling-of-nonzero-is-nonzero
Jubjub-point->u-injective-on-jubjub-r-pointp
Jubjub-point-abscissa-is-not-1
Jubjub-mul
Jubjub-curve
Jubjub-a
Jubjub-neg
Jubjub-r
Jubjub-point-satisfies-curve-equation
Jubjub-h
Jubjub-mul-of-2
*jubjub-l*
Verify-zcash-r1cs
Lift-zcash-r1cs
Pedersen-hash
Zcash-gadgets
Bit/byte/integer-conversions
Constants
Blake2-hash
Randomness-beacon
Proof-checker-itp13
Bigmem
Regex
ACL2-programming-language
Json
X86isa
Jfkr
Equational
Cryptography
Poseidon
Where-do-i-place-my-book
Builtins
Axe
Execloader
Solidity
Leo
Paco
Concurrent-programs
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Jubjub
Jubjub-r-properties
Properties about
jubjub-r-pointp
.
Subtopics
Not-jubjub-r-pointp-when-0-ordinate
A Jubjub point with 0 ordinate is not in
jubjub-r-pointp
.
Jubjub-r-doubling-injectivity
Injectivity of doubling in
jubjub-r-pointp
.
Point-0-m1
The point
(0,-1)
.
Not-jubjub-r-pointp-of-jubjub-r-point-with-neg-ordinate
Negating the ordinate of a point in
jubjub-r-pointp
yields a point that is not in
jubjub-r-pointp
.
Not-jubjub-r-pointp-when-lower-order
If multiplying a non-zero point by a positive integer below
jubjub-r
yields the zero point, the non-zero point is not in
jubjub-r-pointp
.
Jubjub-r-doubling-of-nonzero-is-nonzero
Doubling a non-zero point in
jubjub-r-pointp
yields a non-zero point.
Jubjub-point->u-injective-on-jubjub-r-pointp
jubjub-point->u
is injective in
jubjub-r-pointp
.