From f5abbbc8652468599b319bb47e76c2549284f842 Mon Sep 17 00:00:00 2001
From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Thu, 23 Mar 2017 21:06:33 +0100
Subject: [PATCH] Validity of Lemma 11 in krypto1.pdf

---
 numbertheory.txt | 75 ++++++++++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 68 insertions(+), 7 deletions(-)

diff --git a/numbertheory.txt b/numbertheory.txt
index 11702c3..479d6d4 100644
--- a/numbertheory.txt
+++ b/numbertheory.txt
@@ -100,29 +100,93 @@ proc isquadraticresidue(a:nat,p:nat): Bool
 // ==  1   a is quadratic residue modulo p
 // == -1   a is NOT quadratic residue modulo p
 // ==  2   if p is not prime
+// pure definition implementation
 ////////////////////////////////////////////////////////////////////
 proc legendre(a:nat,p:nat): integer
    ensures (((result =  0) ∧ divides(p,a)) ∨
-            ((result =  1) ∧ isquadraticresidue(p,a)) ∨
-            ((result = -1) ∧ ~isquadraticresidue(p,a)) ∨
+            ((result =  1) ∧ isquadraticresidue(a,p)) ∨
+            ((result = -1) ∧ ~isquadraticresidue(a,p)) ∨
             ((result =  2) ∧ ~isprime(p)));
 {
-   var res:integer = 0;
+   var res:integer = 3;
 
    if isprime(p) then
+   {
       if divides(p,a) then
+      {
          res = 0;
-      else if isquadraticresidue(p,a) then
+      }
+      else if isquadraticresidue(a,p) then
+      {
          res = 1;
+      }
       else
+      {
          res = -1;
+      }
+   }
    else
+   {
       res = 2;
+   }
+   return res;
+}
+
+////////////////////////////////////////////////////////////////////
+// Legendre Symbol   (a/p)
+// ==  0   divides(p,a)
+// ==  1   a is quadratic residue modulo p
+// == -1   a is NOT quadratic residue modulo p
+// ==  2   if p is not prime
+// implementation as in Lemma 11 of krypto1.pdf
+////////////////////////////////////////////////////////////////////
+proc legendre2(a:nat,p:nat): integer
+   ensures (((result =  0) ∧ divides(p,a)) ∨
+            ((result =  1) ∧ isquadraticresidue(a,p)) ∨
+            ((result = -1) ∧ ~isquadraticresidue(a,p)) ∨
+            ((result =  2) ∧ ~isprime(p)));
+{
+   var res:integer = 0;
+
+   if isprime(p) then
+   {
+      // Lemma 11
+      if divides(p,a) then
+      {
+         res = 0;
+      }
+      else if a ≠ 0 then 
+      {
+         if a^((p-1)/2)%p ≠ 1 then
+         {
+             res = -1;
+         }
+         else
+         {
+             res = 1;
+         }
+      }
+      else
+      {
+         res = 0;
+      }
+   }
+   else
+   {
+      res = 2;
+   }
 
    return res;
 }
 
 ////////////////////////////////////////////////////////////////////
+// Heuristic for proving the validity of Lemma 11
+////////////////////////////////////////////////////////////////////
+theorem lemma11(a:nat,p:nat) ⇔ 
+   ∀ap:nat. ∀pp:nat. (1 ≤ ap ∧ ap ≤ a ∧ 1 ≤ pp ∧ pp ≤ p) ⇒ 
+                     (legendre(ap,pp) = legendre2(ap,pp));
+
+////////////////////////////////////////////////////////////////////
 // Algorithm: Calculate x^n by Right-To-Left Exponentation
 ////////////////////////////////////////////////////////////////////
 proc r2lexponentation(x:Base,n:Exp): Result
@@ -163,6 +227,3 @@ proc xpowern(x:Base,n:Exp): Result
    return res;
 }
 
-
-
-
-- 
2.1.4