Skip to main content

🧑‍⚖️ Amendment.v

Proofs

See code, Gitlab , OCaml

The function [select_winning_proposal] is valid
Lemma select_winning_proposal_is_valid ctxt :
  Raw_context.Valid.t ctxt
  letP? _ := Amendment.select_winning_proposal ctxt in
  True.
Proof.
  intros H.
  unfold Amendment.select_winning_proposal.
  eapply Error.split_letP. {
    now apply Vote_storage.get_proposals_is_valid.
  }
  intros.
  step; [|easy].
  do 2 step; [easy|].
  step; [|easy].
  eapply Error.split_letP. {
    now apply Vote_storage.get_total_voting_power_free_is_valid.
  }
  intros.
  now step.
Qed.

The function [approval_and_participation_ema_is_valid] is valid
The function [get_approval_and_update_participation_ema] is valid
Lemma get_approval_and_update_participation_ema_is_valid ctxt :
  Raw_context.Valid.t ctxt
  letP? '(ctxt', _) :=
    Amendment.get_approval_and_update_participation_ema ctxt in
  Raw_context.Valid.t ctxt'.
Proof.
  intros H.
  unfold Amendment.get_approval_and_update_participation_ema.
  eapply Error.split_letP; [|intros]. {
    now apply Vote_storage.get_ballots_is_valid.
  }
  eapply Error.split_letP; [|intros]. {
    now apply Vote_storage.get_total_voting_power_free_is_valid.
  }
  eapply Error.split_letP; [|intros]. {
    now apply Vote_storage.get_participation_ema_is_valid.
  }
  eapply Error.split_letP; [|intros]. {
    now apply Vote_storage.get_current_quorum_is_valid.
  }
  eapply Error.split_letP; [|intros]. {
    now apply Vote_storage.clear_ballots_is_valid.
  }
  step.
  eapply Error.split_letP.
  { pose proof
      (approval_and_participation_ema_is_valid x x0 x1 x2)
      as H_approval'.
    repeat match goal with
    | H_approval' : ?T _,
      H : ?T |- _
        specialize (H_approval' H)
    end.
    apply Vote_storage.set_participation_ema_is_valid; [easy|].
    hauto lq:on.
  }
  { hauto lq:on. }
Qed.

The function [start_new_voting_period] is valid
Lemma start_new_voting_period_is_valid ctxt :
  Raw_context.Valid.t ctxt
  letP? ctxt' :=
    Amendment.start_new_voting_period ctxt in
  Raw_context.Valid.t ctxt'.
Proof.
  intros. unfold Amendment.start_new_voting_period.
  eapply Error.split_letP; [|intros]. {
    now apply Voting_period_storage.get_current_kind_is_valid.
  }
  step.
  { eapply Error.split_letP.
    { eapply Error.split_letP; [|intros]. {
        now apply select_winning_proposal_is_valid.
      }
      eapply Error.split_letP; [|intros]. {
        now apply Vote_storage.clear_proposals_is_valid.
      }
      step.
      { eapply Error.split_letP; [|intros]. {
          now apply Vote_storage.init_current_proposal_is_valid.
        }
        now apply Voting_period_storage.succ_is_valid.
      }
      { now apply Voting_period_storage.reset_is_valid. }
    }
    { intros.
      now apply Vote_storage.update_listings_is_valid.
    }
  }
  { eapply Error.split_letP.
    { eapply Error.split_letP.
      { now apply get_approval_and_update_participation_ema_is_valid. }
      { intro. cbn. intros. step. step.
        { now apply Voting_period_storage.succ_is_valid. }
        { apply Voting_period_storage.reset_is_valid.
          now apply Vote_storage.clear_current_proposal_is_valid.
        }
      }
    }
    { intros.
      now eapply Vote_storage.update_listings_is_valid.
    }
  }
  { eapply Error.split_letP; [|intros]. {
      now apply Voting_period_storage.succ_is_valid.
    }
    now apply Vote_storage.update_listings_is_valid.
  }
  { eapply Error.split_letP.
    { eapply Error.split_letP; [|intros]. {
        now apply get_approval_and_update_participation_ema_is_valid.
      }
      do 2 step.
      { now apply Voting_period_storage.succ_is_valid. }
      { unfold Error_monad.op_gtgteq.
        apply Voting_period_storage.reset_is_valid.
        now apply Vote_storage.clear_current_proposal_is_valid.
      }
    }
    { intros.
      now apply Vote_storage.update_listings_is_valid.
    }
  }
  { eapply Error.split_letP.
    { eapply Error.split_letP; [|intros]. {
        now apply Vote_storage.get_current_proposal_is_valid.
      }
      eapply Error.split_letP.
      { apply Voting_period_storage.common_is_valid.
        apply Vote_storage.clear_current_proposal_is_valid.
        now apply Raw_context.activate_is_valid.
      }
      { intros.
        do 2 step.
        apply Voting_period_storage.set_current_is_valid; [easy|].
        now apply Voting_period_repr.raw_reset_is_valid.
      }
    }
    { intros.
      now apply Vote_storage.update_listings_is_valid.
    }
  }
Qed.

The function [may_start_new_voting_period] is valid
Lemma may_start_new_voting_period_is_valid ctxt :
  Raw_context.Valid.t ctxt
  letP? ctxt' :=
    Amendment.may_start_new_voting_period ctxt in
  Raw_context.Valid.t ctxt'.
Proof.
  intros H.
  eapply Error.split_letP; [|intros]. {
     now apply Voting_period_storage.is_last_block_is_valid.
  }
  step.
  { now apply start_new_voting_period_is_valid. }
  { easy. }
Qed.

(* @TODO remove Proofs/Apply_results.v from blacklist *)
The function [apply_proposals] is valid
Lemma apply_proposals_is_valid ctxt chain_id contents :
  Raw_context.Valid.t ctxt
  letP? '(ctxt', contents') :=
    Amendment.apply_proposals ctxt chain_id contents in
  Raw_context.Valid.t ctxt'.
Proof.
Admitted.

(* @TODO remove Proofs/Apply_results.v from blacklist *)
The function [apply_ballot] is valid