From a1fdf4457c77e20673bb20a40aef171379f2b890 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 15 Nov 2017 18:24:54 -0500 Subject: Update README.md --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'README.md') diff --git a/README.md b/README.md index e875767b2..ffa36b872 100644 --- a/README.md +++ b/README.md @@ -67,11 +67,11 @@ Some selected cuve-level proofs live in [`src/Curves/Edwards/AffineProofs.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 +### Demo of Synthesis The idea of the synthesis process is demoed in [`src/Demo.v`](./src/Demo.v). -# Actual Synthesis +### 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). -- cgit v1.2.3