theory verifyPlurality imports

"Game_Based_Crypto.Elgamal"

begin

context ind_cpa

begin

fun ballotEncrypt :: "'grp pub_key ⇒ 'a list ⇒ 'a cipher list spmf"

  where

   ballotEncryptNil: "ballotEncrypt pk [] = []" |

   ballotEncryptCons: "ballotEncrypt pk (x # xs) = (aencrypt pk x) # ballotEncrypt pk  xs"

fun ballotDecrypt :: "'a priv_key ⇒ 'a cipher list ⇒ 'a option"

  where

    ballotDecryptNil: "ballotDecrypt sk [] = []" |

    ballotDecryptCons: "ballotDecrypt  sk(x # xs) = (adecrypt sk x) # ballotDecrypt sk xs"

end

end

Undefined type name: "pub_key"⌂

Failed to parse type

type_synonym 'grp' pub_key = "'grp'"

type_synonym 'grp' priv_key = nat

type_synonym 'grp' plain = 'grp'

type_synonym 'grp' cipher = "'grp' × 'grp'"

Type unification failed: Clash of types "_ list" and "_ pmf"

Type error in application: incompatible operand type

Operator:  (=) (ballotEncrypt pk []) :: ('a × 'a) list spmf ⇒ bool

Operand:   [] :: ??'a list

Coercion Inference:

Local coercion insertion on the operand failed:

No coercion known for type constructors: "list" and "pmf"

Type unification failed: Clash of types "_ list" and "_ option"

Type error in application: incompatible operand type

Operator:  (=) (ballotDecrypt sk []) :: 'a option ⇒ bool
Operand:   [] :: ??'a list

Coercion Inference:

Local coercion insertion on the operand failed:
No coercion known for type constructors: "list" and "option"

theory verifyPlurality imports
"Game_Based_Crypto.Elgamal"
begin
context elgamal_base
begin

fun ballotEncrypt :: "'grp pub_key => 'grp list => 'grp cipher spmf list"
  where
   ballotEncryptNil: "ballotEncrypt pk [] = []" |
   ballotEncryptCons: "ballotEncrypt pk (x # xs) = (aencrypt pk x) # ballotEncrypt pk xs"

fun ballotDecrypt :: "'grp priv_key => 'grp cipher list => 'grp option list"
  where
    ballotDecryptNil: "ballotDecrypt sk [] = []" |
    ballotDecryptCons: "ballotDecrypt sk (x # xs) = (adecrypt sk x) # ballotDecrypt sk xs"
end
end