Skip to content

Commit

Permalink
Generate p521_32
Browse files Browse the repository at this point in the history 
Ignore p424_32 in the table below, it's from a different version of this
commit.

<details><summary>Timing</summary>
<p>

```
      Time |   Peak Mem | File Name
-------------------------------------------------------------------------------------------------------------------
254m50.98s | 3857976 ko | Total Time / Peak Mem
-------------------------------------------------------------------------------------------------------------------
  9m09.24s | 2340948 ko | Bedrock/End2End/X25519/GarageDoor.vo
  6m52.61s | 2067876 ko | Curves/Weierstrass/AffineProofs.vo
  5m24.81s | 2846272 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo
  4m43.41s | 3857976 ko | fiat-json/src/p434_32.json
  4m41.94s | 3549180 ko | fiat-java/src/FiatP434.java
  4m40.51s | 3510128 ko | fiat-go/32/p434/p434.go
  4m38.01s | 3112012 ko | fiat-rust/src/p434_32.rs
  4m36.06s | 1005000 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.vo
  4m35.63s | 3460760 ko | fiat-c/src/p434_32.c
  4m24.81s | 3479832 ko | fiat-bedrock2/src/p434_32.c
  4m21.82s | 1805944 ko | Curves/EdwardsMontgomery.vo
  4m16.62s |  969388 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.vo
  4m05.49s | 3689096 ko | fiat-zig/src/p434_32.zig
  4m02.12s | 2558072 ko | Assembly/WithBedrock/Proofs.vo
  3m45.39s | 1784600 ko | Rewriter/Passes/ArithWithCasts.vo
  3m21.77s | 3298648 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.vo
  3m14.18s | 2606244 ko | Bedrock/End2End/RupicolaCrypto/ChaCha20.vo
  3m01.52s | 1449620 ko | Curves/Weierstrass/Projective.vo
  2m51.65s |  781792 ko | rupicola/bedrock2/compiler/src/compiler/FlattenExpr.vo
  2m43.49s | 1590284 ko | Curves/Montgomery/XZProofs.vo
  2m41.57s | 1467320 ko | Curves/Montgomery/AffineProofs.vo
  2m30.06s | 1114396 ko | Fancy/Compiler.vo
  2m16.49s | 1561432 ko | Rewriter/Passes/NBE.vo
  1m58.96s | 2787304 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.vo
  1m56.94s | 2010232 ko | fiat-json/src/p384_scalar_32.json
  1m54.69s |  442236 ko | Spec/Test/X25519.vo
  1m54.17s | 2271728 ko | fiat-bedrock2/src/p384_scalar_32.c
  1m53.70s | 1745936 ko | fiat-zig/src/p384_32.zig
  1m53.52s | 2115820 ko | fiat-go/32/p384/p384.go
  1m53.19s | 1674280 ko | fiat-json/src/p384_32.json
  1m53.14s | 1628960 ko | fiat-java/src/FiatP384.java
  1m53.05s | 1699924 ko | fiat-rust/src/p384_scalar_32.rs
  1m52.61s | 1822712 ko | fiat-bedrock2/src/p384_32.c
  1m51.65s | 1604284 ko | Bedrock/End2End/X25519/Field25519.vo
  1m51.49s | 1435476 ko | Rewriter/Passes/ToFancyWithCasts.vo
  1m51.33s | 1635188 ko | fiat-c/src/p384_scalar_32.c
  1m49.51s | 1953272 ko | fiat-rust/src/p384_32.rs
  1m49.44s | 2074092 ko | fiat-c/src/p384_32.c
  1m47.54s | 2392824 ko | Fancy/Barrett256.vo
  1m46.52s | 1924084 ko | fiat-go/32/p384scalar/p384scalar.go
  1m46.35s | 1693196 ko | fiat-zig/src/p384_scalar_32.zig
  1m45.28s | 2107680 ko | fiat-java/src/FiatP384Scalar.java
  1m33.15s |  860988 ko | Util/FSets/FMapTrie.vo
  1m28.26s | 2040924 ko | SlowPrimeSynthesisExamples.vo
  1m22.76s |  744076 ko | rupicola/bedrock2/compiler/src/compiler/MMIO.vo
  1m21.24s |  607772 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.vo
  1m20.59s | 1528152 ko | Assembly/EquivalenceProofs.vo
  1m20.11s |  750284 ko | Arithmetic/SolinasReduction.vo
  1m19.98s | 1135724 ko | UnsaturatedSolinasHeuristics/Tests.vo
  1m19.07s | 1580872 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.vo
  1m16.09s | 1015848 ko | PushButtonSynthesis/SolinasReductionReificationCache.vo
  1m09.19s | 1436812 ko | Assembly/WithBedrock/SymbolicProofs.vo
  1m07.33s |  803216 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/LAN9250.vo
  1m04.55s |  881276 ko | AbstractInterpretation/Wf.vo
  1m04.51s |  931300 ko | Curves/Weierstrass/Jacobian.vo
  1m03.62s |  782744 ko | Rewriter/Rewriter/Wf.vo
  0m59.64s |  704332 ko | Rewriter/RulesProofs.vo
  0m57.69s |  733928 ko | Rewriter/Language/UnderLetsProofs.vo
  0m56.72s | 1004580 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.vo
  0m53.99s |  833600 ko | AbstractInterpretation/ZRangeProofs.vo
  0m53.23s | 1044640 ko | Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo
  0m52.35s |  944996 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.vo
  0m51.52s |  625496 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/EncodeDecode.vo
  0m51.41s | 1011348 ko | Rewriter/Rewriter/Examples.vo
  0m51.35s | 1023708 ko | Rewriter/Passes/MultiRetSplit.vo
  0m50.98s |  831264 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo
  0m50.20s | 1302956 ko | Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo
  0m47.60s |  584048 ko | Demo.vo
  0m46.50s |  854544 ko | Rewriter/Rewriter/InterpProofs.vo
  0m45.91s | 1745024 ko | Fancy/Montgomery256.vo
  0m45.90s |  804912 ko | Rewriter/Rewriter/ProofsCommon.vo
  0m44.99s | 1530768 ko | Assembly/Symbolic.vo
  0m44.72s | 1102468 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo
  0m44.72s | 2147808 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery
  0m43.59s | 2147776 ko | ExtractionOCaml/bedrock2_solinas_reduction
  0m43.31s | 2147552 ko | ExtractionOCaml/solinas_reduction
  0m42.97s | 2147820 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery
  0m41.82s |   67656 ko | fiat-go/32/p521/p521.go
  0m41.14s |  569868 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricSane.vo
  0m41.05s |  625248 ko | rupicola/bedrock2/compiler/src/compiler/Spilling.vo
  0m41.01s | 2148412 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas
  0m40.68s | 2148192 ko | ExtractionOCaml/bedrock2_unsaturated_solinas
  0m40.68s | 1072812 ko | Rewriter/Passes/Arith.vo
  0m40.36s | 2147748 ko | ExtractionOCaml/word_by_word_montgomery
  0m39.88s | 1003376 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo
  0m38.76s |   60548 ko | fiat-java/src/FiatP521.java
  0m38.74s |  142728 ko | fiat-bedrock2/src/p521_32.c
  0m38.68s |  110444 ko | fiat-json/src/p521_32.json
  0m38.44s |   58400 ko | fiat-zig/src/p521_32.zig
  0m38.17s | 1691492 ko | ExtractionOCaml/unsaturated_solinas
  0m37.93s | 1633424 ko | ExtractionOCaml/bedrock2_dettman_multiplication
  0m37.93s |   59156 ko | fiat-c/src/p521_32.c
  0m37.73s | 1623156 ko | ExtractionOCaml/with_bedrock2_saturated_solinas
  0m37.70s |  708548 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo
  0m37.54s | 1624828 ko | ExtractionOCaml/with_bedrock2_base_conversion
  0m37.33s | 1624096 ko | ExtractionOCaml/bedrock2_saturated_solinas
  0m37.21s | 1622976 ko | ExtractionOCaml/with_bedrock2_solinas_reduction
  0m37.17s | 1620288 ko | ExtractionOCaml/bedrock2_base_conversion
  0m36.76s | 1623680 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication
  0m35.29s | 1415796 ko | ExtractionOCaml/dettman_multiplication
  0m34.64s | 1538708 ko | ExtractionOCaml/base_conversion
  0m34.35s |   60732 ko | fiat-rust/src/p521_32.rs
  0m34.33s | 1415896 ko | ExtractionOCaml/saturated_solinas
  0m34.18s | 2237120 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml
  0m33.80s | 2211416 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml
  0m33.32s | 2211048 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml
  0m33.32s |  877940 ko | Rewriter/Passes/MulSplit.vo
  0m33.30s | 1255200 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo
  0m32.38s | 2133140 ko | ExtractionOCaml/solinas_reduction.ml
  0m32.05s |  566656 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/EncodeBound.vo
  0m31.56s | 1232064 ko | ExtractionOCaml/perf_word_by_word_montgomery
  0m31.38s | 2108664 ko | ExtractionOCaml/word_by_word_montgomery.ml
  0m30.75s | 1232248 ko | ExtractionOCaml/perf_unsaturated_solinas
  0m30.68s | 2116064 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml
  0m30.48s |  617376 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvLiterals.vo
  0m30.13s | 2115380 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml
  0m30.01s | 1516352 ko | StandaloneDebuggingExamples.vo
  0m29.81s |  702960 ko | AbstractInterpretation/Proofs.vo
  0m28.53s | 2028924 ko | ExtractionOCaml/unsaturated_solinas.ml
  0m28.11s |  664744 ko | rupicola/src/Rupicola/Examples/Utf8/Utf8.vo
  0m27.87s |  876328 ko | Rewriter/Rewriter/Examples/PrefixSums.vo
  0m27.32s | 2051412 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml
  0m26.62s |  687116 ko | Rewriter/Language/Wf.vo
  0m26.58s | 2005604 ko | ExtractionOCaml/bedrock2_base_conversion.ml
  0m26.45s | 1996160 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml
  0m26.36s | 2005536 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml
  0m26.27s | 1996184 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml
  0m26.18s | 1999292 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml
  0m26.15s | 1998300 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml
  0m25.87s |  590672 ko | Rewriter/Language/Inversion.vo
  0m25.26s | 1371200 ko | PerfTesting/PerfTestSearch.vo
  0m25.09s | 1938912 ko | ExtractionOCaml/dettman_multiplication.ml
  0m24.54s | 1924440 ko | ExtractionOCaml/saturated_solinas.ml
  0m24.23s | 1921016 ko | ExtractionOCaml/base_conversion.ml
  0m23.60s | 1179724 ko | PushButtonSynthesis/UnsaturatedSolinas.vo
  0m23.31s |  874692 ko | Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo
  0m22.72s |  499960 ko | Arithmetic/Saturated.vo
  0m21.95s | 1329776 ko | Bedrock/End2End/RupicolaCrypto/Low.vo
  0m20.78s |  813596 ko | Bedrock/Field/Translation/Proofs/Expr.vo
  0m20.30s | 1149392 ko | PushButtonSynthesis/WordByWordMontgomery.vo
  0m20.07s |  747300 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo
  0m19.54s |  629200 ko | Util/FSets/FMapBool.vo
  0m19.45s |  694948 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memmove.vo
  0m19.35s | 1838828 ko | ExtractionOCaml/perf_unsaturated_solinas.ml
  0m19.22s |  680380 ko | rupicola/bedrock2/compiler/src/compiler/FlatImp.vo
  0m19.16s | 1828412 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml
  0m18.94s |  313308 ko | fiat-go/64/p434/p434.go
  0m18.72s |  244116 ko | fiat-zig/src/p434_64.zig
  0m18.38s |  634116 ko | Util/FSets/FMapProd.vo
  0m17.79s |  281552 ko | fiat-json/src/p434_64.json
  0m17.78s |  487432 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_32.c
  0m17.74s | 1370888 ko | PerfTesting/PerfTestSearchPattern.vo
  0m17.71s |  302348 ko | fiat-bedrock2/src/p434_64.c
  0m17.68s |  431072 ko | fiat-zig/src/secp256k1_montgomery_scalar_32.zig
  0m17.67s |  379652 ko | fiat-json/src/secp256k1_montgomery_scalar_32.json
  0m17.58s | 1155688 ko | Bedrock/Field/Translation/Proofs/Cmd.vo
  0m17.52s |  255060 ko | fiat-c/src/p434_64.c
  0m17.50s | 1128196 ko | Bedrock/Field/Translation/Proofs/Func.vo
  0m17.50s |  397092 ko | fiat-bedrock2/src/p256_scalar_32.c
  0m17.41s | 1120356 ko | Bedrock/End2End/Poly1305/Field1305.vo
  0m17.33s |  376544 ko | fiat-go/32/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go
  0m17.32s |  373956 ko | fiat-json/src/p256_scalar_32.json
  0m17.30s |  407340 ko | fiat-json/src/secp256k1_montgomery_32.json
  0m17.26s |  567160 ko | Util/FSets/FMapSum.vo
  0m17.26s |  363444 ko | fiat-java/src/FiatSecp256K1MontgomeryScalar.java
  0m17.20s |  306884 ko | fiat-rust/src/p434_64.rs
  0m17.17s | 1109240 ko | Assembly/Parse/TestAsm.vo
  0m17.17s |  438860 ko | fiat-java/src/FiatP256Scalar.java
  0m17.13s |  413312 ko | fiat-go/32/p256scalar/p256scalar.go
  0m17.06s |  415760 ko | fiat-json/src/curve25519_scalar_32.json
  0m17.03s |  396804 ko | fiat-zig/src/secp256k1_montgomery_32.zig
  0m16.90s |  395476 ko | fiat-bedrock2/src/curve25519_scalar_32.c
  0m16.90s |  436536 ko | fiat-c/src/secp256k1_montgomery_scalar_32.c
  0m16.88s |  422848 ko | fiat-java/src/FiatSecp256K1Montgomery.java
  0m16.85s |  542932 ko | Arithmetic/WordByWordMontgomery.vo
  0m16.84s |  344632 ko | fiat-go/32/secp256k1montgomery/secp256k1montgomery.go
  0m16.79s |  384576 ko | fiat-bedrock2/src/secp256k1_montgomery_32.c
  0m16.77s |  345256 ko | fiat-rust/src/p256_scalar_32.rs
  0m16.68s |  323816 ko | fiat-java/src/FiatCurve25519Scalar.java
  0m16.64s |  340412 ko | fiat-go/32/curve25519scalar/curve25519scalar.go
  0m16.63s |  620464 ko | Util/ZUtil/ArithmeticShiftr.vo
  0m16.63s |  407304 ko | fiat-zig/src/curve25519_scalar_32.zig
  0m16.60s | 1200944 ko | Bedrock/Field/Synthesis/New/Signature.vo
  0m16.60s |  365388 ko | fiat-c/src/p256_scalar_32.c
  0m16.57s |  368480 ko | fiat-rust/src/secp256k1_montgomery_scalar_32.rs
  0m16.53s |  833896 ko | Curves/Edwards/XYZT/Basic.vo
  0m16.50s | 2124656 ko | ExtractionHaskell/bedrock2_solinas_reduction.hs
  0m16.39s | 2120524 ko | ExtractionHaskell/with_bedrock2_solinas_reduction.hs
  0m16.38s |  432820 ko | fiat-json/src/p256_32.json
  0m16.37s |  430104 ko | fiat-zig/src/p256_scalar_32.zig
  0m16.35s |  330524 ko | fiat-c/src/curve25519_scalar_32.c
  0m16.32s |  349716 ko | fiat-zig/src/p256_32.zig
  0m16.27s | 2013724 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs
  0m16.24s |  364604 ko | fiat-rust/src/curve25519_scalar_32.rs
  0m16.19s |  402376 ko | fiat-rust/src/secp256k1_montgomery_32.rs
  0m16.04s |  765616 ko | Language/IdentifiersGENERATED.vo
  0m16.01s |  563772 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_SB.vo
  0m16.00s |  573536 ko | Bedrock/Field/Synthesis/Examples/redc.vo
  0m15.97s | 2014024 ko | ExtractionHaskell/with_bedrock2_word_by_word_montgomery.hs
  0m15.89s |  421264 ko | fiat-c/src/secp256k1_montgomery_32.c
  0m15.84s |  364416 ko | fiat-java/src/FiatP256.java
  0m15.77s |  395208 ko | fiat-bedrock2/src/p256_32.c
  0m15.71s | 1964864 ko | ExtractionHaskell/solinas_reduction.hs
  0m15.69s |  323896 ko | fiat-c/src/p256_32.c
  0m15.66s |  726776 ko | Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo
  0m15.62s |  405156 ko | fiat-go/32/p256/p256.go
  0m15.55s |  766356 ko | Curves/Edwards/AffineProofs.vo
  0m15.37s |  568164 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA.vo
  0m15.33s |  370928 ko | fiat-rust/src/p256_32.rs
  0m15.29s | 1983440 ko | ExtractionHaskell/word_by_word_montgomery.hs
  0m15.19s |  520360 ko | Arithmetic/BarrettReduction.vo
  0m15.12s |  425240 ko | rupicola/bedrock2/deps/coqutil/test/TestGoals.vo
  0m14.91s |  516204 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_66.vo
  0m14.84s | 1909292 ko | ExtractionHaskell/with_bedrock2_base_conversion.hs
  0m14.83s |  596008 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI64.vo
  0m14.79s |  463028 ko | Algebra/Field.vo
  0m14.67s | 1999460 ko | ExtractionHaskell/with_bedrock2_unsaturated_solinas.hs
  0m14.66s | 1860044 ko | ExtractionHaskell/unsaturated_solinas.hs
  0m14.61s | 1998800 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs
  0m14.55s |  487988 ko | rupicola/bedrock2/compiler/src/compiler/RunInstruction.vo
  0m14.49s |  565196 ko | Util/FSets/FMapOption.vo
  0m14.47s | 1910172 ko | ExtractionHaskell/bedrock2_base_conversion.hs
  0m14.45s | 1896592 ko | ExtractionHaskell/bedrock2_dettman_multiplication.hs
  0m14.35s | 1917576 ko | ExtractionHaskell/with_bedrock2_saturated_solinas.hs
  0m14.30s | 1897756 ko | ExtractionHaskell/with_bedrock2_dettman_multiplication.hs
  0m14.22s | 1917456 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs
  0m14.19s |  593376 ko | Language/IdentifiersGENERATEDProofs.vo
  0m14.13s |  526388 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/IPChecksum.vo
  0m14.01s |  660304 ko | Bedrock/Group/AdditionChains.vo
  0m13.89s |  462944 ko | Util/Structures/Orders/Prod.vo
  0m13.85s |  491540 ko | rupicola/src/Rupicola/Examples/Arrays.vo
  0m13.83s |  544744 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA64.vo
  0m13.79s |  498032 ko | rupicola/src/Rupicola/Examples/CMove/CMove.vo
  0m13.77s |  598308 ko | Bedrock/Field/Common/Util.vo
  0m13.61s | 1811276 ko | ExtractionHaskell/dettman_multiplication.hs
  0m13.60s | 1846816 ko | ExtractionHaskell/saturated_solinas.hs
  0m13.55s |  492116 ko | rupicola/src/Rupicola/Examples/Loops.vo
  0m13.46s |  538316 ko | rupicola/src/Rupicola/Examples/KVStore/Manual.vo
  0m13.27s | 1793716 ko | ExtractionHaskell/base_conversion.hs
  0m13.21s |  649252 ko | Bedrock/Group/ScalarMult/LadderStep.vo
  0m12.82s |  494032 ko | Arithmetic/Core.vo
  0m11.93s | 1026788 ko | BoundsPipeline.vo
  0m11.86s |  637944 ko | Rewriter/Demo.vo
  0m11.73s |  545076 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM.vo
  0m11.72s |  707092 ko | Util/ZRange/LandLorBounds.vo
  0m11.52s |  484076 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.vo
  0m11.38s | 1677648 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo
  0m11.28s |  165124 ko | fiat-go/64/p384scalar/p384scalar.go
  0m11.23s |  153540 ko | fiat-c/src/p384_scalar_64.c
  0m11.20s |  197432 ko | fiat-json/src/p384_scalar_64.json
  0m11.13s |  192732 ko | fiat-bedrock2/src/p384_scalar_64.c
  0m11.10s |  165668 ko | fiat-zig/src/p384_scalar_64.zig
  0m11.00s |  658176 ko | rupicola/bedrock2/compiler/src/compiler/SpillingMapGoals.vo
  0m10.96s |  165272 ko | fiat-rust/src/p384_scalar_64.rs
  0m10.65s |  505684 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_UJ.vo
  0m10.64s |  476416 ko | Primitives/MxDHRepChange.vo
  0m10.41s |  742196 ko | Assembly/Syntax.vo
  0m10.37s | 1339924 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo
  0m10.32s |  459448 ko | Util/Structures/Orders/List.vo
  0m10.24s |  451276 ko | Algebra/Ring.vo
  0m10.12s |  622652 ko | Bedrock/Field/Translation/Proofs/Flatten.vo
  0m10.02s |  579416 ko | PushButtonSynthesis/BYInversionReificationCache.vo
  0m09.85s |  182968 ko | fiat-c/src/p384_64.c
  0m09.77s |  173092 ko | fiat-json/src/p384_64.json
  0m09.76s |  164688 ko | fiat-go/64/p384/p384.go
  0m09.66s |  139760 ko | fiat-zig/src/p384_64.zig
  0m09.62s |  872852 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.vo
  0m09.59s |  250704 ko | fiat-zig/src/p224_32.zig
  0m09.52s |  238320 ko | fiat-json/src/p224_32.json
  0m09.49s |  230008 ko | fiat-go/32/p224/p224.go
  0m09.47s |  203968 ko | fiat-bedrock2/src/p384_64.c
  0m09.47s |  272744 ko | fiat-java/src/FiatP224.java
  0m09.43s |  658732 ko | Bedrock/Group/ScalarMult/CSwap.vo
  0m09.43s |  595324 ko | Stringification/IR.vo
  0m09.40s |  558640 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo
  0m09.37s |  554444 ko | PushButtonSynthesis/DettmanMultiplicationReificationCache.vo
  0m09.32s |  258236 ko | fiat-bedrock2/src/p224_32.c
  0m09.29s |  177692 ko | fiat-rust/src/p384_64.rs
  0m09.28s | 1030020 ko | PushButtonSynthesis/BaseConversion.vo
  0m09.27s |  270084 ko | fiat-c/src/p224_32.c
  0m09.24s |  550836 ko | rupicola/bedrock2/compiler/src/compiler/ToplevelLoop.vo
  0m09.10s |  230652 ko | fiat-rust/src/p224_32.rs
  0m09.01s |  506588 ko | Rewriter/Language/IdentifiersLibraryProofs.vo
  0m08.90s |  497908 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/SPI.vo
  0m08.58s |  123780 ko | fiat-json/src/p448_solinas_32.json
  0m08.35s |  600540 ko | Language/IdentifiersBasicGENERATED.vo
  0m08.33s | 1038828 ko | PushButtonSynthesis/Primitives.vo
  0m08.23s |  998908 ko | PushButtonSynthesis/SmallExamples.vo
  0m08.15s |  785760 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed6.vo
  0m08.14s |  912272 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo
  0m08.14s |   59548 ko | fiat-rust/src/p448_solinas_32.rs
  0m08.03s |   58124 ko | fiat-zig/src/p448_solinas_32.zig
  0m07.90s |   58212 ko | fiat-c/src/p448_solinas_32.c
  0m07.80s |  527792 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/FE310CompilerDemo.vo
  0m07.77s |  462448 ko | rupicola/src/Rupicola/Examples/KVStore/Automated.vo
  0m07.70s |  587264 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo
  0m07.52s |  491008 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/uint128_32.vo
  0m07.45s |  471188 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_S.vo
  0m07.44s |  468880 ko | Util/ZRange/CornersMonotoneBounds.vo
  0m07.26s | 1031232 ko | PushButtonSynthesis/SolinasReduction.vo
  0m07.15s |  659224 ko | Util/FSets/FMapTrieEx.vo
  0m06.85s |  471788 ko | rupicola/src/Rupicola/Examples/L64X128.vo
  0m06.84s |  708648 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed4.vo
  0m06.79s |  459008 ko | rupicola/src/Rupicola/Examples/Expr.vo
  0m06.74s |  450284 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/indirect_add.vo
  0m06.54s |  492712 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/bsearch.vo
  0m06.50s |  546780 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo
  0m06.41s |  467236 ko | Arithmetic/FancyMontgomeryReduction.vo
  0m06.37s | 1134776 ko | CLI.vo
  0m06.33s |   49900 ko | fiat-go/64/p521/p521.go
  0m06.32s | 1037180 ko | PushButtonSynthesis/BarrettReduction.vo
  0m06.31s |  679460 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.vo
  0m06.31s |  457988 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_Fence.vo
  0m06.19s |  458048 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R_atomic.vo
  0m06.18s | 1132992 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo
  0m06.16s |  543604 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo
  0m06.06s |  902704 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo
  0m06.06s |  438980 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Minimal.vo
  0m06.05s |  574516 ko | Rewriter/Passes/NoSelect.vo
  0m06.03s |  480020 ko | rupicola/bedrock2/compiler/src/compiler/RegAlloc.vo
  0m06.01s |  671264 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.vo
  0m05.97s |  486436 ko | Util/ZUtil/Modulo.vo
  0m05.86s |  466112 ko | Util/ListUtil.vo
  0m05.85s |  469760 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM64.vo
  0m05.57s |   51132 ko | fiat-json/src/p521_64.json
  0m05.56s |  682812 ko | rupicola/bedrock2/bedrock2/src/bedrock2/HeapletwiseAutoSplitMerge.vo
  0m05.54s |   65620 ko | fiat-bedrock2/src/p521_64.c
  0m05.51s |   36024 ko | fiat-zig/src/p521_64.zig
  0m05.45s |  460124 ko | Util/MSets/MSetSum.vo
  0m05.45s |   36640 ko | fiat-c/src/p521_64.c
  0m05.43s |  532688 ko | Fancy/Prod.vo
  0m05.41s |  576128 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Properties.vo
  0m05.40s |  614228 ko | Bedrock/End2End/RupicolaCrypto/Broadcast.vo
  0m05.40s |   36120 ko | fiat-rust/src/p521_64.rs
  0m05.36s |  461088 ko | rupicola/bedrock2/compiler/src/compiler/ExprImp.vo
  0m05.28s |  453952 ko | Rewriter/Util/ListUtil.vo
  0m05.12s |  513604 ko | Arithmetic/BYInv.vo
  0m05.10s |  454392 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/FlatConstMem.vo
  0m04.95s |  470428 ko | rupicola/src/Rupicola/Lib/Loops.vo
  0m04.94s |  467968 ko | Util/FsatzAutoLemmas.vo
  0m04.93s |  432264 ko | Spec/Curve25519.vo
  0m04.83s |  462000 ko | rupicola/src/Rupicola/Examples/CRC32/CRC32.vo
  0m04.73s |  498572 ko | Curves/Edwards/Pre.vo
  0m04.72s |  550548 ko | Language/InversionExtra.vo
  0m04.61s |  455752 ko | Util/FSets/FMapIso.vo
  0m04.59s |  448220 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.vo
  0m04.55s |  472888 ko | rupicola/src/Rupicola/Examples/CapitalizeThird/Properties.vo
  0m04.49s | 1063260 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo
  0m04.42s |  465320 ko | Util/ZRange/BasicLemmas.vo
  0m04.38s |  445356 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_57.vo
  0m04.38s |  444300 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R.vo
  0m04.37s | 1028072 ko | PushButtonSynthesis/DettmanMultiplication.vo
  0m04.32s | 1034544 ko | PushButtonSynthesis/SaturatedSolinas.vo
  0m04.28s |  553116 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRFile.vo
  0m04.26s |  460864 ko | Util/FSets/FMapSect.vo
  0m04.24s |  434096 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/BenchCancel256.vo
  0m04.24s |  470912 ko | rupicola/bedrock2/compiler/src/compiler/LowerPipeline.vo
  0m04.19s |  446352 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_FenceI.vo
  0m04.18s |  955212 ko | Assembly/Equivalence.vo
  0m04.13s |  445192 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I.vo
  0m04.10s |  474136 ko | Algebra/Field_test.vo
  0m04.02s |  434628 ko | Arithmetic/MontgomeryReduction/Proofs.vo
  0m04.00s |  470212 ko | Rewriter/Language/IdentifiersBasicLibrary.vo
  0m03.97s |  492300 ko | COperationSpecifications.vo
  0m03.96s | 1483248 ko | Bedrock/Everything.vo
  0m03.95s |  565888 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed46.vo
  0m03.92s |  461212 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memequal.vo
  0m03.89s |  438292 ko | rupicola/src/Rupicola/Examples/Cells/IndirectAdd.vo
  0m03.84s | 1047084 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo
  0m03.76s |  460392 ko | rupicola/src/Rupicola/Examples/Uppercase.vo
  0m03.74s |  487816 ko | Curves/Montgomery/Affine.vo
  0m03.62s | 1341008 ko | Everything.vo
  0m03.51s |  451668 ko | Arithmetic/BarrettReduction/Generalized.vo
  0m03.50s |  456840 ko | CastLemmas.vo
  0m03.49s |  545604 ko | PushButtonSynthesis/BaseConversionReificationCache.vo
  0m03.47s |  415800 ko | rupicola/bedrock2/deps/coqutil/test/SlowGoals.vo
  0m03.42s |  394996 ko | Algebra/Group.vo
  0m03.42s |  453312 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memswap.vo
  0m03.37s |  460156 ko | UnsaturatedSolinasHeuristics.vo
  0m03.36s |  435964 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalNoMul.vo
  0m03.35s |  454600 ko | Arithmetic/UniformWeight.vo
  0m03.33s |  444692 ko | Util/ZUtil/LandLorShiftBounds.vo
  0m03.27s |  448912 ko | rupicola/src/Rupicola/Examples/Arithmetic.vo
  0m03.24s |  434864 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_system.vo
  0m03.21s |  449104 ko | Arithmetic/BarrettReduction/HAC.vo
  0m03.20s |  449096 ko | Util/ZUtil/LandLorBounds.vo
  0m03.15s | 1006432 ko | Bedrock/Field/Translation/Cmd.vo
  0m03.14s |  677116 ko | Bedrock/Group/ScalarMult/ScalarMult.vo
  0m03.13s | 1070140 ko | Rewriter/PerfTesting/Core.vo
  0m03.10s |  446044 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO.vo
  0m03.07s | 1343548 ko | PerfTesting/PerfTestPrint.vo
  0m03.06s |  446136 ko | Util/Structures/Orders.vo
  0m02.99s |  446820 ko | rupicola/src/Rupicola/Examples/RevComp.vo
  0m02.97s | 1002728 ko | Bedrock/Field/Translation/Func.vo
  0m02.95s | 1066612 ko | Bedrock/Field/Stringification/Stringification.vo
  0m02.95s |  609264 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo
  0m02.90s |  442416 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/List.vo
  0m02.89s |   75160 ko | fiat-json/src/p256_scalar_64.json
  0m02.84s |  411248 ko | Coqprime/PrimalityTest/PocklingtonCertificat.vo
  0m02.84s |   61996 ko | fiat-go/64/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go
  0m02.82s |   84244 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_64.c
  0m02.82s |   72148 ko | fiat-json/src/secp256k1_montgomery_scalar_64.json
  0m02.80s | 1103808 ko | StandaloneOCamlMain.vo
  0m02.80s |   84916 ko | fiat-bedrock2/src/p256_scalar_64.c
  0m02.80s |  427948 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_U.vo
  0m02.79s |   64876 ko | fiat-go/64/p256scalar/p256scalar.go
  0m02.78s |  439896 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ipow.vo
  0m02.77s | 1059012 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo
  0m02.77s |   57088 ko | fiat-zig/src/secp256k1_montgomery_scalar_64.zig
  0m02.75s | 1143348 ko | Bedrock/Standalone/StandaloneHaskellMain.vo
  0m02.75s |  431748 ko | Util/Structures/Orders/Option.vo
  0m02.75s |  433944 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Properties.vo
  0m02.74s | 1103744 ko | StandaloneHaskellMain.vo
  0m02.74s |   56376 ko | fiat-c/src/p256_scalar_64.c
  0m02.74s |   60560 ko | fiat-rust/src/secp256k1_montgomery_scalar_64.rs
  0m02.74s |  451660 ko | rupicola/bedrock2/compiler/src/compiler/UseImmediate.vo
  0m02.73s |   61824 ko | fiat-zig/src/p256_scalar_64.zig
  0m02.72s | 1064916 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo
  0m02.71s |  519732 ko | Rewriter/Passes/Test.vo
  0m02.71s |   61076 ko | fiat-c/src/secp256k1_montgomery_scalar_64.c
  0m02.71s |   60028 ko | fiat-rust/src/p256_scalar_64.rs
  0m02.70s |  535708 ko | Rewriter/Passes/AddAssocLeft.vo
  0m02.68s |   51016 ko | fiat-go/64/p448solinas/p448solinas.go
  0m02.67s |  442740 ko | Arithmetic/Primitives.vo
  0m02.65s |  438452 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/swap_by_add.vo
  0m02.64s | 1143212 ko | Bedrock/Standalone/StandaloneOCamlMain.vo
  0m02.60s |  443440 ko | rupicola/src/Rupicola/Examples/IO/Echo.vo
  0m02.59s |  549304 ko | Util/FSets/FMapTrie/ShapeEx.vo
  0m02.58s | 1129176 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo
  0m02.58s |  434880 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/MulTrapHandler.vo
  0m02.57s |  621908 ko | Bedrock/Field/Interface/Compilation2.vo
  0m02.56s | 1042648 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo
  0m02.55s |   71208 ko | fiat-go/64/secp256k1montgomery/secp256k1montgomery.go
  0m02.55s |   75224 ko | fiat-json/src/secp256k1_montgomery_64.json
  0m02.54s | 1043268 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo
  0m02.52s |   59660 ko | fiat-zig/src/secp256k1_montgomery_64.zig
  0m02.50s | 1043292 ko | Bedrock/Field/Translation/Parameters/FE310.vo
  0m02.48s |  426684 ko | Util/ZUtil/ZSimplify/Autogenerated.vo
  0m02.48s |   68740 ko | fiat-json/src/curve25519_scalar_64.json
  0m02.47s |   57260 ko | fiat-c/src/secp256k1_montgomery_64.c
  0m02.46s | 1038448 ko | Bedrock/Field/Translation/Parameters/Defaults.vo
  0m02.43s |   82756 ko | fiat-bedrock2/src/secp256k1_montgomery_64.c
  0m02.43s |  447172 ko | rupicola/src/Rupicola/Lib/Core.vo
  0m02.42s |  537004 ko | Rewriter/Passes/FlattenThunkedRects.vo
  0m02.42s |   64252 ko | fiat-rust/src/secp256k1_montgomery_64.rs
  0m02.41s |  425468 ko | Util/Bool/Reflect.vo
  0m02.41s |  441108 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/rpmul.vo
  0m02.40s |  423368 ko | Rewriter/Util/Bool/Reflect.vo
  0m02.40s |  470248 ko | Util/ZUtil/Morphisms.vo
  0m02.38s |  467216 ko | MiscCompilerPassesProofs.vo
  0m02.38s |  468844 ko | rupicola/bedrock2/bedrock2/src/bedrock2/unzify.vo
  0m02.38s |  443668 ko | rupicola/src/Rupicola/Examples/DownTo.vo
  0m02.37s |   67816 ko | fiat-go/64/curve25519scalar/curve25519scalar.go
  0m02.36s |  449676 ko | Util/MSets/MSetIso.vo
  0m02.36s |   77284 ko | fiat-bedrock2/src/curve25519_scalar_64.c
  0m02.35s |  545536 ko | Bedrock/Field/Translation/Expr.vo
  0m02.34s |   55824 ko | fiat-zig/src/curve25519_scalar_64.zig
  0m02.30s |  459484 ko | Spec/MontgomeryCurve.vo
  0m02.29s |  448692 ko | rupicola/src/Rupicola/Examples/LinkedList/Find.vo
  0m02.28s |  444516 ko | Util/ZUtil/Shift.vo
  0m02.28s |   61352 ko | fiat-c/src/curve25519_scalar_64.c
  0m02.26s |   61228 ko | fiat-rust/src/curve25519_scalar_64.rs
  0m02.26s |  463064 ko | rupicola/bedrock2/compiler/src/compiler/Pipeline.vo
  0m02.24s |  429604 ko | Util/ZUtil/TwosComplement.vo
  0m02.17s |  456624 ko | rupicola/bedrock2/compiler/src/compiler/load_save_regs_correct.vo
  0m02.16s |   35384 ko | fiat-go/32/curve25519/curve25519.go
  0m02.13s |  611384 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo
  0m02.12s |  434664 ko | rupicola/bedrock2/bedrock2/src/bedrock2/HeapletwiseHyps.vo
  0m02.12s |  446464 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepAutoArray.vo
  0m02.09s |   67276 ko | fiat-bedrock2/src/p448_solinas_64.c
  0m02.08s |   51372 ko | fiat-json/src/p448_solinas_64.json
  0m02.05s |  456784 ko | Arithmetic/Freeze.vo
  0m02.04s |  541056 ko | Stringification/Language.vo
  0m02.01s |  417420 ko | rupicola/bedrock2/bedrock2/src/bedrock2/AbsintWordToZ.vo
  0m01.97s |   61072 ko | fiat-go/64/p224/p224.go
  0m01.97s |   75016 ko | fiat-json/src/p224_64.json
  0m01.97s |   35100 ko | fiat-zig/src/p448_solinas_64.zig
  0m01.96s |   63284 ko | fiat-bedrock2/src/curve25519_32.c
  0m01.96s |   34764 ko | fiat-rust/src/p448_solinas_64.rs
  0m01.95s |  456464 ko | Arithmetic/BaseConversion.vo
  0m01.95s |  435856 ko | Util/ZUtil/Testbit.vo
  0m01.95s |   49468 ko | fiat-json/src/curve25519_32.json
  0m01.94s |  464252 ko | Curves/TableMult/TableMult.vo
  0m01.92s |  445120 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memconst.vo
  0m01.91s |  389284 ko | Util/Wf2.vo
  0m01.91s |   77496 ko | fiat-bedrock2/src/p224_64.c
  0m01.90s |   34496 ko | fiat-c/src/p448_solinas_64.c
  0m01.89s |   66076 ko | fiat-go/64/p256/p256.go
  0m01.89s |   62320 ko | fiat-zig/src/p224_64.zig
  0m01.88s |  431764 ko | Util/ZUtil/ModInv.vo
  0m01.88s |   34152 ko | fiat-java/src/FiatCurve25519.java
  0m01.88s |   66424 ko | fiat-json/src/p256_64.json
  0m01.86s |   56312 ko | fiat-c/src/p224_64.c
  0m01.86s |  441768 ko | rupicola/bedrock2/bedrock2/src/bedrock2/bottom_up_simpl_ltac1.vo
  0m01.85s |   55924 ko | fiat-zig/src/p256_64.zig
  0m01.83s |  536604 ko | Rewriter/Passes/UnfoldValueBarrier.vo
  0m01.83s |   77644 ko | fiat-bedrock2/src/p256_64.c
  0m01.83s |   33544 ko | fiat-zig/src/curve25519_32.zig
  0m01.82s |   33528 ko | fiat-c/src/curve25519_32.c
  0m01.81s |  535512 ko | Rewriter/Passes/StripLiteralCasts.vo
  0m01.81s |   66316 ko | fiat-rust/src/p224_64.rs
  0m01.79s |  429896 ko | Util/ZUtil/Div.vo
  0m01.79s |   61824 ko | fiat-c/src/p256_64.c
  0m01.76s |   34144 ko | fiat-rust/src/curve25519_32.rs
  0m01.75s |  433864 ko | Arithmetic/BarrettReduction/RidiculousFish.vo
  0m01.75s |   59120 ko | fiat-rust/src/p256_64.rs
  0m01.75s |  435556 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/stackalloc.vo
  0m01.74s |  419580 ko | Util/ListUtil/Forall.vo
  0m01.71s |  634084 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo
  0m01.69s |  463032 ko | Arithmetic/DettmanMultiplication.vo
  0m01.67s |  446804 ko | Arithmetic/ModularArithmeticTheorems.vo
  0m01.67s |  438212 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/WMMFree.vo
  0m01.64s |  454032 ko | Arithmetic/ModOps.vo
  0m01.63s |  446228 ko | Util/FSets/FMapFacts.vo
  0m01.63s |  456584 ko | rupicola/src/Rupicola/Lib/Arrays.vo
  0m01.61s |  536468 ko | Rewriter/Passes/ToFancy.vo
  0m01.60s |  481268 ko | Assembly/Parse.vo
  0m01.59s |  427624 ko | rupicola/bedrock2/bedrock2/src/bedrock2/WeakestPreconditionProperties.vo
  0m01.55s |  605636 ko | Bedrock/Field/Common/Names/MakeNames.vo
  0m01.54s |  511864 ko | AbstractInterpretation/AbstractInterpretation.vo
  0m01.54s |  589320 ko | CompilersTestCases.vo
  0m01.54s |  433340 ko | Util/Tuple.vo
  0m01.52s |  461152 ko | Util/FSets/FMapUnit.vo
  0m01.49s |  451136 ko | rupicola/bedrock2/compiler/src/compiler/GoFlatToRiscv.vo
  0m01.48s |  518524 ko | AbstractInterpretation/ZRange.vo
  0m01.48s |  462156 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised.vo
  0m01.48s |  464356 ko | rupicola/bedrock2/compiler/src/compiler/CompilerInvariant.vo
  0m01.48s |  430244 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/Fib.vo
  0m01.47s |  458800 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed10.vo
  0m01.47s |  436092 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Loops.vo
  0m01.45s |  435748 ko | rupicola/bedrock2/compiler/src/compiler/SeparationLogic.vo
  0m01.44s |  436208 ko | rupicola/src/Rupicola/Examples/Conditionals.vo
  0m01.43s |  446448 ko | rupicola/src/Rupicola/Examples/Nondeterminism/StackAlloc.vo
  0m01.41s |  423320 ko | Algebra/ScalarMult.vo
  0m01.40s |  411744 ko | Rewriter/Util/ListUtil/Forall.vo
  0m01.38s |  541876 ko | Stringification/Go.vo
  0m01.38s |  385056 ko | rupicola/bedrock2/bedrock2/src/bedrock2/StringdumpDemo.vo
  0m01.37s |  452204 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed20.vo
  0m01.37s |  411588 ko | Coqprime/Z/Pmod.vo
  0m01.37s |  436708 ko | Spec/WeierstrassCurve.vo
  0m01.37s |  430856 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Semantics.vo
  0m01.37s |  434736 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ZnWordsTests.vo
  0m01.37s |  438944 ko | rupicola/src/Rupicola/Lib/ControlFlow/DownTo.vo
  0m01.34s |  438172 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/Impl.vo
  0m01.33s |  448576 ko | Util/ZRange/SplitRangeBounds.vo
  0m01.33s |  435892 ko | Util/ZUtil/Pow2Mod.vo
  0m01.33s |  415496 ko | Util/ZUtil/Rshi.vo
  0m01.33s |  414960 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/MapEauto.vo
  0m01.30s |  452228 ko | rupicola/bedrock2/compiler/src/compiler/FitsStack.vo
  0m01.29s |  414900 ko | Util/ListUtil/StdlibCompat.vo
  0m01.28s |  468404 ko | Rewriter/Language/IdentifiersLibrary.vo
  0m01.26s |  436408 ko | Util/ZUtil/TruncatingShiftl.vo
  0m01.26s |  425820 ko | rupicola/bedrock2/bedrock2/src/bedrock2/FrameRule.vo
  0m01.26s |  439488 ko | rupicola/src/Rupicola/Lib/Compiler.vo
  0m01.25s |  445464 ko | rupicola/src/Rupicola/Lib/InlineTables.vo
  0m01.23s |  408764 ko | Rewriter/Rewriter/Examples/PerfTesting/Harness.vo
  0m01.22s |  438096 ko | Util/ZUtil/Bitwise.vo
  0m01.21s |  413612 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Map/SeparationLogic.vo
  0m01.20s |  442084 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ARPResponderProofs.vo
  0m01.18s |  424488 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/InstructionSetOrder.vo
  0m01.15s |  624520 ko | Bedrock/Specs/Field.vo
  0m01.15s |  438748 ko | Util/ZUtil/Quot.vo
  0m01.14s |  431584 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.vo
  0m01.10s |  418728 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/LittleEndianList.vo
  0m01.09s |  430968 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimalMMIO.vo
  0m01.08s |  446720 ko | Arithmetic/Partition.vo
  0m01.08s |  467272 ko | Arithmetic/PrimeFieldTheorems.vo
  0m01.08s |  410040 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/PropSet.vo
  0m01.08s |  411032 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/ident_of_string.vo
  0m01.06s |  445080 ko | Util/ZRange/SplitBounds.vo
  0m01.06s |  424436 ko | Util/ZUtil/AddGetCarry.vo
  0m01.05s |  603076 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo
  0m01.03s |  427980 ko | rupicola/bedrock2/bedrock2/src/bedrock2/sepapp.vo
  0m01.03s |  434252 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/swap.vo
  0m01.03s |  434100 ko | rupicola/src/Rupicola/Examples/Cells/Swap.vo
  0m01.03s |  442092 ko | rupicola/src/Rupicola/Lib/ControlFlow/CondSwap.vo
  0m01.02s |  596904 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo
  0m01.02s |  443508 ko | Fancy/Spec.vo
  0m01.02s |  466996 ko | Rewriter/Rewriter/Rewriter.vo
  0m01.01s |  359856 ko | Util/Wf1.vo
  0m00.98s |  536992 ko | Stringification/JSON.vo
  0m00.97s |  442992 ko | Curves/Edwards/XYZT/Precomputed.vo
  0m00.97s |  434212 ko | Util/ZUtil/Ones.vo
  0m00.97s |  425836 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ZWordMem.vo
  0m00.96s |  414848 ko | Coqprime/PrimalityTest/EGroup.vo
  0m00.96s |  408248 ko | Coqprime/PrimalityTest/LucasLehmer.vo
  0m00.95s |  539748 ko | Bedrock/Field/Translation/LoadStoreList.vo
  0m00.95s |  538524 ko | Stringification/C.vo
  0m00.95s |  443136 ko | rupicola/src/Rupicola/Examples/Nondeterminism/Peek.vo
  0m00.94s |  476676 ko | Rewriter/Rewriter/Reify.vo
  0m00.92s |  442380 ko | rupicola/src/Rupicola/Examples/LinkedList/LinkedList.vo
  0m00.90s |  432192 ko | Rewriter/Language/Language.vo
  0m00.90s |  427340 ko | Util/ZUtil/OnesFrom.vo
  0m00.89s |  420356 ko | Util/NatUtil.vo
  0m00.89s |  426296 ko | Util/Strings/ParseArithmetic.vo
  0m00.88s |  413948 ko | Rewriter/Util/NatUtil.vo
  0m00.88s |  431960 ko | Util/Structures/Orders/Sum.vo
  0m00.87s |  537912 ko | Bedrock/Field/Translation/Proofs/Equivalence.vo
  0m00.87s |  537860 ko | Stringification/Zig.vo
  0m00.85s |  535744 ko | Stringification/Rust.vo
  0m00.84s |  615480 ko | Bedrock/Field/Interface/Representation.vo
  0m00.84s |  408404 ko | Coqprime/Z/ZCAux.vo
  0m00.83s |  535716 ko | Stringification/Java.vo
  0m00.82s |  534452 ko | Bedrock/Field/Common/Types.vo
  0m00.82s |  619304 ko | Bedrock/Group/Point.vo
  0m00.82s |  428464 ko | Curves/Montgomery/AffineInstances.vo
  0m00.82s |  418484 ko | Util/Strings/String_as_OT.vo
  0m00.80s |  560708 ko | Util/FSets/FMapZ.vo
  0m00.79s |  410708 ko | Coqprime/PrimalityTest/Pocklington.vo
  0m00.79s |  413884 ko | Rewriter/Rewriter/Examples/PerfTesting/Sample.vo
  0m00.78s |  434556 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimalNoMul.vo
  0m00.78s |  416052 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/bverify.vo
  0m00.75s |  489812 ko | Rewriter/Rewriter/AllTactics.vo
  0m00.73s |  433592 ko | Arithmetic/BarrettReduction/Wikipedia.vo
  0m00.73s |  590460 ko | Bedrock/Field/Common/Tactics.vo
  0m00.73s |  505840 ko | Language/APINotations.vo
  0m00.73s |  429952 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ArrayCasts.vo
  0m00.72s |  545876 ko | Bedrock/Field/Stringification/FlattenVarData.vo
  0m00.72s |  535532 ko | Bedrock/Field/Translation/Flatten.vo
  0m00.72s |  442796 ko | rupicola/src/Rupicola/Examples/IO/Stdout.vo
  0m00.71s |  422452 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ptsto_bytes.vo
  0m00.71s |  434000 ko | rupicola/src/Rupicola/Examples/Cells/Incr.vo
  0m00.71s |  442724 ko | rupicola/src/Rupicola/Examples/Tree/Tree.vo
  0m00.70s |  451800 ko | Assembly/Equality.vo
  0m00.70s |  526724 ko | Util/FSets/FMapN.vo
  0m00.70s |  416512 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/BigEndian.vo
  0m00.70s |  417860 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/LittleEndian.vo
  0m00.69s |  540192 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo
  0m00.68s |  535428 ko | Bedrock/Field/Translation/Proofs/VarnameSet.vo
  0m00.68s |  438932 ko | Rewriter/Rules.vo
  0m00.68s |  437028 ko | Util/NumTheoryUtil.vo
  0m00.68s |  446204 ko | rupicola/src/Rupicola/Lib/ExprCompiler.vo
  0m00.67s |  506924 ko | AbstractInterpretation/WfExtra.vo
  0m00.67s |  546884 ko | Rewriter/All.vo
  0m00.67s |  422328 ko | Util/ErrorT/List.vo
  0m00.67s |  455056 ko | Util/FSets/FMapFlip.vo
  0m00.67s |  325760 ko | Util/PartiallyReifiedProp.vo
  0m00.66s |  412636 ko | Coqprime/PrimalityTest/Root.vo
  0m00.66s |  382464 ko | Util/Decidable.vo
  0m00.66s |  415468 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/BitOps.vo
  0m00.65s |  503196 ko | MiscCompilerPassesProofsExtra.vo
  0m00.65s |  382116 ko | Rewriter/Util/Decidable.vo
  0m00.64s |  502268 ko | Language/WfExtra.vo
  0m00.64s |  512104 ko | PushButtonSynthesis/ReificationCache.vo
  0m00.63s |  520828 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo
  0m00.63s |   32184 ko | fiat-go/64/curve25519/curve25519.go
  0m00.62s |  511348 ko | Language/API.vo
  0m00.62s |  502280 ko | Rewriter/AllTacticsExtra.vo
  0m00.62s |  459732 ko | Util/FSets/FMapEmpty.vo
  0m00.61s |  420704 ko | Algebra/IntegralDomain.vo
  0m00.61s |  412776 ko | Coqprime/PrimalityTest/Cyclic.vo
  0m00.61s |  410172 ko | Coqprime/PrimalityTest/PGroup.vo
  0m00.60s |  422004 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Array.vo
  0m00.60s |  442884 ko | rupicola/src/Rupicola/Examples/IO/IO.vo
  0m00.59s |  506272 ko | Language/UnderLetsProofsExtra.vo
  0m00.59s |  444160 ko | Util/Structures/OrdersEx.vo
  0m00.58s |  452780 ko | Bedrock/Group/Loops.vo
  0m00.58s |  410960 ko | Coqprime/Z/ZSum.vo
  0m00.58s |  429976 ko | Util/Arg.vo
  0m00.58s |  422924 ko | Util/CPSUtil.vo
  0m00.58s |  409592 ko | Util/OptionList.vo
  0m00.58s |  445376 ko | Util/QUtil.vo
  0m00.58s |  417484 ko | Util/Strings/ParseArithmeticToTaps.vo
  0m00.57s |  419668 ko | Algebra/SubsetoidRing.vo
  0m00.57s |  441260 ko | Util/MSets/MSetN.vo
  0m00.57s |  414972 ko | Util/ZUtil/Modulo/PullPush.vo
  0m00.57s |  420508 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Map/DisjointUnion.vo
  0m00.57s |  443676 ko | rupicola/bedrock2/compiler/src/compiler/RiscvEventLoop.vo
  0m00.55s |  121780 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi
  0m00.55s |  459972 ko | Rewriter/Language/IdentifiersGenerate.vo
  0m00.55s |  472808 ko | Rewriter/Rewriter/ProofsCommonTactics.vo
  0m00.55s |  503488 ko | Util/Strings/ParseFlagOptions.vo
  0m00.55s |  427604 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/Trace.vo
  0m00.55s |  437368 ko | rupicola/src/Rupicola/Lib/NoExprReflection.vo
  0m00.54s |  414808 ko | Util/Structures/Orders/Flip.vo
  0m00.53s |  123852 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi
  0m00.53s |  119860 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi
  0m00.53s |  121504 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi
  0m00.53s |  120132 ko | ExtractionOCaml/word_by_word_montgomery.cmi
  0m00.53s |  439364 ko | Util/ZRange/OperationsBounds.vo
  0m00.53s |  421736 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/OfListWord.vo
  0m00.53s |  442848 ko | rupicola/src/Rupicola/Examples/KVStore/Properties.vo
  0m00.53s |  442324 ko | rupicola/src/Rupicola/Lib/ExprReflection.vo
  0m00.53s |  441816 ko | rupicola/src/Rupicola/Lib/SepLocals.vo
  0m00.52s |  463832 ko | ArithmeticCPS/WordByWordMontgomery.vo
  0m00.52s |  117456 ko | ExtractionOCaml/base_conversion.cmi
  0m00.52s |  120696 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi
  0m00.52s |  121620 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi
  0m00.52s |  118688 ko | ExtractionOCaml/solinas_reduction.cmi
  0m00.52s |  483816 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings.vo
  0m00.52s |  437180 ko | Util/FSets/FMapTrie/Shape.vo
  0m00.52s |   37768 ko | fiat-bedrock2/src/curve25519_64.c
  0m00.51s |  461376 ko | ArithmeticCPS/Freeze.vo
  0m00.51s |  123816 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi
  0m00.51s |  458244 ko | MiscCompilerPasses.vo
  0m00.51s |  433796 ko | Util/ZUtil/CC.vo
  0m00.51s |  434188 ko | Util/ZUtil/Stabilization.vo
  0m00.51s |  426748 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/SMTVerif.vo
  0m00.50s |  450952 ko | Bedrock/Specs/Group.vo
  0m00.50s |  119804 ko | ExtractionOCaml/bedrock2_base_conversion.cmi
  0m00.50s |  121292 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi
  0m00.50s |  121036 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi
  0m00.50s |  119196 ko | ExtractionOCaml/saturated_solinas.cmi
  0m00.50s |  120512 ko | ExtractionOCaml/unsaturated_solinas.cmi
  0m00.50s |  123036 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi
  0m00.50s |  481664 ko | Rewriter/Util/plugins/RewriterBuildRegistry.vo
  0m00.50s |  480192 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports.vo
  0m00.50s |  415196 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/OperatorOverloading.vo
  0m00.50s |  410648 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SortedList.vo
  0m00.49s |  121232 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi
  0m00.49s |  458452 ko | Rewriter/Language/IdentifiersGenerateProofs.vo
  0m00.49s |  427212 ko | Util/Decidable/Decidable2Bool.vo
  0m00.49s |  414848 ko | Util/Structures/Orders/Bool.vo
  0m00.49s |  359872 ko | Util/Wf.vo
  0m00.49s |   32564 ko | fiat-json/src/curve25519_64.json
  0m00.49s |  415904 ko | rupicola/bedrock2/compiler/src/compiler/DivisibleBy4.vo
  0m00.49s |  402296 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/Example64Literal.vo
  0m00.48s |  468584 ko | Assembly/WithBedrock/Semantics.vo
  0m00.48s |  413160 ko | Coqprime/PrimalityTest/Zp.vo
  0m00.48s |  119488 ko | ExtractionOCaml/dettman_multiplication.cmi
  0m00.48s |  494280 ko | Rewriter/Util/plugins/RewriterBuild.vo
  0m00.48s |  411076 ko | Util/ListUtil/SetoidListFlatMap.vo
  0m00.48s |  412388 ko | Util/Loops.vo
  0m00.48s |   27008 ko | fiat-zig/src/curve25519_64.zig
  0m00.48s |  413600 ko | rupicola/bedrock2/compiler/src/compiler/ZLemmas.vo
  0m00.48s |  434564 ko | rupicola/src/Rupicola/Examples/Swap/Properties.vo
  0m00.47s |  442008 ko | Rewriter/Language/IdentifiersBasicGenerate.vo
  0m00.47s |  425064 ko | rupicola/bedrock2/bedrock2/src/bedrock2/FE310CSemantics.vo
  0m00.46s |  449188 ko | ArithmeticCPS/Core.vo
  0m00.46s |  449384 ko | Util/FSets/FMapString.vo
  0m00.46s |  452064 ko | Util/MSets/MSetPositive/Show.vo
  0m00.46s |   27256 ko | fiat-c/src/curve25519_64.c
  0m00.46s |  413232 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/bitblast.vo
  0m00.46s |  430640 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalCSRs.vo
  0m00.45s |  456604 ko | ArithmeticCPS/ModOps.vo
  0m00.45s |  475284 ko | Bedrock/End2End/RupicolaCrypto/Spec.vo
  0m00.45s |   26156 ko | fiat-rust/src/curve25519_64.rs
  0m00.45s |  415424 ko | rupicola/bedrock2/compiler/src/compiler/NaiveRiscvWordProperties.vo
  0m00.45s |  350324 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Monads.vo
  0m00.45s |  442172 ko | rupicola/src/Rupicola/Examples/Utf8/Utils.vo
  0m00.44s |  451428 ko | ArithmeticCPS/Saturated.vo
  0m00.44s |  418984 ko | rupicola/bedrock2/compiler/src/compiler/Registers.vo
  0m00.44s |  392856 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/ident_to_string.vo
  0m00.44s |  405496 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/PushPullMod.vo
  0m00.43s |  461376 ko | ArithmeticCPS/BaseConversion.vo
  0m00.43s |  408168 ko | Coqprime/Z/ZCmisc.vo
  0m00.43s |  434424 ko | Util/Strings/NamingConventions.vo
  0m00.43s |  429284 ko | Util/ZUtil/Log2.vo
  0m00.43s |  436420 ko | Util/ZUtil/SignBit.vo
  0m00.43s |   40432 ko | fiat-bedrock2/src/curve25519_solinas_64.c
  0m00.43s |  419836 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/ZList.vo
  0m00.43s |  405960 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/ZLib.vo
  0m00.43s |  420352 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeProver.vo
  0m00.43s |  442260 ko | rupicola/src/Rupicola/Examples/KVStore/KVStore.vo
  0m00.42s |  430812 ko | Util/MSets/MSetString.vo
  0m00.42s |  429680 ko | Util/ZUtil/Divide.vo
  0m00.42s |  436336 ko | Util/ZUtil/Lxor.vo
  0m00.42s |   37240 ko | fiat-go/64/curve25519solinas/curve25519solinas.go
  0m00.42s |   39236 ko | fiat-json/src/curve25519_solinas_64.json
  0m00.42s |   36340 ko | fiat-zig/src/curve25519_solinas_64.zig
  0m00.42s |  422916 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Memory.vo
  0m00.42s |  411132 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/ListSet.vo
  0m00.42s |  442280 ko | rupicola/src/Rupicola/Examples/Cells/Cells.vo
  0m00.41s |  470096 ko | Arithmetic/FLia.vo
  0m00.41s |  433732 ko | Util/ZUtil/Land.vo
  0m00.41s |   35504 ko | fiat-c/src/curve25519_solinas_64.c
  0m00.41s |  431584 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepCalls.vo
  0m00.41s |  429580 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ARPResponder.vo
  0m00.41s |  430800 ko | rupicola/bedrock2/compiler/src/compiler/FlatImpUniqueSepLog.vo
  0m00.41s |  423376 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRGetSet.vo
  0m00.41s |  438972 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/Spec.vo
  0m00.41s |  438804 ko | rupicola/src/Rupicola/Lib/Alloc.vo
  0m00.41s |  437364 ko | rupicola/src/Rupicola/Lib/SepReflection.vo
  0m00.40s |  428624 ko | Util/Listable.vo
  0m00.40s |  384448 ko | Util/Sum.vo
  0m00.40s |   36040 ko | fiat-rust/src/curve25519_solinas_64.rs
  0m00.40s |  461144 ko | rupicola/bedrock2/compiler/src/compiler/ExprImpEventLoopSpec.vo
  0m00.40s |  425220 ko | rupicola/bedrock2/compiler/src/compiler/UniqueSepLog.vo
  0m00.39s |  395832 ko | Assembly/Parse/Examples/boringssl_nasm_full_mul_p256.vo
  0m00.39s |  441064 ko | Rewriter/Language/Reify.vo
  0m00.39s |  426988 ko | Util/ZBounded.vo
  0m00.39s |  429644 ko | Util/ZUtil/Divide/Bool.vo
  0m00.39s |  400344 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepAutoExports.vo
  0m00.39s |  415396 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ToCString.vo
  0m00.39s |  421432 ko | rupicola/src/Rupicola/Examples/KVStore/kv.vo
  0m00.38s |  412772 ko | Util/ListUtil/GroupAllBy.vo
  0m00.38s |  431556 ko | Util/ZUtil/EquivModulo.vo
  0m00.38s |  422764 ko | rupicola/bedrock2/compiler/src/compiler/StringNameGen.vo
  0m00.38s |  411464 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Naive.vo
  0m00.38s |  417720 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/ZifyLittleEndian.vo
  0m00.38s |  420828 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteI.vo
  0m00.38s |  426000 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/MetricPrimitives.vo
  0m00.38s |  405528 ko | rupicola/src/Rupicola/Examples/CRC32/Table.vo
  0m00.37s |  430116 ko | Arithmetic/ModularArithmeticPre.vo
  0m00.37s |  413572 ko | Language/IdentifierParameters.vo
  0m00.37s |  420780 ko | Util/HList.vo
  0m00.37s |  422648 ko | Util/Level.vo
  0m00.37s |  426960 ko | Util/ZRange.vo
  0m00.37s |  420356 ko | Util/ZUtil/Ltz.vo
  0m00.37s |  426472 ko | Util/ZUtil/Pow.vo
  0m00.37s |  427680 ko | rupicola/bedrock2/bedrock2/src/bedrock2/OperatorOverloading.vo
  0m00.37s |  431904 ko | rupicola/bedrock2/bedrock2/src/bedrock2/RecordPredicates.vo
  0m00.37s |  427624 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/chacha20.vo
  0m00.37s |  438128 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvDef.vo
  0m00.37s |  443552 ko | rupicola/bedrock2/compiler/src/compiler/ForeverSafe.vo
  0m00.37s |  430788 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO_Post.vo
  0m00.37s |  424720 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Primitives.vo
  0m00.37s |  443060 ko | rupicola/src/Rupicola/Examples/IO/Writer.vo
  0m00.36s |  385140 ko | Coqprime/List/UList.vo
  0m00.36s |  419844 ko | Util/Structures/Equalities/List.vo
  0m00.36s |  427828 ko | rupicola/bedrock2/bedrock2/src/bedrock2/TransferSepsOrder.vo
  0m00.36s |  419892 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/OfFunc.vo
  0m00.36s |  417232 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/prove_Zeq_bitwise.vo
  0m00.36s |  426352 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Sane.vo
  0m00.36s |  443080 ko | rupicola/src/Rupicola/Examples/Nondeterminism/NonDeterminism.vo
  0m00.35s |  385364 ko | Coqprime/List/Permutation.vo
  0m00.35s |  384172 ko | Rewriter/Util/Sum.vo
  0m00.35s |  429404 ko | Util/Strings/Show.vo
  0m00.35s |  412512 ko | Util/Strings/String.vo
  0m00.35s |  421004 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/Result.vo
  0m00.35s |  439560 ko | rupicola/src/Rupicola/Lib/Conditionals.vo
  0m00.34s |  408188 ko | Coqprime/PrimalityTest/IGroup.vo
  0m00.34s |  393816 ko | Language/PreExtra.vo
  0m00.34s |  402648 ko | Rewriter/TestRules.vo
  0m00.34s |  412756 ko | Rewriter/Util/Strings/ParseArithmetic.vo
  0m00.34s |  393864 ko | Util/Strings/String_as_OT_old.vo
  0m00.34s |  410768 ko | Util/ZUtil/CPS.vo
  0m00.34s |  415816 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/Demos.vo
  0m00.34s |  401728 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalCSRsDet.vo
  0m00.33s |  375960 ko | Util/ZUtil.vo
  0m00.33s |  400708 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepLib.vo
  0m00.33s |  414856 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Decode.vo
  0m00.33s |  375792 ko | rupicola/src/Rupicola/Examples/KVStore/Tactics.vo
  0m00.33s |  398752 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/SpecExtraction.vo
  0m00.32s |  409072 ko | Coqprime/PrimalityTest/Euler.vo
  0m00.32s |  424228 ko | Curves/Weierstrass/Affine.vo
  0m00.32s |  354496 ko | Util/ZUtil/Lor.vo
  0m00.32s |  353664 ko | rupicola/bedrock2/bedrock2/src/bedrock2/BasicC64Semantics.vo
  0m00.32s |  372204 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepAuto.vo
  0m00.32s |  376436 ko | rupicola/bedrock2/compiler/src/compiler/FlattenExprDef.vo
  0m00.32s |  375132 ko | rupicola/bedrock2/compiler/src/compiler/MemoryLayout.vo
  0m00.32s |  420972 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Memory.vo
  0m00.32s |  369524 ko | rupicola/src/Rupicola/Lib/Api.vo
  0m00.32s |  419200 ko | rupicola/src/Rupicola/Lib/Monads.vo
  0m00.31s |  408224 ko | Coqprime/PrimalityTest/Lagrange.vo
  0m00.31s |  375364 ko | Rewriter/Util/MSetPositive/Facts.vo
  0m00.31s |  421500 ko | Spec/CompleteEdwardsCurve.vo
  0m00.31s |  377312 ko | Util/MSets/MSetPositive/Facts.vo
  0m00.31s |  377252 ko | Util/Strings/Sorting.vo
  0m00.31s |  351748 ko | Util/ZUtil/Land/Fold.vo
  0m00.31s |  355732 ko | Util/ZUtil/Tactics/SolveRange.vo
  0m00.30s |  384652 ko | Algebra/Monoid.vo
  0m00.30s |  383176 ko | Coqprime/List/ListAux.vo
  0m00.30s |  342728 ko | Util/Strings/Show/Enum.vo
  0m00.30s |  391212 ko | Util/Structures/Orders/Unit.vo
  0m00.30s |  319900 ko | Util/ZUtil/Tactics.vo
  0m00.30s |  350824 ko | Util/ZUtil/Tactics/SolveTestbit.vo
  0m00.30s |  353168 ko | rupicola/bedrock2/bedrock2/src/bedrock2/safe_f_equal.vo
  0m00.30s |  368372 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimal.vo
  0m00.30s |  357516 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalLogging.vo
  0m00.30s |  379772 ko | rupicola/src/Rupicola/Lib/Notations.vo
  0m00.30s |  364432 ko | rupicola/src/Rupicola/Lib/Tactics.vo
  0m00.30s |  357996 ko | rupicola/src/Rupicola/Lib/WordNotations.vo
  0m00.29s |  364272 ko | Rewriter/TestRulesProofs.vo
  0m00.29s |  333924 ko | Spec/ModularArithmetic.vo
  0m00.29s |   25660 ko | fiat-go/32/poly1305/poly1305.go
  0m00.29s |  352048 ko | rupicola/bedrock2/bedrock2/src/bedrock2/BasicC32Semantics.vo
  0m00.29s |  345272 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ProgramLogic.vo
  0m00.29s |  341028 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepCallsExports.vo
  0m00.29s |  349008 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/FE310ExtSpec.vo
  0m00.29s |  354512 ko | rupicola/src/Rupicola/Examples/CapitalizeThird/CapitalizeThird.vo
  0m00.29s |  338736 ko | rupicola/src/Rupicola/Examples/Swap/Swap.vo
  0m00.29s |  381560 ko | rupicola/src/Rupicola/Lib/Invariants.vo
  0m00.29s |  411108 ko | rupicola/src/Rupicola/Lib/ToCString.vo
  0m00.28s |  392356 ko | Rewriter/Language/UnderLets.vo
  0m00.28s |  382364 ko | Util/Structures/Equalities/Sum.vo
  0m00.28s |  378252 ko | Util/Structures/Orders/Empty.vo
  0m00.28s |  360100 ko | Util/Structures/Orders/Iso.vo
  0m00.28s |  342356 ko | Util/ZUtil/Tactics/Ztestbit.vo
  0m00.28s |  310160 ko | rupicola/bedrock2/bedrock2/src/bedrock2/PurifyHeapletwise.vo
  0m00.28s |  334436 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepLogAddrArith.vo
  0m00.28s |  342680 ko | rupicola/bedrock2/compiler/src/compiler/UseImmediateDef.vo
  0m00.28s |  354192 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/AtomicMinimal.vo
  0m00.27s |  385140 ko | Coqprime/List/Iterator.vo
  0m00.27s |  367396 ko | Curves/Montgomery/XZ.vo
  0m00.27s |  337868 ko | Rewriter/Util/MSetPositive/Equality.vo
  0m00.27s |  347388 ko | Util/ListUtil/SetoidList.vo
  0m00.27s |  369612 ko | Util/ZUtil/Combine.vo
  0m00.27s |  379216 ko | Util/ZUtil/Le.vo
  0m00.27s |  349972 ko | rupicola/bedrock2/bedrock2/src/bedrock2/WeakestPrecondition.vo
  0m00.27s |  377088 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteA64.vo
  0m00.27s |  379772 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Encode.vo
  0m00.26s |  368384 ko | Rewriter/Util/Strings/String.vo
  0m00.26s |  376924 ko | Util/ZUtil/Peano.vo
  0m00.26s |  360084 ko | Util/ZUtil/Tactics/LtbToLt.vo
  0m00.26s |  340944 ko | Util/ZUtil/Tactics/RewriteModSmall.vo
  0m00.26s |   32592 ko | fiat-bedrock2/src/poly1305_32.c
  0m00.26s |  346712 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb_spec.vo
  0m00.26s |  339000 ko | rupicola/bedrock2/compiler/src/compiler/FlatImpConstraints.vo
  0m00.26s |  377484 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteA.vo
  0m00.26s |  385172 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/StringRecords.vo
  0m00.25s |  334716 ko | Util/ListUtil/Filter.vo
  0m00.25s |  338148 ko | Util/MSets/MSetPositive/Equality.vo
  0m00.25s |  362452 ko | Util/ZRange/Operations.vo
  0m00.25s |  325960 ko | Util/ZUtil/Tactics/LinearSubstitute.vo
  0m00.25s |   29108 ko | fiat-json/src/poly1305_32.json
  0m00.25s |  288032 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ToCStringExprTypecheckingTest.vo
  0m00.25s |  292340 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ToCStringStackallocLoopTest.vo
  0m00.25s |  389460 ko | rupicola/bedrock2/bedrock2/src/bedrock2/footpr.vo
  0m00.25s |  337192 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/RiscvMachine.vo
  0m00.25s |  374904 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteCSR.vo
  0m00.25s |  325428 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Machine.vo
  0m00.24s |  311644 ko | Algebra/Nsatz.vo
  0m00.24s |  326236 ko | Arithmetic/MontgomeryReduction/Definition.vo
  0m00.24s |  360664 ko | Util/AdditionChainExponentiation.vo
  0m00.24s |  322652 ko | Util/MSets/Show.vo
  0m00.24s |  340708 ko | Util/NUtil/WithoutReferenceToZ.vo
  0m00.24s |  318760 ko | Util/ZRange/Show.vo
  0m00.24s |  328440 ko | Util/ZUtil/Odd.vo
  0m00.24s |  308944 ko | Util/ZUtil/Opp.vo
  0m00.24s |  316532 ko | Util/ZUtil/Tactics/RewriteModDivide.vo
  0m00.24s |  321008 ko | rupicola/bedrock2/compiler/src/compiler/ZNameGen.vo
  0m00.24s |  353544 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/SimplWordExpr.vo
  0m00.24s |  341560 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/LogInstructionTrace.vo
  0m00.23s |  300228 ko | Bedrock/Field/Common/Names/VarnameGenerator.vo
  0m00.23s |  377268 ko | Coqprime/List/ZProgression.vo
  0m00.23s |  313720 ko | Rewriter/Util/Option.vo
  0m00.23s |  320764 ko | Util/ErrorT/Show.vo
  0m00.23s |  333864 ko | Util/ListUtil/Permutation.vo
  0m00.23s |  323108 ko | Util/NUtil/Testbit.vo
  0m00.23s |  286696 ko | Util/Strings/StringMap.vo
  0m00.23s |  348464 ko | Util/Structures/Equalities/Prod.vo
  0m00.23s |   25268 ko | fiat-java/src/FiatPoly1305.java
  0m00.23s |  300056 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ZnWords.vo
  0m00.23s |  314040 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/RecordSetters.vo
  0m00.22s |  333880 ko | Coqprime/PrimalityTest/FGroup.vo
  0m00.22s |  310312 ko | Rewriter/Language/PreLemmas.vo
  0m00.22s |  324896 ko | Rewriter/Language/UnderLetsCacheProofs.vo
  0m00.22s |  345352 ko | Rewriter/Util/ListUtil/SetoidList.vo
  0m00.22s |  313848 ko | Util/Option.vo
  0m00.22s |  291212 ko | Util/SideConditions/ModInvPackage.vo
  0m00.22s |  287668 ko | Util/ZUtil/Definitions.vo
  0m00.22s |  279424 ko | Util/ZUtil/Sgn.vo
  0m00.22s |  321444 ko | Util/ZUtil/Tactics/SimplifyFractionsLe.vo
  0m00.22s |  259676 ko | Util/ZUtil/Tactics/SplitMinMax.vo
  0m00.22s |  318104 ko | Util/ZUtil/Tactics/ZeroBounds.vo
  0m00.22s |   23992 ko | fiat-c/src/poly1305_32.c
  0m00.22s |   24364 ko | fiat-rust/src/poly1305_32.rs
  0m00.22s |   24480 ko | fiat-zig/src/poly1305_32.zig
  0m00.22s |  312072 ko | rupicola/bedrock2/bedrock2/src/bedrock2/PurifySep.vo
  0m00.22s |  299808 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepClause.vo
  0m00.22s |  329056 ko | rupicola/bedrock2/compiler/src/compiler/mod4_0.vo
  0m00.22s |  308236 ko | rupicola/bedrock2/compiler/src/compiler/regs_initialized.vo
  0m00.22s |  298992 ko | rupicola/bedrock2/compiler/src/compiler/util/Common.vo
  0m00.22s |  315128 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Byte.vo
  0m00.22s |  336016 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MaterializeRiscvProgram.vo
  0m00.22s |  289828 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricRiscvMachine.vo
  0m00.22s |  299720 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncode.vo
  0m00.22s |  314352 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteI64.vo
  0m00.22s |  300972 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteM64.vo
  0m00.21s |  315792 ko | Util/IdfunWithAlt.vo
  0m00.21s |  262576 ko | Util/NUtil/Sorting.vo
  0m00.21s |  292716 ko | Util/Strings/Parse/Common.vo
  0m00.21s |  265724 ko | Util/ZUtil/Hints/PullPush.vo
  0m00.21s |  310364 ko | Util/ZUtil/Z2Nat.vo
  0m00.21s |  305796 ko | Util/ZUtil/ZSimplify/Simple.vo
  0m00.21s |  273568 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ListIndexNotations.vo
  0m00.21s |  277260 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepBulletPoints.vo
  0m00.21s |  283964 ko | rupicola/bedrock2/bedrock2/src/bedrock2/cancel_div.vo
  0m00.21s |  313100 ko | rupicola/bedrock2/compiler/src/compiler/RiscvWordProperties.vo
  0m00.21s |  359956 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/MapKeys.vo
  0m00.21s |  274236 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Solver.vo
  0m00.21s |  328060 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/DebugWordEq.vo
  0m00.21s |  310856 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/SoftmulInsts.vo
  0m00.21s |  301280 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Run.vo
  0m00.21s |  278812 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRSpec.vo
  0m00.21s |  276044 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Execute.vo
  0m00.21s |  307864 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteM.vo
  0m00.21s |  294416 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/D…
  • Loading branch information
@JasonGross
JasonGross committed Apr 26, 2023
1 parent 0494e45 commit 9584e6c
Show file tree
Hide file tree
Showing 14 changed files with 72,886 additions and 17 deletions.
19 changes: 12 additions & 7 deletions Makefile.examples
View file
Original file line number Diff line number Diff line change
Expand Up @@ -99,14 +99,19 @@ WORD_BY_WORD_MONTGOMERY_BASE_FILES := # p434_32
ALL_BASE_FILES := $(UNSATURATED_SOLINAS_BASE_FILES) $(WORD_BY_WORD_MONTGOMERY_BASE_FILES)

BASE_FILES_NEEDING_INT128 := p448_solinas_32
BASE_FILES_WITH_CODESIZE_GT_65535 := p434_32

INVALID_JAVA_BASE_FILES := $(BASE_FILES_WITH_CODESIZE_GT_65535) $(BASE_FILES_NEEDING_INT128)
INVALID_BEDROCK2_BASE_FILES := $(BASE_FILES_NEEDING_INT128)
INVALID_GO_BASE_FILES := $(BASE_FILES_NEEDING_INT128)

GO_EXTRA_UNSATURATED_SOLINAS_FUNCTIONS := carry_add carry_sub carry_opp
GO_EXTRA_WORD_BY_WORD_MONTGOMERY_FUNCTIONS :=

$(foreach bw,64 32,$(eval $(call add_curve_keys,curve25519_$(bw),UNSATURATED_SOLINAS,'25519',$(bw),'(auto)' '2^255 - 19',$(FUNCTIONS_FOR_25519),UNSATURATED_SOLINAS)))
$(eval $(call add_curve_keys,poly1305_64,UNSATURATED_SOLINAS,'poly1305',64,'3' '2^130 - 5',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
$(eval $(call add_curve_keys,poly1305_32,UNSATURATED_SOLINAS,'poly1305',32,'(auto)' '2^130 - 5',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
$(eval $(call add_curve_keys,p521_64,UNSATURATED_SOLINAS,'p521',64,'9' '2^521 - 1',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
$(foreach bw,64 32,$(eval $(call add_curve_keys,p521_$(bw),UNSATURATED_SOLINAS,'p521',$(bw),'(auto)' '2^521 - 1',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS)))
## 2^224 - 2^96 + 1 ## does not bounds check
#$(eval $(call add_curve_keys,p224_solinas_64,UNSATURATED_SOLINAS,'p224',64,'4' '2^224 - 2^96 + 1',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
$(eval $(call add_curve_keys,p448_solinas_64,UNSATURATED_SOLINAS,'p448',64,'8' '2^448 - 2^224 - 1',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
Expand All @@ -133,20 +138,20 @@ LITE_BASE_FILES := curve25519_64 poly1305_64 poly1305_32 p256_64 secp256k1_dettm
EXTRA_C_FILES := inversion/c/*_test.c

ALL_C_FILES := $(patsubst %,$(C_DIR)%.c,$(ALL_BASE_FILES))
ALL_BEDROCK2_FILES := $(patsubst %,$(BEDROCK2_DIR)%.c,$(filter-out $(BASE_FILES_NEEDING_INT128),$(ALL_BASE_FILES)))
ALL_BEDROCK2_FILES := $(patsubst %,$(BEDROCK2_DIR)%.c,$(filter-out $(INVALID_BEDROCK2_BASE_FILES),$(ALL_BASE_FILES)))
ALL_RUST_FILES := $(patsubst %,$(RUST_DIR)%.rs,$(ALL_BASE_FILES))
ALL_RUST_MODS := $(ALL_BASE_FILES)
ALL_GO_FILES := $(patsubst %,$(GO_DIR)%.go,$(call GO_RENAME_TO_FILE,$(filter-out $(BASE_FILES_NEEDING_INT128),$(ALL_BASE_FILES))))
ALL_GO_FILES := $(patsubst %,$(GO_DIR)%.go,$(call GO_RENAME_TO_FILE,$(filter-out $(INVALID_GO_BASE_FILES),$(ALL_BASE_FILES))))
ALL_JSON_FILES := $(patsubst %,$(JSON_DIR)%.json,$(ALL_BASE_FILES))
ALL_JAVA_FILES := $(patsubst %,$(JAVA_DIR)%.java,$(call JAVA_RENAME,$(filter-out $(BASE_FILES_NEEDING_INT128),$(ALL_BASE_FILES))))
ALL_JAVA_FILES := $(patsubst %,$(JAVA_DIR)%.java,$(call JAVA_RENAME,$(filter-out $(INVALID_JAVA_BASE_FILES),$(ALL_BASE_FILES))))
ALL_ZIG_FILES := $(patsubst %,$(ZIG_DIR)%.zig,$(ALL_BASE_FILES))

LITE_C_FILES := $(patsubst %,$(C_DIR)%.c,$(LITE_BASE_FILES))
LITE_BEDROCK2_FILES := $(patsubst %,$(BEDROCK2_DIR)%.c,$(filter-out $(BASE_FILES_NEEDING_INT128),$(LITE_BASE_FILES)))
LITE_BEDROCK2_FILES := $(patsubst %,$(BEDROCK2_DIR)%.c,$(filter-out $(INVALID_BEDROCK2_BASE_FILES),$(LITE_BASE_FILES)))
LITE_RUST_FILES := $(patsubst %,$(RUST_DIR)%.rs,$(LITE_BASE_FILES))
LITE_GO_FILES := $(patsubst %,$(GO_DIR)%.go,$(call GO_RENAME_TO_FILE,$(filter-out $(BASE_FILES_NEEDING_INT128),$(LITE_BASE_FILES))))
LITE_GO_FILES := $(patsubst %,$(GO_DIR)%.go,$(call GO_RENAME_TO_FILE,$(filter-out $(INVALID_GO_BASE_FILES),$(LITE_BASE_FILES))))
LITE_JSON_FILES := $(patsubst %,$(JSON_DIR)%.json,$(LITE_BASE_FILES))
LITE_JAVA_FILES := $(patsubst %,$(JAVA_DIR)%.java,$(call JAVA_RENAME,$(filter-out $(BASE_FILES_NEEDING_INT128),$(LITE_BASE_FILES))))
LITE_JAVA_FILES := $(patsubst %,$(JAVA_DIR)%.java,$(call JAVA_RENAME,$(filter-out $(INVALID_JAVA_BASE_FILES),$(LITE_BASE_FILES))))
LITE_ZIG_FILES := $(patsubst %,$(ZIG_DIR)%.zig,$(LITE_BASE_FILES))

BEDROCK2_UNSATURATED_SOLINAS := src/ExtractionOCaml/bedrock2_unsaturated_solinas
Expand Down
5,341 changes: 5,341 additions & 0 deletions fiat-bedrock2/src/p521_32.c
View file

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions fiat-bedrock2/src/p521_64.c
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

0 comments on commit 9584e6c

Please sign in to comment.