Theory Voting
theory Voting
imports Solidity_Main
begin
section ‹Voting Contract›
text ‹
In the following we verify the Voting contract from the official Solidity documentation:
🌐‹https://docs.soliditylang.org/en/v0.8.25/solidity-by-example.html#voting›.
›
lemma kdequals_true[wpdrules]:
assumes "kdequals (rvalue.Value (Uint w)) (rvalue.Value (Uint x)) = Some (rvalue.Value (Bool True))"
shows "w = x"
using assms unfolding kdequals_def by simp
subsection ‹Specification›
abbreviation TT::"((String.literal ⇒ 'a storage_data) × nat) ⇒ bool" where "TT a ≡ True"
context Solidity
begin
abbreviation Voter where "Voter ≡ storage_data.Array [storage_data.Value (Uint 0),storage_data.Value (Bool False),storage_data.Value (Address null),storage_data.Value (Uint 0::'a valtype)]"
abbreviation "weight ≡ return (rvalue.Value ((Uint 0)::'a valtype))"
abbreviation "voted ≡ 1::nat"
abbreviation "sdelegate ≡ 2::nat"
abbreviation "svote ≡ 3::nat"
abbreviation "Proposal name voteCount ≡ storage_data.Array [name::'a valtype storage_data, voteCount]"
abbreviation "name ≡ 0::nat"
abbreviation "voteCount ≡ 1::nat"
end
text ‹
The contract can now be specified using the "contract" command.
This command requires the following:
▪ A sequence of member variables
▪ A constructor
▪ A sequence of methods
›
context Solidity
begin
abbreviation "SUMM (x::('a valtype ⇒ 'a valtype storage_data)) ≡ ∑ad|∃v. x (Address ad) = storage_data.Array v ∧ valtype.bool (storage_data.vt (v ! 1)). (THE y. ∃v. x (Address ad) = storage_data.Array v ∧ y=unat (valtype.uint (storage_data.vt (v ! 0))))"
abbreviation "SUMM2 (x::'a valtype storage_data list) ≡ ∑i<length x. (THE y. ∃p. x ! i = storage_data.Array p ∧ y=unat (valtype.uint (storage_data.vt (p ! 1))))"
definition inv':: "(id ⇒ 'a valtype storage_data) ⇒ bool"
where "inv' s ≡ (∀x y. s (STR ''voters'') = storage_data.Map x
∧ s (STR ''proposals'') = storage_data.Array y
⟶ (SUMM2 y ≤ SUMM x))"
end