diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml deleted file mode 100644 index a1c2f0ea..00000000 --- a/.github/workflows/ci.yml +++ /dev/null @@ -1,45 +0,0 @@ -name: Hakyber - -on: - workflow_dispatch: - push: - branches: - - master - -env: - OPAMROOT: /home/charlie/.opam - OPAMYES: true - OPAMJOBS: 2 - ECRJOBS: 1 - -jobs: - ec: - name: Check Hakyber EasyCrypt Project - runs-on: ubuntu-20.04 - container: - image: easycryptpa/ec-build-box - strategy: - fail-fast: false - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - uses: actions/checkout@v4 - name: Checkout EasyCrypt - with: - repository: EasyCrypt/easycrypt - ref: refs/heads/main - path: easycrypt - - name: Update OPAM & EasyCrypt dependencies - run: | - opam update - opam pin add -n easycrypt easycrypt - opam install --deps-only easycrypt - - name: Compile & Install EasyCrypt - run: opam install easycrypt - - name: Detect SMT provers - run: | - rm -f ~/.why3.conf - opam config exec -- easycrypt why3config -why3 ~/.why3.conf - - name: Compile Project - run: opam config exec -- make checkec diff --git a/.github/workflows/ct.yml b/.github/workflows/ct.yml index f71d25fa..2b03ed9b 100644 --- a/.github/workflows/ct.yml +++ b/.github/workflows/ct.yml @@ -18,4 +18,4 @@ jobs: nix_path: nixpkgs=channel:nixos-unstable - uses: DeterminateSystems/magic-nix-cache-action@v3 - run: nix-shell --arg full false --run "echo Dependencies OK…" - - run: nix-shell --arg full false --run "make -C code/jasmin/mlkem_${{matrix.dir}}/ ct" + - run: nix-shell --arg full false --run "make -C code/jasmin/mlkem_${{matrix.dir}}/ check-constant-time" diff --git a/.github/workflows/exec.yml b/.github/workflows/exec.yml new file mode 100644 index 00000000..de101d0c --- /dev/null +++ b/.github/workflows/exec.yml @@ -0,0 +1,23 @@ +name: "Interpret Jasmin Implementations" +on: + pull_request: + push: + +jobs: + tests: + name: Exec + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + with: + submodules: recursive + - uses: cachix/install-nix-action@v26 + with: + nix_path: nixpkgs=channel:nixos-unstable + - uses: DeterminateSystems/magic-nix-cache-action@v4 + - run: nix-shell --arg full false --run "echo Dependencies OK…" + - run: nix-shell --arg full false --run "make -C code/jasmin/test/ -j2" + - uses: actions/upload-artifact@v4 + with: + name: mlkem-exec + path: code/jasmin/test/*.log diff --git a/.github/workflows/prover-ec-dev-version.yml b/.github/workflows/prover-ec-dev-version.yml new file mode 100644 index 00000000..2ccd8b51 --- /dev/null +++ b/.github/workflows/prover-ec-dev-version.yml @@ -0,0 +1,36 @@ +name: Hakyber on EasyCrypt/dev + +on: + workflow_dispatch: + push: + branches: + - master + +env: + OPAMROOT: /home/charlie/.opam + OPAMYES: true + OPAMJOBS: 2 + ECRJOBS: 2 + +jobs: + ec: + name: Hakyber on EasyCrypt/dev + runs-on: ubuntu-20.04 + container: + image: ghcr.io/easycrypt/ec-build-box + strategy: + fail-fast: false + steps: + - uses: actions/checkout@v4 + with: + submodules: recursive + - name: Compile & Install EasyCrypt + run: | + opam pin --dev-repo add -n easycrypt https://github.com/EasyCrypt/easycrypt.git + opam install -v easycrypt + - name: Detect SMT provers + run: | + opam exec -- easycrypt why3config + - name: Compile Project + run: | + opam exec -- make checkec diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml new file mode 100644 index 00000000..b23450f5 --- /dev/null +++ b/.github/workflows/test.yml @@ -0,0 +1,21 @@ +name: "Tests" +on: + pull_request: + push: + +jobs: + tests: + name: tests + runs-on: ubuntu-latest + strategy: + fail-fast: false + matrix: + dir: [ 'ref', 'avx2' ] + steps: + - uses: actions/checkout@v4 + - uses: cachix/install-nix-action@v25 + with: + nix_path: nixpkgs=channel:nixos-unstable + - uses: DeterminateSystems/magic-nix-cache-action@v3 + - run: nix-shell --arg full false --run "echo Dependencies OK…" + - run: nix-shell --arg full false --run "make -C code/jasmin/mlkem_${{matrix.dir}}/ run-tests" diff --git a/.gitignore b/.gitignore new file mode 100644 index 00000000..5761abcf --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +*.o diff --git a/LICENSE b/LICENSE new file mode 100644 index 00000000..59ff3e16 --- /dev/null +++ b/LICENSE @@ -0,0 +1 @@ +SPDX-License-Identifier: CC0-1.0 OR Apache-2.0 diff --git a/LICENSES/Apache-2.0.txt b/LICENSES/Apache-2.0.txt new file mode 100644 index 00000000..d6456956 --- /dev/null +++ b/LICENSES/Apache-2.0.txt @@ -0,0 +1,202 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/LICENSES/CC0-1.0.txt b/LICENSES/CC0-1.0.txt new file mode 100644 index 00000000..0e259d42 --- /dev/null +++ b/LICENSES/CC0-1.0.txt @@ -0,0 +1,121 @@ +Creative Commons Legal Code + +CC0 1.0 Universal + + CREATIVE COMMONS CORPORATION IS NOT A LAW FIRM AND DOES NOT PROVIDE + LEGAL SERVICES. DISTRIBUTION OF THIS DOCUMENT DOES NOT CREATE AN + ATTORNEY-CLIENT RELATIONSHIP. CREATIVE COMMONS PROVIDES THIS + INFORMATION ON AN "AS-IS" BASIS. CREATIVE COMMONS MAKES NO WARRANTIES + REGARDING THE USE OF THIS DOCUMENT OR THE INFORMATION OR WORKS + PROVIDED HEREUNDER, AND DISCLAIMS LIABILITY FOR DAMAGES RESULTING FROM + THE USE OF THIS DOCUMENT OR THE INFORMATION OR WORKS PROVIDED + HEREUNDER. + +Statement of Purpose + +The laws of most jurisdictions throughout the world automatically confer +exclusive Copyright and Related Rights (defined below) upon the creator +and subsequent owner(s) (each and all, an "owner") of an original work of +authorship and/or a database (each, a "Work"). + +Certain owners wish to permanently relinquish those rights to a Work for +the purpose of contributing to a commons of creative, cultural and +scientific works ("Commons") that the public can reliably and without fear +of later claims of infringement build upon, modify, incorporate in other +works, reuse and redistribute as freely as possible in any form whatsoever +and for any purposes, including without limitation commercial purposes. +These owners may contribute to the Commons to promote the ideal of a free +culture and the further production of creative, cultural and scientific +works, or to gain reputation or greater distribution for their Work in +part through the use and efforts of others. + +For these and/or other purposes and motivations, and without any +expectation of additional consideration or compensation, the person +associating CC0 with a Work (the "Affirmer"), to the extent that he or she +is an owner of Copyright and Related Rights in the Work, voluntarily +elects to apply CC0 to the Work and publicly distribute the Work under its +terms, with knowledge of his or her Copyright and Related Rights in the +Work and the meaning and intended legal effect of CC0 on those rights. + +1. Copyright and Related Rights. A Work made available under CC0 may be +protected by copyright and related or neighboring rights ("Copyright and +Related Rights"). Copyright and Related Rights include, but are not +limited to, the following: + + i. the right to reproduce, adapt, distribute, perform, display, + communicate, and translate a Work; + ii. moral rights retained by the original author(s) and/or performer(s); +iii. publicity and privacy rights pertaining to a person's image or + likeness depicted in a Work; + iv. rights protecting against unfair competition in regards to a Work, + subject to the limitations in paragraph 4(a), below; + v. rights protecting the extraction, dissemination, use and reuse of data + in a Work; + vi. database rights (such as those arising under Directive 96/9/EC of the + European Parliament and of the Council of 11 March 1996 on the legal + protection of databases, and under any national implementation + thereof, including any amended or successor version of such + directive); and +vii. other similar, equivalent or corresponding rights throughout the + world based on applicable law or treaty, and any national + implementations thereof. + +2. Waiver. To the greatest extent permitted by, but not in contravention +of, applicable law, Affirmer hereby overtly, fully, permanently, +irrevocably and unconditionally waives, abandons, and surrenders all of +Affirmer's Copyright and Related Rights and associated claims and causes +of action, whether now known or unknown (including existing as well as +future claims and causes of action), in the Work (i) in all territories +worldwide, (ii) for the maximum duration provided by applicable law or +treaty (including future time extensions), (iii) in any current or future +medium and for any number of copies, and (iv) for any purpose whatsoever, +including without limitation commercial, advertising or promotional +purposes (the "Waiver"). Affirmer makes the Waiver for the benefit of each +member of the public at large and to the detriment of Affirmer's heirs and +successors, fully intending that such Waiver shall not be subject to +revocation, rescission, cancellation, termination, or any other legal or +equitable action to disrupt the quiet enjoyment of the Work by the public +as contemplated by Affirmer's express Statement of Purpose. + +3. Public License Fallback. Should any part of the Waiver for any reason +be judged legally invalid or ineffective under applicable law, then the +Waiver shall be preserved to the maximum extent permitted taking into +account Affirmer's express Statement of Purpose. In addition, to the +extent the Waiver is so judged Affirmer hereby grants to each affected +person a royalty-free, non transferable, non sublicensable, non exclusive, +irrevocable and unconditional license to exercise Affirmer's Copyright and +Related Rights in the Work (i) in all territories worldwide, (ii) for the +maximum duration provided by applicable law or treaty (including future +time extensions), (iii) in any current or future medium and for any number +of copies, and (iv) for any purpose whatsoever, including without +limitation commercial, advertising or promotional purposes (the +"License"). The License shall be deemed effective as of the date CC0 was +applied by Affirmer to the Work. Should any part of the License for any +reason be judged legally invalid or ineffective under applicable law, such +partial invalidity or ineffectiveness shall not invalidate the remainder +of the License, and in such case Affirmer hereby affirms that he or she +will not (i) exercise any of his or her remaining Copyright and Related +Rights in the Work or (ii) assert any associated claims and causes of +action with respect to the Work, in either case contrary to Affirmer's +express Statement of Purpose. + +4. Limitations and Disclaimers. + + a. No trademark or patent rights held by Affirmer are waived, abandoned, + surrendered, licensed or otherwise affected by this document. + b. Affirmer offers the Work as-is and makes no representations or + warranties of any kind concerning the Work, express, implied, + statutory or otherwise, including without limitation warranties of + title, merchantability, fitness for a particular purpose, non + infringement, or the absence of latent or other defects, accuracy, or + the present or absence of errors, whether or not discoverable, all to + the greatest extent permissible under applicable law. + c. Affirmer disclaims responsibility for clearing rights of other persons + that may apply to the Work or any use thereof, including without + limitation any person's Copyright and Related Rights in the Work. + Further, Affirmer disclaims responsibility for obtaining any necessary + consents, permissions or other rights required for any use of the + Work. + d. Affirmer understands and acknowledges that Creative Commons is not a + party to this document and has no duty or obligation with respect to + this CC0 or use of the Work. diff --git a/Makefile b/Makefile index daa3a98b..b36e18c1 100644 --- a/Makefile +++ b/Makefile @@ -1,22 +1,44 @@ # -*- Makefile -*- # -------------------------------------------------------------------- -ECCONF := config/tests.config +ECCONF := config/tests.config CHECKS ?= mlkem # -------------------------------------------------------------------- -.PHONY: default check checkec jasmin clean_eco +.PHONY: default check checkec jasmin clean_eco test bench default: check check: jasmin checkec jasmin: - make -C code/jasmin/mlkem_ref/extraction - make -C code/jasmin/mlkem_avx2/extraction + $(MAKE) -C code/jasmin/mlkem_ref/extraction + $(MAKE) -C code/jasmin/mlkem_avx2/extraction checkec: easycrypt runtest $(ECCONF) $(CHECKS) clean_eco: find proof -name '*.eco' -exec rm '{}' ';' + +test: + $(MAKE) -C code/jasmin/mlkem_ref/ -j$(nproc) compile-tests + $(MAKE) -C code/jasmin/mlkem_avx2/ -j$(nproc) compile-tests + @echo "\n\n### Testing the reference implementation" + $(MAKE) -C code/jasmin/mlkem_ref/ run-tests + @echo "\n\n### Testing the avx2 implementation" + $(MAKE) -C code/jasmin/mlkem_avx2/ run-tests + +bench: + $(MAKE) -C code/jasmin/mlkem_ref/ -j$(nproc) compile-speed + $(MAKE) -C code/jasmin/mlkem_avx2/ -j$(nproc) compile-speed + @echo "\n\n### Benchmarking the reference implementation" + $(MAKE) -C code/jasmin/mlkem_ref/ run-speed + @echo "\n\n### Benchmarking the avx2 implementation" + $(MAKE) -C code/jasmin/mlkem_avx2/ run-speed + +example: + $(MAKE) -C code/jasmin/mlkem_ref/example + $(MAKE) -C code/jasmin/mlkem_avx2/example + + diff --git a/code/Makefile.conf b/code/Makefile.conf index 0e97dc6a..c9fa6822 100644 --- a/code/Makefile.conf +++ b/code/Makefile.conf @@ -1,7 +1,9 @@ # -*- Makefile -*- # -------------------------------------------------------------------- -current_dir := $(dir $(realpath $(lastword $(MAKEFILE_LIST)))) +CURRENT_DIR := $(dir $(realpath $(lastword $(MAKEFILE_LIST)))) +PROJECT_DIR := $(abspath $(CURRENT_DIR)/../) # -------------------------------------------------------------------- -JASMINC ?= $(current_dir)/../jasmin/compiler/jasminc +JASMINC ?= $(abspath $(PROJECT_DIR)/jasmin/compiler/jasminc) +JASMIN_CT ?= $(abspath $(PROJECT_DIR)/jasmin/compiler/jasmin-ct) diff --git a/code/jasmin/mlkem_avx2/.gitignore b/code/jasmin/mlkem_avx2/.gitignore index 20b463a8..cfa7440f 100644 --- a/code/jasmin/mlkem_avx2/.gitignore +++ b/code/jasmin/mlkem_avx2/.gitignore @@ -1 +1,36 @@ +jfips202.s +jindcpa.s jkem.s +jpoly.s +jpolyvec.s +jspeed.s +test/test_fips202 +test/test_indcpa +test/test_kem +test/test_poly_add2 +test/test_poly_basemul +test/test_poly_compress +test/test_poly_csubq +test/test_poly_decompress +test/test_poly_frombytes +test/test_poly_frommont +test/test_poly_frommsg +test/test_poly_getnoise +test/test_poly_invntt +test/test_poly_ntt +test/test_poly_reduce +test/test_poly_sub +test/test_poly_tobytes +test/test_poly_tomsg +test/test_polyvec_add2 +test/test_polyvec_compress +test/test_polyvec_csubq +test/test_polyvec_decompress +test/test_polyvec_frombytes +test/test_polyvec_invntt +test/test_polyvec_ntt +test/test_polyvec_pointwise_acc +test/test_polyvec_reduce +test/test_polyvec_tobytes +test/speed_indcpa +test/speed_mlkem diff --git a/code/jasmin/mlkem_avx2/Makefile b/code/jasmin/mlkem_avx2/Makefile index 5bb618f0..09b46ef6 100644 --- a/code/jasmin/mlkem_avx2/Makefile +++ b/code/jasmin/mlkem_avx2/Makefile @@ -1,146 +1,199 @@ # -*- Makefile -*- - -include ../../Makefile.conf CC ?= /usr/bin/gcc GFLAGS ?= -CFLAGS := -Wall -Wextra -g -Ofast -fomit-frame-pointer +CFLAGS := -Wall -Wextra -g -O3 -fomit-frame-pointer JFLAGS := ${JADDFLAGS} OS := $(shell uname -s) -.SECONDARY: jpoly.s jpolyvec.s jfips202.s jindcpa.s jindcpa.o jkem.s - -default: test speed - -test: test/test_poly_compress \ - test/test_poly_decompress \ - test/test_poly_tobytes \ - test/test_poly_frombytes \ - test/test_poly_tomsg \ - test/test_poly_frommsg \ - test/test_poly_add2 \ - test/test_poly_sub \ - test/test_poly_ntt \ - test/test_poly_invntt \ - test/test_poly_basemul \ - test/test_poly_frommont \ - test/test_poly_reduce \ - test/test_poly_csubq \ - test/test_poly_getnoise \ - test/test_polyvec_compress\ - test/test_polyvec_decompress\ - test/test_polyvec_tobytes \ - test/test_polyvec_frombytes \ - test/test_polyvec_add2 \ - test/test_polyvec_ntt \ - test/test_polyvec_invntt \ - test/test_polyvec_pointwise_acc \ - test/test_polyvec_reduce\ - test/test_polyvec_csubq \ - test/test_fips202 \ - test/test_indcpa \ - test/test_kem - -speed: test/speed_indcpa \ - test/speed_mlkem - -HEADERS = params.h poly.h fips202.h ntt.h indcpa.h kem.h \ - -JHEADERS = params.jinc \ - reduce.jinc \ - fips202_common.jinc \ - fips202.jinc \ - fips202_4x.jinc \ - keccakf1600.jinc \ - consts.jinc \ - shuffle.jinc \ - indcpa.jinc \ - verify.jinc - -POLYHEADERS = poly.jinc \ - consts.jinc \ - -POLYVECHEADERS = polyvec.jinc \ - gen_matrix.jinc \ - -INCS = fq.inc shuffle.inc -SOURCES = poly.c polyvec.c cbd.c fips202.c ntt.c reduce.c symmetric-fips202.c indcpa.c kem.c consts.c shuffle.S fq.S\ - -test/test_indcpa: test/test_indcpa.c $(HEADERS) $(SOURCES) $(INCS) jindcpa.o - $(CC) $(CFLAGS) -o $@ $(SOURCES) jindcpa.o $< - -test/test_kem: test/test_kem.c $(HEADERS) $(SOURCES) $(INCS) jkem.o - $(CC) $(CFLAGS) -o $@ $(SOURCES) jkem.o ~/Desktop/Repos/jasmin/compiler/syscall/jasmin_syscall.o $< - -test/speed_indcpa: test/speed_indcpa.c $(HEADERS) $(SOURCES) $(INCS) jindcpa.o - $(CC) $(CFLAGS) -o $@ $(SOURCES) jindcpa.o $< - -test/speed_mlkem: test/speed_mlkem.c $(HEADERS) $(SOURCES) $(INCS) jspeed.s - $(CC) $(CFLAGS) -o $@ $(SOURCES) jspeed.s $< - -test/test_fips202: test/test_fips202.c $(HEADERS) fips202.c jfips202.s - $(CC) $(CFLAGS) -o $@ fips202.c jfips202.s $< - -test/test_gen_matrix: test/test_gen_matrix.c $(HEADERS) gen_matrix.s - $(CC) $(CFLAGS) -o $@ gen_matrix.s $< - -test/test_poly_%: test/test_poly_%.c $(HEADERS) $(SOURCES) $(INCS) jpoly.s - $(CC) $(CFLAGS) -o $@ $(SOURCES) jpoly.s $< - -test/test_polyvec_%: test/test_polyvec_%.c $(HEADERS) $(SOURCES) $(INCS) jpolyvec.s - $(CC) $(CFLAGS) -o $@ $(SOURCES) jpolyvec.s $< - +default: run-tests run-speed + +# -- +TESTS_POLY := \ + test/test_poly_compress \ + test/test_poly_decompress \ + test/test_poly_tobytes \ + test/test_poly_frombytes \ + test/test_poly_tomsg \ + test/test_poly_frommsg \ + test/test_poly_add2 \ + test/test_poly_sub \ + test/test_poly_ntt \ + test/test_poly_invntt \ + test/test_poly_basemul \ + test/test_poly_frommont \ + test/test_poly_reduce \ + test/test_poly_csubq \ + test/test_poly_getnoise + +TESTS_POLYVEC := \ + test/test_polyvec_compress\ + test/test_polyvec_decompress\ + test/test_polyvec_tobytes \ + test/test_polyvec_frombytes \ + test/test_polyvec_add2 \ + test/test_polyvec_ntt \ + test/test_polyvec_invntt \ + test/test_polyvec_pointwise_acc \ + test/test_polyvec_reduce\ + test/test_polyvec_csubq + +TESTS := \ + $(TESTS_POLY) \ + $(TESTS_POLYVEC) \ + test/test_fips202 \ + test/test_indcpa \ + test/test_kem + +test: $(TESTS) + +speed: test/speed_mlkem + +# -- + +HEADERS := \ + params.h \ + poly.h \ + fips202.h \ + ntt.h \ + indcpa.h \ + kem.h + +C_SOURCES := \ + poly.c \ + polyvec.c \ + cbd.c \ + fips202.c \ + ntt.c \ + reduce.c \ + symmetric-fips202.c \ + indcpa.c \ + kem.c \ + consts.c \ + shuffle.S \ + fq.S + +JHEADERS := \ + params.jinc \ + reduce.jinc \ + fips202_common.jinc \ + fips202.jinc \ + fips202_4x.jinc \ + keccakf1600.jinc \ + consts.jinc \ + shuffle.jinc \ + indcpa.jinc \ + verify.jinc + +POLYHEADERS := \ + poly.jinc \ + consts.jinc + +POLYVECHEADERS := \ + polyvec.jinc \ + gen_matrix.jinc + +S_INC := \ + fq.inc \ + shuffle.inc + +# -- + +# -- + +JASMIN_SOURCES := \ + jpoly.jazz \ + jpolyvec.jazz \ + jfips202.jazz \ + jindcpa.jazz \ + jkem.jazz \ + jspeed.jazz + +JASMIN_ASSEMBLY := $(JASMIN_SOURCES:%.jazz=%.s) + +# - + +RANDOMBYTES := $(PROJECT_DIR)/ext/randombytes/jasmin_syscall.o + +$(RANDOMBYTES): $(PROJECT_DIR)/ext/randombytes/jasmin_syscall.c $(PROJECT_DIR)/ext/randombytes/jasmin_syscall.h + $(MAKE) -C $(@D) + +$(JASMIN_ASSEMBLY): %.s: %.jazz - $(JASMINC) -o $@ $(JFLAGS) $^ + $(JASMINC) -nowarning -o $@ $(JFLAGS) $^ + +#-- + +compile-tests-poly: $(TESTS_POLY) +$(TESTS_POLY): +test/test_poly_%: test/test_poly_%.c $(HEADERS) $(C_SOURCES) $(S_INC) jpoly.s + $(CC) $(CFLAGS) -o $@ $(C_SOURCES) jpoly.s $< + +compile-tests-polyvec: $(TESTS_POLYVEC) +$(TESTS_POLYVEC): +test/test_polyvec_%: test/test_polyvec_%.c $(HEADERS) $(C_SOURCES) $(S_INC) jpolyvec.s + $(CC) $(CFLAGS) -o $@ $(C_SOURCES) jpolyvec.s $< + +test/test_fips202: test/test_fips202.c $(HEADERS) $(C_SOURCES) jfips202.s + $(CC) $(CFLAGS) -o $@ $(C_SOURCES) jfips202.s $< + +test/test_gen_matrix: test/test_gen_matrix.c $(HEADERS) $(C_SOURCES) gen_matrix.s + $(CC) $(CFLAGS) -o $@ $(C_SOURCES) gen_matrix.s $< + +test/test_indcpa: test/test_indcpa.c $(HEADERS) $(C_SOURCES) $(S_INC) jindcpa.s + $(CC) $(CFLAGS) -o $@ $(C_SOURCES) jindcpa.s $< + +test/test_kem: test/test_kem.c $(HEADERS) $(C_SOURCES) $(S_INC) $(RANDOMBYTES) jkem.s + $(CC) $(CFLAGS) -o $@ $(C_SOURCES) $(RANDOMBYTES) jkem.s $< + +compile-tests: test + +# -- +# note: to improve speed, remove for loop and define *.out targets + +run-tests-poly: compile-tests-poly + for i in $(TESTS_POLY); do ./$$i; done + +run-tests-polyvec: compile-tests-polyvec + for i in $(TESTS_POLYVEC); do ./$$i; done + +run-tests: compile-tests + @for i in $(TESTS); do ./$$i; done + +# -- + +test/speed_mlkem: test/speed_mlkem.c $(HEADERS) $(C_SOURCES) $(S_INC) $(RANDOMBYTES) jspeed.s + $(CC) $(CFLAGS) -o $@ $(C_SOURCES) $(RANDOMBYTES) jspeed.s $< + +compile-speed: test/speed_mlkem + +run-speed: compile-speed + ./test/speed_mlkem + +# -- + +.PHONY: check-constant-time check-speculative-constant-time + +check-constant-time: + $(JASMIN_CT) --infer jkem.jazz -.PHONY: ct sct clean +check-speculative-constant-time: + $(JASMIN_CT) --infer --speculative jkem.jazz -ct: - $(JASMINC) -checkCT -infer jkem.jazz +# -- -sct: - $(JASMINC) -checkSCT jkem.jazz +.PHONY: clean clean: - -rm -f *.o - -rm -f gen_matrix.s - -rm -f jindcpa.s - -rm -f jkem.s - -rm -f jfips202.s - -rm -f jpoly.s - -rm -f jpolyvec.s - -rm -f jspeed.s - -rm -f test/test_poly_compress - -rm -f test/test_poly_decompress - -rm -f test/test_poly_tobytes - -rm -f test/test_poly_frombytes - -rm -f test/test_poly_tomsg - -rm -f test/test_poly_frommsg - -rm -f test/test_poly_add2 - -rm -f test/test_poly_sub - -rm -f test/test_poly_ntt - -rm -f test/test_poly_invntt - -rm -f test/test_poly_basemul - -rm -f test/test_poly_frommont - -rm -f test/test_poly_reduce - -rm -f test/test_poly_csubq - -rm -f test/test_poly_getnoise - -rm -f test/test_polyvec_compress - -rm -f test/test_polyvec_decompress - -rm -f test/test_polyvec_tobytes - -rm -f test/test_polyvec_frombytes - -rm -f test/test_polyvec_add2 - -rm -f test/test_polyvec_ntt - -rm -f test/test_polyvec_invntt - -rm -f test/test_polyvec_pointwise_acc - -rm -f test/test_polyvec_reduce - -rm -f test/test_polyvec_csubq + -rm -f $(JASMIN_ASSEMBLY) + -rm -f $(TESTS_POLY) + -rm -f $(TESTS_POLYVEC) -rm -f test/test_fips202 -rm -f test/test_gen_matrix -rm -f test/test_indcpa -rm -f test/test_kem - -rm -f test/speed_indcpa -rm -f test/speed_mlkem ifeq ($(OS),Darwin) -rm -r -f test/*.dSYM diff --git a/code/jasmin/mlkem_avx2/cycles.jinc b/code/jasmin/mlkem_avx2/cycles.jinc new file mode 100644 index 00000000..bcdf5f10 --- /dev/null +++ b/code/jasmin/mlkem_avx2/cycles.jinc @@ -0,0 +1,23 @@ +inline fn tsc() -> stack u32[2] +{ + reg u64 l h; + stack u32[2] t; + + h, l = #RDTSC(); + + t[0] = (32u) l; + t[1] = (32u) h; + + return t; +} + +inline fn cycles(stack u32[2] start end) -> reg u64 +{ + reg u64 t; + + t = end[u64 0]; + t -= start[u64 0]; + + return t; +} + diff --git a/code/jasmin/mlkem_avx2/example/.gitignore b/code/jasmin/mlkem_avx2/example/.gitignore new file mode 100644 index 00000000..7ff73178 --- /dev/null +++ b/code/jasmin/mlkem_avx2/example/.gitignore @@ -0,0 +1,2 @@ +example +jkem.s diff --git a/code/jasmin/mlkem_avx2/example/Makefile b/code/jasmin/mlkem_avx2/example/Makefile new file mode 100644 index 00000000..011e0ef7 --- /dev/null +++ b/code/jasmin/mlkem_avx2/example/Makefile @@ -0,0 +1,35 @@ +include ../../../Makefile.conf + +CC ?= /usr/bin/gcc +CFLAGS := -Wall -Wextra -g -O3 -fomit-frame-pointer + +default: run-example + +RANDOMBYTES := $(PROJECT_DIR)/ext/randombytes/jasmin_syscall.o +$(RANDOMBYTES): $(PROJECT_DIR)/ext/randombytes/jasmin_syscall.c $(PROJECT_DIR)/ext/randombytes/jasmin_syscall.h + $(MAKE) -C $(@D) + +.PHONY: ../jkem.s +../jkem.s: + $(MAKE) -C $(@D) $(@F) + +jkem.s: ../jkem.s + cp $< $@ + + +example: example.c jkem.s api.h $(RANDOMBYTES) + $(CC) $(CFLAGS) -o $@ example.c jkem.s $(RANDOMBYTES) + +run-example: example + ./example + + + +.PHONY: clean distclean +clean: + rm -f example jkem.s + +distclean: clean + rm -f ../jkem.s + $(MAKE) -C $(dir $(RANDOMBYTES)) clean + diff --git a/code/jasmin/mlkem_avx2/example/api.h b/code/jasmin/mlkem_avx2/example/api.h new file mode 100644 index 00000000..7e9a8b82 --- /dev/null +++ b/code/jasmin/mlkem_avx2/example/api.h @@ -0,0 +1,47 @@ +#ifndef JADE_KEM_mlkem_mlkem768_amd64_avx2_API_H +#define JADE_KEM_mlkem_mlkem768_amd64_avx2_API_H + +#include + +#define JADE_KEM_mlkem_mlkem768_amd64_avx2_SECRETKEYBYTES 2400 +#define JADE_KEM_mlkem_mlkem768_amd64_avx2_PUBLICKEYBYTES 1184 +#define JADE_KEM_mlkem_mlkem768_amd64_avx2_CIPHERTEXTBYTES 1088 +#define JADE_KEM_mlkem_mlkem768_amd64_avx2_KEYPAIRCOINBYTES 64 +#define JADE_KEM_mlkem_mlkem768_amd64_avx2_ENCCOINBYTES 32 +#define JADE_KEM_mlkem_mlkem768_amd64_avx2_BYTES 32 + +#define JADE_KEM_mlkem_mlkem768_amd64_avx2_ALGNAME "mlkem768" +#define JADE_KEM_mlkem_mlkem768_amd64_avx2_ARCH "amd64" +#define JADE_KEM_mlkem_mlkem768_amd64_avx2_IMPL "avx2" + +int jade_kem_mlkem_mlkem768_amd64_avx2_keypair_derand( + uint8_t *public_key, + uint8_t *secret_key, + const uint8_t *coins +); + +int jade_kem_mlkem_mlkem768_amd64_avx2_keypair( + uint8_t *public_key, + uint8_t *secret_key +); + +int jade_kem_mlkem_mlkem768_amd64_avx2_enc_derand( + uint8_t *ciphertext, + uint8_t *shared_secret, + const uint8_t *public_key, + const uint8_t *coins +); + +int jade_kem_mlkem_mlkem768_amd64_avx2_enc( + uint8_t *ciphertext, + uint8_t *shared_secret, + const uint8_t *public_key +); + +int jade_kem_mlkem_mlkem768_amd64_avx2_dec( + uint8_t *shared_secret, + const uint8_t *ciphertext, + const uint8_t *secret_key +); + +#endif diff --git a/code/jasmin/mlkem_avx2/example/example.c b/code/jasmin/mlkem_avx2/example/example.c new file mode 100644 index 00000000..d88c8fd3 --- /dev/null +++ b/code/jasmin/mlkem_avx2/example/example.c @@ -0,0 +1,139 @@ +#include +#include +#include +#include +#include + +#include "api.h" + +// print functions +static void print_info(const char *algname, const char *arch, const char *impl) +{ + printf("// {\"%s\" : { architecture : \"%s\", implementation : \"%s\"} }", + algname, arch, impl); + printf("\n"); +} + +static void print_u8(const uint8_t *a, size_t l) +{ + size_t i; + + if(l == 0) + { return; } + + printf("{\n "); + for(i=0; i<(l-1); i++) + { printf("0x%02" PRIx8 ", ", a[i]); + if((i+1)%16 == 0) + { printf("\n "); } + } + + printf("0x%02" PRIx8 "\n};\n", a[i]); + return; +} + +static void print_str_u8(const char *str, const uint8_t *a, size_t l) +{ + if( l == 0 ) + { printf("uint8_t *%s = NULL;\n", str); + return; + } + + printf("uint8_t %s[%zu] = ",str, l); + print_u8(a, l); +} + +// randombytes implementation, in this case we use the __jasmin_syscall_randombytes__ +extern uint8_t* __jasmin_syscall_randombytes__(uint8_t* x, uint64_t xlen); + +uint8_t* randombytes(uint8_t* x, uint64_t xlen) +{ + return __jasmin_syscall_randombytes__(x, xlen); +} + +// mapping the fully namespaced macros from api.h into shorter names +#define JADE_KEM_SECRETKEYBYTES JADE_KEM_mlkem_mlkem768_amd64_avx2_SECRETKEYBYTES +#define JADE_KEM_PUBLICKEYBYTES JADE_KEM_mlkem_mlkem768_amd64_avx2_PUBLICKEYBYTES +#define JADE_KEM_CIPHERTEXTBYTES JADE_KEM_mlkem_mlkem768_amd64_avx2_CIPHERTEXTBYTES +#define JADE_KEM_KEYPAIRCOINBYTES JADE_KEM_mlkem_mlkem768_amd64_avx2_KEYPAIRCOINBYTES +#define JADE_KEM_ENCCOINBYTES JADE_KEM_mlkem_mlkem768_amd64_avx2_ENCCOINBYTES +#define JADE_KEM_BYTES JADE_KEM_mlkem_mlkem768_amd64_avx2_BYTES + +#define jade_kem_keypair jade_kem_mlkem_mlkem768_amd64_avx2_keypair +#define jade_kem_enc jade_kem_mlkem_mlkem768_amd64_avx2_enc +#define jade_kem_dec jade_kem_mlkem_mlkem768_amd64_avx2_dec + +#define jade_kem_keypair_derand jade_kem_mlkem_mlkem768_amd64_avx2_keypair_derand +#define jade_kem_enc_derand jade_kem_mlkem_mlkem768_amd64_avx2_enc_derand + +#define JADE_KEM_ALGNAME JADE_KEM_mlkem_mlkem768_amd64_avx2_ALGNAME +#define JADE_KEM_ARCH JADE_KEM_mlkem_mlkem768_amd64_avx2_ARCH +#define JADE_KEM_IMPL JADE_KEM_mlkem_mlkem768_amd64_avx2_IMPL + +// this example program does the following: +// - creates a keypair (with the randomized api +// - encapsulates/decapsulates and checks that the shared secret is the same +// +// - it repeats the process using the derandomized ('derand') functions +// +int main(void) +{ + int r; + uint8_t public_key[JADE_KEM_PUBLICKEYBYTES]; + uint8_t secret_key[JADE_KEM_SECRETKEYBYTES]; + + uint8_t shared_secret_a[JADE_KEM_BYTES]; + uint8_t ciphertext[JADE_KEM_CIPHERTEXTBYTES]; + uint8_t shared_secret_b[JADE_KEM_BYTES]; + + uint8_t keypair_coins[JADE_KEM_KEYPAIRCOINBYTES]; + uint8_t enc_coins[JADE_KEM_ENCCOINBYTES]; + + // create key pair + r = jade_kem_keypair(public_key, secret_key); + assert(r == 0); + + // encapsulate + r = jade_kem_enc(ciphertext, shared_secret_a, public_key); + assert(r == 0); + + // decapsulate + r = jade_kem_dec(shared_secret_b, ciphertext, secret_key); + assert(r == 0); + assert(memcmp(shared_secret_a, shared_secret_b, JADE_KEM_BYTES) == 0); + + print_info(JADE_KEM_ALGNAME, JADE_KEM_ARCH, JADE_KEM_IMPL); + print_str_u8("secret_key", secret_key, JADE_KEM_SECRETKEYBYTES); + print_str_u8("public_key", public_key, JADE_KEM_PUBLICKEYBYTES); + print_str_u8("ciphertext", ciphertext, JADE_KEM_CIPHERTEXTBYTES); + print_str_u8("shared_secret", shared_secret_a, JADE_KEM_BYTES); + + // create key pair using derand function (random coins are given as input) + randombytes(keypair_coins, JADE_KEM_KEYPAIRCOINBYTES); + r = jade_kem_keypair_derand(public_key, secret_key, keypair_coins); + assert(r == 0); + + // encapsulate using derand function (random coins are given as input) + randombytes(enc_coins, JADE_KEM_ENCCOINBYTES); + r = jade_kem_enc_derand(ciphertext, shared_secret_a, public_key, enc_coins); + assert(r == 0); + + // decapsulate + r = jade_kem_dec(shared_secret_b, ciphertext, secret_key); + assert(r == 0); + assert(memcmp(shared_secret_a, shared_secret_b, JADE_KEM_BYTES) == 0); + + print_info(JADE_KEM_ALGNAME, JADE_KEM_ARCH, JADE_KEM_IMPL); + print_str_u8("keypair_derand_coins", keypair_coins, JADE_KEM_KEYPAIRCOINBYTES); + print_str_u8("secret_key_derand", secret_key, JADE_KEM_SECRETKEYBYTES); + print_str_u8("public_key_derand", public_key, JADE_KEM_PUBLICKEYBYTES); + + print_str_u8("enc_derand_coins", enc_coins, JADE_KEM_ENCCOINBYTES); + print_str_u8("ciphertext_derand", ciphertext, JADE_KEM_CIPHERTEXTBYTES); + print_str_u8("shared_secret_derand", shared_secret_a, JADE_KEM_BYTES); + + + + return 0; +} + diff --git a/code/jasmin/mlkem_avx2/gen_matrix.jazz b/code/jasmin/mlkem_avx2/gen_matrix.jazz deleted file mode 100644 index 4e4d1852..00000000 --- a/code/jasmin/mlkem_avx2/gen_matrix.jazz +++ /dev/null @@ -1,59 +0,0 @@ -require "gen_matrix.jinc" -/* -require "gen_matrix_old.jinc" - -export fn gen_matrix_old_jazz(reg u64 ap, reg u64 seedp) -{ - stack u16[MLKEM_K*MLKEM_VECN] aa; - stack u8[MLKEM_SYMBYTES] seed; - reg u8 c; - reg u16 t; - inline int i; - stack u64 sap; - - sap = ap; - - for i = 0 to MLKEM_SYMBYTES - { - c = (u8)[seedp + i]; - seed[i] = c; - } - - aa = __gen_matrix_old(seed, 1); - - ap = sap; - - for i = 0 to MLKEM_K*MLKEM_VECN - { - t = aa[i]; - (u16)[ap + 2*i] = t; - } -} -*/ -export fn gen_matrix_jazz(reg u64 ap, reg u64 seedp) -{ - stack u16[MLKEM_K*MLKEM_VECN] aa; - stack u8[MLKEM_SYMBYTES] seed; - reg u8 c; - reg u16 t; - inline int i; - stack u64 sap; - - sap = ap; - - for i = 0 to MLKEM_SYMBYTES - { - c = (u8)[seedp + i]; - seed[i] = c; - } - - aa = __gen_matrix(seed, 1); - - ap = sap; - - for i = 0 to MLKEM_K*MLKEM_VECN - { - t = aa[i]; - (u16)[ap + 2*i] = t; - } -} diff --git a/code/jasmin/mlkem_avx2/jgen_matrix.jazz b/code/jasmin/mlkem_avx2/jgen_matrix.jazz new file mode 100644 index 00000000..8f444570 --- /dev/null +++ b/code/jasmin/mlkem_avx2/jgen_matrix.jazz @@ -0,0 +1,30 @@ +require "gen_matrix.jinc" + +export fn gen_matrix_jazz(reg u64 ap, reg u64 seedp) +{ + stack u16[MLKEM_K*MLKEM_VECN] aa; + stack u8[MLKEM_SYMBYTES] seed; + reg u8 c; + reg u16 t; + inline int i; + stack u64 sap; + + sap = ap; + + for i = 0 to MLKEM_SYMBYTES + { + #[declassify] + c = (u8)[seedp + i]; + seed[i] = c; + } + + aa = __gen_matrix(seed, 1); + + ap = sap; + + for i = 0 to MLKEM_K*MLKEM_VECN + { + t = aa[i]; + (u16)[ap + 2*i] = t; + } +} diff --git a/code/jasmin/mlkem_avx2/jspeed.jazz b/code/jasmin/mlkem_avx2/jspeed.jazz index 911a3d43..8f787640 100644 --- a/code/jasmin/mlkem_avx2/jspeed.jazz +++ b/code/jasmin/mlkem_avx2/jspeed.jazz @@ -5,193 +5,296 @@ require "indcpa.jinc" require "kem.jinc" require "verify.jinc" -/* Exported functions only for benchmarking */ -export fn gen_matrix_jazz(reg u64 ap, reg u64 seedp) +require "cycles.jinc" + +// note: this code needs to be reviewed and properly tested + +// exported functions only for benchmarking + +export fn gen_matrix_jazz(reg u64 ap seedp) -> reg u64 { - stack u16[MLKEM_K*MLKEM_VECN] aa; + stack u32[2] start end; + reg u64 t; + stack u64 aps; + stack u16[MLKEM_K*MLKEM_VECN] a; stack u8[MLKEM_SYMBYTES] seed; + reg u64 i; - aa = __gen_matrix(seed, 1); -} + aps = ap; + i=0; while(i < MLKEM_SYMBYTES){ seed[i] = (u8)[seedp + i]; i += 1; } -export fn poly_compress_jazz(reg u64 rp, reg u64 ap) -{ - stack u16[MLKEM_N] a; + start = tsc(); - a = _poly_compress(rp, a); -} + a = __gen_matrix(seed, 1); -export fn poly_decompress_jazz(reg u64 rp, reg u64 ap) -{ - stack u16[MLKEM_N] r; + end = tsc(); - r = _poly_decompress(r, ap); + ap = aps; + i=0; while(i < MLKEM_K*MLKEM_VECN){ (u16)[ap + 2*i] = a[i]; i += 1; } + + t = cycles(start, end); + return t; } -export fn poly_tomsg_jazz(reg u64 rp, reg u64 ap) +// ////////////////////////////////////////////////////////////////// + +export fn poly_getnoise_4x_jazz(reg u64 r0p r1p r2p r3p, reg u64 seedp, reg u8 nonce) -> reg u64 { - stack u16[MLKEM_N] a; + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_N] r0 r1 r2 r3; + stack u8[MLKEM_SYMBYTES] seed; + reg u64 i; - a = _poly_tomsg(rp, a); -} + () = #spill(r0p, r1p, r2p, r3p); + i=0; while(i < MLKEM_SYMBYTES){ seed[i] = (u8)[seedp + i]; i += 1; } -export fn poly_frommsg_jazz(reg u64 rp, reg u64 ap) -{ - stack u16[MLKEM_N] r; + start = tsc(); + + r0, r1, r2, r3 = _poly_getnoise_eta1_4x(r0, r1, r2, r3, seed, nonce); - r = _poly_frommsg(r, ap); + end = tsc(); + + () = #unspill(r0p, r1p, r2p, r3p); + + i=0; while(i < MLKEM_N) + { (u16)[r0p + 2*i] = r0[i]; + (u16)[r1p + 2*i] = r1[i]; + (u16)[r2p + 2*i] = r2[i]; + (u16)[r3p + 2*i] = r3[i]; + i+= 1; + } + + t = cycles(start, end); + return t; } -export fn poly_ntt_jazz(reg u64 rp) + +export fn poly_ntt_jazz(reg u64 rp) -> reg u64 { + stack u32[2] start end; + reg u64 t; stack u16[MLKEM_N] r; + reg u64 i; + + () = #spill(rp); + i=0; while(i < MLKEM_N){ r[i] = (u16)[rp + 2*i]; i += 1; } + + start = tsc(); r = _poly_ntt(r); + + end = tsc(); + + () = #unspill(rp); + i=0; while(i < MLKEM_N){ (u16)[rp + 2*i] = r[i]; i += 1; } + + t = cycles(start, end); + return t; } -export fn poly_invntt_jazz(reg u64 rp) + +export fn poly_invntt_jazz(reg u64 rp) -> reg u64 { + stack u32[2] start end; + reg u64 t; stack u16[MLKEM_N] r; + reg u64 i; + + () = #spill(rp); + i=0; while(i < MLKEM_N){ r[i] = (u16)[rp + 2*i]; i += 1; } + + start = tsc(); r = _poly_invntt(r); + + end = tsc(); + + () = #unspill(rp); + i=0; while(i < MLKEM_N){ (u16)[rp + 2*i] = r[i]; i += 1; } + + t = cycles(start, end); + return t; } -export fn poly_getnoise_jazz(reg u64 rp, reg u64 seedp, reg u8 nonce) +export fn poly_tomsg_jazz(reg u64 rp ap) -> reg u64 { - stack u16[MLKEM_N] r; - stack u8[MLKEM_SYMBYTES] seed; + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_N] a; + reg u64 i; + + () = #spill(ap); + i=0; while(i < MLKEM_N){ a[i] = (u16)[ap + 2*i]; i += 1; } + + start = tsc(); - //r = _poly_getnoise_eta1_4x(r, seed, nonce); + a = _poly_tomsg(rp, a); + + end = tsc(); + + () = #unspill(ap); + i=0; while(i < MLKEM_N){ (u16)[ap + 2*i] = a[i]; i += 1; } + + t = cycles(start, end); + return t; } -export fn poly_getnoise_4x_jazz(reg u64 r0 r1 r2 r3, reg u64 seedp, reg u8 nonce) +export fn poly_frommsg_jazz(reg u64 rp ap) -> reg u64 { - stack u16[MLKEM_N] r0 r1 r2 r3; - stack u8[MLKEM_SYMBYTES] seed; + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_N] r; + reg u64 i; - r0, r1, r2, r3 = _poly_getnoise_eta1_4x(r0, r1, r2, r3, seed, nonce); -} + () = #spill(rp); + i=0; while(i < MLKEM_N){ r[i] = (u16)[rp + 2*i]; i += 1; } + start = tsc(); + r = _poly_frommsg(r, ap); -export fn polyvec_decompress_jazz(reg u64 rp, reg u64 ap) -{ - stack u16[MLKEM_VECN] r; + end = tsc(); - r = __polyvec_decompress(ap); + () = #unspill(rp); + i=0; while(i < MLKEM_N){ (u16)[rp + 2*i] = r[i]; i += 1; } + + t = cycles(start, end); + return t; } -export fn polyvec_compress_jazz(reg u64 rp, reg u64 ap) +export fn poly_compress_jazz(reg u64 rp ap) -> reg u64 { - stack u16[MLKEM_VECN] a; + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_N] a; + reg u64 i; - __polyvec_compress(rp, a); -} + () = #spill(ap); + i=0; while(i < MLKEM_N){ a[i] = (u16)[ap + 2*i]; i += 1; } + start = tsc(); -export fn polyvec_pointwise_acc_jazz(reg u64 rp, reg u64 ap, reg u64 bp) + a = _poly_compress(rp, a); + + end = tsc(); + + () = #unspill(ap); + i=0; while(i < MLKEM_N){ (u16)[ap + 2*i] = a[i]; i += 1; } + + t = cycles(start, end); + return t; +} + +export fn poly_decompress_jazz(reg u64 rp ap) -> reg u64 { - stack u16[MLKEM_VECN] a; - stack u16[MLKEM_VECN] b; + stack u32[2] start end; + reg u64 t; stack u16[MLKEM_N] r; + reg u64 i; - r = __polyvec_pointwise_acc(r, a, b); -} + () = #spill(rp); + i=0; while(i < MLKEM_N){ r[i] = (u16)[rp + 2*i]; i += 1; } + start = tsc(); + + r = _poly_decompress(r, ap); + + end = tsc(); + + () = #unspill(rp); + i=0; while(i < MLKEM_N){ (u16)[rp + 2*i] = r[i]; i += 1; } + + t = cycles(start, end); + return t; -export fn indcpa_keypair_jazz(reg u64 pkp, reg u64 skp, reg u64 randomnessp) -{ - //__indcpa_keypair(pkp, skp, randomnessp); } +// ////////////////////////////////////////////////////////////////// -export fn indcpa_enc_jazz(reg u64 ctp, reg u64 msgp, reg u64 pkp, reg u64 coinsp) +export fn polyvec_pointwise_acc_jazz(reg u64 rp ap bp) -> reg u64 { - stack u16[MLKEM_VECN] pkpv sp ep bp; - stack u16[MLKEM_K*MLKEM_VECN] aat; - stack u16[MLKEM_N] k epp v; - stack u8[MLKEM_SYMBYTES] publicseed; - stack u8[MLKEM_SYMBYTES] noiseseed; + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_VECN] a; + stack u16[MLKEM_VECN] b; + stack u16[MLKEM_N] r; reg u64 i; - reg u8 c nonce; - stack u64 sctp; - sctp = ctp; + () = #spill(rp); + i=0; while(i < MLKEM_VECN){ a[i] = (u16)[ap + 2*i]; i += 1; } + i=0; while(i < MLKEM_VECN){ b[i] = (u16)[bp + 2*i]; i += 1; } - i = 0; - while (i < MLKEM_SYMBYTES) - { - c = (u8)[coinsp+i]; - noiseseed[(int)i] = c; - i += 1; - } + start = tsc(); - pkpv = __polyvec_frombytes(pkp); + r = __polyvec_pointwise_acc(r, a, b); - i = 0; - pkp += MLKEM_POLYVECBYTES; - while (i < MLKEM_SYMBYTES) - { - c = (u8)[pkp]; - publicseed[(int)i] = c; - pkp += 1; - i += 1; - } + end = tsc(); - k = _poly_frommsg(k, msgp); + () = #unspill(rp); + i=0; while(i < MLKEM_N){ (u16)[rp + 2*i] = r[i]; i += 1; } - aat = __gen_matrix(publicseed, 1); + t = cycles(start, end); + return t; +} - nonce = 0; - sp[0:MLKEM_N], sp[MLKEM_N:MLKEM_N], sp[2*MLKEM_N:MLKEM_N], ep[0:MLKEM_N] = _poly_getnoise_eta1_4x(sp[0:MLKEM_N], sp[MLKEM_N:MLKEM_N], sp[2*MLKEM_N:MLKEM_N], ep[0:MLKEM_N], noiseseed, nonce); +export fn polyvec_compress_jazz(reg u64 rp ap) -> reg u64 +{ + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_VECN] a; + reg u64 i; - nonce = 4; - ep[MLKEM_N:MLKEM_N], ep[2*MLKEM_N:MLKEM_N], epp, bp[0:MLKEM_N] = _poly_getnoise_eta1_4x(ep[MLKEM_N:MLKEM_N], ep[2*MLKEM_N:MLKEM_N], epp, bp[0:MLKEM_N], noiseseed, nonce); + i=0; while(i < MLKEM_VECN){ a[i] = (u16)[ap + 2*i]; i += 1; } - sp = __polyvec_ntt(sp); - - bp[0:MLKEM_N] = __polyvec_pointwise_acc(bp[0:MLKEM_N], aat[0:MLKEM_VECN], sp); - bp[MLKEM_N:MLKEM_N]= __polyvec_pointwise_acc(bp[MLKEM_N:MLKEM_N], aat[MLKEM_VECN:MLKEM_VECN], sp); - bp[2*MLKEM_N:MLKEM_N] = __polyvec_pointwise_acc(bp[2*MLKEM_N:MLKEM_N], aat[2*MLKEM_VECN:MLKEM_VECN], sp); - - v = __polyvec_pointwise_acc(v, pkpv, sp); + start = tsc(); - bp = __polyvec_invntt(bp); - v = _poly_invntt(v); + __polyvec_compress(rp, a); - bp = __polyvec_add2(bp, ep); - v = _poly_add2(v, epp); - v = _poly_add2(v, k); - bp = __polyvec_reduce(bp); - v = __poly_reduce(v); + end = tsc(); - ctp = sctp; - __polyvec_compress(ctp, bp); - ctp += MLKEM_POLYVECCOMPRESSEDBYTES; - v = _poly_compress(ctp, v); + t = cycles(start, end); + return t; } - -export fn indcpa_dec_jazz(reg u64 msgp, reg u64 ctp, reg u64 skp) +export fn polyvec_decompress_jazz(reg u64 rp ap) -> reg u64 { - __indcpa_dec_0(msgp, ctp, skp); + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_VECN] r; + reg u64 i; + + () = #spill(rp); + start = tsc(); + + r = __polyvec_decompress(ap); + + end = tsc(); + + () = #unspill(rp); + i=0; while(i < MLKEM_N){ (u16)[rp + 2*i] = r[i]; i += 1; } + + t = cycles(start, end); + return t; } -export fn crypto_kem_keypair_jazz(reg u64 pkp, reg u64 skp, reg u64 randomnessp) +// ////////////////////////////////////////////////////////////////// + +export fn crypto_kem_keypair_jazz(reg u64 pkp skp, reg ptr u8[MLKEM_SYMBYTES*2] randomnessp) { - //__crypto_kem_keypair_jazz(pkp, skp, randomnessp); + __crypto_kem_keypair_jazz(pkp, skp, randomnessp); } - -export fn crypto_kem_enc_jazz(reg u64 ctp, reg u64 shkp, reg u64 pkp, reg u64 randomnessp) +export fn crypto_kem_enc_jazz(reg u64 ctp shkp pkp, reg ptr u8[MLKEM_SYMBYTES] randomnessp) { - //__crypto_kem_enc_jazz(ctp, shkp, pkp, randomnessp); + __crypto_kem_enc_jazz(ctp, shkp, pkp, randomnessp); } -export fn crypto_kem_dec_jazz(reg u64 shkp, reg u64 ctp, reg u64 skp) +export fn crypto_kem_dec_jazz(reg u64 shkp ctp skp) { __crypto_kem_dec_jazz(shkp, ctp, skp); } + diff --git a/code/jasmin/mlkem_avx2/kem.h b/code/jasmin/mlkem_avx2/kem.h index c86b2540..130c142d 100644 --- a/code/jasmin/mlkem_avx2/kem.h +++ b/code/jasmin/mlkem_avx2/kem.h @@ -16,24 +16,24 @@ void crypto_kem_dec(unsigned char *m, const unsigned char *c, const unsigned char *sk); -void jade_kem_mlkem_mlkem768_amd64_avx2v_keypair_derand(unsigned char *pk, +void jade_kem_mlkem_mlkem768_amd64_avx2_keypair_derand(unsigned char *pk, unsigned char *sk, const unsigned char *randomness); -void jade_kem_mlkem_mlkem768_amd64_avx2v_enc_derand(unsigned char *c, +void jade_kem_mlkem_mlkem768_amd64_avx2_enc_derand(unsigned char *c, const unsigned char *m, const unsigned char *pk, const unsigned char *coins); -void jade_kem_mlkem_mlkem768_amd64_avx2v_keypair(unsigned char *pk, +void jade_kem_mlkem_mlkem768_amd64_avx2_keypair(unsigned char *pk, unsigned char *sk); -void jade_kem_mlkem_mlkem768_amd64_avx2v_enc(unsigned char *c, +void jade_kem_mlkem_mlkem768_amd64_avx2_enc(unsigned char *c, const unsigned char *m, const unsigned char *pk); -void jade_kem_mlkem_mlkem768_amd64_avx2v_dec(unsigned char *m, +void jade_kem_mlkem_mlkem768_amd64_avx2_dec(unsigned char *m, const unsigned char *c, const unsigned char *sk); diff --git a/code/jasmin/mlkem_avx2/kem.jinc b/code/jasmin/mlkem_avx2/kem.jinc index 7be45bb2..96df10f0 100644 --- a/code/jasmin/mlkem_avx2/kem.jinc +++ b/code/jasmin/mlkem_avx2/kem.jinc @@ -25,12 +25,10 @@ fn __crypto_kem_keypair_jazz(reg u64 pkp, reg u64 skp, reg ptr u8[MLKEM_SYMBYTES for i=0 to MLKEM_INDCPA_PUBLICKEYBYTES/8 { - t64 = (u64)[pkp + 8*i]; - (u64)[skp] = t64; - skp += 8; + (u64)[skp + 8 * i] = (u64)[pkp + 8 * i]; } - s_skp = skp; + s_skp += MLKEM_POLYVECBYTES + MLKEM_INDCPA_PUBLICKEYBYTES; pkp = s_pkp; t64 = MLKEM_PUBLICKEYBYTES; @@ -39,9 +37,7 @@ fn __crypto_kem_keypair_jazz(reg u64 pkp, reg u64 skp, reg ptr u8[MLKEM_SYMBYTES for i=0 to 4 { - t64 = h_pk[u64 i]; - (u64)[skp] = t64; - skp += 8; + (u64)[skp + 8 * i] = h_pk[u64 i]; } randomnessp = s_randomnessp; @@ -49,9 +45,7 @@ fn __crypto_kem_keypair_jazz(reg u64 pkp, reg u64 skp, reg ptr u8[MLKEM_SYMBYTES for i=0 to MLKEM_SYMBYTES/8 { - t64 = randomnessp2[u64 i]; - (u64)[skp] = t64; - skp += 8; + (u64)[skp + 8 * i + 32] = randomnessp2[u64 i]; } } diff --git a/code/jasmin/mlkem_avx2/ntt.h b/code/jasmin/mlkem_avx2/ntt.h index dd5498a2..eb24d751 100644 --- a/code/jasmin/mlkem_avx2/ntt.h +++ b/code/jasmin/mlkem_avx2/ntt.h @@ -8,7 +8,9 @@ extern int16_t zetas[128]; extern int16_t zetas_inv[128]; -void invntt(int16_t *poly); +void ntt(int16_t r[256]); +void invntt(int16_t r[256]); + void basemul(int16_t r[2], const int16_t a[2], const int16_t b[2], int16_t zeta); #define ntt_avx MLKEM_NAMESPACE(ntt_avx) @@ -39,7 +41,4 @@ void ntttobytes_avx(uint8_t *r, const int16_t *a, const uint16_t *qdata); #define nttfrombytes_avx MLKEM_NAMESPACE(nttfrombytes_avx) void nttfrombytes_avx(int16_t *r, const uint8_t *a, const uint16_t *qdata); - -void ntt(int16_t *poly); - #endif diff --git a/code/jasmin/mlkem_avx2/poly.h b/code/jasmin/mlkem_avx2/poly.h index a583f034..17960c94 100644 --- a/code/jasmin/mlkem_avx2/poly.h +++ b/code/jasmin/mlkem_avx2/poly.h @@ -22,7 +22,7 @@ void poly_frommsg(poly *r, const unsigned char msg[MLKEM_SYMBYTES]); void poly_tomsg(unsigned char msg[MLKEM_SYMBYTES], poly *r); void poly_getnoise_eta1(poly *r,const unsigned char *seed, unsigned char nonce); -void poly_getnoise_eta2(poly *r,const unsigned char *seed, unsigned char nonce); +void poly_getnoise_eta2(poly *r,const uint8_t seed[MLKEM_SYMBYTES], unsigned char nonce); void poly_ntt(poly *r); void poly_invntt(poly *r); diff --git a/code/jasmin/mlkem_avx2/speed.h b/code/jasmin/mlkem_avx2/speed.h index 070b30ac..e521f72d 100644 --- a/code/jasmin/mlkem_avx2/speed.h +++ b/code/jasmin/mlkem_avx2/speed.h @@ -12,28 +12,26 @@ typedef struct{ poly vec[MLKEM_K]; } polyvec; -void gen_matrix_jazz(polyvec *a, unsigned char *seed); +uint64_t gen_matrix_jazz(polyvec *a, unsigned char *seed); -/*Poly functions*/ -void poly_compress_jazz(unsigned char *r, poly *a); -void poly_decompress_jazz(poly *r, const unsigned char *a); +// Poly functions +uint64_t poly_getnoise_4x_jazz(poly *r0, poly *r1, poly *r2, poly *r3,const unsigned char *seed, unsigned char nonce); -void poly_frommsg_jazz(poly *r, const unsigned char msg[MLKEM_SYMBYTES]); -void poly_tomsg_jazz(unsigned char msg[MLKEM_SYMBYTES], poly *r); +uint64_t poly_ntt_jazz(poly *r); +uint64_t poly_invntt_jazz(poly *r); -void poly_getnoise_jazz(poly *r,const unsigned char *seed, unsigned char nonce); -void poly_getnoise_4x_jazz(poly *r0, poly *r1, poly *r2, poly *r3,const unsigned char *seed, unsigned char nonce); +uint64_t poly_frommsg_jazz(poly *r, const unsigned char msg[MLKEM_SYMBYTES]); +uint64_t poly_tomsg_jazz(unsigned char msg[MLKEM_SYMBYTES], poly *r); -void poly_ntt_jazz(poly *r); -void poly_invntt_jazz(poly *r); +uint64_t poly_compress_jazz(unsigned char *r, poly *a); +uint64_t poly_decompress_jazz(poly *r, const unsigned char *a); -/*Polyvec functions*/ -void polyvec_compress_jazz(unsigned char *r, polyvec *a); -void polyvec_decompress_jazz(polyvec *r, const unsigned char *a); +// Polyvec functions +uint64_t polyvec_pointwise_acc_jazz(poly *r, const polyvec *a, const polyvec *b); +uint64_t polyvec_compress_jazz(unsigned char *r, polyvec *a); +uint64_t polyvec_decompress_jazz(polyvec *r, const unsigned char *a); -void polyvec_pointwise_acc_jazz(poly *r, const polyvec *a, const polyvec *b); - -/* Indcpa functions*/ +// Indcpa functions void indcpa_keypair_jazz(unsigned char *pk, unsigned char *sk, const unsigned char *randomness); @@ -47,7 +45,7 @@ void indcpa_dec_jazz(unsigned char *m, const unsigned char *c, const unsigned char *sk); -/* KEM functions */ +// KEM functions void crypto_kem_keypair_jazz(unsigned char *pk, unsigned char *sk, const unsigned char *randomness); @@ -56,6 +54,7 @@ void crypto_kem_enc_jazz(unsigned char *c, const unsigned char *m, const unsigned char *pk, const unsigned char *coins); + void crypto_kem_dec_jazz(unsigned char *m, const unsigned char *c, const unsigned char *sk); diff --git a/code/jasmin/mlkem_avx2/test/speed_indcpa.c b/code/jasmin/mlkem_avx2/test/speed_indcpa.c deleted file mode 100644 index b1dc32f5..00000000 --- a/code/jasmin/mlkem_avx2/test/speed_indcpa.c +++ /dev/null @@ -1,100 +0,0 @@ -#include -#include -#include -#include - -#include "../params.h" -#include "../ntt.h" -#include "../indcpa.h" - -#define NRUNS 100 - -static inline uint64_t cpucycles(void) { - uint64_t result; - - asm volatile("rdtsc; shlq $32,%%rdx; orq %%rdx,%%rax" - : "=a" (result) : : "%rdx"); - - return result; -} - -static int cmp_uint64(const void *a, const void *b) { - if(*(uint64_t *)a < *(uint64_t *)b) return -1; - if(*(uint64_t *)a > *(uint64_t *)b) return 1; - return 0; -} - -static uint64_t median(uint64_t *l, size_t llen) { - qsort(l,llen,sizeof(uint64_t),cmp_uint64); - - if(llen%2) return l[llen/2]; - else return (l[llen/2-1]+l[llen/2])/2; -} - -static uint64_t average(uint64_t *t, size_t tlen) { - size_t i; - uint64_t acc=0; - - for(i=0;i #include #include +#include #include "../params.h" #include "../speed.h" -#define NRUNS 1000 +#define NRUNS 10000 static inline uint64_t cpucycles(void) { uint64_t result; @@ -72,6 +73,14 @@ void print_results(const char *s, uint64_t *t, size_t tlen) { printf("\n"); } +void print_results_jasmin(const char *s, uint64_t *t, size_t tlen) { + printf("%s\n", s); + printf("median: %llu cycles/ticks\n", (unsigned long long)median(t, tlen)); + printf("average: %llu cycles/ticks\n", (unsigned long long)average(t, tlen)); + printf("\n"); +} + + int main(void) { unsigned char sk[MLKEM_INDCPA_SECRETKEYBYTES]; @@ -86,134 +95,110 @@ int main(void) uint8_t seed[MLKEM_SYMBYTES] = {0}; poly ap; - FILE *urandom = fopen("/dev/urandom", "r"); - fread(randomness0, MLKEM_SYMBYTES, 1, urandom); - fread(randomness1, MLKEM_SYMBYTES, 1, urandom); - fread(message, MLKEM_SYMBYTES, 1, urandom); - uint64_t t[NRUNS], i; + size_t ri; - /* Test gen_matrix */ - for(i=0;i +#include #include "../fips202.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + #define MAXINLEN 33 #define MAXOUTLEN 168 int main(void) { + int test_ok = 1, test_ok_shake256_128_33 = 1, test_ok_sha3512_32 = 1, + test_ok_shake128_absorb34 = 1, test_ok_shake128_squeezeblock = 1; + size_t test_iteration = 0; unsigned char in[MAXINLEN]; unsigned char out0[MAXOUTLEN]; unsigned char out1[MAXOUTLEN]; @@ -14,35 +22,83 @@ int main(void) int k; FILE *urandom = fopen("/dev/urandom", "r"); - fread(in, 1, sizeof(in), urandom); - shake256(out0, 128, in, 33); - shake256_128_33_jazz(out1, in); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + size_t ri = fread(in, 1, sizeof(in), urandom); + assert(ri == sizeof(in)); + + // + shake256(out0, 128, in, 33); + shake256_128_33_jazz(out1, in); - for(k=0;k<128;k++) - if(out0[k] != out1[k]) printf("error shake256 at %d: %d %d\n", k, out0[k], out1[k]); + for(k=0;k<128;k++) + { if(out0[k] != out1[k]) + { fprintf(stderr, "ERROR: shake256_128_33 at %d: %d %d\n", k, out0[k], out1[k]); + test_ok_shake256_128_33 = 0; + test_ok = 0; + } + } - sha3_512(out0, in, 32); - sha3_512_32_jazz(out1, in); + // + sha3_512(out0, in, 32); + sha3_512_32_jazz(out1, in); - for(k=0;k<64;k++) - if(out0[k] != out1[k]) printf("error sha3512 at %d: %d %d\n", k, out0[k], out1[k]); + for(k=0;k<64;k++) + { if(out0[k] != out1[k]) + { fprintf(stderr, "ERROR: sha3512 at %d: %d %d\n", k, out0[k], out1[k]); + test_ok_sha3512_32 = 0; + test_ok = 0; + } + } - shake128_absorb(state0, in, 34); - shake128_absorb34_jazz(state1, in); + // + shake128_absorb(state0, in, 34); + shake128_absorb34_jazz(state1, in); - for(k=0;k<25;k++) - if(state0[k] != state1[k]) printf("error shake128_absorb at %d: %lu %lu\n", k, state0[k], state1[k]); + for(k=0;k<25;k++) + { if(state0[k] != state1[k]) + { fprintf(stderr, "ERROR: shake128_absorb at %d: %lu %lu\n", k, state0[k], state1[k]); + test_ok_shake128_absorb34 = 0; + test_ok = 0; + } + } - shake128_squeezeblocks(out0, 1, state0); - shake128_squeezeblock_jazz(out1, state1); + // + shake128_squeezeblocks(out0, 1, state0); + shake128_squeezeblock_jazz(out1, state1); - for(k=0;k<25;k++) - if(state0[k] != state1[k]) printf("error shake128_squeezeblock (state) at %d: %lu %lu\n", k, state0[k], state1[k]); + for(k=0;k<25;k++) + { if(state0[k] != state1[k]) + { fprintf(stderr, "ERROR: shake128_squeezeblock (state) at %d: %lu %lu\n", k, state0[k], state1[k]); + test_ok_shake128_squeezeblock = 0; + test_ok = 0; + } + } - for(k=0;k - +#include #include "../params.h" #include "../ntt.h" #include "../indcpa.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + int main(void) { + int test_ok = 1, test_ok_indcpa_keypair_sk = 1, test_ok_indcpa_keypair_pk = 1, + test_ok_indcpa_enc = 1, test_ok_indcpa_dec = 1, test_ok_decryption = 1; + size_t test_iteration = 0; + size_t ri; + unsigned char sk0[MLKEM_INDCPA_SECRETKEYBYTES]; unsigned char sk1[MLKEM_INDCPA_SECRETKEYBYTES]; unsigned char pk0[MLKEM_INDCPA_PUBLICKEYBYTES]; @@ -25,38 +34,88 @@ int main(void) unsigned char outmsg1[MLKEM_POLYVECBYTES]; FILE *urandom = fopen("/dev/urandom", "r"); - fread(randomness0, MLKEM_SYMBYTES, 1, urandom); - fread(randomness1, MLKEM_SYMBYTES, 1, urandom); - fread(message, MLKEM_SYMBYTES, 1, urandom); - fclose(urandom); - /* TEST KEYPAIR */ - indcpa_keypair_jazz(pk1, sk1, randomness0); - indcpa_keypair(pk0, sk0, randomness0); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + ri = fread(randomness0, MLKEM_SYMBYTES, 1, urandom); + assert(ri == 1); - for(int i=0;i -#include +#include +#include #include "../params.h" #include "../ntt.h" #include "../kem.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + int main(void) { + int test_ok = 1, test_ok_kem_keypair_sk = 1, test_ok_kem_keypair_pk = 1, + test_ok_kem_enc_ct = 1, test_ok_kem_enc_ss = 1, + test_ok_kem_dec_success = 1, test_ok_kem_dec_failure = 1; + size_t test_iteration = 0; + size_t ri; + unsigned char sk0[MLKEM_SECRETKEYBYTES]; unsigned char sk1[MLKEM_SECRETKEYBYTES]; unsigned char pk0[MLKEM_PUBLICKEYBYTES]; @@ -20,52 +31,108 @@ int main(void) unsigned char randomness1[2*MLKEM_SYMBYTES]; FILE *urandom = fopen("/dev/urandom", "r"); - fread(randomness0, 2*MLKEM_SYMBYTES, 1, urandom); - fread(randomness1, 2*MLKEM_SYMBYTES, 1, urandom); - fclose(urandom); - - /* TEST KEYPAIR */ - jade_kem_mlkem_mlkem768_amd64_avx2v_keypair_derand(pk1, sk1, randomness0); - crypto_kem_keypair(pk0, sk0, randomness0); - - for(int i=0;i #include "../poly.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;icoeffs[i] %= MLKEM_Q; - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly a, b, r0; - poly_setrandom(&a); - poly_setrandom(&b); - - poly_add(&r0, &a, &b); - - poly_add2_jazz(&a, &b); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom(&a); + poly_setrandom(&b); + + poly_add(&r0, &a, &b); + + poly_add2_jazz(&a, &b); + + for(int i=0;icoeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;icoeffs[i] %= MLKEM_Q; - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly a, b, r0, r1; - poly_setrandom(&a); - poly_setrandom(&b); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom(&a); + poly_setrandom(&b); + + poly_basemul(&r0, &a, &b); + + poly_basemul_jazz(&r1, &a, &b); + + for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - fclose(urandom); - poly_reduce(r); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; unsigned char out0[128]; unsigned char out1[128]; poly a; - poly_setrandom(&a); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom_nomodq(&a); - poly_compress(out0, &a); - poly_compress_jazz(out1, &a); + poly_compress(out0, &a); + poly_compress_jazz(out1, &a); - for(int i=0;i<128;i++) - { - if(out0[i] != out1[i]) - printf("error compress %d, %d, %d\n", i, out0[i], out1[i]); + for(int i=0;i<128;i++) + { if(out0[i] != out1[i]) + { fprintf(stderr, "ERROR: poly_compress: %d, %d, %d\n", i, out0[i], out1[i]); + test_ok = 0; + } + } + + test_iteration += 1; } + if(test_ok == 1) + { printf("OK: poly_compress\n"); } + return 0; } diff --git a/code/jasmin/mlkem_avx2/test/test_poly_csubq.c b/code/jasmin/mlkem_avx2/test/test_poly_csubq.c index fbaf8478..aa56ba63 100644 --- a/code/jasmin/mlkem_avx2/test/test_poly_csubq.c +++ b/code/jasmin/mlkem_avx2/test/test_poly_csubq.c @@ -1,32 +1,42 @@ #include +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - fclose(urandom); - poly_reduce(r); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly r0, r1; - poly_setrandom(&r0); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom_nomodq(&r0); - for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + int main(void) { + int test_ok = 1; + size_t test_iteration = 0; + size_t ri; unsigned char in[MLKEM_POLYCOMPRESSEDBYTES]; poly r0, r1; - - FILE *urandom = fopen("/dev/urandom", "r"); - fread(in, 1, MLKEM_POLYCOMPRESSEDBYTES, urandom); - fclose(urandom); - poly_decompress(&r0, in); - poly_decompress_jazz(&r1, in); + FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + int main(void) { + int test_ok = 1; + size_t test_iteration = 0; + size_t ri; unsigned char in[MLKEM_POLYBYTES]; poly r0, r1; - - FILE *urandom = fopen("/dev/urandom", "r"); - fread(in, 1, MLKEM_POLYBYTES, urandom); - fclose(urandom); - poly_frombytes(&r0, in); - poly_frombytes_jazz(&r1, in); + FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;icoeffs[i] %= MLKEM_Q; - } - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly r0, r1; - poly_setrandom(&r0); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom(&r0); + for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + int main(void) { + int test_ok = 1; + size_t test_iteration = 0; + size_t ri; unsigned char in[32]; poly r0, r1; - - FILE *urandom = fopen("/dev/urandom", "r"); - fread(in, 1, 32, urandom); - fclose(urandom); - poly_frommsg(&r0, in); - poly_frommsg_jazz(&r1, in); + FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" #include "../params.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif int main(void) { + int test_ok = 1, test_ok_poly_getnoise_eta1_4x = 1, + test_ok_poly_getnoise_eta1122_4x = 1; + size_t test_iteration = 0; + size_t ri; poly r0[4], r1[4]; unsigned char seed[MLKEM_SYMBYTES]; FILE *urandom = fopen("/dev/urandom", "r"); - fread(seed, 1, MLKEM_SYMBYTES, urandom); - fclose(urandom); - - poly_getnoise_eta1(r0, seed, 0); - poly_getnoise_eta1(&r0[1], seed, 1); - poly_getnoise_eta1(&r0[2], seed, 2); - poly_getnoise_eta1(&r0[3], seed, 3); - poly_getnoise_eta1_4x_jazz(r1, seed, 0); - for(int i=0;i<4;i++) + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) { - for(int j=0;j +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;icoeffs[i] %= MLKEM_Q; - } - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly r0, r1; - poly_setrandom(&r0); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom_mod2q(&r0); + for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;icoeffs[i] %= MLKEM_Q; - } - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly r0, r1; - poly_setrandom(&r0); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom_mod2q(&r0); - for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly r0, r1; - poly_setrandom(&r0); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom_nomodq(&r0); - for(int i=0;i +#include +#include "../poly.h" + +// note: extend to *_setrandom_open; *_setrandom; *_setrandom_close; +// to not open the file so many times + +void poly_setrandom(poly *r) +{ + FILE *urandom = fopen("/dev/urandom", "r"); + size_t ri = fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); + assert(ri == MLKEM_N); + for(int i=0;icoeffs[i] %= MLKEM_Q; } + fclose(urandom); +} + +void poly_setrandom_mod2q(poly *r) +{ + FILE *urandom = fopen("/dev/urandom", "r"); + size_t ri = fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); + assert(ri == MLKEM_N); + for(int i=0;icoeffs[i] %= 2*MLKEM_Q; } + fclose(urandom); +} + +void poly_setrandom_nomodq(poly *r) +{ + FILE *urandom = fopen("/dev/urandom", "r"); + size_t ri = fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); + assert(ri == MLKEM_N); + fclose(urandom); + poly_reduce(r); +} + +#endif diff --git a/code/jasmin/mlkem_avx2/test/test_poly_sub.c b/code/jasmin/mlkem_avx2/test/test_poly_sub.c index f46326f2..08510804 100644 --- a/code/jasmin/mlkem_avx2/test/test_poly_sub.c +++ b/code/jasmin/mlkem_avx2/test/test_poly_sub.c @@ -1,29 +1,40 @@ #include +#include #include "../poly.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;icoeffs[i] %= MLKEM_Q; - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly a, b, r0, r1; - poly_setrandom(&a); - poly_setrandom(&b); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom(&a); + poly_setrandom(&b); + + poly_sub(&r0, &a, &b); + + poly_sub_jazz(&r1, &a, &b); + + for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - fclose(urandom); - poly_reduce(r); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; unsigned char out0[MLKEM_POLYBYTES]; unsigned char out1[MLKEM_POLYBYTES]; poly a; - - poly_setrandom(&a); - - poly_tobytes(out0, &a); - poly_tobytes_jazz(out1, &a); - for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - fclose(urandom); - poly_reduce(r); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; unsigned char out0[MLKEM_INDCPA_MSGBYTES]; unsigned char out1[MLKEM_INDCPA_MSGBYTES]; poly a; - - poly_setrandom(&a); - - poly_tomsg(out0, &a); - poly_tomsg_jazz(out1, &a); - for(int i=0;i +#include #include "../polyvec.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;ivec[i].coeffs[j] %= MLKEM_Q; - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; polyvec a, b, r0; - polyvec_setrandom(&a); - polyvec_setrandom(&b); - - polyvec_add(&r0, &a, &b); - polyvec_add2_jazz(&a, &b); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + polyvec_setrandom(&a); + polyvec_setrandom(&b); + + polyvec_add(&r0, &a, &b); + polyvec_add2_jazz(&a, &b); + + for(int i=0;i +#include #include "../polyvec.h" #include "../ntt.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif - polyvec_reduce(r); - fclose(urandom); -} +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; unsigned char out0[MLKEM_POLYVECCOMPRESSEDBYTES]; unsigned char out1[MLKEM_POLYVECCOMPRESSEDBYTES]; polyvec a; - polyvec_setrandom(&a); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + polyvec_setrandom_reduce(&a); - polyvec_compress(out0, &a); - polyvec_compress_jazz(out1, &a); + polyvec_compress(out0, &a); + polyvec_compress_jazz(out1, &a); - for(int i=0;i +#include #include "../poly.h" #include "../polyvec.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); - fclose(urandom); - polyvec_reduce(r); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; polyvec r0, r1; - polyvec_setrandom(&r0); - - for(int i = 0;i +#include #include "../polyvec.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + int main(void) { + int test_ok = 1; + size_t test_iteration = 0; + size_t ri; + unsigned char in[MLKEM_POLYVECCOMPRESSEDBYTES]; polyvec r0, r1; - + FILE *urandom = fopen("/dev/urandom", "r"); - fread(in, 1, MLKEM_POLYVECCOMPRESSEDBYTES, urandom); - fclose(urandom); - polyvec_decompress(&r0, in); - polyvec_decompress_jazz(&r1, in); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + ri = fread(in, 1, MLKEM_POLYVECCOMPRESSEDBYTES, urandom); + assert(ri == MLKEM_POLYVECCOMPRESSEDBYTES); + + polyvec_decompress(&r0, in); + polyvec_decompress_jazz(&r1, in); + + for(int i=0;i +#include #include "../polyvec.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + int main(void) { + int test_ok = 1; + size_t test_iteration = 0; + size_t ri; unsigned char in[MLKEM_POLYVECBYTES]; polyvec r0, r1; - + FILE *urandom = fopen("/dev/urandom", "r"); - fread(in, 1, MLKEM_POLYVECBYTES, urandom); - fclose(urandom); - polyvec_frombytes(&r0, in); - polyvec_frombytes_jazz(&r1, in); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + ri = fread(in, 1, MLKEM_POLYVECBYTES, urandom); + assert(ri == MLKEM_POLYVECBYTES); + + polyvec_frombytes(&r0, in); + polyvec_frombytes_jazz(&r1, in); + + for(int i=0;i +#include #include "../ntt.h" #include "../poly.h" #include "../polyvec.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;ivec[i].coeffs[j] %= MLKEM_Q; - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; polyvec r0, r1; - polyvec_setrandom(&r0); - - for(int i = 0;i +#include #include "../ntt.h" #include "../poly.h" #include "../polyvec.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;ivec[i].coeffs[j] %= 2*MLKEM_Q; - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; polyvec r0, r1; - polyvec_setrandom(&r0); - - for(int i = 0;i +#include #include "../ntt.h" #include "../polyvec.h" +#include "../poly.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;ivec[i].coeffs[j] %= MLKEM_Q; - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; polyvec a, b; poly r0, r1; - polyvec_setrandom(&a); - polyvec_setrandom(&b); - - polyvec_pointwise_acc(&r0, &a, &b); - polyvec_pointwise_acc_jazz(&r1, &a, &b); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + polyvec_setrandom(&a); + polyvec_setrandom(&b); + + polyvec_pointwise_acc(&r0, &a, &b); + polyvec_pointwise_acc_jazz(&r1, &a, &b); for(int j=0;j +#include #include "../poly.h" #include "../polyvec.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; polyvec r0, r1; - polyvec_setrandom(&r0); - - for(int i = 0;i +#include +#include "../polyvec.h" + +// note: extend to *_setrandom_open; *_setrandom; *_setrandom_close; +// to not open the file so many times + +void polyvec_setrandom(polyvec *r) +{ + FILE *urandom = fopen("/dev/urandom", "r"); + for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); + assert(ri == MLKEM_N); + } + for(int i=0;ivec[i].coeffs[j] %= MLKEM_Q; + fclose(urandom); +} + +void polyvec_setrandom_reduce(polyvec *r) +{ + FILE *urandom = fopen("/dev/urandom", "r"); + for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); + assert(ri == MLKEM_N); + } + polyvec_reduce(r); + fclose(urandom); +} + +void polyvec_setrandom_mod2q(polyvec *r) +{ + FILE *urandom = fopen("/dev/urandom", "r"); + for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); + assert(ri == MLKEM_N); + } + for(int i=0;ivec[i].coeffs[j] %= 2*MLKEM_Q; + fclose(urandom); +} + +void polyvec_setrandom_nomodq(polyvec *r) +{ + FILE *urandom = fopen("/dev/urandom", "r"); + for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); + assert(ri == MLKEM_N); + } + fclose(urandom); +} + +#endif diff --git a/code/jasmin/mlkem_avx2/test/test_polyvec_tobytes.c b/code/jasmin/mlkem_avx2/test/test_polyvec_tobytes.c index a23b160a..6a51f5c5 100644 --- a/code/jasmin/mlkem_avx2/test/test_polyvec_tobytes.c +++ b/code/jasmin/mlkem_avx2/test/test_polyvec_tobytes.c @@ -1,35 +1,42 @@ #include +#include #include "../polyvec.h" #include "../ntt.h" -#include "../reduce.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); - - polyvec_reduce(r); +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif - fclose(urandom); -} +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; unsigned char out0[MLKEM_POLYVECBYTES]; unsigned char out1[MLKEM_POLYVECBYTES]; polyvec a; - - polyvec_setrandom(&a); - polyvec_tobytes(out0, &a); - polyvec_tobytes_jazz(out1, &a); - - for(int i=0;i stack u32[2] +{ + reg u64 l h; + stack u32[2] t; + + h, l = #RDTSC(); + + t[0] = (32u) l; + t[1] = (32u) h; + + return t; +} + +inline fn cycles(stack u32[2] start end) -> reg u64 +{ + reg u64 t; + + t = end[u64 0]; + t -= start[u64 0]; + + return t; +} + diff --git a/code/jasmin/mlkem_ref/example/.gitignore b/code/jasmin/mlkem_ref/example/.gitignore new file mode 100644 index 00000000..7ff73178 --- /dev/null +++ b/code/jasmin/mlkem_ref/example/.gitignore @@ -0,0 +1,2 @@ +example +jkem.s diff --git a/code/jasmin/mlkem_ref/example/Makefile b/code/jasmin/mlkem_ref/example/Makefile new file mode 100644 index 00000000..011e0ef7 --- /dev/null +++ b/code/jasmin/mlkem_ref/example/Makefile @@ -0,0 +1,35 @@ +include ../../../Makefile.conf + +CC ?= /usr/bin/gcc +CFLAGS := -Wall -Wextra -g -O3 -fomit-frame-pointer + +default: run-example + +RANDOMBYTES := $(PROJECT_DIR)/ext/randombytes/jasmin_syscall.o +$(RANDOMBYTES): $(PROJECT_DIR)/ext/randombytes/jasmin_syscall.c $(PROJECT_DIR)/ext/randombytes/jasmin_syscall.h + $(MAKE) -C $(@D) + +.PHONY: ../jkem.s +../jkem.s: + $(MAKE) -C $(@D) $(@F) + +jkem.s: ../jkem.s + cp $< $@ + + +example: example.c jkem.s api.h $(RANDOMBYTES) + $(CC) $(CFLAGS) -o $@ example.c jkem.s $(RANDOMBYTES) + +run-example: example + ./example + + + +.PHONY: clean distclean +clean: + rm -f example jkem.s + +distclean: clean + rm -f ../jkem.s + $(MAKE) -C $(dir $(RANDOMBYTES)) clean + diff --git a/code/jasmin/mlkem_ref/example/api.h b/code/jasmin/mlkem_ref/example/api.h new file mode 100644 index 00000000..5768789c --- /dev/null +++ b/code/jasmin/mlkem_ref/example/api.h @@ -0,0 +1,47 @@ +#ifndef JADE_KEM_mlkem_mlkem768_amd64_ref_API_H +#define JADE_KEM_mlkem_mlkem768_amd64_ref_API_H + +#include + +#define JADE_KEM_mlkem_mlkem768_amd64_ref_SECRETKEYBYTES 2400 +#define JADE_KEM_mlkem_mlkem768_amd64_ref_PUBLICKEYBYTES 1184 +#define JADE_KEM_mlkem_mlkem768_amd64_ref_CIPHERTEXTBYTES 1088 +#define JADE_KEM_mlkem_mlkem768_amd64_ref_KEYPAIRCOINBYTES 64 +#define JADE_KEM_mlkem_mlkem768_amd64_ref_ENCCOINBYTES 32 +#define JADE_KEM_mlkem_mlkem768_amd64_ref_BYTES 32 + +#define JADE_KEM_mlkem_mlkem768_amd64_ref_ALGNAME "mlkem768" +#define JADE_KEM_mlkem_mlkem768_amd64_ref_ARCH "amd64" +#define JADE_KEM_mlkem_mlkem768_amd64_ref_IMPL "ref" + +int jade_kem_mlkem_mlkem768_amd64_ref_keypair_derand( + uint8_t *public_key, + uint8_t *secret_key, + const uint8_t *coins +); + +int jade_kem_mlkem_mlkem768_amd64_ref_keypair( + uint8_t *public_key, + uint8_t *secret_key +); + +int jade_kem_mlkem_mlkem768_amd64_ref_enc_derand( + uint8_t *ciphertext, + uint8_t *shared_secret, + const uint8_t *public_key, + const uint8_t *coins +); + +int jade_kem_mlkem_mlkem768_amd64_ref_enc( + uint8_t *ciphertext, + uint8_t *shared_secret, + const uint8_t *public_key +); + +int jade_kem_mlkem_mlkem768_amd64_ref_dec( + uint8_t *shared_secret, + const uint8_t *ciphertext, + const uint8_t *secret_key +); + +#endif diff --git a/code/jasmin/mlkem_ref/example/example.c b/code/jasmin/mlkem_ref/example/example.c new file mode 100644 index 00000000..a92e2d1b --- /dev/null +++ b/code/jasmin/mlkem_ref/example/example.c @@ -0,0 +1,139 @@ +#include +#include +#include +#include +#include + +#include "api.h" + +// print functions +static void print_info(const char *algname, const char *arch, const char *impl) +{ + printf("// {\"%s\" : { architecture : \"%s\", implementation : \"%s\"} }", + algname, arch, impl); + printf("\n"); +} + +static void print_u8(const uint8_t *a, size_t l) +{ + size_t i; + + if(l == 0) + { return; } + + printf("{\n "); + for(i=0; i<(l-1); i++) + { printf("0x%02" PRIx8 ", ", a[i]); + if((i+1)%16 == 0) + { printf("\n "); } + } + + printf("0x%02" PRIx8 "\n};\n", a[i]); + return; +} + +static void print_str_u8(const char *str, const uint8_t *a, size_t l) +{ + if( l == 0 ) + { printf("uint8_t *%s = NULL;\n", str); + return; + } + + printf("uint8_t %s[%zu] = ",str, l); + print_u8(a, l); +} + +// randombytes implementation, in this case we use the __jasmin_syscall_randombytes__ +extern uint8_t* __jasmin_syscall_randombytes__(uint8_t* x, uint64_t xlen); + +uint8_t* randombytes(uint8_t* x, uint64_t xlen) +{ + return __jasmin_syscall_randombytes__(x, xlen); +} + +// mapping the fully namespaced macros from api.h into shorter names +#define JADE_KEM_SECRETKEYBYTES JADE_KEM_mlkem_mlkem768_amd64_ref_SECRETKEYBYTES +#define JADE_KEM_PUBLICKEYBYTES JADE_KEM_mlkem_mlkem768_amd64_ref_PUBLICKEYBYTES +#define JADE_KEM_CIPHERTEXTBYTES JADE_KEM_mlkem_mlkem768_amd64_ref_CIPHERTEXTBYTES +#define JADE_KEM_KEYPAIRCOINBYTES JADE_KEM_mlkem_mlkem768_amd64_ref_KEYPAIRCOINBYTES +#define JADE_KEM_ENCCOINBYTES JADE_KEM_mlkem_mlkem768_amd64_ref_ENCCOINBYTES +#define JADE_KEM_BYTES JADE_KEM_mlkem_mlkem768_amd64_ref_BYTES + +#define jade_kem_keypair jade_kem_mlkem_mlkem768_amd64_ref_keypair +#define jade_kem_enc jade_kem_mlkem_mlkem768_amd64_ref_enc +#define jade_kem_dec jade_kem_mlkem_mlkem768_amd64_ref_dec + +#define jade_kem_keypair_derand jade_kem_mlkem_mlkem768_amd64_ref_keypair_derand +#define jade_kem_enc_derand jade_kem_mlkem_mlkem768_amd64_ref_enc_derand + +#define JADE_KEM_ALGNAME JADE_KEM_mlkem_mlkem768_amd64_ref_ALGNAME +#define JADE_KEM_ARCH JADE_KEM_mlkem_mlkem768_amd64_ref_ARCH +#define JADE_KEM_IMPL JADE_KEM_mlkem_mlkem768_amd64_ref_IMPL + +// this example program does the following: +// - creates a keypair (with the randomized api +// - encapsulates/decapsulates and checks that the shared secret is the same +// +// - it repeats the process using the derandomized ('derand') functions +// +int main(void) +{ + int r; + uint8_t public_key[JADE_KEM_PUBLICKEYBYTES]; + uint8_t secret_key[JADE_KEM_SECRETKEYBYTES]; + + uint8_t shared_secret_a[JADE_KEM_BYTES]; + uint8_t ciphertext[JADE_KEM_CIPHERTEXTBYTES]; + uint8_t shared_secret_b[JADE_KEM_BYTES]; + + uint8_t keypair_coins[JADE_KEM_KEYPAIRCOINBYTES]; + uint8_t enc_coins[JADE_KEM_ENCCOINBYTES]; + + // create key pair + r = jade_kem_keypair(public_key, secret_key); + assert(r == 0); + + // encapsulate + r = jade_kem_enc(ciphertext, shared_secret_a, public_key); + assert(r == 0); + + // decapsulate + r = jade_kem_dec(shared_secret_b, ciphertext, secret_key); + assert(r == 0); + assert(memcmp(shared_secret_a, shared_secret_b, JADE_KEM_BYTES) == 0); + + print_info(JADE_KEM_ALGNAME, JADE_KEM_ARCH, JADE_KEM_IMPL); + print_str_u8("secret_key", secret_key, JADE_KEM_SECRETKEYBYTES); + print_str_u8("public_key", public_key, JADE_KEM_PUBLICKEYBYTES); + print_str_u8("ciphertext", ciphertext, JADE_KEM_CIPHERTEXTBYTES); + print_str_u8("shared_secret", shared_secret_a, JADE_KEM_BYTES); + + // create key pair using derand function (random coins are given as input) + randombytes(keypair_coins, JADE_KEM_KEYPAIRCOINBYTES); + r = jade_kem_keypair_derand(public_key, secret_key, keypair_coins); + assert(r == 0); + + // encapsulate using derand function (random coins are given as input) + randombytes(enc_coins, JADE_KEM_ENCCOINBYTES); + r = jade_kem_enc_derand(ciphertext, shared_secret_a, public_key, enc_coins); + assert(r == 0); + + // decapsulate + r = jade_kem_dec(shared_secret_b, ciphertext, secret_key); + assert(r == 0); + assert(memcmp(shared_secret_a, shared_secret_b, JADE_KEM_BYTES) == 0); + + print_info(JADE_KEM_ALGNAME, JADE_KEM_ARCH, JADE_KEM_IMPL); + print_str_u8("keypair_derand_coins", keypair_coins, JADE_KEM_KEYPAIRCOINBYTES); + print_str_u8("secret_key_derand", secret_key, JADE_KEM_SECRETKEYBYTES); + print_str_u8("public_key_derand", public_key, JADE_KEM_PUBLICKEYBYTES); + + print_str_u8("enc_derand_coins", enc_coins, JADE_KEM_ENCCOINBYTES); + print_str_u8("ciphertext_derand", ciphertext, JADE_KEM_CIPHERTEXTBYTES); + print_str_u8("shared_secret_derand", shared_secret_a, JADE_KEM_BYTES); + + + + return 0; +} + diff --git a/code/jasmin/mlkem_ref/gen_matrix.jazz b/code/jasmin/mlkem_ref/gen_matrix.jazz index 444017dc..ae7012ea 100644 --- a/code/jasmin/mlkem_ref/gen_matrix.jazz +++ b/code/jasmin/mlkem_ref/gen_matrix.jazz @@ -1,3 +1,4 @@ +require "params.jinc" require "gen_matrix.jinc" export fn gen_matrix_jazz(reg u64 ap, reg u64 seedp, reg u64 transposed) @@ -11,6 +12,7 @@ export fn gen_matrix_jazz(reg u64 ap, reg u64 seedp, reg u64 transposed) for i = 0 to MLKEM_SYMBYTES { + #[declassify] c = (u8)[seedp + i]; seed[i] = c; } diff --git a/code/jasmin/mlkem_ref/jpoly.jazz b/code/jasmin/mlkem_ref/jpoly.jazz index 7d72519d..4ccd1492 100644 --- a/code/jasmin/mlkem_ref/jpoly.jazz +++ b/code/jasmin/mlkem_ref/jpoly.jazz @@ -7,9 +7,7 @@ export fn poly_compress_jazz(reg u64 rp, reg u64 ap) { inline int i; reg u16 t; - reg u8 c; stack u16[MLKEM_N] a; - stack u8[128] r; for i = 0 to MLKEM_N { t = (u16)[ap + 2*i]; @@ -23,9 +21,7 @@ export fn poly_decompress_jazz(reg u64 rp, reg u64 ap) { inline int i; reg u16 t; - reg u8 c; stack u16[MLKEM_N] r; - stack u8[128] a; r = _poly_decompress(r, ap); @@ -39,7 +35,6 @@ export fn poly_tobytes_jazz(reg u64 rp, reg u64 ap) { inline int i; reg u16 t; - reg u8 c; stack u16[MLKEM_N] a; for i = 0 to MLKEM_N { @@ -54,7 +49,6 @@ export fn poly_frombytes_jazz(reg u64 rp, reg u64 ap) { inline int i; reg u16 t; - reg u8 c; stack u16[MLKEM_N] r; r = _poly_frombytes(r, ap); @@ -69,9 +63,7 @@ export fn poly_tomsg_jazz(reg u64 rp, reg u64 ap) { inline int i; reg u16 t; - reg u8 c; stack u16[MLKEM_N] a; - stack u8[32] r; for i = 0 to MLKEM_N { t = (u16)[ap + 2*i]; @@ -85,7 +77,6 @@ export fn poly_frommsg_jazz(reg u64 rp, reg u64 ap) { inline int i; reg u16 t; - reg u8 c; stack u16[MLKEM_N] r; r = _poly_frommsg(r, ap); diff --git a/code/jasmin/mlkem_ref/jpolyvec.jazz b/code/jasmin/mlkem_ref/jpolyvec.jazz index d4080f03..b34cce62 100644 --- a/code/jasmin/mlkem_ref/jpolyvec.jazz +++ b/code/jasmin/mlkem_ref/jpolyvec.jazz @@ -7,7 +7,6 @@ export fn polyvec_tobytes_jazz(reg u64 rp, reg u64 ap) { inline int i; reg u16 t; - reg u8 c; stack u16[MLKEM_VECN] a; for i = 0 to MLKEM_VECN { @@ -23,7 +22,6 @@ export fn polyvec_decompress_jazz(reg u64 rp, reg u64 ap) { inline int i; reg u16 t; - reg u8 c; stack u16[MLKEM_VECN] r; r = __polyvec_decompress(ap); @@ -39,7 +37,6 @@ export fn polyvec_compress_jazz(reg u64 rp, reg u64 ap) { inline int i; reg u16 t; - reg u8 c; stack u16[MLKEM_VECN] a; for i = 0 to MLKEM_VECN { @@ -55,7 +52,6 @@ export fn polyvec_frombytes_jazz(reg u64 rp, reg u64 ap) { inline int i; reg u16 t; - reg u8 c; stack u16[MLKEM_VECN] r; r = __polyvec_frombytes(ap); diff --git a/code/jasmin/mlkem_ref/jspeed.jazz b/code/jasmin/mlkem_ref/jspeed.jazz new file mode 100644 index 00000000..d03fa4b0 --- /dev/null +++ b/code/jasmin/mlkem_ref/jspeed.jazz @@ -0,0 +1,297 @@ +require "poly.jinc" +require "polyvec.jinc" +require "gen_matrix.jinc" +require "indcpa.jinc" +require "kem.jinc" +require "verify.jinc" + +require "cycles.jinc" + +// note: this code needs to be reviewed and properly tested + +// exported functions only for benchmarking + +export fn gen_matrix_jazz(reg u64 ap seedp) -> reg u64 +{ + stack u32[2] start end; + reg u64 t; + stack u64 aps; + stack u16[MLKEM_K*MLKEM_VECN] a; + stack u8[MLKEM_SYMBYTES] seed; + reg u64 i; + + aps = ap; + i=0; while(i < MLKEM_SYMBYTES){ seed[i] = (u8)[seedp + i]; i += 1; } + + start = tsc(); + + a = __gen_matrix(seed, 1); + + end = tsc(); + + ap = aps; + i=0; while(i < MLKEM_K*MLKEM_VECN){ (u16)[ap + 2*i] = a[i]; i += 1; } + + t = cycles(start, end); + return t; +} + +// ////////////////////////////////////////////////////////////////// + +export fn poly_getnoise_jazz(reg u64 rp, reg u64 seedp, reg u8 nonce) -> reg u64 +{ + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_N] r; + stack u8[MLKEM_SYMBYTES] seed; + reg u64 i; + + nonce = nonce; + () = #spill(rp); + i=0; while(i < MLKEM_SYMBYTES){ seed[i] = (u8)[seedp + i]; i += 1; } + + start = tsc(); + + r = _poly_getnoise(r, seed, nonce); + + end = tsc(); + + () = #unspill(rp); + i=0; while(i < MLKEM_N) + { (u16)[rp + 2*i] = r[i]; + i+= 1; + } + + t = cycles(start, end); + return t; +} + + +export fn poly_ntt_jazz(reg u64 rp) -> reg u64 +{ + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_N] r; + reg u64 i; + + () = #spill(rp); + i=0; while(i < MLKEM_N){ r[i] = (u16)[rp + 2*i]; i += 1; } + + start = tsc(); + + r = _poly_ntt(r); + + end = tsc(); + + () = #unspill(rp); + i=0; while(i < MLKEM_N){ (u16)[rp + 2*i] = r[i]; i += 1; } + + t = cycles(start, end); + return t; +} + + +export fn poly_invntt_jazz(reg u64 rp) -> reg u64 +{ + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_N] r; + reg u64 i; + + () = #spill(rp); + i=0; while(i < MLKEM_N){ r[i] = (u16)[rp + 2*i]; i += 1; } + + start = tsc(); + + r = _poly_invntt(r); + + end = tsc(); + + () = #unspill(rp); + i=0; while(i < MLKEM_N){ (u16)[rp + 2*i] = r[i]; i += 1; } + + t = cycles(start, end); + return t; +} + + +export fn poly_tomsg_jazz(reg u64 rp ap) -> reg u64 +{ + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_N] a; + reg u64 i; + + () = #spill(ap); + i=0; while(i < MLKEM_N){ a[i] = (u16)[ap + 2*i]; i += 1; } + + start = tsc(); + + a = _poly_tomsg(rp, a); + + end = tsc(); + + () = #unspill(ap); + i=0; while(i < MLKEM_N){ (u16)[ap + 2*i] = a[i]; i += 1; } + + t = cycles(start, end); + return t; +} + + +export fn poly_frommsg_jazz(reg u64 rp ap) -> reg u64 +{ + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_N] r; + reg u64 i; + + () = #spill(rp); + i=0; while(i < MLKEM_N){ r[i] = (u16)[rp + 2*i]; i += 1; } + + start = tsc(); + + r = _poly_frommsg(r, ap); + + end = tsc(); + + () = #unspill(rp); + i=0; while(i < MLKEM_N){ (u16)[rp + 2*i] = r[i]; i += 1; } + + t = cycles(start, end); + return t; +} + + +export fn poly_compress_jazz(reg u64 rp ap) -> reg u64 +{ + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_N] a; + reg u64 i; + + () = #spill(ap); + i=0; while(i < MLKEM_N){ a[i] = (u16)[ap + 2*i]; i += 1; } + + start = tsc(); + + a = _poly_compress(rp, a); + + end = tsc(); + + () = #unspill(ap); + i=0; while(i < MLKEM_N){ (u16)[ap + 2*i] = a[i]; i += 1; } + + t = cycles(start, end); + return t; +} + +export fn poly_decompress_jazz(reg u64 rp ap) -> reg u64 +{ + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_N] r; + reg u64 i; + + () = #spill(rp); + i=0; while(i < MLKEM_N){ r[i] = (u16)[rp + 2*i]; i += 1; } + + start = tsc(); + + r = _poly_decompress(r, ap); + + end = tsc(); + + () = #unspill(rp); + i=0; while(i < MLKEM_N){ (u16)[rp + 2*i] = r[i]; i += 1; } + + t = cycles(start, end); + return t; + +} + +// ////////////////////////////////////////////////////////////////// + +export fn polyvec_pointwise_acc_jazz(reg u64 rp ap bp) -> reg u64 +{ + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_VECN] a; + stack u16[MLKEM_VECN] b; + stack u16[MLKEM_N] r; + reg u64 i; + + () = #spill(rp); + i=0; while(i < MLKEM_VECN){ a[i] = (u16)[ap + 2*i]; i += 1; } + i=0; while(i < MLKEM_VECN){ b[i] = (u16)[bp + 2*i]; i += 1; } + + start = tsc(); + + r = __polyvec_pointwise_acc(a, b); + + end = tsc(); + + () = #unspill(rp); + i=0; while(i < MLKEM_N){ (u16)[rp + 2*i] = r[i]; i += 1; } + + t = cycles(start, end); + return t; +} + +export fn polyvec_compress_jazz(reg u64 rp ap) -> reg u64 +{ + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_VECN] a; + reg u64 i; + + i=0; while(i < MLKEM_VECN){ a[i] = (u16)[ap + 2*i]; i += 1; } + + start = tsc(); + + __polyvec_compress(rp, a); + + end = tsc(); + + t = cycles(start, end); + return t; +} + +export fn polyvec_decompress_jazz(reg u64 rp ap) -> reg u64 +{ + stack u32[2] start end; + reg u64 t; + stack u16[MLKEM_VECN] r; + reg u64 i; + + () = #spill(rp); + start = tsc(); + + r = __polyvec_decompress(ap); + + end = tsc(); + + () = #unspill(rp); + i=0; while(i < MLKEM_N){ (u16)[rp + 2*i] = r[i]; i += 1; } + + t = cycles(start, end); + return t; +} + +// ////////////////////////////////////////////////////////////////// + +export fn crypto_kem_keypair_jazz(reg u64 pkp skp, reg ptr u8[MLKEM_SYMBYTES*2] randomnessp) +{ + __crypto_kem_keypair_jazz(pkp, skp, randomnessp); +} + +export fn crypto_kem_enc_jazz(reg u64 ctp shkp pkp, reg ptr u8[MLKEM_SYMBYTES] randomnessp) +{ + __crypto_kem_enc_jazz(ctp, shkp, pkp, randomnessp); +} + +export fn crypto_kem_dec_jazz(reg u64 shkp ctp skp) +{ + __crypto_kem_dec_jazz(shkp, ctp, skp); +} + diff --git a/code/jasmin/mlkem_ref/kem.jinc b/code/jasmin/mlkem_ref/kem.jinc index 33dca3a1..889db0f2 100644 --- a/code/jasmin/mlkem_ref/kem.jinc +++ b/code/jasmin/mlkem_ref/kem.jinc @@ -25,12 +25,10 @@ fn __crypto_kem_keypair_jazz(reg u64 pkp, reg u64 skp, reg ptr u8[MLKEM_SYMBYTES for i=0 to MLKEM_INDCPA_PUBLICKEYBYTES/8 { - t64 = (u64)[pkp + 8*i]; - (u64)[skp] = t64; - skp += 8; + (u64)[skp + 8 * i] = (u64)[pkp + 8 * i]; } - s_skp = skp; + s_skp += MLKEM_POLYVECBYTES + MLKEM_INDCPA_PUBLICKEYBYTES; pkp = s_pkp; t64 = MLKEM_POLYVECBYTES + MLKEM_SYMBYTES; @@ -39,9 +37,7 @@ fn __crypto_kem_keypair_jazz(reg u64 pkp, reg u64 skp, reg ptr u8[MLKEM_SYMBYTES for i=0 to 4 { - t64 = h_pk[u64 i]; - (u64)[skp] = t64; - skp += 8; + (u64)[skp + 8 * i] = h_pk[u64 i]; } randomnessp = s_randomnessp; @@ -49,9 +45,7 @@ fn __crypto_kem_keypair_jazz(reg u64 pkp, reg u64 skp, reg ptr u8[MLKEM_SYMBYTES for i=0 to MLKEM_SYMBYTES/8 { - t64 = randomnessp2[u64 i]; - (u64)[skp] = t64; - skp += 8; + (u64)[skp + 8 * i + 32] = randomnessp2[u64 i]; } } diff --git a/code/jasmin/mlkem_ref/ntt.h b/code/jasmin/mlkem_ref/ntt.h index f7ad4605..aedaed09 100644 --- a/code/jasmin/mlkem_ref/ntt.h +++ b/code/jasmin/mlkem_ref/ntt.h @@ -6,10 +6,10 @@ extern int16_t zetas[128]; extern int16_t zetas_inv[128]; -void ntt(int16_t *poly); +void ntt(int16_t poly[256]); void splitntt(int16_t *poly); -void invntt(int16_t *poly); +void invntt(int16_t poly[256]); void basemul(int16_t r[2], const int16_t a[2], const int16_t b[2], int16_t zeta); #endif diff --git a/code/jasmin/mlkem_ref/speed.h b/code/jasmin/mlkem_ref/speed.h new file mode 100644 index 00000000..f03345d9 --- /dev/null +++ b/code/jasmin/mlkem_ref/speed.h @@ -0,0 +1,61 @@ +#ifndef SPEED_H +#define SPEED_H + +#include +#include "params.h" + +typedef struct{ + int16_t __attribute__((aligned(32))) coeffs[MLKEM_N]; +} poly; + +typedef struct{ + poly vec[MLKEM_K]; +} polyvec; + +uint64_t gen_matrix_jazz(polyvec *a, unsigned char *seed); + +// Poly functions +uint64_t poly_getnoise_jazz(poly *r,const unsigned char *seed, unsigned char nonce); + +uint64_t poly_ntt_jazz(poly *r); +uint64_t poly_invntt_jazz(poly *r); + +uint64_t poly_frommsg_jazz(poly *r, const unsigned char msg[MLKEM_SYMBYTES]); +uint64_t poly_tomsg_jazz(unsigned char msg[MLKEM_SYMBYTES], poly *r); + +uint64_t poly_compress_jazz(unsigned char *r, poly *a); +uint64_t poly_decompress_jazz(poly *r, const unsigned char *a); + +// Polyvec functions +uint64_t polyvec_pointwise_acc_jazz(poly *r, const polyvec *a, const polyvec *b); +uint64_t polyvec_compress_jazz(unsigned char *r, polyvec *a); +uint64_t polyvec_decompress_jazz(polyvec *r, const unsigned char *a); + +// Indcpa functions +void indcpa_keypair_jazz(unsigned char *pk, + unsigned char *sk, + const unsigned char *randomness); + +void indcpa_enc_jazz(unsigned char *c, + const unsigned char *m, + const unsigned char *pk, + const unsigned char *coins); + +void indcpa_dec_jazz(unsigned char *m, + const unsigned char *c, + const unsigned char *sk); + +// KEM functions +void crypto_kem_keypair_jazz(unsigned char *pk, + unsigned char *sk, + const unsigned char *randomness); + +void crypto_kem_enc_jazz(unsigned char *c, + const unsigned char *m, + const unsigned char *pk, + const unsigned char *coins); + +void crypto_kem_dec_jazz(unsigned char *m, + const unsigned char *c, + const unsigned char *sk); +#endif diff --git a/code/jasmin/mlkem_ref/test/speed_indcpa.c b/code/jasmin/mlkem_ref/test/speed_indcpa.c index b1dc32f5..9fb8fca5 100644 --- a/code/jasmin/mlkem_ref/test/speed_indcpa.c +++ b/code/jasmin/mlkem_ref/test/speed_indcpa.c @@ -2,6 +2,7 @@ #include #include #include +#include #include "../params.h" #include "../ntt.h" @@ -65,11 +66,15 @@ int main(void) unsigned char outmsg[MLKEM_POLYVECBYTES]; uint64_t t[NRUNS], i; + size_t ri; FILE *urandom = fopen("/dev/urandom", "r"); - fread(randomness0, MLKEM_SYMBYTES, 1, urandom); - fread(randomness1, MLKEM_SYMBYTES, 1, urandom); - fread(message, MLKEM_SYMBYTES, 1, urandom); + ri = fread(randomness0, MLKEM_SYMBYTES, 1, urandom); + assert( ri == 1 ); + ri = fread(randomness1, MLKEM_SYMBYTES, 1, urandom); + assert( ri == 1 ); + ri = fread(message, MLKEM_SYMBYTES, 1, urandom); + assert( ri == 1 ); fclose(urandom); /* TEST KEYPAIR */ diff --git a/code/jasmin/mlkem_ref/test/speed_mlkem.c b/code/jasmin/mlkem_ref/test/speed_mlkem.c new file mode 100644 index 00000000..d70ff119 --- /dev/null +++ b/code/jasmin/mlkem_ref/test/speed_mlkem.c @@ -0,0 +1,226 @@ +#include +#include +#include +#include +#include + +#include "../params.h" +#include "../speed.h" + +#define NRUNS 10000 + +static inline uint64_t cpucycles(void) { + uint64_t result; + + asm volatile("rdtsc; shlq $32,%%rdx; orq %%rdx,%%rax" + : "=a" (result) : : "%rdx"); + + return result; +} + +static int cmp_uint64(const void *a, const void *b) { + if(*(uint64_t *)a < *(uint64_t *)b) return -1; + if(*(uint64_t *)a > *(uint64_t *)b) return 1; + return 0; +} + +static uint64_t median(uint64_t *l, size_t llen) { + qsort(l,llen,sizeof(uint64_t),cmp_uint64); + + if(llen%2) return l[llen/2]; + else return (l[llen/2-1]+l[llen/2])/2; +} + +static uint64_t average(uint64_t *t, size_t tlen) { + size_t i; + uint64_t acc=0; + + for(i=0;i +#include #include "../fips202.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + #define MAXINLEN 33 #define MAXOUTLEN 168 int main(void) { + int test_ok = 1, test_ok_shake256_128_33 = 1, test_ok_sha3512_32 = 1, + test_ok_shake128_absorb34 = 1, test_ok_shake128_squeezeblock = 1; + size_t test_iteration = 0; unsigned char in[MAXINLEN]; unsigned char out0[MAXOUTLEN]; unsigned char out1[MAXOUTLEN]; @@ -14,35 +22,83 @@ int main(void) int k; FILE *urandom = fopen("/dev/urandom", "r"); - fread(in, 1, sizeof(in), urandom); - shake256(out0, 128, in, 33); - shake256_128_33_jazz(out1, in); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + size_t ri = fread(in, 1, sizeof(in), urandom); + assert(ri == sizeof(in)); + + // + shake256(out0, 128, in, 33); + shake256_128_33_jazz(out1, in); - for(k=0;k<128;k++) - if(out0[k] != out1[k]) printf("error shake256 at %d: %d %d\n", k, out0[k], out1[k]); + for(k=0;k<128;k++) + { if(out0[k] != out1[k]) + { fprintf(stderr, "ERROR: shake256_128_33 at %d: %d %d\n", k, out0[k], out1[k]); + test_ok_shake256_128_33 = 0; + test_ok = 0; + } + } - sha3_512(out0, in, 32); - sha3512_32_jazz(out1, in); + // + sha3_512(out0, in, 32); + sha3512_32_jazz(out1, in); - for(k=0;k<64;k++) - if(out0[k] != out1[k]) printf("error sha3512 at %d: %d %d\n", k, out0[k], out1[k]); + for(k=0;k<64;k++) + { if(out0[k] != out1[k]) + { fprintf(stderr, "ERROR: sha3512 at %d: %d %d\n", k, out0[k], out1[k]); + test_ok_sha3512_32 = 0; + test_ok = 0; + } + } - shake128_absorb(state0, in, 34); - shake128_absorb34_jazz(state1, in); + // + shake128_absorb(state0, in, 34); + shake128_absorb34_jazz(state1, in); - for(k=0;k<25;k++) - if(state0[k] != state1[k]) printf("error shake128_absorb at %d: %lu %lu\n", k, state0[k], state1[k]); + for(k=0;k<25;k++) + { if(state0[k] != state1[k]) + { fprintf(stderr, "ERROR: shake128_absorb at %d: %lu %lu\n", k, state0[k], state1[k]); + test_ok_shake128_absorb34 = 0; + test_ok = 0; + } + } - shake128_squeezeblocks(out0, 1, state0); - shake128_squeezeblock_jazz(out1, state1); + // + shake128_squeezeblocks(out0, 1, state0); + shake128_squeezeblock_jazz(out1, state1); - for(k=0;k<25;k++) - if(state0[k] != state1[k]) printf("error shake128_squeezeblock (state) at %d: %lu %lu\n", k, state0[k], state1[k]); + for(k=0;k<25;k++) + { if(state0[k] != state1[k]) + { fprintf(stderr, "ERROR: shake128_squeezeblock (state) at %d: %lu %lu\n", k, state0[k], state1[k]); + test_ok_shake128_squeezeblock = 0; + test_ok = 0; + } + } - for(k=0;k - +#include #include "../params.h" #include "../ntt.h" #include "../indcpa.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + int main(void) { + int test_ok = 1, test_ok_indcpa_keypair_sk = 1, test_ok_indcpa_keypair_pk = 1, + test_ok_indcpa_enc = 1, test_ok_indcpa_dec = 1, test_ok_decryption = 1; + size_t test_iteration = 0; + size_t ri; + unsigned char sk0[MLKEM_INDCPA_SECRETKEYBYTES]; unsigned char sk1[MLKEM_INDCPA_SECRETKEYBYTES]; unsigned char pk0[MLKEM_INDCPA_PUBLICKEYBYTES]; @@ -25,38 +34,88 @@ int main(void) unsigned char outmsg1[MLKEM_POLYVECBYTES]; FILE *urandom = fopen("/dev/urandom", "r"); - fread(randomness0, MLKEM_SYMBYTES, 1, urandom); - fread(randomness1, MLKEM_SYMBYTES, 1, urandom); - fread(message, MLKEM_SYMBYTES, 1, urandom); - fclose(urandom); - /* TEST KEYPAIR */ - indcpa_keypair_jazz(pk1, sk1, randomness0); - indcpa_keypair(pk0, sk0, randomness0); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + ri = fread(randomness0, MLKEM_SYMBYTES, 1, urandom); + assert(ri == 1); - for(int i=0;i -#include +#include +#include #include "../params.h" #include "../ntt.h" #include "../kem.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + int main(void) { + int test_ok = 1, test_ok_kem_keypair_sk = 1, test_ok_kem_keypair_pk = 1, + test_ok_kem_enc_ct = 1, test_ok_kem_enc_ss = 1, + test_ok_kem_dec_success = 1, test_ok_kem_dec_failure = 1; + size_t test_iteration = 0; + size_t ri; + unsigned char sk0[MLKEM_SECRETKEYBYTES]; unsigned char sk1[MLKEM_SECRETKEYBYTES]; unsigned char pk0[MLKEM_PUBLICKEYBYTES]; @@ -20,52 +31,108 @@ int main(void) unsigned char randomness1[2*MLKEM_SYMBYTES]; FILE *urandom = fopen("/dev/urandom", "r"); - fread(randomness0, 2*MLKEM_SYMBYTES, 1, urandom); - fread(randomness1, 2*MLKEM_SYMBYTES, 1, urandom); - fclose(urandom); - - /* TEST KEYPAIR */ - jade_kem_mlkem_mlkem768_amd64_ref_keypair_derand(pk1, sk1, randomness0); - crypto_kem_keypair(pk0, sk0, randomness0); - - for(int i=0;i #include "../poly.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;icoeffs[i] %= MLKEM_Q; - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly a, b, r0; - poly_setrandom(&a); - poly_setrandom(&b); - - poly_add(&r0, &a, &b); - - poly_add2_jazz(&a, &b); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom(&a); + poly_setrandom(&b); + + poly_add(&r0, &a, &b); + + poly_add2_jazz(&a, &b); + + for(int i=0;icoeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;icoeffs[i] %= MLKEM_Q; - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly a, b, r0, r1; - poly_setrandom(&a); - poly_setrandom(&b); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom(&a); + poly_setrandom(&b); + + poly_basemul(&r0, &a, &b); + + poly_basemul_jazz(&r1, &a, &b); + + for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - fclose(urandom); - poly_reduce(r); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; unsigned char out0[128]; unsigned char out1[128]; poly a; - poly_setrandom(&a); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom_nomodq(&a); - poly_compress(out0, &a); - poly_compress_jazz(out1, &a); + poly_compress(out0, &a); + poly_compress_jazz(out1, &a); - for(int i=0;i<128;i++) - { - if(out0[i] != out1[i]) - printf("error compress %d, %d, %d\n", i, out0[i], out1[i]); + for(int i=0;i<128;i++) + { if(out0[i] != out1[i]) + { fprintf(stderr, "ERROR: poly_compress: %d, %d, %d\n", i, out0[i], out1[i]); + test_ok = 0; + } + } + + test_iteration += 1; } + if(test_ok == 1) + { printf("OK: poly_compress\n"); } + return 0; } diff --git a/code/jasmin/mlkem_ref/test/test_poly_csubq.c b/code/jasmin/mlkem_ref/test/test_poly_csubq.c index fbaf8478..aa56ba63 100644 --- a/code/jasmin/mlkem_ref/test/test_poly_csubq.c +++ b/code/jasmin/mlkem_ref/test/test_poly_csubq.c @@ -1,32 +1,42 @@ #include +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - fclose(urandom); - poly_reduce(r); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly r0, r1; - poly_setrandom(&r0); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom_nomodq(&r0); - for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + int main(void) { + int test_ok = 1; + size_t test_iteration = 0; + size_t ri; unsigned char in[MLKEM_POLYCOMPRESSEDBYTES]; poly r0, r1; - - FILE *urandom = fopen("/dev/urandom", "r"); - fread(in, 1, MLKEM_POLYCOMPRESSEDBYTES, urandom); - fclose(urandom); - poly_decompress(&r0, in); - poly_decompress_jazz(&r1, in); + FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + int main(void) { + int test_ok = 1; + size_t test_iteration = 0; + size_t ri; unsigned char in[MLKEM_POLYBYTES]; poly r0, r1; - - FILE *urandom = fopen("/dev/urandom", "r"); - fread(in, 1, MLKEM_POLYBYTES, urandom); - fclose(urandom); - poly_frombytes(&r0, in); - poly_frombytes_jazz(&r1, in); + FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;icoeffs[i] %= MLKEM_Q; - } - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly r0, r1; - poly_setrandom(&r0); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom(&r0); + for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + int main(void) { + int test_ok = 1; + size_t test_iteration = 0; + size_t ri; unsigned char in[32]; poly r0, r1; - - FILE *urandom = fopen("/dev/urandom", "r"); - fread(in, 1, 32, urandom); - fclose(urandom); - poly_frommsg(&r0, in); - poly_frommsg_jazz(&r1, in); + FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" #include "../params.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif int main(void) { + int test_ok = 1; + size_t test_iteration = 0; + size_t ri; poly r0, r1; unsigned char seed[MLKEM_SYMBYTES]; FILE *urandom = fopen("/dev/urandom", "r"); - fread(seed, 1, MLKEM_SYMBYTES, urandom); - fclose(urandom); - for(int i = 0; i < 1; i++) + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) { - poly_getnoise(&r0, seed, i); - poly_getnoise_jazz(&r1, seed, i); + ri = fread(seed, 1, MLKEM_SYMBYTES, urandom); + assert(ri == MLKEM_SYMBYTES); - for(int j=0;j +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;icoeffs[i] %= 2*MLKEM_Q; - } - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly r0, r1; - poly_setrandom(&r0); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom_mod2q(&r0); + for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;icoeffs[i] %= 2*MLKEM_Q; - } - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly r0, r1; - poly_setrandom(&r0); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom_mod2q(&r0); - for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly r0, r1; - poly_setrandom(&r0); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom_nomodq(&r0); - for(int i=0;i +#include +#include "../poly.h" + +// note: extend to *_setrandom_open; *_setrandom; *_setrandom_close; +// to not open the file so many times + +void poly_setrandom(poly *r) +{ + FILE *urandom = fopen("/dev/urandom", "r"); + size_t ri = fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); + assert(ri == MLKEM_N); + for(int i=0;icoeffs[i] %= MLKEM_Q; } + fclose(urandom); +} + +void poly_setrandom_mod2q(poly *r) +{ + FILE *urandom = fopen("/dev/urandom", "r"); + size_t ri = fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); + assert(ri == MLKEM_N); + for(int i=0;icoeffs[i] %= 2*MLKEM_Q; } + fclose(urandom); +} + +void poly_setrandom_nomodq(poly *r) +{ + FILE *urandom = fopen("/dev/urandom", "r"); + size_t ri = fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); + assert(ri == MLKEM_N); + fclose(urandom); + poly_reduce(r); +} + +#endif diff --git a/code/jasmin/mlkem_ref/test/test_poly_sub.c b/code/jasmin/mlkem_ref/test/test_poly_sub.c index f46326f2..08510804 100644 --- a/code/jasmin/mlkem_ref/test/test_poly_sub.c +++ b/code/jasmin/mlkem_ref/test/test_poly_sub.c @@ -1,29 +1,40 @@ #include +#include #include "../poly.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;icoeffs[i] %= MLKEM_Q; - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; poly a, b, r0, r1; - poly_setrandom(&a); - poly_setrandom(&b); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + poly_setrandom(&a); + poly_setrandom(&b); + + poly_sub(&r0, &a, &b); + + poly_sub_jazz(&r1, &a, &b); + + for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - fclose(urandom); - poly_reduce(r); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; unsigned char out0[MLKEM_POLYBYTES]; unsigned char out1[MLKEM_POLYBYTES]; poly a; - - poly_setrandom(&a); - - poly_tobytes(out0, &a); - poly_tobytes_jazz(out1, &a); - for(int i=0;i +#include #include "../poly.h" #include "../ntt.h" -void poly_setrandom(poly *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - fread(r->coeffs, sizeof(int16_t), MLKEM_N, urandom); - fclose(urandom); - poly_reduce(r); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_poly_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; unsigned char out0[MLKEM_INDCPA_MSGBYTES]; unsigned char out1[MLKEM_INDCPA_MSGBYTES]; poly a; - - poly_setrandom(&a); - - poly_tomsg(out0, &a); - poly_tomsg_jazz(out1, &a); - for(int i=0;i +#include #include "../polyvec.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;ivec[i].coeffs[j] %= MLKEM_Q; - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; polyvec a, b, r0; - polyvec_setrandom(&a); - polyvec_setrandom(&b); - - polyvec_add(&r0, &a, &b); - polyvec_add2_jazz(&a, &b); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + polyvec_setrandom(&a); + polyvec_setrandom(&b); + + polyvec_add(&r0, &a, &b); + polyvec_add2_jazz(&a, &b); + + for(int i=0;i +#include #include "../polyvec.h" #include "../ntt.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif - polyvec_reduce(r); - fclose(urandom); -} +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; unsigned char out0[MLKEM_POLYVECCOMPRESSEDBYTES]; unsigned char out1[MLKEM_POLYVECCOMPRESSEDBYTES]; polyvec a; - polyvec_setrandom(&a); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + polyvec_setrandom_reduce(&a); - polyvec_compress(out0, &a); - polyvec_compress_jazz(out1, &a); + polyvec_compress(out0, &a); + polyvec_compress_jazz(out1, &a); - for(int i=0;i +#include #include "../poly.h" #include "../polyvec.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); - fclose(urandom); - polyvec_reduce(r); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; polyvec r0, r1; - polyvec_setrandom(&r0); - - for(int i = 0;i +#include #include "../polyvec.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + int main(void) { + int test_ok = 1; + size_t test_iteration = 0; + size_t ri; + unsigned char in[MLKEM_POLYVECCOMPRESSEDBYTES]; polyvec r0, r1; - + FILE *urandom = fopen("/dev/urandom", "r"); - fread(in, 1, MLKEM_POLYVECCOMPRESSEDBYTES, urandom); - fclose(urandom); - polyvec_decompress(&r0, in); - polyvec_decompress_jazz(&r1, in); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + ri = fread(in, 1, MLKEM_POLYVECCOMPRESSEDBYTES, urandom); + assert(ri == MLKEM_POLYVECCOMPRESSEDBYTES); + + polyvec_decompress(&r0, in); + polyvec_decompress_jazz(&r1, in); + + for(int i=0;i +#include #include "../polyvec.h" +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + int main(void) { + int test_ok = 1; + size_t test_iteration = 0; + size_t ri; unsigned char in[MLKEM_POLYVECBYTES]; polyvec r0, r1; - + FILE *urandom = fopen("/dev/urandom", "r"); - fread(in, 1, MLKEM_POLYVECBYTES, urandom); - fclose(urandom); - polyvec_frombytes(&r0, in); - polyvec_frombytes_jazz(&r1, in); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + ri = fread(in, 1, MLKEM_POLYVECBYTES, urandom); + assert(ri == MLKEM_POLYVECBYTES); + + polyvec_frombytes(&r0, in); + polyvec_frombytes_jazz(&r1, in); + + for(int i=0;i +#include #include "../ntt.h" #include "../poly.h" #include "../polyvec.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;ivec[i].coeffs[j] %= 2*MLKEM_Q; - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; polyvec r0, r1; - polyvec_setrandom(&r0); - - for(int i = 0;i +#include #include "../ntt.h" #include "../poly.h" #include "../polyvec.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;ivec[i].coeffs[j] %= 2*MLKEM_Q; - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; polyvec r0, r1; - polyvec_setrandom(&r0); - - for(int i = 0;i +#include #include "../ntt.h" #include "../polyvec.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;ivec[i].coeffs[j] %= MLKEM_Q; - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; polyvec a, b; poly r0, r1; - polyvec_setrandom(&a); - polyvec_setrandom(&b); - - polyvec_pointwise_acc(&r0, &a, &b); - polyvec_pointwise_acc_jazz(&r1, &a, &b); + while(test_ok == 1 && test_iteration < TEST_ITERATIONS) + { + polyvec_setrandom(&a); + polyvec_setrandom(&b); + + polyvec_pointwise_acc(&r0, &a, &b); + polyvec_pointwise_acc_jazz(&r1, &a, &b); for(int j=0;j +#include #include "../poly.h" #include "../polyvec.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; polyvec r0, r1; - polyvec_setrandom(&r0); - - for(int i = 0;i +#include +#include "../polyvec.h" + +// note: extend to *_setrandom_open; *_setrandom; *_setrandom_close; +// to not open the file so many times + +void polyvec_setrandom(polyvec *r) +{ + FILE *urandom = fopen("/dev/urandom", "r"); + for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); + assert(ri == MLKEM_N); + } + for(int i=0;ivec[i].coeffs[j] %= MLKEM_Q; + fclose(urandom); +} + +void polyvec_setrandom_reduce(polyvec *r) +{ + FILE *urandom = fopen("/dev/urandom", "r"); + for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); + assert(ri == MLKEM_N); + } + polyvec_reduce(r); + fclose(urandom); +} + +void polyvec_setrandom_mod2q(polyvec *r) +{ + FILE *urandom = fopen("/dev/urandom", "r"); + for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); + assert(ri == MLKEM_N); + } + for(int i=0;ivec[i].coeffs[j] %= 2*MLKEM_Q; + fclose(urandom); +} + +void polyvec_setrandom_nomodq(polyvec *r) +{ + FILE *urandom = fopen("/dev/urandom", "r"); + for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); + assert(ri == MLKEM_N); + } + fclose(urandom); +} + +#endif diff --git a/code/jasmin/mlkem_ref/test/test_polyvec_tobytes.c b/code/jasmin/mlkem_ref/test/test_polyvec_tobytes.c index d23acb49..d17f8941 100644 --- a/code/jasmin/mlkem_ref/test/test_polyvec_tobytes.c +++ b/code/jasmin/mlkem_ref/test/test_polyvec_tobytes.c @@ -1,34 +1,42 @@ #include +#include #include "../polyvec.h" #include "../ntt.h" -void polyvec_setrandom(polyvec *r) -{ - FILE *urandom = fopen("/dev/urandom", "r"); - for(int i=0;ivec[i].coeffs, sizeof(int16_t), MLKEM_N, urandom); - for(int i=0;ivec[i].coeffs[j] %= MLKEM_Q; - fclose(urandom); -} +#ifndef TEST_ITERATIONS +#define TEST_ITERATIONS 10000 +#endif + +#include "test_polyvec_setrandom.c" int main(void) { + int test_ok = 1; + size_t test_iteration = 0; unsigned char out0[MLKEM_POLYVECBYTES]; unsigned char out1[MLKEM_POLYVECBYTES]; polyvec a; - - polyvec_setrandom(&a); - polyvec_tobytes(out0, &a); - polyvec_tobytes_jazz(out1, &a); - - for(int i=0;i reg bool { + reg bool r; + r = true; + inline int i; + for i = 0 to 32 { + r = r && (u8)[p + i] == (u8)[q + i]; + } + return r; +} + +inline fn setup(inline bool withCoins) -> reg u64, reg u64, reg u64, reg u64, reg u64, reg u64 { + reg u64 pk sk ct ss1 ss2 coins; + pk = 0x1000; + sk = 0x2000; + ct = 0x3000; + ss1 = 0x4000; + ss2 = 0x5000; + coins = 0x6000; + if withCoins { + inline int i; + for i = 0 to 8 { [coins + 8 * i] = 0; } + } + return pk, sk, ct, ss1, ss2, coins; +} + +fn test_ref_derand() -> reg bool { + reg u64 pk sk ct ss1 ss2 coins; + pk, sk, ct, ss1, ss2, coins = setup(true); + + #[inline] + _ = ref::jade_kem_mlkem_mlkem768_amd64_ref_keypair_derand(pk, sk, coins); + #[inline] + _ = ref::jade_kem_mlkem_mlkem768_amd64_ref_enc_derand(ct, ss1, pk, coins + 32); + #[inline] + _ = ref::jade_kem_mlkem_mlkem768_amd64_ref_dec(ss2, ct, sk); + + reg bool r; + r = check(ss1, ss2); + return r; +} + +fn test_avx_derand() -> reg bool { + reg u64 pk sk ct ss1 ss2 coins; + pk, sk, ct, ss1, ss2, coins = setup(true); + + #[inline] + _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2_keypair_derand(pk, sk, coins); + #[inline] + _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2_enc_derand(ct, ss1, pk, coins + 32); + #[inline] + _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2_dec(ss2, ct, sk); + + reg bool r; + r = check(ss1, ss2); + return r; +} + +fn test_ref() -> reg bool { + reg u64 pk sk ct ss1 ss2; + pk, sk, ct, ss1, ss2, _ = setup(false); + + #[inline] + _ = ref::jade_kem_mlkem_mlkem768_amd64_ref_keypair(pk, sk); + #[inline] + _ = ref::jade_kem_mlkem_mlkem768_amd64_ref_enc(ct, ss1, pk); + #[inline] + _ = ref::jade_kem_mlkem_mlkem768_amd64_ref_dec(ss2, ct, sk); + + reg bool r; + r = check(ss1, ss2); + return r; +} + +fn test_avx() -> reg bool { + reg u64 pk sk ct ss1 ss2; + pk, sk, ct, ss1, ss2, _ = setup(false); + + #[inline] + _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2_keypair(pk, sk); + #[inline] + _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2_enc(ct, ss1, pk); + #[inline] + _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2_dec(ss2, ct, sk); + + reg bool r; + r = check(ss1, ss2); + return r; +} diff --git a/config/alt-ergo.nix b/config/alt-ergo.nix deleted file mode 100644 index 9cc57ca0..00000000 --- a/config/alt-ergo.nix +++ /dev/null @@ -1,78 +0,0 @@ -{ stdenv, autoreconfHook, fetchFromGitHub, fetchpatch, lib, which, ocamlPackages }: - -let ocplib-simplex = - - let - inherit (ocamlPackages) ocaml findlib; - pname = "ocplib-simplex"; - version = "0.4"; - in - - stdenv.mkDerivation { - name = "ocaml${ocaml.version}-${pname}-${version}"; - - src = fetchFromGitHub { - owner = "OCamlPro-Iguernlala"; - repo = pname; - rev = "v${version}"; - sha256 = "09niyidrjzrj8g1qwx4wgsdf5m6cwrnzg7zsgala36jliic4di60"; - }; - - nativeBuildInputs = [ autoreconfHook ocaml findlib ]; - - strictDeps = true; - - installFlags = [ "LIBDIR=$(OCAMLFIND_DESTDIR)" ]; - - createFindlibDestdir = true; - - }; -in - -let - pname = "alt-ergo"; - version = "2.4.3"; - - configureScript = "ocaml unix.cma configure.ml"; - - src = fetchFromGitHub { - owner = "OCamlPro"; - repo = pname; - rev = "refs/tags/${version}"; - hash = "sha256-2XARGr8rLiPMOM0rBBoRv5tZvKYtkLkJctGqLYkMe7Q="; - }; -in - -let alt-ergo-lib = ocamlPackages.buildDunePackage rec { - pname = "alt-ergo-lib"; - inherit version src configureScript; - configureFlags = [ pname ]; - nativeBuildInputs = [ which ]; - buildInputs = with ocamlPackages; [ dune-configurator ]; - propagatedBuildInputs = with ocamlPackages; [ dune-build-info num ocplib-simplex seq stdlib-shims zarith ]; -}; in - -let alt-ergo-parsers = ocamlPackages.buildDunePackage rec { - pname = "alt-ergo-parsers"; - inherit version src configureScript; - configureFlags = [ pname ]; - nativeBuildInputs = [ which ocamlPackages.menhir ]; - propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [ camlzip psmt2-frontend ]); -}; in - -ocamlPackages.buildDunePackage { - - inherit pname version src configureScript; - - configureFlags = [ pname ]; - - nativeBuildInputs = [ which ocamlPackages.menhir ]; - buildInputs = [ alt-ergo-parsers ocamlPackages.cmdliner ]; - - meta = { - description = "High-performance theorem prover and SMT solver"; - homepage = "https://alt-ergo.ocamlpro.com/"; - license = lib.licenses.ocamlpro_nc; - maintainers = [ lib.maintainers.thoughtpolice ]; - }; -} diff --git a/config/tests.config b/config/tests.config index d783a576..00f140bb 100644 --- a/config/tests.config +++ b/config/tests.config @@ -1,3 +1,12 @@ [test-mlkem] okdirs = !proof exclude = !proof/attic + +[test-mlkem-spec-sec] +okdirs = proof/security + +[test-mlkem-spec-corr] +okdirs = proof/spec + +[test-mlkem-impl-corr] +okdirs = !proof/correctness !proof/eclib diff --git a/easycrypt.project b/easycrypt.project index 842092c4..f49b5e2f 100644 --- a/easycrypt.project +++ b/easycrypt.project @@ -1,7 +1,7 @@ [general] timeout = 30 -provers = Alt-Ergo@2.4 +provers = Alt-Ergo@2.5 provers = CVC4@1.8 provers = Z3@4.8 diff --git a/ext/randombytes/Makefile b/ext/randombytes/Makefile new file mode 100644 index 00000000..cecfea6c --- /dev/null +++ b/ext/randombytes/Makefile @@ -0,0 +1,6 @@ +all: jasmin_syscall.o + +jasmin_syscall.o: jasmin_syscall.c jasmin_syscall.h + +clean: + rm -f jasmin_syscall.o diff --git a/ext/randombytes/jasmin_syscall.c b/ext/randombytes/jasmin_syscall.c new file mode 100644 index 00000000..628b900a --- /dev/null +++ b/ext/randombytes/jasmin_syscall.c @@ -0,0 +1,45 @@ + +#include "jasmin_syscall.h" + +#if defined(__linux__) + +#include +#include +#include + +uint8_t* __jasmin_syscall_randombytes__(uint8_t* _x, uint64_t xlen) +{ + int i; + uint8_t* x = _x; + + while (xlen > 0) { + if (xlen < 1048576) i = xlen; else i = 1048576; + + i = getrandom(x,i,0); + if (i < 1) { + sleep(1); + continue; + } + x += i; + xlen -= i; + } + + return _x; +} + +#endif + +#if defined(__APPLE__) + +#include + +#if !(defined(__MAC_OS_X_VERSION_MIN_REQUIRED) && __MAC_OS_X_VERSION_MIN_REQUIRED >= 101200) +#error "macOS version not supported (>= 10.12)" +#endif + +uint8_t* __jasmin_syscall_randombytes__(uint8_t* x, uint64_t xlen){ + arc4random_buf(x, xlen); + return x; +} + +#endif diff --git a/ext/randombytes/jasmin_syscall.h b/ext/randombytes/jasmin_syscall.h new file mode 100644 index 00000000..5ba562a2 --- /dev/null +++ b/ext/randombytes/jasmin_syscall.h @@ -0,0 +1,8 @@ +#include +#ifndef JASMIN_SYSCALL +#define JASMIN_SYSCALL +/* FIXME this need xlen to be Uptr */ +uint8_t* __jasmin_syscall_randombytes__(uint8_t* x, uint64_t xlen) +asm("__jasmin_syscall_randombytes__"); + +#endif diff --git a/proof/correctness/MLKEM_KEM.ec b/proof/correctness/MLKEM_KEM.ec index 1149b043..fa1ac1af 100644 --- a/proof/correctness/MLKEM_KEM.ec +++ b/proof/correctness/MLKEM_KEM.ec @@ -67,7 +67,7 @@ swap {1} 1 14. seq 19 4 : ( z{2} =Array32.init (fun i => randomnessp{1}.[32 + i]) /\ - to_uint skp{1} = _skp + 1152 + 1152 + 32 + 32 /\ + to_uint skp{1} = _skp + 1152 + 1152 + 32 /\ valid_disj_reg _pkp (384*3+32) _skp (384*3 + 384*3 + 32 + 32 + 32 + 32) /\ touches2 Glob.mem{1} mem _pkp (384 * 3 + 32) _skp (384*3 + 384*3 + 32 + 32 + 32 + 32) /\ sk{2} = load_array1152 Glob.mem{1} _skp /\ @@ -79,7 +79,7 @@ seq 19 4 : ( ); last first. + while {1} (aux{1} = 4 /\ z{2} = Array32.init (fun i => randomnessp2{1}.[i]) /\ - to_uint skp{1} = _skp + 1152 + 1152 + 32 + 32 + i{1}*8 /\ + to_uint skp{1} = _skp + 1152 + 1152 + 32 /\ valid_disj_reg _pkp (384*3+32) _skp (384*3 + 384*3 + 32 + 32 + 32 + 32) /\ touches2 Glob.mem{1} mem _pkp (384 * 3 + 32) _skp (384*3 + 384*3 + 32 + 32 + 32 + 32) /\ sk{2} = load_array1152 Glob.mem{1} _skp /\ @@ -94,9 +94,8 @@ seq 19 4 : ( pack8_t (W8u8.Pack.init (fun i => z{2}.[k*8+i]))) (4 - i{1}). + move => &m z0; auto => /> &hr; rewrite /touches2 /load_array1152 /load_array32 !tP => - skv ????? touch pk1vs pk2vs pk1v pk2v ??prev? ; rewrite !to_uintD_small /=. - + by smt(). - do split; 1,9,12: by smt(). + skv ????? touch pk1vs pk2vs pk1v pk2v ??prev? ; rewrite !to_uintD_small !to_uint_small /= 1..3:/#. + do split. + by move => a H1 H2; rewrite /storeW64 /loadW64 /stores /= !get_set_neqE_s /#. + by move => k kb; rewrite !initiE //= /storeW64 /loadW64 /stores /= !get_set_neqE_s /#. + move => k kb; rewrite !initiE //= /storeW64 /loadW64 @@ -114,6 +113,7 @@ seq 19 4 : ( /stores /= !get_set_neqE_s; 1..8: smt(). by rewrite pk2v // initiE //=. + by smt(). + + by smt(). + move => k kbl kbh. case (k < i{hr}). + move => hk. @@ -132,13 +132,14 @@ seq 19 4 : ( rewrite WArray32.WArray32.get64E !pack8bE 1..8:/# !initiE 1..8:/# /= /init8. rewrite !WArray32.WArray32.initiE 1..8:/#. by smt(get_set_neqE_s get_set_eqE_s). + by smt(). auto => />;move => ????????touch????; do split. + rewrite tP => k kb; rewrite !initiE /#. + smt(). - move => memL iL skpL. + move => memL iL. split; 1: smt(). - move => ???touch2????????store???. + move => ???touch2???????store???. rewrite /load_array32 tP => k kb. rewrite !initiE //=. move : (store (k %/ 8) _); 1: smt(). @@ -152,7 +153,7 @@ swap {2} 2 2. swap {1} [2..3] 1; sp 4 1. wp;conseq (_: _ ==> -to_uint skp{1} = _skp + 2368 /\ +to_uint skp{1} = _skp + 2336 /\ touches2 Glob.mem{1} mem (_pkp) 1184 (_skp) 2432 /\ sk{2} = load_array1152 Glob.mem{1} (_skp) /\ pk{2}.`1 = load_array1152 Glob.mem{1} (_skp + 1152) /\ @@ -185,19 +186,17 @@ seq 8 0 : (#{/~to_uint skp{1} = _skp}pre /\ pk{2}.`2 = load_array32 Glob.mem{1} (_skp+ 2304) ). -+ wp;while {1} (#{/~to_uint skp{1} = _skp}{~s_skp{1} = skp{1}}pre /\ ++ wp; while {1} (#{/~to_uint skp{1} = _skp}{~s_skp{1} = skp{1}}pre /\ aux{1} = (3 * 384 + 32) %/ 8 /\ 0<=i{1} <= aux{1} /\ - to_uint skp{1} = _skp + 3*384 + i{1}*8 /\ + to_uint skp{1} = _skp + 3*384 /\ (forall k, 0<= k < min (8 * i{1}) 1152 => pk{2}.`1.[k] = Glob.mem{1}.[_skp + 3*384 + k]) /\ (forall k, min (8 * i{1}) 1152 <= k < min (8 * i{1}) (1152 + 32) => pk{2}.`2.[k-1152] = Glob.mem{1}.[_skp + 3*384 + k])) ((3 * 384 + 32) %/ 8 - i{1}). - move => &m z;auto => /> &hr. rewrite /load_array32 /load_array1152 !tP /touches2. - move => ???????touch pkv1 pkv2???prev1 prev2 ?;rewrite !to_uintD_small /=. - + by rewrite of_uintK /= modz_small /=; smt(). - by smt(). - do split; 5..7:smt(). + move => &m z;auto => /> &hr. rewrite !tP /touches2. + move => ???????touch pkv1 pkv2???prev1 prev2 ?; rewrite !to_uintD_small !to_uint_small /=; 1..5: smt(). + do split. + move => i ib ibb. rewrite /storeW64 /loadW64 /stores /=. rewrite !get_set_neqE_s; 1..8:smt(). @@ -214,12 +213,13 @@ seq 8 0 : (#{/~to_uint skp{1} = _skp}pre /\ rewrite /storeW64 /loadW64 /stores /=. rewrite !get_set_neqE_s; 1..8:smt(). by move : (pkv2 k kb); rewrite initiE //=. + + smt(). + + smt(). + move => kk kkbl kkbh. rewrite /storeW64 /loadW64 /stores /=. case (kk < i{hr} * 8). + by move => *; rewrite !get_set_neqE_s; smt(). move => ?. - rewrite !of_uintK /= modz_small;1:smt(). move : (pkv1 kk _); 1: smt(). rewrite initiE /=; 1: smt(). by smt(get_set_neqE_s get_set_eqE_s). @@ -228,21 +228,24 @@ seq 8 0 : (#{/~to_uint skp{1} = _skp}pre /\ case (kk < i{hr} * 8). + by move => *; rewrite !get_set_neqE_s; smt(). move => ?. - rewrite !of_uintK /= modz_small;1:smt(). move : (pkv2 (kk - 1152) _); 1: smt(). rewrite initiE /=; 1: smt(). by smt(get_set_neqE_s get_set_eqE_s). + by smt(). - auto => /> &1 &2; rewrite /load_array1152 /load_array32 !tP. + + auto => /> &1 &2; rewrite !tP. move => ??????????. rewrite to_uintD_small /=; 1: by smt(). do split; 1..2: by smt(). - move => meml il skpl. + move => meml il. rewrite !tP; split; 1: smt(). - move => ??????????; do split; 1: smt(). + move => ????????X; do split. + + rewrite to_uintD_small //= /#. + by move => *; rewrite initiE //= /#. - by move => *; rewrite initiE //= /#. - + move => j hj. + have {1}-> : j = (j + 1152) - 1152 by ring. + rewrite X 1:/# initiE /#. + seq 4 1 : (to_uint skp{1} = _skp + 2336 /\ valid_disj_reg _pkp 1184 _skp 2432 /\ @@ -258,10 +261,10 @@ inline *; auto => /> &1 &2; rewrite /touches /touches2 /load_array1152 /load_arr + move => i ib; congr; rewrite /H_pk; congr. by smt(Array32.initiE Array1152.initiE Array32.tP Array1152.tP). -while {1} (#{/~to_uint skp{1} = _skp + 2336}pre /\ 0 <= i{1} <= 4 /\ to_uint skp{1} = _skp + 2336 + 8*i{1} /\ forall k, 0 <= k < i{1} * 8 => Glob.mem{1}.[_skp + 2336 + k] = (H_pk pk{2}).[k]) (4 - i{1}). +while {1} (#pre /\ 0 <= i{1} <= 4 /\ forall k, 0 <= k < i{1} * 8 => Glob.mem{1}.[_skp + 2336 + k] = (H_pk pk{2}).[k]) (4 - i{1}). move => &m z; auto => /> &1 &2; rewrite /load_array1152 /load_array32 /touches2 !tP. -move => ?????pkv1s pkv2s pkv1 pkv2 ??? prev ?. -rewrite !to_uintD_small /= 1:/#. +move => ??????pkv1s pkv2s pkv1 pkv2 ?? prev ?. +rewrite !to_uintD_small /= !to_uint_small; 1..3: smt(). do split. + move => i ib ih. rewrite /storeW64 /loadW64 /stores /=. @@ -287,7 +290,6 @@ do split. by move : (pkv2 i ib); rewrite initiE //=. + by smt(). + by smt(). -+ by smt(). + move => k kbl kbh. case (k < (i{1} * 8)). + by move => kl;rewrite /storeW64 /loadW64 /stores /= !get_set_neqE_s;smt(). @@ -306,9 +308,8 @@ do split. + move => i ib ih. rewrite /storeW64 /loadW64 /stores /=. by smt(get_set_neqE_s get_set_eqE_s). -move => memL iL skL; do split; 1: by smt(). -move => *; split; 1: by smt(). -by rewrite tP => i ib; smt(Array32.initiE). +move => memL iL; split; 1: by smt(). +by move => 9? X; rewrite Array32.tP => *; rewrite -X 1:/# initiE. qed. lemma mlkem_kem_correct_enc mem _ctp _pkp _kp : diff --git a/proof/correctness/avx2/MLKEM_KEM_avx2.ec b/proof/correctness/avx2/MLKEM_KEM_avx2.ec index 82783948..469853f8 100644 --- a/proof/correctness/avx2/MLKEM_KEM_avx2.ec +++ b/proof/correctness/avx2/MLKEM_KEM_avx2.ec @@ -66,7 +66,7 @@ swap {1} 1 14. seq 19 4 : ( z{2} = Array32.init(fun i => randomnessp{1}.[32 + i]) /\ - to_uint skp{1} = _skp + 1152 + 1152 + 32 + 32 /\ + to_uint skp{1} = _skp + 1152 + 1152 + 32 /\ valid_disj_reg _pkp (384*3+32) _skp (384*3 + 384*3 + 32 + 32 + 32 + 32) /\ touches2 Glob.mem{1} mem _pkp (384 * 3 + 32) _skp (384*3 + 384*3 + 32 + 32 + 32 + 32) /\ sk{2} = load_array1152 Glob.mem{1} _skp /\ @@ -78,7 +78,7 @@ seq 19 4 : ( ); last first. + while {1} (aux{1} = 4 /\ z{2} = Array32.init(fun i => randomnessp2{1}.[0 + i]) /\ - to_uint skp{1} = _skp + 1152 + 1152 + 32 + 32 + i{1}*8 /\ + to_uint skp{1} = _skp + 1152 + 1152 + 32 /\ valid_disj_reg _pkp (384*3+32) _skp (384*3 + 384*3 + 32 + 32 + 32 + 32) /\ touches2 Glob.mem{1} mem _pkp (384 * 3 + 32) _skp (384*3 + 384*3 + 32 + 32 + 32 + 32) /\ sk{2} = load_array1152 Glob.mem{1} _skp /\ @@ -93,9 +93,8 @@ seq 19 4 : ( pack8_t (W8u8.Pack.init (fun i => z{2}.[k*8+i]))) (4 - i{1}). + move => &m z0; auto => /> &hr; rewrite /touches2 /load_array1152 /load_array32 !tP => - ?????? touch pk1vs pk2vs pk1v pk2v ??prev? ; rewrite !to_uintD_small /=. - + by smt(). - do split; 1,9,12: by smt(). + ?????? touch pk1vs pk2vs pk1v pk2v ??prev? ; rewrite !to_uintD_small !to_uint_small /= 1..3:/#. + do split. + by move => a H1 H2; rewrite /storeW64 /loadW64 /stores /= !get_set_neqE_s /#. + by move => k kb; rewrite !initiE //= /storeW64 /loadW64 /stores /= !get_set_neqE_s /#. + move => k kb; rewrite !initiE //= /storeW64 /loadW64 @@ -113,6 +112,7 @@ seq 19 4 : ( /stores /= !get_set_neqE_s; 1..8: smt(). by rewrite pk2v // initiE //=. + by smt(). + + smt(). + move => k kbl kbh. case (k < i{hr}). + move => hk. @@ -131,14 +131,15 @@ seq 19 4 : ( rewrite WArray32.WArray32.get64E !pack8bE 1..8:/# !initiE 1..8:/# /= /init8. rewrite !WArray32.WArray32.initiE 1..8:/#. by smt(get_set_neqE_s get_set_eqE_s). + smt(). auto => />;move => ????????touch????; do split. + rewrite tP => k kb; rewrite !initiE 1..3:/# /=. + smt(). + smt(). - move => memL iL skpL. + move => memL iL. split; 1: smt(). - move => ???touch2????????store???. + move => ???touch2???????store???. rewrite /load_array32 tP => k kb. rewrite !initiE //=. move : (store (k %/ 8) _); 1: smt(). @@ -152,7 +153,7 @@ swap {2} 2 2. swap {1} [2..3] 1; sp 4 1. wp;conseq (_: _ ==> -to_uint skp{1} = _skp + 2368 /\ +to_uint skp{1} = _skp + 2336 /\ touches2 Glob.mem{1} mem (_pkp) 1184 (_skp) 2432 /\ sk{2} = load_array1152 Glob.mem{1} (_skp) /\ pk{2}.`1 = load_array1152 Glob.mem{1} (_skp + 1152) /\ @@ -185,19 +186,17 @@ seq 8 0 : (#{/~to_uint skp{1} = _skp}pre /\ pk{2}.`2 = load_array32 Glob.mem{1} (_skp+ 2304) ). -+ wp;while {1} (#{/~to_uint skp{1} = _skp}{~s_skp{1} = skp{1}}pre /\ ++ wp; while {1} (#{/~to_uint skp{1} = _skp}{~s_skp{1} = skp{1}}pre /\ aux{1} = (3 * 384 + 32) %/ 8 /\ 0<=i{1} <= aux{1} /\ - to_uint skp{1} = _skp + 3*384 + i{1}*8 /\ + to_uint skp{1} = _skp + 3*384 /\ (forall k, 0<= k < min (8 * i{1}) 1152 => pk{2}.`1.[k] = Glob.mem{1}.[_skp + 3*384 + k]) /\ (forall k, min (8 * i{1}) 1152 <= k < min (8 * i{1}) (1152 + 32) => pk{2}.`2.[k-1152] = Glob.mem{1}.[_skp + 3*384 + k])) ((3 * 384 + 32) %/ 8 - i{1}). - move => &m z;auto => /> &hr. rewrite /load_array32 /load_array1152 !tP /touches2. - move => ???????touch pkv1 pkv2???prev1 prev2 ?;rewrite !to_uintD_small /=. - + by rewrite of_uintK /= modz_small /=; smt(). - by smt(). - do split; 5..7:smt(). + move => &m z;auto => /> &hr. rewrite !tP /touches2. + move => ???????touch pkv1 pkv2???prev1 prev2 ?;rewrite !to_uintD_small !to_uint_small /=; 1..5: smt(). + do split. + move => i ib ibb. rewrite /storeW64 /loadW64 /stores /=. rewrite !get_set_neqE_s; 1..8:smt(). @@ -214,12 +213,13 @@ seq 8 0 : (#{/~to_uint skp{1} = _skp}pre /\ rewrite /storeW64 /loadW64 /stores /=. rewrite !get_set_neqE_s; 1..8:smt(). by move : (pkv2 k kb); rewrite initiE //=. + + smt(). + + smt(). + move => kk kkbl kkbh. rewrite /storeW64 /loadW64 /stores /=. case (kk < i{hr} * 8). + by move => *; rewrite !get_set_neqE_s; smt(). move => ?. - rewrite !of_uintK /= modz_small;1:smt(). move : (pkv1 kk _); 1: smt(). rewrite initiE /=; 1: smt(). by smt(get_set_neqE_s get_set_eqE_s). @@ -228,7 +228,6 @@ seq 8 0 : (#{/~to_uint skp{1} = _skp}pre /\ case (kk < i{hr} * 8). + by move => *; rewrite !get_set_neqE_s; smt(). move => ?. - rewrite !of_uintK /= modz_small;1:smt(). move : (pkv2 (kk - 1152) _); 1: smt(). rewrite initiE /=; 1: smt(). by smt(get_set_neqE_s get_set_eqE_s). @@ -237,13 +236,16 @@ seq 8 0 : (#{/~to_uint skp{1} = _skp}pre /\ move => ??????????. rewrite to_uintD_small /=; 1: by smt(). do split; 1..2: by smt(). - move => meml il skpl. + move => meml il. rewrite !tP; split; 1: smt(). - move => ??????????; do split; 1: smt(). + move => ????????X; do split. + + rewrite to_uintD_small //= /#. + by move => *; rewrite initiE //= /#. - by move => *; rewrite initiE //= /#. - -seq 4 1 : + move => j hj. + have {1}-> : j = (j + 1152) - 1152 by ring. + rewrite X 1:/# initiE /#. + +seq 4 1 : (to_uint skp{1} = _skp + 2336 /\ valid_disj_reg _pkp 1184 _skp 2432 /\ touches2 Glob.mem{1} mem _pkp 1184 _skp 2432 /\ @@ -258,10 +260,10 @@ inline *; auto => /> &1 &2; rewrite /touches /touches2 /load_array1152 /load_arr + move => i ib; congr; rewrite /H_pk; congr. by smt(Array32.initiE Array1152.initiE Array32.tP Array1152.tP). -while {1} (#{/~to_uint skp{1} = _skp + 2336}pre /\ 0 <= i{1} <= 4 /\ to_uint skp{1} = _skp + 2336 + 8*i{1} /\ forall k, 0 <= k < i{1} * 8 => Glob.mem{1}.[_skp + 2336 + k] = ((H_pk pk{2})).[k]) (4 - i{1}). +while {1} (#pre /\ 0 <= i{1} <= 4 /\ forall k, 0 <= k < i{1} * 8 => Glob.mem{1}.[_skp + 2336 + k] = ((H_pk pk{2})).[k]) (4 - i{1}). move => &m z; auto => /> &1 &2; rewrite /load_array1152 /load_array32 /touches2 !tP. -move => ?????pkv1s pkv2s pkv1 pkv2 ??? prev ?. -rewrite !to_uintD_small /= 1:/#. +move => ??????pkv1s pkv2s pkv1 pkv2 ?? prev ?. +rewrite !to_uintD_small to_uint_small /=; 1..3: smt(). do split. + move => i ib ih. rewrite /storeW64 /loadW64 /stores /=. @@ -287,7 +289,6 @@ do split. by move : (pkv2 i ib); rewrite initiE //=. + by smt(). + by smt(). -+ by smt(). + move => k kbl kbh. case (k < (i{1} * 8)). + by move => kl;rewrite /storeW64 /loadW64 /stores /= !get_set_neqE_s;smt(). @@ -306,9 +307,8 @@ do split. + move => i ib ih. rewrite /storeW64 /loadW64 /stores /=. by smt(get_set_neqE_s get_set_eqE_s). -move => memL iL skL; do split; 1: by smt(). -move => *; split; 1: by smt(). -by rewrite tP => i ib; smt(Array32.initiE). +move => memL iL; split; 1: by smt(). +by move => 9? X; rewrite Array32.tP => *; rewrite -X 1:/# initiE. qed. diff --git a/proof/correctness/avx2/MLKEM_avx2_encdec.ec b/proof/correctness/avx2/MLKEM_avx2_encdec.ec index 4827ff4e..0ea7cfd2 100644 --- a/proof/correctness/avx2/MLKEM_avx2_encdec.ec +++ b/proof/correctness/avx2/MLKEM_avx2_encdec.ec @@ -358,6 +358,44 @@ have Hjm: (0 <= j < 0 + 8). rewrite Hj => />. move :Hjm. rewrite -mema_iota -iot rewrite !modzDml -addrA !modzDml -!addrA !modzDml -!addrA !modzDml !modz_dvd //=. do 8!(try (move => Hjm; case Hjm => />); first by smt()). qed. +lemma fill0 f k (t : ipoly): fill f k 0 t = t. +proof. +rewrite /fill &(Array256.tP) /= => i *. +by rewrite !initE /#. +qed. + +lemma fillSm f k n (t : ipoly): 0 < n => + fill f k n t = fill f (k+1) (n-1) t.[k <- f k]. +proof. +move=> ge0_n @/fill; apply/Array256.tP => i rg_i. +by rewrite !initE /= get_set_if /#. +qed. + +lemma fill_swap (i j ki kj : int) f g (t : ipoly) : + i + ki <= j => fill f i ki (fill g j kj t) = fill g j kj (fill f i ki t). +proof. +move=> rg @/fill; apply/Array256.tP => k *. +do rewrite initE /=. smt(). +qed. + +op [opaque] fillC ['a] = Array256.fill<:'a>. + +lemma fillCE ['a] : fillC<:'a> = Array256.fill. +proof. by rewrite /fillC. qed. + +lemma fillC_swap (i j ki kj : int) f g (t : ipoly) : + i + ki <= j => fillC f i ki (fillC g j kj t) = fillC g j kj (fillC f i ki t). +proof. by rewrite !fillCE &(fill_swap). qed. + +lemma fillC0 f k (t : ipoly): fillC f k 0 t = t. +proof. by rewrite fillCE &(fill0). qed. + +lemma fillCSm f k n (t : ipoly): 0 < n => + fillC f k n t = fillC f (k+1) (n - 1) t.[k <- f k]. +proof. by rewrite fillCE &(fillSm). qed. + +hint simplify fillC_swap. + equiv eq_decode1_opt : EncDec_AVX2.decode1_opt ~ EncDec.decode1 : ={a} ==> ={res}. @@ -365,10 +403,8 @@ proc. unroll for {1} ^while. do 8!(unroll for {1} ^while). unroll for {2} ^while. -auto => /> &m. -apply tP_red256. -move => i. -(* FIXME: TOO LONG => *) do 255!(move => Hi; case Hi => |>). +auto=> /= &1 &2 ->; rewrite -!fillCE /=. +by do 32! ((do 8! rewrite fillCSm 1://); rewrite /= fillC0). qed. equiv decode10_vec_corr: @@ -392,23 +428,23 @@ proof. unroll for {2} 2. wp; skip; auto => />. move => &1 &2 [#] k_lb k_ub c_eq k_tub />. - rewrite (mulzDr 320 _ _) (mulzDr 256 _ _) mulz1 //=. + rewrite (mulzDr 320 _ _) (mulzDr 256 _ _) mulz1 /=. split. + move : k_lb k_tub => /#. + move => j j_lb j_ub. - rewrite filliE 1:/# //=. - rewrite j_ub //=. + rewrite filliE 1:/# ~-1://=. + rewrite j_ub ~-1://=. case (j < 256 * k{2}) => j_tub. + have -> /=: !(256 * k{2} <= j). by rewrite -ltzNge j_tub. rewrite c_eq; first by rewrite j_lb j_tub. - do (rewrite Array768.set_neqiE 1:/#; first by move : j_tub j_lb => /#). - done. + rewrite !Array768.get_set_if ~-1://. + by have /#: k{2} = 1 \/ k{2} = 2 by smt(). + move : j_tub => /lezNgt j_tlb. rewrite j_tlb /=. have j_iota: j \in iota_ (256*k{2}) 256; first by rewrite mem_iota j_ub j_tlb. - move : j_iota. - do (rewrite Array768.get_setE 1:/#). - smt(mem_iota). + move : j_iota; rewrite !Array768.get_set_if ~-1://. + have: k{2} = 0 \/ k{2} = 1 \/ k{2} = 2 by smt(). + by rewrite -iotaredE /=; do 2! (move=> [#|] -> /=). auto => />. move => cL cR k k_tlb _ k_lb k_ub. have -> /=: k = 3. move : k_tlb k_ub => /#. diff --git a/shell.nix b/shell.nix index 81081568..81ca9434 100644 --- a/shell.nix +++ b/shell.nix @@ -1,7 +1,7 @@ { pkgs ? import (fetchTarball { - url = https://github.com/NixOS/nixpkgs/archive/53fbe41cf76b6a685004194e38e889bc8857e8c2.tar.gz; - sha256 = "sha256:1fyc4kbhv7rrfzya74yprvd70prlcsv56b7n0fv47kn7rznvvr2b"; + url = "https://github.com/NixOS/nixpkgs/archive/46397778ef1f73414b03ed553a3368f0e7e33c2f.tar.gz"; + sha256 = "sha256:1kl124v7ny2ar49s5498vx2jl3g8dwaqqvkdaqbjalhn9npl6dlv"; }) {} , full ? true }: @@ -15,26 +15,28 @@ let ideSupport = false; coqPackages = { coq = null; flocq = null; }; }; - ecVersion = "a8274feb63b62d281db350cd6dd8940c69aca835"; - ec = (easycrypt.overrideAttrs (_: { + ecVersion = "0df85113c4a399990f3f8ed93db5047a8844f8a9"; + ec = (easycrypt.overrideAttrs (o: { src = fetchFromGitHub { owner = "EasyCrypt"; repo = "easycrypt"; rev = ecVersion; - hash = "sha256-Rbs3alnnnDPbKrAqPq1pj/kedHWC+PvPFES4d+V8EAk="; + hash = "sha256-+3qI/Z9EpQXe75yHfkqt/N0Uwb+iN8ziTYg4Z4yBaSk="; }; postPatch = '' substituteInPlace dune-project --replace '(name easycrypt)' '(name easycrypt)(version ${ecVersion})' ''; + buildInputs = o.buildInputs ++ [ oc.dune-site ]; })).override { ocamlPackages = oc; why3 = why; }; - altergo = callPackage ./config/alt-ergo.nix { ocamlPackages = oc; } ; + altergo = alt-ergo.override { ocamlPackages = oc; } ; in mkShell ({ JASMINC = "${jasmin-compiler.bin}/bin/jasminc"; + JASMIN_CT = "${jasmin-compiler.bin}/bin/jazzct"; } // lib.optionalAttrs full { packages = [ ec