//go:build ignore // +build ignore // Code Generation using fiat-crypto // // Download and unpack `ExtractionOCaml-Ubuntu LTS` from // https://github.com/mit-plv/fiat-crypto/suites/3241842351/artifacts/75305272 // // Then run this program specifying the path to the word_by_word_montgomery binary. // $ FIAT_BINARY= go run gen.go // // References: // [1] Erbsen et al. "Simple High-Level Code For Cryptographic Arithmetic – With // Proofs, Without Compromises" https://github.com/mit-plv/fiat-crypto package main import ( "log" "os" "os/exec" "strings" "text/template" ) const ( packName = "ff" headerCIRCL = "Code generated by gen.go using fiat-crypto." ) var ( FIAT_BINARY = "./word_by_word_montgomery" FIAT_PARAMS = []string{ "--output", "{{.Name}}.go", "--lang", "Go", "--package-name", "{{.PackageName}}", "--doc-prepend-header", "{{.Header}}", "--package-case", "lowerCamelCase", "--public-function-case", "lowerCamelCase", "--public-type-case", "lowerCamelCase", "--doc-newline-before-package-declaration", "--no-primitives", "--widen-carry", "--no-field-element-typedefs", "--relax-primitive-carry-to-bitwidth", "64", "{{.Prefix}}", "64", "{{.Prime}}", "add", "sub", "mul", "square", } ) var fields = []struct{ Prefix, Name, Prime, Header, PackageName string }{ { Prefix: "FpMont", Name: "fpMont381", Prime: "0x1a0111ea397fe69a4b1ba7b6434bacd764774b84f38512bf6730d2a0f6b0f6241eabfffeb153ffffb9feffffffffaaab", Header: headerCIRCL, PackageName: packName, }, { Prefix: "ScMont", Name: "scMont255", Prime: "0x73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000001", Header: headerCIRCL, PackageName: packName, }, } func main() { if s := os.Getenv("FIAT_BINARY"); s != "" { FIAT_BINARY = s } var err error t := template.New("params") buf := new(strings.Builder) for _, f := range fields { params := []string{} for _, p := range FIAT_PARAMS { buf.Reset() t = template.Must(t.Parse(p)) err = t.Execute(buf, f) if err != nil { log.Fatalf("executing template:", err) } params = append(params, buf.String()) } cmd := exec.Command(FIAT_BINARY, params...) out, err := cmd.CombinedOutput() if len(out) != 0 || err != nil { log.Fatalf("command output: %s\n command error: %v\n", out, err) } } }