https://github.com/mit-plv/fiat-crypto
Revision 42eeb35b3c50e777ed131b24a40737016362bed2 authored by Jason Gross on 09 October 2021, 02:08:26 UTC, committed by Jason Gross on 09 October 2021, 18:06:40 UTC
1 parent 44771e0
Tip revision: 42eeb35b3c50e777ed131b24a40737016362bed2 authored by Jason Gross on 09 October 2021, 02:08:26 UTC
Prove gensym part of asm equivalence checker
Prove gensym part of asm equivalence checker
Tip revision: 42eeb35
| File | Mode | Size |
|---|---|---|
| AbstractInterpretation | ||
| Algebra | ||
| Arithmetic | ||
| ArithmeticCPS | ||
| Assembly | ||
| Bedrock | ||
| Curves | ||
| ExtractionHaskell | ||
| ExtractionOCaml | ||
| Fancy | ||
| Language | ||
| Primitives | ||
| PushButtonSynthesis | ||
| Rewriter | ||
| Spec | ||
| Stringification | ||
| UnsaturatedSolinasHeuristics | ||
| Util | ||
| BoundsPipeline.v | -rw-r--r-- | 64.8 KB |
| CLI.v | -rw-r--r-- | 57.7 KB |
| COperationSpecifications.v | -rw-r--r-- | 28.7 KB |
| CastLemmas.v | -rw-r--r-- | 8.9 KB |
| CompilersTestCases.v | -rw-r--r-- | 16.3 KB |
| Demo.v | -rw-r--r-- | 9.7 KB |
| MiscCompilerPasses.v | -rw-r--r-- | 6.8 KB |
| MiscCompilerPassesProofs.v | -rw-r--r-- | 9.0 KB |
| MiscCompilerPassesProofsExtra.v | -rw-r--r-- | 1.7 KB |
| SlowPrimeSynthesisExamples.v | -rw-r--r-- | 249.8 KB |
| StandaloneDebuggingExamples.v | -rw-r--r-- | 8.4 KB |
| StandaloneHaskellMain.v | -rw-r--r-- | 4.6 KB |
| StandaloneOCamlMain.v | -rw-r--r-- | 8.1 KB |
| TAPSort.v | -rw-r--r-- | 512 bytes |
| UnsaturatedSolinasHeuristics.v | -rw-r--r-- | 17.6 KB |
| haskell.sed | -rw-r--r-- | 536 bytes |
Computing file changes ...
