search

mit-plv / fiat-crypto

Cryptographic Primitive Code Generation by Fiat
http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf
Other
705 stars 147 forks source link

Coq CI Targets? #1549

Open JasonGross opened 1 year ago

JasonGross commented 1 year ago

We've been timing out a bunch on Coq's CI recently, and I imagine #368 makes things a bit worse (though not much worse). Perhaps we should offer some target that does not build everything for Coq's CI to use? Thoughts? (@andres-erbsen ?)

andres-erbsen commented 1 year ago

I've suggested dropping Java targets before. I am adamant that we should keep GarageDoor. We might consider dropping Curves, or splitting it out to a separate Coq CI job.

Overall, this question would be much easier to answer if I was able to query "how much time does the following make invocation take" without rebuilding.

JasonGross commented 1 year ago

The CI job that is timing out is the one that builds only .v files. There is a separate one for making sure the extracted OCaml code compiles which builds standalone-ocaml lite-generated-files.

Overall, this question would be much easier to answer if I was able to query "how much time does the following make invocation take" without rebuilding.

You can get the timing data from the bottom of all-except-generated on any successful CI run, for example starting on this line. If you do something like git ls-files "*.v" | xargs touch and then do make --dry-run $target, combined with grep COQC or similar, you should be able to get a list of the .v files built. You can then grep the timing table for those particular targets and add them up.

Here is the timing table from the most recent successful Coq CI run of fiat-crypto. Note that we're just 3 minutes under the 3h timeout there.

The slowest files on Coq's CI ``` Time | Peak Mem | File Name -------------------------------------------------------------------------------------------------------------------------------------------------------------- 167m29.98s | 3393184 ko | Total Time / Peak Mem -------------------------------------------------------------------------------------------------------------------------------------------------------------- 6m26.79s | 3393184 ko | Curves/Weierstrass/AffineProofs.vo 6m14.23s | 981276 ko | _build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.vo 6m02.51s | 2402188 ko | Bedrock/End2End/X25519/GarageDoor.vo 5m34.73s | 961948 ko | _build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.vo 5m01.87s | 2886512 ko | _build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.vo 4m56.16s | 2915396 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo 4m14.55s | 1629668 ko | Curves/EdwardsMontgomery.vo 4m00.82s | 2540352 ko | Assembly/WithBedrock/Proofs.vo 3m52.28s | 1878216 ko | Rewriter/Passes/ArithWithCasts.vo 3m13.24s | 1853152 ko | Curves/Weierstrass/Projective.vo 2m52.25s | 821152 ko | _build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.vo 2m49.06s | 2792344 ko | _build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.vo 2m34.28s | 699764 ko | Arithmetic/BarrettReduction.vo 2m32.10s | 1102856 ko | Fancy/Compiler.vo 2m19.49s | 1247416 ko | Curves/Montgomery/XZProofs.vo 2m15.41s | 759636 ko | _build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler/MMIO.vo 2m10.68s | 490384 ko | Spec/Test/X25519.vo 2m05.13s | 1534680 ko | Rewriter/Passes/ToFancyWithCasts.vo 2m04.93s | 1607240 ko | Rewriter/Passes/NBE.vo 2m02.42s | 1510452 ko | Curves/Montgomery/AffineProofs.vo 1m59.72s | 1004232 ko | PushButtonSynthesis/SolinasReductionReificationCache.vo 1m54.94s | 644516 ko | _build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.vo 1m53.23s | 1074536 ko | UnsaturatedSolinasHeuristics/Tests.vo 1m47.82s | 2459620 ko | Fancy/Barrett256.vo 1m45.25s | 829096 ko | Arithmetic/SolinasReduction.vo 1m38.76s | 3030920 ko | Bedrock/End2End/RupicolaCrypto/Derive.vo 1m31.22s | 1594476 ko | Bedrock/End2End/X25519/Field25519.vo 1m24.42s | 1045772 ko | _build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.vo 1m19.96s | 992776 ko | Util/FSets/FMapTrie.vo 1m19.96s | 1443932 ko | _build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.vo 1m19.74s | 1527192 ko | Assembly/EquivalenceProofs.vo 1m17.84s | 907644 ko | _build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.vo 1m14.52s | 618136 ko | Demo.vo 1m13.82s | 718040 ko | _build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/EncodeDecode.vo 1m09.95s | 842808 ko | _build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/LAN9250.vo 1m08.21s | 1459992 ko | Assembly/WithBedrock/SymbolicProofs.vo 1m06.52s | 1076300 ko | Curves/Weierstrass/Jacobian.vo 1m05.43s | 870624 ko | AbstractInterpretation/Wf.vo 1m03.74s | 2088392 ko | SlowPrimeSynthesisExamples.vo 1m03.23s | 802704 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo 1m00.43s | 1072304 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo 0m59.29s | 1065240 ko | Rewriter/Passes/MultiRetSplit.vo 0m51.49s | 1083292 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo 0m49.82s | 746100 ko | Rewriter/RulesProofs.vo 0m48.36s | 2169948 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml 0m47.36s | 686984 ko | _build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvLiterals.vo 0m47.00s | 2128916 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml 0m46.54s | 852012 ko | AbstractInterpretation/ZRangeProofs.vo 0m45.33s | 2056768 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml 0m44.20s | 2056912 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml 0m42.48s | 653624 ko | _build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler/Spilling.vo 0m41.92s | 1949896 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml 0m39.62s | 598068 ko | _build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/EncodeBound.vo 0m38.88s | 1154940 ko | Rewriter/Passes/Arith.vo 0m38.49s | 688848 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo 0m38.38s | 677172 ko | _build_ci/fiat_crypto/rupicola/src/Rupicola/Examples/Utf8/Utf8.vo 0m37.14s | 1953688 ko | ExtractionOCaml/unsaturated_solinas.ml 0m36.38s | 745688 ko | AbstractInterpretation/Proofs.vo 0m36.01s | 2128684 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml 0m35.87s | 1527204 ko | Assembly/Symbolic.vo 0m34.99s | 841792 ko | Rewriter/Passes/MulSplit.vo 0m34.71s | 2067252 ko | ExtractionOCaml/word_by_word_montgomery.ml 0m34.10s | 1950688 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml 0m32.77s | 1975140 ko | ExtractionOCaml/bedrock2_base_conversion.ml 0m31.61s | 1259688 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo 0m31.46s | 1852964 ko | Fancy/Montgomery256.vo 0m31.22s | 2045268 ko | ExtractionOCaml/solinas_reduction.ml 0m30.83s | 685688 ko | _build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler/FlatImp.vo 0m30.77s | 1793972 ko | ExtractionOCaml/perf_unsaturated_solinas.ml 0m30.27s | 1881796 ko | ExtractionOCaml/saturated_solinas.ml ```

or splitting it out to a separate Coq CI job.

I don't think the Coq devs will be happy with this solution. The 3h timeout is set by the devs, and see, e.g., https://github.com/coq/coq/pull/16968#issuecomment-1344308607

andres-erbsen commented 1 year ago
JasonGross commented 1 year ago
  • can ExtractionOCaml not be a part of this target?

I would like to keep this, because not many developments test Extraction. (And plausibly we should ask the Coq devs to speed up extraction?). We might be able to build the extraction files in parallel though.

  • is to keep one use of par:abstract

Pierre Marie recently had to disable par altogether on the Fiat Crypto CI because it was too memory hungry. So we're only testing par in serial mode, and maybe it's better to just move a dumb test into Coq's test-suite if there isn't already one

The other points sound good, can we make some relevant targets?

andres-erbsen commented 1 year ago

I think we should stop pretending these targets make any sense and just have a coq-ci target (and ideally get rid of all other halfway targets with the possible exception of curves).

andres-erbsen commented 1 year ago

Build time visualization: https://andres.systems/tmp/time.html

Script:

```python import sys def parsetime(s): try: return float(s) except: pass m, s = s.split('m') if s.endswith('s'): s = s[:-1] return float(m)*60+float(s) def parsemem(s): assert s.endswith(' ko') return 1024 * float(s[:-3]) names = [] values = [] parents = [] started = False for line in sys.stdin: try: time, mem, path = [s.strip() for s in line.split(' | ')] if path.strip() in ['File Name', 'Total Time / Peak Mem']: continue time = parsetime(time.strip()) mem = parsemem(mem.strip()) print (time, mem, path) except: continue names.append(path) values.append(time) parents.append(path.rsplit('/', 1)[0] if '/' in path else '') while parents[-1] not in names: path = parents[-1] names.append(path) values.append(0) parents.append(path.rsplit('/', 1)[0] if '/' in path else '') print (list(zip(names, parents))) import plotly.graph_objects as go fig = go.Figure(go.Treemap(ids=names, labels=names, parents=parents, values=values, branchvalues="remainder", textinfo="label+value+percent parent+percent entry+percent root")) fig.update_layout(margin = dict(t=50, l=25, r=25, b=25)) fig.show() ```

I think for the testing of Coq, it is a good idea to include a small slice of each major category.

andres-erbsen commented 1 year ago

Do you think Fancy code is valuable enough as a fiat-crypto test even to justify maintaining and building it just for that purpose?