From c9f0fbd61caafe95f9790da50aa1bb15bdecb1ff Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 15 Nov 2017 18:27:27 -0500 Subject: Update README.md Formatting --- README.md | 33 ++++++++++++++++++++++++++++----- 1 file changed, 28 insertions(+), 5 deletions(-) (limited to 'README.md') diff --git a/README.md b/README.md index ffa36b872..f302612ff 100644 --- a/README.md +++ b/README.md @@ -61,11 +61,22 @@ This will build all the necessary `.vo` and `.c` files, as well as the `fibe` bi ### Curve Correctness Theorems Specifications live in [`src/Spec`](./src/Spec), e.g., [`src/Spec/Ed25519.v`](./src/Spec/Ed25519.v). -Some selected cuve-level proofs live in [`src/Curves/Edwards/AffineProofs.v`](./src/Curves/Edwards/AffineProofs.v), [`src/Curves/Edwards/XYZT/Basic.v`](./src/Curves/Edwards/XYZT/Basic.v), [`src/Curves/Montgomery/AffineProofs.v`](./src/Curves/Montgomery/AffineProofs.v) [`src/Curves/Montgomery/XZProofs.v`](src/Curves/Montgomery/XZProofs.v). +Some selected cuve-level proofs live in +- [`src/Curves/Edwards/AffineProofs.v`](./src/Curves/Edwards/AffineProofs.v), +- [`src/Curves/Edwards/XYZT/Basic.v`](./src/Curves/Edwards/XYZT/Basic.v), +- [`src/Curves/Montgomery/AffineProofs.v`](./src/Curves/Montgomery/AffineProofs.v), +- [`src/Curves/Montgomery/XZProofs.v`](src/Curves/Montgomery/XZProofs.v). ### Arithmetic Core -Generic mathematical optimization strategies live in [`src/Arithmetic`](./src/Arithmetic). Good examples include [`src/Arithmetic/Core.v`](src/Arithmetic/Core.v), [`src/Arithmetic/Karatsuba.v`](src/Arithmetic/Karatsuba.v), [`src/Arithmetic/Saturated/Core.v`](./src/Arithmetic/Saturated/Core.v), [`src/Arithmetic/BarrettReduction/HAC.v`](./src/Arithmetic/BarrettReduction/HAC.v), [`src/Arithmetic/MontgomeryReduction/Definition.v`](./src/Arithmetic/MontgomeryReduction/Definition.v), [`src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition.v`](./src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition.v). +Generic mathematical optimization strategies live in [`src/Arithmetic`](./src/Arithmetic). +Good examples include +- [`src/Arithmetic/Core.v`](src/Arithmetic/Core.v), +- [`src/Arithmetic/Karatsuba.v`](src/Arithmetic/Karatsuba.v), +- [`src/Arithmetic/Saturated/Core.v`](./src/Arithmetic/Saturated/Core.v), +- [`src/Arithmetic/BarrettReduction/HAC.v`](./src/Arithmetic/BarrettReduction/HAC.v), +- [`src/Arithmetic/MontgomeryReduction/Definition.v`](./src/Arithmetic/MontgomeryReduction/Definition.v), +- [`src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition.v`](./src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition.v). ### Demo of Synthesis @@ -73,9 +84,21 @@ The idea of the synthesis process is demoed in [`src/Demo.v`](./src/Demo.v). ### Actual Synthesis -The curve-non-specific synthesis framework lives in [`src/Compilers/Z/Bounds/Pipeline`](./src/Compilers/Z/Bounds/Pipeline). The API for the reflective simplification and bounds analysis pipeline is in [`src/Compilers/Z/Bounds/Pipeline.v`](./src/Compilers/Z/Bounds/Pipeline.v). The definition of the pipeline and the correctness proof are in [`src/Compilers/Z/Bounds/Pipeline/Definition.v`](./src/Compilers/Z/Bounds/Pipeline/Definition.v). Generic reflective syntax trees are defined in [`src/Compilers/Syntax.v`](./src/Compilers/Syntax.v); the specialization to the arithmetic operations on Z that we use occurs in [`src/Compilers/Z/Syntax.v`](./src/Compilers/Z/Syntax.v). The trusted pretty-printer lives in [`src/Compilers/Z/CNotations.v`](./src/Compilers/Z/CNotations.v) and [`src/Compilers/Z/HexNotationConstants.v`](./src/Compilers/Z/HexNotationConstants.v), which were generated by the couple-hundred-line Python scripts in a comment near the top of each file. The core of the bounds-analysis transformation lives in [`src/Compilers/Z/Bounds/Interpretation.v`](./src/Compilers/Z/Bounds/Interpretation.v); the corresponding proofs live in [`src/Compilers/Z/Bounds/InterpretationLemmas`](./src/Compilers/Z/Bounds/InterpretationLemmas), and the instantation of the bounds-analysis transformation with the core lives in [`src/Compilers/Z/Bounds/MapCastByDeBruijn.v`](./src/Compilers/Z/Bounds/MapCastByDeBruijn.v). - -The curve-specific synthesis framework lives in [`src/Specific/Framework`](./src/Specific/Framework). The input `.json` files live in [`src/Specific/CurveParameters`](./src/Specific/CurveParameters), and the processor for those files lives in [`src/Specific/Framework/make_curve.py`](./src/Specific/Framework/make_curve.py). The record of curve specific parameters is defined in [`src/Specific/Framework/RawCurveParameters.v`](./src/Specific/Framework/RawCurveParameters.v), and defaults are filled in [`src/Specific/Framework/CurveParameters.v`](src/Specific/Framework/CurveParameters.v). The tactics that specialize the various arithmetic optimizations to specific curves live in [`src/Specific/Framework/ArithmeticSynthesis`](./src/Specific/Framework/ArithmeticSynthesis), e.g., [`src/Specific/Framework/ArithmeticSynthesis/Montgomery.v`](./src/Specific/Framework/ArithmeticSynthesis/Montgomery.v). The script at [`src/Specific/Framework/ArithmeticSynthesis/remake_packages.py`](./src/Specific/Framework/ArithmeticSynthesis/remake_packages.py) processes these files to add relevant boilerplate, and gets run after significantly changing an optimization, or after adding a new optimization. The synthesis tactics are assembled in [`src/Specific/Framework/SynthesisFramework.v`](./src/Specific/Framework/SynthesisFramework.v). Note that magic[¹](#magic) is used to create identifiers refering to the curve-specific parameters, from tactics, so that they can be used in other curve-specific files. +- The curve-non-specific synthesis framework lives in [`src/Compilers/Z/Bounds/Pipeline`](./src/Compilers/Z/Bounds/Pipeline). +- The API for the reflective simplification and bounds analysis pipeline is in [`src/Compilers/Z/Bounds/Pipeline.v`](./src/Compilers/Z/Bounds/Pipeline.v). +- The definition of the pipeline and the correctness proof are in [`src/Compilers/Z/Bounds/Pipeline/Definition.v`](./src/Compilers/Z/Bounds/Pipeline/Definition.v). +- Generic reflective syntax trees are defined in [`src/Compilers/Syntax.v`](./src/Compilers/Syntax.v); the specialization to the arithmetic operations on Z that we use occurs in [`src/Compilers/Z/Syntax.v`](./src/Compilers/Z/Syntax.v). +- The trusted pretty-printer lives in [`src/Compilers/Z/CNotations.v`](./src/Compilers/Z/CNotations.v) and [`src/Compilers/Z/HexNotationConstants.v`](./src/Compilers/Z/HexNotationConstants.v), which were generated by the couple-hundred-line Python scripts in a comment near the top of each file. +- The core of the bounds-analysis transformation lives in [`src/Compilers/Z/Bounds/Interpretation.v`](./src/Compilers/Z/Bounds/Interpretation.v); the corresponding proofs live in [`src/Compilers/Z/Bounds/InterpretationLemmas`](./src/Compilers/Z/Bounds/InterpretationLemmas), and the instantation of the bounds-analysis transformation with the core lives in [`src/Compilers/Z/Bounds/MapCastByDeBruijn.v`](./src/Compilers/Z/Bounds/MapCastByDeBruijn.v). + + +The curve-specific synthesis framework lives in [`src/Specific/Framework`](./src/Specific/Framework). +- The input `.json` files live in [`src/Specific/CurveParameters`](./src/Specific/CurveParameters), and the processor for those files lives in [`src/Specific/Framework/make_curve.py`](./src/Specific/Framework/make_curve.py). +- The record of curve specific parameters is defined in [`src/Specific/Framework/RawCurveParameters.v`](./src/Specific/Framework/RawCurveParameters.v), and defaults are filled in [`src/Specific/Framework/CurveParameters.v`](src/Specific/Framework/CurveParameters.v). +- The tactics that specialize the various arithmetic optimizations to specific curves live in [`src/Specific/Framework/ArithmeticSynthesis`](./src/Specific/Framework/ArithmeticSynthesis), e.g., [`src/Specific/Framework/ArithmeticSynthesis/Montgomery.v`](./src/Specific/Framework/ArithmeticSynthesis/Montgomery.v). +- The script at [`src/Specific/Framework/ArithmeticSynthesis/remake_packages.py`](./src/Specific/Framework/ArithmeticSynthesis/remake_packages.py) processes these files to add relevant boilerplate, and gets run after significantly changing an optimization, or after adding a new optimization. +- The synthesis tactics are assembled in [`src/Specific/Framework/SynthesisFramework.v`](./src/Specific/Framework/SynthesisFramework.v). +Note that magic[¹](#magic) is used to create identifiers refering to the curve-specific parameters, from tactics, so that they can be used in other curve-specific files. ### Example Output -- cgit v1.2.3