Main.hs

import qualified Prelude

__ :: any
__ = Prelude.error "Logical or arity value used"

data Bool =
   True
 | False
 deriving (Prelude.Show)

data Nat =
   O
 | S Nat
 deriving (Prelude.Show)

data Prod a b =
   Pair a b
   deriving (Prelude.Show)

snd :: (Prod a1 a2) -> a2
snd p0 =
  case p0 of {
   Pair _ y -> y}

data Comparison =
   Eq
 | Lt
 | Gt
  deriving (Prelude.Show)

compOpp :: Comparison -> Comparison
compOpp r =
  case r of {
   Eq -> Eq;
   Lt -> Gt;
   Gt -> Lt}

data Sumbool =
   Left
 | Right
  deriving (Prelude.Show)

sumbool_rect :: (() -> a1) -> (() -> a1) -> Sumbool -> a1
sumbool_rect f f0 s =
  case s of {
   Left -> f __;
   Right -> f0 __}

sumbool_rec :: (() -> a1) -> (() -> a1) -> Sumbool -> a1
sumbool_rec =
  sumbool_rect

data Positive =
   XI Positive
 | XO Positive
 | XH
  deriving (Prelude.Show)

positive_rect :: (Positive -> a1 -> a1) -> (Positive -> a1 -> a1) -> a1 ->
                 Positive -> a1
positive_rect f f0 f1 p0 =
  case p0 of {
   XI p1 -> f p1 (positive_rect f f0 f1 p1);
   XO p1 -> f0 p1 (positive_rect f f0 f1 p1);
   XH -> f1}

positive_rec :: (Positive -> a1 -> a1) -> (Positive -> a1 -> a1) -> a1 ->
                Positive -> a1
positive_rec =
  positive_rect

data N =
   N0
 | Npos Positive
  deriving (Prelude.Show)

data Z =
   Z0
 | Zpos Positive
 | Zneg Positive
  deriving (Prelude.Show)

z_rect :: a1 -> (Positive -> a1) -> (Positive -> a1) -> Z -> a1
z_rect f f0 f1 z =
  case z of {
   Z0 -> f;
   Zpos p0 -> f0 p0;
   Zneg p0 -> f1 p0}

z_rec :: a1 -> (Positive -> a1) -> (Positive -> a1) -> Z -> a1
z_rec =
  z_rect

succ :: Positive -> Positive
succ x0 =
  case x0 of {
   XI p0 -> XO (succ p0);
   XO p0 -> XI p0;
   XH -> XO XH}

add :: Positive -> Positive -> Positive
add x0 y =
  case x0 of {
   XI p0 ->
    case y of {
     XI q0 -> XO (add_carry p0 q0);
     XO q0 -> XI (add p0 q0);
     XH -> XO (succ p0)};
   XO p0 ->
    case y of {
     XI q0 -> XI (add p0 q0);
     XO q0 -> XO (add p0 q0);
     XH -> XI p0};
   XH -> case y of {
          XI q0 -> XO (succ q0);
          XO q0 -> XI q0;
          XH -> XO XH}}

add_carry :: Positive -> Positive -> Positive
add_carry x0 y =
  case x0 of {
   XI p0 ->
    case y of {
     XI q0 -> XI (add_carry p0 q0);
     XO q0 -> XO (add_carry p0 q0);
     XH -> XI (succ p0)};
   XO p0 ->
    case y of {
     XI q0 -> XO (add_carry p0 q0);
     XO q0 -> XI (add p0 q0);
     XH -> XO (succ p0)};
   XH ->
    case y of {
     XI q0 -> XI (succ q0);
     XO q0 -> XO (succ q0);
     XH -> XI XH}}

pred_double :: Positive -> Positive
pred_double x0 =
  case x0 of {
   XI p0 -> XI (XO p0);
   XO p0 -> XI (pred_double p0);
   XH -> XH}

data Mask =
   IsNul
 | IsPos Positive
 | IsNeg
  deriving (Prelude.Show)

succ_double_mask :: Mask -> Mask
succ_double_mask x0 =
  case x0 of {
   IsNul -> IsPos XH;
   IsPos p0 -> IsPos (XI p0);
   IsNeg -> IsNeg}

double_mask :: Mask -> Mask
double_mask x0 =
  case x0 of {
   IsPos p0 -> IsPos (XO p0);
   x1 -> x1}

double_pred_mask :: Positive -> Mask
double_pred_mask x0 =
  case x0 of {
   XI p0 -> IsPos (XO (XO p0));
   XO p0 -> IsPos (XO (pred_double p0));
   XH -> IsNul}

sub_mask :: Positive -> Positive -> Mask
sub_mask x0 y =
  case x0 of {
   XI p0 ->
    case y of {
     XI q0 -> double_mask (sub_mask p0 q0);
     XO q0 -> succ_double_mask (sub_mask p0 q0);
     XH -> IsPos (XO p0)};
   XO p0 ->
    case y of {
     XI q0 -> succ_double_mask (sub_mask_carry p0 q0);
     XO q0 -> double_mask (sub_mask p0 q0);
     XH -> IsPos (pred_double p0)};
   XH -> case y of {
          XH -> IsNul;
          _ -> IsNeg}}

sub_mask_carry :: Positive -> Positive -> Mask
sub_mask_carry x0 y =
  case x0 of {
   XI p0 ->
    case y of {
     XI q0 -> succ_double_mask (sub_mask_carry p0 q0);
     XO q0 -> double_mask (sub_mask p0 q0);
     XH -> IsPos (pred_double p0)};
   XO p0 ->
    case y of {
     XI q0 -> double_mask (sub_mask_carry p0 q0);
     XO q0 -> succ_double_mask (sub_mask_carry p0 q0);
     XH -> double_pred_mask p0};
   XH -> IsNeg}

mul :: Positive -> Positive -> Positive
mul x0 y =
  case x0 of {
   XI p0 -> add y (XO (mul p0 y));
   XO p0 -> XO (mul p0 y);
   XH -> y}

compare_cont :: Comparison -> Positive -> Positive -> Comparison
compare_cont r x0 y =
  case x0 of {
   XI p0 ->
    case y of {
     XI q0 -> compare_cont r p0 q0;
     XO q0 -> compare_cont Gt p0 q0;
     XH -> Gt};
   XO p0 ->
    case y of {
     XI q0 -> compare_cont Lt p0 q0;
     XO q0 -> compare_cont r p0 q0;
     XH -> Gt};
   XH -> case y of {
          XH -> r;
          _ -> Lt}}

compare :: Positive -> Positive -> Comparison
compare =
  compare_cont Eq

succ0 :: Positive -> Positive
succ0 x0 =
  case x0 of {
   XI p0 -> XO (succ0 p0);
   XO p0 -> XI p0;
   XH -> XO XH}

add0 :: Positive -> Positive -> Positive
add0 x0 y =
  case x0 of {
   XI p0 ->
    case y of {
     XI q0 -> XO (add_carry0 p0 q0);
     XO q0 -> XI (add0 p0 q0);
     XH -> XO (succ0 p0)};
   XO p0 ->
    case y of {
     XI q0 -> XI (add0 p0 q0);
     XO q0 -> XO (add0 p0 q0);
     XH -> XI p0};
   XH -> case y of {
          XI q0 -> XO (succ0 q0);
          XO q0 -> XI q0;
          XH -> XO XH}}

add_carry0 :: Positive -> Positive -> Positive
add_carry0 x0 y =
  case x0 of {
   XI p0 ->
    case y of {
     XI q0 -> XI (add_carry0 p0 q0);
     XO q0 -> XO (add_carry0 p0 q0);
     XH -> XI (succ0 p0)};
   XO p0 ->
    case y of {
     XI q0 -> XO (add_carry0 p0 q0);
     XO q0 -> XI (add0 p0 q0);
     XH -> XO (succ0 p0)};
   XH ->
    case y of {
     XI q0 -> XI (succ0 q0);
     XO q0 -> XO (succ0 q0);
     XH -> XI XH}}

mul0 :: Positive -> Positive -> Positive
mul0 x0 y =
  case x0 of {
   XI p0 -> add0 y (XO (mul0 p0 y));
   XO p0 -> XO (mul0 p0 y);
   XH -> y}

eq_dec :: Positive -> Positive -> Sumbool
eq_dec x0 y =
  positive_rec (\_ x1 x2 ->
    case x2 of {
     XI p0 -> sumbool_rec (\_ -> Left) (\_ -> Right) (x1 p0);
     _ -> Right}) (\_ x1 x2 ->
    case x2 of {
     XO p0 -> sumbool_rec (\_ -> Left) (\_ -> Right) (x1 p0);
     _ -> Right}) (\x1 -> case x1 of {
                           XH -> Left;
                           _ -> Right})
    x0 y

succ_double :: N -> N
succ_double x0 =
  case x0 of {
   N0 -> Npos XH;
   Npos p0 -> Npos (XI p0)}

double :: N -> N
double n =
  case n of {
   N0 -> N0;
   Npos p0 -> Npos (XO p0)}

sub :: N -> N -> N
sub n m =
  case n of {
   N0 -> N0;
   Npos n' ->
    case m of {
     N0 -> n;
     Npos m' -> case sub_mask n' m' of {
                 IsPos p0 -> Npos p0;
                 _ -> N0}}}

compare0 :: N -> N -> Comparison
compare0 n m =
  case n of {
   N0 -> case m of {
          N0 -> Eq;
          Npos _ -> Lt};
   Npos n' -> case m of {
               N0 -> Gt;
               Npos m' -> compare n' m'}}

leb :: N -> N -> Bool
leb x0 y =
  case compare0 x0 y of {
   Gt -> False;
   _ -> True}

pos_div_eucl :: Positive -> N -> Prod N N
pos_div_eucl a b =
  case a of {
   XI a' ->
    case pos_div_eucl a' b of {
     Pair q0 r ->
      let {r' = succ_double r} in
      case leb b r' of {
       True -> Pair (succ_double q0) (sub r' b);
       False -> Pair (double q0) r'}};
   XO a' ->
    case pos_div_eucl a' b of {
     Pair q0 r ->
      let {r' = double r} in
      case leb b r' of {
       True -> Pair (succ_double q0) (sub r' b);
       False -> Pair (double q0) r'}};
   XH ->
    case b of {
     N0 -> Pair N0 (Npos XH);
     Npos p0 -> case p0 of {
                 XH -> Pair (Npos XH) N0;
                 _ -> Pair N0 (Npos XH)}}}

mul1 :: N -> N -> N
mul1 n m =
  case n of {
   N0 -> N0;
   Npos p0 -> case m of {
               N0 -> N0;
               Npos q0 -> Npos (mul0 p0 q0)}}

div_eucl :: N -> N -> Prod N N
div_eucl a b =
  case a of {
   N0 -> Pair N0 N0;
   Npos na -> case b of {
               N0 -> Pair N0 a;
               Npos _ -> pos_div_eucl na b}}

modulo :: N -> N -> N
modulo a b =
  snd (div_eucl a b)

double0 :: Z -> Z
double0 x0 =
  case x0 of {
   Z0 -> Z0;
   Zpos p0 -> Zpos (XO p0);
   Zneg p0 -> Zneg (XO p0)}

succ_double0 :: Z -> Z
succ_double0 x0 =
  case x0 of {
   Z0 -> Zpos XH;
   Zpos p0 -> Zpos (XI p0);
   Zneg p0 -> Zneg (pred_double p0)}

pred_double0 :: Z -> Z
pred_double0 x0 =
  case x0 of {
   Z0 -> Zneg XH;
   Zpos p0 -> Zpos (pred_double p0);
   Zneg p0 -> Zneg (XI p0)}

pos_sub :: Positive -> Positive -> Z
pos_sub x0 y =
  case x0 of {
   XI p0 ->
    case y of {
     XI q0 -> double0 (pos_sub p0 q0);
     XO q0 -> succ_double0 (pos_sub p0 q0);
     XH -> Zpos (XO p0)};
   XO p0 ->
    case y of {
     XI q0 -> pred_double0 (pos_sub p0 q0);
     XO q0 -> double0 (pos_sub p0 q0);
     XH -> Zpos (pred_double p0)};
   XH ->
    case y of {
     XI q0 -> Zneg (XO q0);
     XO q0 -> Zneg (pred_double q0);
     XH -> Z0}}

add1 :: Z -> Z -> Z
add1 x0 y =
  case x0 of {
   Z0 -> y;
   Zpos x' ->
    case y of {
     Z0 -> x0;
     Zpos y' -> Zpos (add x' y');
     Zneg y' -> pos_sub x' y'};
   Zneg x' ->
    case y of {
     Z0 -> x0;
     Zpos y' -> pos_sub y' x';
     Zneg y' -> Zneg (add x' y')}}

opp :: Z -> Z
opp x0 =
  case x0 of {
   Z0 -> Z0;
   Zpos x1 -> Zneg x1;
   Zneg x1 -> Zpos x1}

sub0 :: Z -> Z -> Z
sub0 m n =
  add1 m (opp n)

mul2 :: Z -> Z -> Z
mul2 x0 y =
  case x0 of {
   Z0 -> Z0;
   Zpos x' ->
    case y of {
     Z0 -> Z0;
     Zpos y' -> Zpos (mul x' y');
     Zneg y' -> Zneg (mul x' y')};
   Zneg x' ->
    case y of {
     Z0 -> Z0;
     Zpos y' -> Zneg (mul x' y');
     Zneg y' -> Zpos (mul x' y')}}

compare1 :: Z -> Z -> Comparison
compare1 x0 y =
  case x0 of {
   Z0 -> case y of {
          Z0 -> Eq;
          Zpos _ -> Lt;
          Zneg _ -> Gt};
   Zpos x' -> case y of {
               Zpos y' -> compare x' y';
               _ -> Gt};
   Zneg x' -> case y of {
               Zneg y' -> compOpp (compare x' y');
               _ -> Lt}}

leb0 :: Z -> Z -> Bool
leb0 x0 y =
  case compare1 x0 y of {
   Gt -> False;
   _ -> True}

ltb :: Z -> Z -> Bool
ltb x0 y =
  case compare1 x0 y of {
   Lt -> True;
   _ -> False}

of_N :: N -> Z
of_N n =
  case n of {
   N0 -> Z0;
   Npos p0 -> Zpos p0}

pos_div_eucl0 :: Positive -> Z -> Prod Z Z
pos_div_eucl0 a b =
  case a of {
   XI a' ->
    case pos_div_eucl0 a' b of {
     Pair q0 r ->
      let {r' = add1 (mul2 (Zpos (XO XH)) r) (Zpos XH)} in
      case ltb r' b of {
       True -> Pair (mul2 (Zpos (XO XH)) q0) r';
       False -> Pair (add1 (mul2 (Zpos (XO XH)) q0) (Zpos XH)) (sub0 r' b)}};
   XO a' ->
    case pos_div_eucl0 a' b of {
     Pair q0 r ->
      let {r' = mul2 (Zpos (XO XH)) r} in
      case ltb r' b of {
       True -> Pair (mul2 (Zpos (XO XH)) q0) r';
       False -> Pair (add1 (mul2 (Zpos (XO XH)) q0) (Zpos XH)) (sub0 r' b)}};
   XH ->
    case leb0 (Zpos (XO XH)) b of {
     True -> Pair Z0 (Zpos XH);
     False -> Pair (Zpos XH) Z0}}

div_eucl0 :: Z -> Z -> Prod Z Z
div_eucl0 a b =
  case a of {
   Z0 -> Pair Z0 Z0;
   Zpos a' ->
    case b of {
     Z0 -> Pair Z0 a;
     Zpos _ -> pos_div_eucl0 a' b;
     Zneg b' ->
      case pos_div_eucl0 a' (Zpos b') of {
       Pair q0 r ->
        case r of {
         Z0 -> Pair (opp q0) Z0;
         _ -> Pair (opp (add1 q0 (Zpos XH))) (add1 b r)}}};
   Zneg a' ->
    case b of {
     Z0 -> Pair Z0 a;
     Zpos _ ->
      case pos_div_eucl0 a' b of {
       Pair q0 r ->
        case r of {
         Z0 -> Pair (opp q0) Z0;
         _ -> Pair (opp (add1 q0 (Zpos XH))) (sub0 b r)}};
     Zneg b' ->
      case pos_div_eucl0 a' (Zpos b') of {
       Pair q0 r -> Pair q0 (opp r)}}}

modulo0 :: Z -> Z -> Z
modulo0 a b =
  case div_eucl0 a b of {
   Pair _ r -> r}

to_N :: Z -> N
to_N z =
  case z of {
   Zpos p0 -> Npos p0;
   _ -> N0}

eq_dec0 :: Z -> Z -> Sumbool
eq_dec0 x0 y =
  z_rec (\x1 -> case x1 of {
                 Z0 -> Left;
                 _ -> Right})
    (\p0 x1 ->
    case x1 of {
     Zpos p1 -> sumbool_rec (\_ -> Left) (\_ -> Right) (eq_dec p0 p1);
     _ -> Right}) (\p0 x1 ->
    case x1 of {
     Zneg p1 -> sumbool_rec (\_ -> Left) (\_ -> Right) (eq_dec p0 p1);
     _ -> Right}) x0 y

data T a =
   Nil
 | Cons a Nat (T a)
  deriving (Prelude.Show)

caseS :: (a1 -> Nat -> (T a1) -> a2) -> Nat -> (T a1) -> a2
caseS h0 _ v =
  case v of {
   Nil -> __;
   Cons h1 n0 t -> h0 h1 n0 t}

hd :: Nat -> (T a1) -> a1
hd =
  caseS (\h0 _ _ -> h0)

repeat_op_ntimes_rec :: N -> Positive -> N -> N
repeat_op_ntimes_rec e n w =
  case n of {
   XI p0 ->
    let {ret = repeat_op_ntimes_rec e p0 w} in
    modulo (mul1 e (mul1 ret ret)) w;
   XO p0 ->
    let {ret = repeat_op_ntimes_rec e p0 w} in modulo (mul1 ret ret) w;
   XH -> modulo e w}

npow_mod :: N -> N -> N -> N
npow_mod e n w =
  case n of {
   N0 -> Npos XH;
   Npos p0 -> repeat_op_ntimes_rec e p0 w}

type Zp = Z
  -- singleton inductive, whose constructor was mk_zp
  
zp_add :: Z -> Zp -> Zp -> Zp
zp_add p0 x0 y =
  modulo0 (add1 x0 y) p0

zp_mul :: Z -> Zp -> Zp -> Zp
zp_mul p0 x0 y =
  modulo0 (mul2 x0 y) p0

type Schnorr_group =
  Z 
  -- singleton inductive, whose constructor was mk_schnorr
  
dec_zpstar :: Z -> Z -> Schnorr_group -> Schnorr_group -> Sumbool
dec_zpstar _ _ =
  eq_dec0

mul_schnorr_group :: Z -> Z -> Schnorr_group -> Schnorr_group ->
                     Schnorr_group
mul_schnorr_group p0 _ u0 v =
  modulo0 (mul2 u0 v) p0

pow :: Z -> Z -> Z -> Schnorr_group -> Zp -> Schnorr_group
pow _ p0 _ g0 y =
  of_N (npow_mod (to_N g0) (to_N y) (to_N p0))

data Sigma_proto f g =
   Mk_sigma (T g) (T f) (T f)
  deriving (Prelude.Show)

schnorr_protocol :: (a1 -> a1 -> a1) -> (a1 -> a1 -> a1) -> (a2 -> a1 -> a2)
                    -> a1 -> a2 -> a1 -> a1 -> Sigma_proto a1 a2
schnorr_protocol add2 mul3 gpow x0 g0 u0 c0 =
  Mk_sigma (Cons (gpow g0 u0) O Nil) (Cons c0 O Nil) (Cons
    (add2 u0 (mul3 c0 x0)) O Nil)

accepting_conversation :: (a2 -> a2 -> a2) -> (a2 -> a1 -> a2) -> (a2 -> a2
                          -> Sumbool) -> a2 -> a2 -> (Sigma_proto a1 
                          a2) -> Bool
accepting_conversation gop gpow gdec g0 h0 v =
  case v of {
   Mk_sigma a c0 r ->
    case gdec (gpow g0 (hd O r)) (gop (hd O a) (gpow h0 (hd O c0))) of {
     Left -> True;
     Right -> False}}

q :: Z
q =
  Zpos (XI (XI (XO XH)))

p :: Z
p =
  Zpos (XI (XI (XI (XO XH))))

x :: Zp
x =
  Zpos (XI XH)

g :: Schnorr_group
g =
  Zpos (XO (XO XH))

u :: Zp
u =
  Zpos (XO (XI XH))

c :: Zp
c =
  Zpos (XO (XO XH))

h :: Schnorr_group
h =
  Zpos (XO (XI (XO (XO XH))))

transcript :: Sigma_proto Zp Schnorr_group
transcript =
  schnorr_protocol (zp_add q) (zp_mul q) (pow (Zpos (XO XH)) p q) x g u c

verify :: Bool
verify =
  accepting_conversation (mul_schnorr_group p q) (pow (Zpos (XO XH)) p q)
    (dec_zpstar p q) g h transcript

main :: Prelude.IO () = Prelude.print verify