-
Notifications
You must be signed in to change notification settings - Fork 26
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
19 changed files
with
12,656 additions
and
32 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,178 @@ | ||
| package bign | ||
|
|
||
| import ( | ||
| "errors" | ||
| "math/big" | ||
| "crypto/elliptic" | ||
| ) | ||
|
|
||
| // bignPoint is a generic constraint for the bign Point types. | ||
| type bignPoint[T any] interface { | ||
| Bytes() []byte | ||
| SetBytes([]byte) (T, error) | ||
| Add(T, T) T | ||
| Double(T) T | ||
| ScalarMult(T, []byte) (T, error) | ||
| ScalarBaseMult([]byte) (T, error) | ||
| } | ||
|
|
||
| // bignCurve is a Curve implementation based on a bign Point. | ||
| type bignCurve[Point bignPoint[Point]] struct { | ||
| newPoint func() Point | ||
| params *elliptic.CurveParams | ||
| } | ||
|
|
||
| func (curve *bignCurve[Point]) Params() *elliptic.CurveParams { | ||
| return curve.params | ||
| } | ||
|
|
||
| func (curve *bignCurve[Point]) IsOnCurve(x, y *big.Int) bool { | ||
| // IsOnCurve is documented to reject (0, 0), the conventional point at | ||
| // infinity, which however is accepted by pointFromAffine. | ||
| if x.Sign() == 0 && y.Sign() == 0 { | ||
| return false | ||
| } | ||
| _, err := curve.pointFromAffine(x, y) | ||
| return err == nil | ||
| } | ||
|
|
||
| func (curve *bignCurve[Point]) pointFromAffine(x, y *big.Int) (p Point, err error) { | ||
| // (0, 0) is by convention the point at infinity, which can't be represented | ||
| // in affine coordinates. See Issue 37294. | ||
| if x.Sign() == 0 && y.Sign() == 0 { | ||
| return curve.newPoint(), nil | ||
| } | ||
| // Reject values that would not get correctly encoded. | ||
| if x.Sign() < 0 || y.Sign() < 0 { | ||
| return p, errors.New("negative coordinate") | ||
| } | ||
| if x.BitLen() > curve.params.BitSize || y.BitLen() > curve.params.BitSize { | ||
| return p, errors.New("overflowing coordinate") | ||
| } | ||
| // Encode the coordinates and let SetBytes reject invalid points. | ||
| byteLen := (curve.params.BitSize + 7) / 8 | ||
| buf := make([]byte, 1+2*byteLen) | ||
| buf[0] = 4 // uncompressed point | ||
| x.FillBytes(buf[1 : 1+byteLen]) | ||
| y.FillBytes(buf[1+byteLen : 1+2*byteLen]) | ||
| return curve.newPoint().SetBytes(buf) | ||
| } | ||
|
|
||
| func (curve *bignCurve[Point]) pointToAffine(p Point) (x, y *big.Int) { | ||
| out := p.Bytes() | ||
| if len(out) == 1 && out[0] == 0 { | ||
| // This is the encoding of the point at infinity, which the affine | ||
| // coordinates API represents as (0, 0) by convention. | ||
| return new(big.Int), new(big.Int) | ||
| } | ||
| byteLen := (curve.params.BitSize + 7) / 8 | ||
| x = new(big.Int).SetBytes(out[1 : 1+byteLen]) | ||
| y = new(big.Int).SetBytes(out[1+byteLen:]) | ||
| return x, y | ||
| } | ||
|
|
||
| func (curve *bignCurve[Point]) Add(x1, y1, x2, y2 *big.Int) (*big.Int, *big.Int) { | ||
| p1, err := curve.pointFromAffine(x1, y1) | ||
| if err != nil { | ||
| panic("crypto/elliptic: Add was called on an invalid point") | ||
| } | ||
| p2, err := curve.pointFromAffine(x2, y2) | ||
| if err != nil { | ||
| panic("crypto/elliptic: Add was called on an invalid point") | ||
| } | ||
| return curve.pointToAffine(p1.Add(p1, p2)) | ||
| } | ||
|
|
||
| func (curve *bignCurve[Point]) Double(x1, y1 *big.Int) (*big.Int, *big.Int) { | ||
| p, err := curve.pointFromAffine(x1, y1) | ||
| if err != nil { | ||
| panic("crypto/elliptic: Double was called on an invalid point") | ||
| } | ||
| return curve.pointToAffine(p.Double(p)) | ||
| } | ||
|
|
||
| // normalizeScalar brings the scalar within the byte size of the order of the | ||
| // curve, as expected by the bign scalar multiplication functions. | ||
| func (curve *bignCurve[Point]) normalizeScalar(scalar []byte) []byte { | ||
| byteSize := (curve.params.N.BitLen() + 7) / 8 | ||
| if len(scalar) == byteSize { | ||
| return scalar | ||
| } | ||
| s := new(big.Int).SetBytes(scalar) | ||
| if len(scalar) > byteSize { | ||
| s.Mod(s, curve.params.N) | ||
| } | ||
| out := make([]byte, byteSize) | ||
| return s.FillBytes(out) | ||
| } | ||
|
|
||
| func (curve *bignCurve[Point]) ScalarMult(Bx, By *big.Int, scalar []byte) (*big.Int, *big.Int) { | ||
| p, err := curve.pointFromAffine(Bx, By) | ||
| if err != nil { | ||
| panic("crypto/elliptic: ScalarMult was called on an invalid point") | ||
| } | ||
| scalar = curve.normalizeScalar(scalar) | ||
| p, err = p.ScalarMult(p, scalar) | ||
| if err != nil { | ||
| panic("crypto/elliptic: bign rejected normalized scalar") | ||
| } | ||
| return curve.pointToAffine(p) | ||
| } | ||
|
|
||
| func (curve *bignCurve[Point]) ScalarBaseMult(scalar []byte) (*big.Int, *big.Int) { | ||
| scalar = curve.normalizeScalar(scalar) | ||
| p, err := curve.newPoint().ScalarBaseMult(scalar) | ||
| if err != nil { | ||
| panic("crypto/elliptic: bign rejected normalized scalar") | ||
| } | ||
| return curve.pointToAffine(p) | ||
| } | ||
|
|
||
| // CombinedMult returns [s1]G + [s2]P where G is the generator. It's used | ||
| // through an interface upgrade in crypto/ecdsa. | ||
| func (curve *bignCurve[Point]) CombinedMult(Px, Py *big.Int, s1, s2 []byte) (x, y *big.Int) { | ||
| s1 = curve.normalizeScalar(s1) | ||
| q, err := curve.newPoint().ScalarBaseMult(s1) | ||
| if err != nil { | ||
| panic("crypto/elliptic: bign rejected normalized scalar") | ||
| } | ||
| p, err := curve.pointFromAffine(Px, Py) | ||
| if err != nil { | ||
| panic("crypto/elliptic: CombinedMult was called on an invalid point") | ||
| } | ||
| s2 = curve.normalizeScalar(s2) | ||
| p, err = p.ScalarMult(p, s2) | ||
| if err != nil { | ||
| panic("crypto/elliptic: bign rejected normalized scalar") | ||
| } | ||
| return curve.pointToAffine(p.Add(p, q)) | ||
| } | ||
|
|
||
| func (curve *bignCurve[Point]) Unmarshal(data []byte) (x, y *big.Int) { | ||
| if len(data) == 0 || data[0] != 4 { | ||
| return nil, nil | ||
| } | ||
| // Use SetBytes to check that data encodes a valid point. | ||
| _, err := curve.newPoint().SetBytes(data) | ||
| if err != nil { | ||
| return nil, nil | ||
| } | ||
| // We don't use pointToAffine because it involves an expensive field | ||
| // inversion to convert from Jacobian to affine coordinates, which we | ||
| // already have. | ||
| byteLen := (curve.params.BitSize + 7) / 8 | ||
| x = new(big.Int).SetBytes(data[1 : 1+byteLen]) | ||
| y = new(big.Int).SetBytes(data[1+byteLen:]) | ||
| return x, y | ||
| } | ||
|
|
||
| func (curve *bignCurve[Point]) UnmarshalCompressed(data []byte) (x, y *big.Int) { | ||
| if len(data) == 0 || (data[0] != 2 && data[0] != 3) { | ||
| return nil, nil | ||
| } | ||
| p, err := curve.newPoint().SetBytes(data) | ||
| if err != nil { | ||
| return nil, nil | ||
| } | ||
| return curve.pointToAffine(p) | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,11 @@ | ||
| # Copyright 2021 The Go Authors. All rights reserved. | ||
| # Use of this source code is governed by a BSD-style | ||
| # license that can be found in the LICENSE file. | ||
|
|
||
| FROM coqorg/coq:8.20.0 | ||
|
|
||
| RUN git clone https://github.com/mit-plv/fiat-crypto && cd fiat-crypto && \ | ||
| git submodule update --init --recursive | ||
| RUN cd fiat-crypto && eval $(opam env) && make standalone-ocaml SKIP_BEDROCK2=1 | ||
|
|
||
| ENV PATH /home/coq/fiat-crypto/src/ExtractionOCaml:$PATH |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,34 @@ | ||
| The code in this package was autogenerated by the fiat-crypto project | ||
| at version v0.0.9 from a formally verified model, and by the addchain | ||
| project at a recent tip version. | ||
|
|
||
| docker build -t fiat-crypto:v0.0.9 . | ||
| go install github.com/mmcloughlin/addchain/cmd/addchain@v0.4.0 | ||
| go run generate.go | ||
|
|
||
| fiat-crypto code comes under the following license. | ||
|
|
||
| Copyright (c) 2015-2020 The fiat-crypto Authors. All rights reserved. | ||
|
|
||
| Redistribution and use in source and binary forms, with or without | ||
| modification, are permitted provided that the following conditions are | ||
| met: | ||
|
|
||
| 1. Redistributions of source code must retain the above copyright | ||
| notice, this list of conditions and the following disclaimer. | ||
|
|
||
| THIS SOFTWARE IS PROVIDED BY the fiat-crypto authors "AS IS" | ||
| AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, | ||
| THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR | ||
| PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL Berkeley Software Design, | ||
| Inc. BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, | ||
| EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, | ||
| PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR | ||
| PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF | ||
| LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING | ||
| NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS | ||
| SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. | ||
|
|
||
| The authors are listed at | ||
|
|
||
| https://github.com/mit-plv/fiat-crypto/blob/master/AUTHORS |
Oops, something went wrong.