Merge pull request #936 from jedisct1/zig-backend

Add code generation for Zig

Author: JasonGross

.gitattributes

@@ -5,10 +5,12 @@
 *.h    text
 *.rs   text
 *.go   text
+*.zig  text
 
 fiat-bedrock2/**/*.c  linguist-generated
 fiat-c/**/*.c         linguist-generated
 fiat-go/**/*.go       linguist-generated
 fiat-java/**/*.java   linguist-generated
 fiat-json/**/*.json   linguist-generated
 fiat-rust/**/*.rs     linguist-generated
+fiat-zig/**/*.zig     linguist-generated

.github/workflows/zig.yml

@@ -0,0 +1,20 @@
+name: Test Generated Zig
+
+on:
+  push:
+  pull_request:
+  schedule:
+    - cron: "0 0 1 * *"
+
+jobs:
+  test-zig:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Install Zig
+        uses: goto-bus-stop/setup-zig@v1
+        with:
+          version: master
+      - uses: actions/checkout@v2
+      - name: Test Zig files
+        run: (cd fiat-zig && zig build && zig build test)

.gitignore

@@ -16,6 +16,7 @@ tramp
 
 # misc
 *.pyc
+zig-cache
 
 # java
 *.class

Makefile

@@ -12,6 +12,7 @@ GHCFLAGS?= # -XStrict
 CFLAGS?=
 
 CARGO_BUILD := cargo build
+ZIG_BUILD := zig build
 
 SKIP_BEDROCK2?=
 
@@ -30,17 +31,17 @@ INSTALLDEFAULTROOT := Crypto
 	install-standalone install-standalone-ocaml install-standalone-haskell \
 	uninstall-standalone uninstall-standalone-ocaml uninstall-standalone-haskell \
 	util all-except-generated \
-	c-files bedrock2-files rust-files go-files json-files java-files generated-files \
-	lite-c-files lite-bedrock2-files lite-rust-files lite-go-files lite-json-files lite-java-files lite-generated-files \
+	c-files bedrock2-files rust-files go-files json-files java-files zig-files generated-files \
+	lite-c-files lite-bedrock2-files lite-rust-files lite-go-files lite-json-files lite-java-files lite-zig-files lite-generated-files \
 	bedrock2-backend \
 	update-go-pkg-cache \
 	deps \
 	nobigmem print-nobigmem \
 	lite only-heavy printlite \
 	all-except-compiled \
 	some-early pre-standalone pre-standalone-extracted standalone standalone-haskell standalone-ocaml \
-	test-c-files test-bedrock2-files test-rust-files test-go-files test-json-files test-java-files \
-	only-test-c-files only-test-bedrock2-files only-test-rust-files only-test-go-files only-test-json-files only-test-java-files \
+	test-c-files test-bedrock2-files test-rust-files test-go-files test-json-files test-java-files test-zig-files \
+	only-test-c-files only-test-bedrock2-files only-test-rust-files only-test-go-files only-test-json-files only-test-java-files only-test-zig-files \
 	test-go-module only-test-go-module \
 	javadoc only-javadoc \
 	check-output accept-output
@@ -140,6 +141,7 @@ GO_DIR := fiat-go/
 JSON_DIR := fiat-json/src/
 JAVA_DIR := fiat-java/src/
 JAVADOC_DIR := fiat-java/doc/
+ZIG_DIR := fiat-zig/src/
 
 # Java only really supports 32-bit builds, because we have neither 64x64->64x64 multiplication, nor uint128
 # Java also requires that class names match file names
@@ -218,13 +220,15 @@ ALL_RUST_FILES := $(patsubst %,$(RUST_DIR)%.rs,$(ALL_BASE_FILES))
 ALL_GO_FILES := $(patsubst %,$(GO_DIR)%.go,$(call GO_RENAME_TO_FILE,$(filter-out $(BASE_FILES_NEEDING_INT128),$(ALL_BASE_FILES))))
 ALL_JSON_FILES := $(patsubst %,$(JSON_DIR)%.json,$(ALL_BASE_FILES))
 ALL_JAVA_FILES := $(patsubst %,$(JAVA_DIR)%.java,$(call JAVA_RENAME,$(filter-out $(BASE_FILES_NEEDING_INT128),$(ALL_BASE_FILES))))
+ALL_ZIG_FILES := $(patsubst %,$(ZIG_DIR)%.zig,$(ALL_BASE_FILES))
 
 LITE_C_FILES := $(patsubst %,$(C_DIR)%.c,$(LITE_BASE_FILES))
 LITE_BEDROCK2_FILES := $(patsubst %,$(BEDROCK2_DIR)%.c,$(filter-out $(BASE_FILES_NEEDING_INT128),$(LITE_BASE_FILES)))
 LITE_RUST_FILES := $(patsubst %,$(RUST_DIR)%.rs,$(LITE_BASE_FILES))
 LITE_GO_FILES := $(patsubst %,$(GO_DIR)%.go,$(call GO_RENAME_TO_FILE,$(filter-out $(BASE_FILES_NEEDING_INT128),$(LITE_BASE_FILES))))
 LITE_JSON_FILES := $(patsubst %,$(JSON_DIR)%.json,$(LITE_BASE_FILES))
 LITE_JAVA_FILES := $(patsubst %,$(JAVA_DIR)%.java,$(call JAVA_RENAME,$(filter-out $(BASE_FILES_NEEDING_INT128),$(LITE_BASE_FILES))))
+LITE_ZIG_FILES := $(patsubst %,$(ZIG_DIR)%.zig,$(LITE_BASE_FILES))
 
 BEDROCK2_UNSATURATED_SOLINAS := src/ExtractionOCaml/bedrock2_unsaturated_solinas
 BEDROCK2_WORD_BY_WORD_MONTGOMERY := src/ExtractionOCaml/bedrock2_word_by_word_montgomery
@@ -273,8 +277,8 @@ endif
 CHECK_OUTPUTS := $(addprefix check-,$(OUTPUT_PREOUTS))
 ACCEPT_OUTPUTS := $(addprefix accept-,$(OUTPUT_PREOUTS))
 
-generated-files: c-files rust-files go-files json-files java-files
-lite-generated-files: lite-c-files lite-rust-files lite-go-files lite-json-files lite-java-files
+generated-files: c-files rust-files go-files json-files java-files zig-files
+lite-generated-files: lite-c-files lite-rust-files lite-go-files lite-json-files lite-java-files lite-zig-files
 all-except-compiled: coq pre-standalone-extracted check-output
 all-except-generated: standalone-ocaml perf-standalone all-except-compiled
 all: all-except-generated generated-files
@@ -291,13 +295,15 @@ rust-files: $(ALL_RUST_FILES)
 go-files: $(ALL_GO_FILES)
 json-files: $(ALL_JSON_FILES)
 java-files: $(ALL_JAVA_FILES)
+zig-files: $(ALL_ZIG_FILES)
 
 lite-c-files: $(LITE_C_FILES)
 lite-bedrock2-files: $(LITE_BEDROCK2_FILES)
 lite-rust-files: $(LITE_RUST_FILES)
 lite-go-files: $(LITE_GO_FILES)
 lite-json-files: $(LITE_JSON_FILES)
 lite-java-files: $(LITE_JAVA_FILES)
+lite-zig-files: $(LITE_ZIG_FILES)
 
 lite: $(LITE_VOFILES)
 nobigmem: $(NOBIGMEM_VOFILES)
@@ -537,6 +543,17 @@ test-rust-files: $(ALL_RUST_FILES)
 test-rust-files only-test-rust-files:
 	cd fiat-rust; $(CARGO_BUILD)
 
+$(ALL_ZIG_FILES) : $(ZIG_DIR)%.zig : $$($$($$*_BINARY_NAME))
+	$(SHOW)'SYNTHESIZE > $@'
+	$(HIDE)rm -f $@.ok
+	$(HIDE)($(TIMER) $($($*_BINARY_NAME)) --lang Zig --internal-static --public-function-case camelCase --private-function-case camelCase $($*_DESCRIPTION) $($*_ARGS) $($*_FUNCTIONS) && touch $@.ok) > $@.tmp
+	$(HIDE)(rm $@.ok && mv $@.tmp $@) || ( RV=$$?; cat $@.tmp; exit $$RV )
+
+test-zig-files: $(ALL_ZIG_FILES)
+
+test-zig-files only-test-zig-files:
+	cd fiat-zig; $(ZIG_BUILD)
+
 all: $(addprefix fiat-rust/,$(COPY_TO_FIAT_RUST))
 all: $(addprefix fiat-go/,$(COPY_TO_FIAT_GO))
 

_CoqProject

@@ -214,6 +214,7 @@ src/Stringification/JSON.v
 src/Stringification/Java.v
 src/Stringification/Language.v
 src/Stringification/Rust.v
+src/Stringification/Zig.v
 src/UnsaturatedSolinasHeuristics/Tests.v
 src/Util/AdditionChainExponentiation.v
 src/Util/Arg.v