Jamie (May 12 2024 at 06:26): Jamie (May 12 2024 at 06:26):Hello everyone,
I am trying to implement a pluraity voting system and i have problem when adding the ballots...
I have the isabelle code below with which I want to take a sorted Preference-List (most favoured at top, least at bottom) and add a 1 which was encrypted with aencrypt from "Game_Based_Crypto.Elgamal" to another list. The other list has Pairs which consist of one element like the ones in the Preference-List and a second one which holds the encrypted numeric value of how many times someone voted for it:
theory verifyPlurality imports
"Game_Based_Crypto.Elgamal"
"...lot of folders.../Preference_List"
begin
context elgamal_base
begin
(*The Preference_List is already encrypted,
this function takes the encrypted Preference_List finds its first element in
the Pair-List representing the Ballot where the votes are accumulated and adds 1
(encrypted 1 because of the homomorphic adding)*)
fun add_plurality_ballot :: "'grp pub_key ⇒'a Preference_List ⇒ ('a × 'b) list ⇒ ('a × 'b) list"
where
"add_plurality_ballot _ [] (s) = s"|
"add_plurality_ballot pk (x # xs) (s) =
(case find (λ(y,c). (x = y)) s of
None ⇒ add_plurality_ballot pk xs (s) |
Some (y, c) ⇒ (y,c + (aencrypt pk 1)) # remove1 (λ(a,_).a = y) s)"
end
end
A Preference_List is just this with some functions: type_synonym 'a Preference_List = " 'a list"
I get this error:
Type unification failed: Variable 'grp::type not of sort one
Type error in application: incompatible operand type
Operator: aencrypt pk :: 'grp ⇒ ('grp × 'grp) spmf
Operand: 1 :: ??'a
Coercion Inference:
Local coercion insertion on the operand failed:
Variable 'grp::type not of sort one
Now trying to infer coercions globally.
Coercion inference failed:
weak unification of subtype constraints fails
Clash of types "_ × _" and "_ ⇒ _"
I mean, I get these are not the same types but is there a way to convert one or is there an altogether different/better solution?
Thank you for the help :)
Yong Kiam (May 12 2024 at 08:06):I haven't looked deeply, but the comment says "Preference_List" is already encrypted, so shouldn't your type variable 'a be 'grp ?
Jamie (May 12 2024 at 11:52):Yong Kiam schrieb:
I haven't looked deeply, but the comment says "Preference_List" is already encrypted, so shouldn't your type variable
'abe'grp?
Thank you! You are right I just fixed it up, but i still have the same problem. I don't know how I can encrypt the numer 1 with aencrypt, even if I only write this functrion:
fun encrypt1::"'grp pub_key ⇒ nat ⇒ 'grp ⇒ 'grp cipher spmf" where
"encrypt1 = aencrypt pk 1"
I get the same error as above. I don't know how I can make the 1 fit in.
Yong Kiam (May 12 2024 at 13:42):I think you want either:
term "aencrypt pk 𝟭"
term "aencrypt pk (one 𝒢)"
Yong Kiam (May 12 2024 at 13:47):I don't know why but that entry is using groups from HOL-Algebra which is older(?), probably there's a reason for it and someone else would be able to answer better, but the unit is written as I've typed above (\<one>)
edit: I believe I have it the other way around in terms of age ^
Jamie (May 12 2024 at 16:32):Yong Kiam schrieb:
I think you want either:
term "aencrypt pk 𝟭"
term "aencrypt pk (one 𝒢)"
This worked, thank you very much :)
Unfortunately now I have the problem that "+" does not add two elements of type "('grp × 'grp) spmf" (or even only type 'grp) like i thought it would with homomorphically encrypted.
If you (or someone else) had a solution for this I would be very grateful :)
Yong Kiam (May 12 2024 at 23:51):you want ⊗
Yong Kiam (May 12 2024 at 23:51):in general, it'd be good to look up the HOL-Algebra libraries, e.g.:
record 'a monoid = "'a partial_object" +
mult :: "['a, 'a] ⇒ 'a" (infixl "⊗ı" 70)
one :: 'a ("𝟭ı")
Yong Kiam schrieb:
you want ⊗
Thank you! :D
I tried that one before but apparently had some other issue and it didn't work then, but now it does :tada:
Jamie (May 13 2024 at 13:00):In case anyone has a similar problem in the future, here is my solution:
definition add_pair :: "('grp × 'grp) spmf ⇒ ('grp × 'grp) spmf ⇒ ('grp × 'grp) spmf" where
"add_pair x_spmf y_spmf = do {
(x1, x2) ← x_spmf;
(y1, y2) ← y_spmf;
return_spmf (x1 ⊗ y1, x2 ⊗ y2)
}"
And thanks again for the help :)
Yong Kiam (May 13 2024 at 14:35):no worries, do note that you can write this using map_spmf and pair_spmf
Last updated: Dec 21 2024 at 16:20 UTC