From aeedfe5bd2f49ce1a3e9905d2c7291472044e8ad Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 12 Nov 2017 18:13:00 -0500
Subject: Remove outdated C128 files

---
 .gitignore                                |  2 --
 src/Specific/X2555/C128/CurveParameters.v | 39 -------------------------------
 src/Specific/X2555/C128/Synthesis.v       |  9 -------
 src/Specific/X2555/C128/ladderstep.v      | 24 -------------------
 src/Specific/X2555/C128/py_interpreter.sh |  4 ----
 5 files changed, 78 deletions(-)
 delete mode 100644 src/Specific/X2555/C128/CurveParameters.v
 delete mode 100644 src/Specific/X2555/C128/Synthesis.v
 delete mode 100644 src/Specific/X2555/C128/ladderstep.v
 delete mode 100755 src/Specific/X2555/C128/py_interpreter.sh

diff --git a/.gitignore b/.gitignore
index fbde72c56..dddbc9e73 100644
--- a/.gitignore
+++ b/.gitignore
@@ -75,8 +75,6 @@ src/Specific/X25519/C32/freeze.c
 src/Specific/X25519/C32/freeze.h
 src/Specific/X25519/C32/measure
 src/Specific/X25519/C32/test
-src/Specific/X2555/C128/ladderstep.c
-src/Specific/X2555/C128/ladderstep.h
 src/Specific/X2448/Karatsuba/C64/femul.c
 src/Specific/X2448/Karatsuba/C64/femul.h
 third_party/openssl-curve25519/measure
diff --git a/src/Specific/X2555/C128/CurveParameters.v b/src/Specific/X2555/C128/CurveParameters.v
deleted file mode 100644
index 1171f7583..000000000
--- a/src/Specific/X2555/C128/CurveParameters.v
+++ /dev/null
@@ -1,39 +0,0 @@
-Require Import Crypto.Specific.Framework.RawCurveParameters.
-Require Import Crypto.Util.LetIn.
-
-(***
-Modulus : 2^255-5
-Base: 130
-***)
-
-Definition curve : CurveParameters :=
-  {|
-    sz := 3%nat;
-    base := 130;
-    bitwidth := 128;
-    s := 2^255;
-    c := [(1, 5)];
-    carry_chains := Some [seq 0 (pred 3); [0; 1]]%nat;
-
-    a24 := Some (121665 (* XXX TODO(andreser) FIXME?  Is this right for this curve? *));
-    coef_div_modulus := Some 2%nat;
-
-    goldilocks := None;
-    karatsuba := None;
-    montgomery := false;
-    freeze := Some false;
-    ladderstep := true;
-
-    mul_code := None;
-
-    square_code := None;
-
-    upper_bound_of_exponent_loose := None;
-    upper_bound_of_exponent_tight := None;
-    allowable_bit_widths := None;
-    freeze_extra_allowable_bit_widths := None;
-    modinv_fuel := None
-  |}.
-
-Ltac extra_prove_mul_eq _ := idtac.
-Ltac extra_prove_square_eq _ := idtac.
diff --git a/src/Specific/X2555/C128/Synthesis.v b/src/Specific/X2555/C128/Synthesis.v
deleted file mode 100644
index af7b8ae33..000000000
--- a/src/Specific/X2555/C128/Synthesis.v
+++ /dev/null
@@ -1,9 +0,0 @@
-Require Import Crypto.Specific.Framework.SynthesisFramework.
-Require Import Crypto.Specific.X2555.C128.CurveParameters.
-
-Module P <: PrePackage.
-  Definition package : Tag.Context.
-  Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined.
-End P.
-
-Module Export S := PackageSynthesis P.
diff --git a/src/Specific/X2555/C128/ladderstep.v b/src/Specific/X2555/C128/ladderstep.v
deleted file mode 100644
index 16984403b..000000000
--- a/src/Specific/X2555/C128/ladderstep.v
+++ /dev/null
@@ -1,24 +0,0 @@
-Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.Framework.ArithmeticSynthesis.Ladderstep.
-Require Import Crypto.Specific.X2555.C128.Synthesis.
-
-(* TODO : change this to field once field isomorphism happens *)
-Definition xzladderstep :
-  { xzladderstep : feW -> feW * feW -> feW * feW -> feW * feW * (feW * feW)
-  | forall x1 Q Q',
-      let xz := xzladderstep x1 Q Q' in
-      let eval := B.Positional.Fdecode wt in
-      feW_tight_bounded x1
-      -> feW_tight_bounded (fst Q) /\ feW_tight_bounded (snd Q)
-      -> feW_tight_bounded (fst Q') /\ feW_tight_bounded (snd Q')
-      -> ((feW_tight_bounded (fst (fst xz)) /\ feW_tight_bounded (snd (fst xz)))
-          /\ (feW_tight_bounded (fst (snd xz)) /\ feW_tight_bounded (snd (snd xz))))
-         /\ Tuple.map (n:=2) (Tuple.map (n:=2) phiW) xz = FMxzladderstep (m:=m) (eval (proj1_sig a24_sig)) (phiW x1) (Tuple.map (n:=2) phiW Q) (Tuple.map (n:=2) phiW Q') }.
-Proof.
-  Set Ltac Profiling.
-  synthesize_xzladderstep ().
-  Show Ltac Profile.
-Time Defined.
-
-Print Assumptions xzladderstep.
diff --git a/src/Specific/X2555/C128/py_interpreter.sh b/src/Specific/X2555/C128/py_interpreter.sh
deleted file mode 100755
index 7ec3fa6ab..000000000
--- a/src/Specific/X2555/C128/py_interpreter.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/sh
-set -eu
-
-/usr/bin/env python3 "$@" -Dq='2**255-5' -Dmodulus_bytes='130' -Da24='121665 (* XXX TODO(andreser) FIXME?  Is this right for this curve? *)'
-- 
cgit v1.2.3