Library ConCert.Examples.Congress.tests.Congress_BuggyTests

From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import Containers.
From ConCert.Execution Require Import Serializable.
From ConCert.Execution Require Import ResultMonad.
From ConCert.Execution Require Import Monad.
#[warnings="-notation-incompatible-prefix"]
From ConCert.Execution.Test Require Import QCTest.
From ConCert.Examples.Congress Require Import Congress_Buggy.
From ConCert.Examples.Congress Require Export Congress_BuggyGens.
From ConCert.Examples.Congress Require Export Congress_BuggyPrinters.
From ConCert.Utils Require Import Extras.

From Coq Require Import ZArith.
From Coq Require Import List.
Import ListNotations.

(* -------------------------- Tests of the Buggy Congress Implementation -------------------------- *)

Definition creator := addr_of_Z 10.

Definition rules := {|
  min_vote_count_permille := 200;
  margin_needed_permille := 501;
  debating_period_in_blocks := 0;
|}.

Definition exploit_example : option (Address * ChainBuilder) :=
  let chain := builder_initial in
  let add_block (chain : ChainBuilder) act_bodies :=
      let next_header :=
          {| block_height := S (chain_height chain);
             block_slot := S (current_slot chain);
             block_finalized_height := finalized_height chain;
             block_creator := creator;
             block_reward := 50; |} in
      let acts := map (build_act creator creator) act_bodies in
      option_of_result (builder_add_block chain next_header acts) in
  (* Get some money on the creator *)
  (* Deploy congress and exploit contracts *)
  do chain <- add_block chain [];
  let dep_congress := create_deployment 50 contract {| setup_rules := rules |} in
  let dep_exploit := create_deployment 0 exploit_contract tt in
  do chain <- add_block chain [dep_congress; dep_exploit];
  let exploit := addr_of_N 129%N in
  let congress := addr_of_N 128%N in
  (* Add creator to congress *)
  let add_creator := add_member creator in
  let act_bodies :=
      map (fun m => act_call congress 0 (serialize _ _ m))
          [add_creator] in
  do chain <- add_block chain act_bodies;
  Some (congress, chain).

Definition unpacked_exploit_example : Address * ChainBuilder :=
  unpack_option exploit_example.

Definition congress_caddr := addr_of_Z 128%Z.

Module NotationInfo <: TestNotationParameters.
  Definition gAction := (fun env => GCongressAction env act_depth congress_caddr).
  Definition init_cb := (snd unpacked_exploit_example).
End NotationInfo.
Module TN := TestNotations NotationInfo. Import TN.
(* Sample gChain. *)

(* Definition gCongressChain max_acts_per_block congress_cb max_length :=
  let act_depth := 2 in
  gChain congress_cb
    (fun env act_depth => GCongressAction env act_depth congress_caddr) max_length act_depth max_acts_per_block.

Definition forAllCongressChainTraces n :=
  forAllBlocks n (snd unpacked_exploit_example) (gCongressChain 2).

Definition pre_post_assertion_congress P c Q :=
  pre_post_assertion 2 (snd unpacked_exploit_example) (gCongressChain 1) Congress_Buggy.contract c P Q.
Notation "{{ P }} c {{ Q }}" := (pre_post_assertion_congress P c Q) (at level 50). *)

Local Close Scope Z_scope.

Definition num_cacts_in_state state :=
  sumnat (fun '(k, v) => length (actions v)) (FMap.elements (proposals state)).

Definition num_cacts_safe_P (msg : Congress_Buggy.Msg)
                            (resp_acts : list ActionBody)
                            (old_state : Congress_Buggy.State)
                            (new_state : Congress_Buggy.State) :=
  let nr_cacts := match msg with
                  | create_proposal ls => length ls
                  | _ => 0
                  end in
  (num_cacts_in_state new_state + length resp_acts <=?
  num_cacts_in_state old_state + nr_cacts)%nat.

Definition receive_state_well_behaved_P (chain : Chain)
                                        (cctx : ContractCallContext)
                                        (old_state : Congress_Buggy.State)
                                        (msg : Congress_Buggy.Msg)
                                        (result : option (Congress_Buggy.State * list ActionBody)) :=
  match result with
  | Some (new_state, resp_acts) =>
    checker (num_cacts_safe_P msg resp_acts old_state new_state)
  | _ => checker false
  end.

(* QuickChick (
  {{fun _ _ => true}}
  congress_caddr
  {{receive_state_well_behaved_P}}
). *)

(*
Chain{|
Block 1 ;
Block 2  Action{act_from: 10%256, act_body: (act_deploy 50, <FAILED DESERIALIZATION>)}; Action{act_from: 10%256, act_body: (act_deploy 0, <FAILED DESERIALIZATION>)};
Block 3  Action{act_from: 10%256, act_body: (act_call 128%256, 0, add_member 10%256)};
Block 4  Action{act_from: 10%256, act_body: (act_call 128%256, 79, create_proposal (call: 128%256, 80, add_member 0%256))};
Block 5  Action{act_from: 10%256, act_body: (act_call 128%256, 13, finish_proposal 1)}; |}

*** Failed after 33 tests and 0 shrinks. (0 discards)
*)