LB/PBT: Check an attacker cannot get richer by interacting with CPMM

src/proto_alpha/lib_protocol/test/helpers/liquidity_baking_generator.ml

@@ -266,3 +266,31 @@ let arb_scenario :
     ~shrink:(fun (specs, steps) ->
       QCheck.Iter.pair (QCheck.Iter.return specs) (shrinked_list steps))
     (gen_scenario total_tzbtc total_liquidity size)
+
+let gen_adversary_scenario :
+    tzbtc ->
+    liquidity ->
+    int ->
+    (specs * contract_id * contract_id step list) QCheck.Gen.t =
+ fun total_tzbtc total_liquidity size ->
+  let* specs = gen_specs total_tzbtc total_liquidity in
+  let (state, env) = SymbolicMachine.build ~subsidy:0L specs in
+  let* c = oneofl env.implicit_accounts in
+  let* scenario = gen_steps ~source:c ~destination:c env state size in
+  return (specs, c, scenario)
+
+let arb_adversary_scenario :
+    tzbtc ->
+    liquidity ->
+    int ->
+    (specs * contract_id * contract_id step list) QCheck.arbitrary =
+ fun total_tzbtc total_liquidity size ->
+  QCheck.make
+    ~print:(fun (specs, _, steps) ->
+      Format.asprintf "%a" pp_scenario (specs, steps))
+    ~shrink:(fun (specs, c, steps) ->
+      QCheck.Iter.triple
+        (QCheck.Iter.return specs)
+        (QCheck.Iter.return c)
+        (shrinked_list steps))
+    (gen_adversary_scenario total_tzbtc total_liquidity size)

src/proto_alpha/lib_protocol/test/helpers/liquidity_baking_generator.mli

@@ -31,3 +31,9 @@ val arb_steps :
 
 val arb_scenario :
   tzbtc -> liquidity -> int -> (specs * contract_id step list) QCheck.arbitrary
+
+val arb_adversary_scenario :
+  tzbtc ->
+  liquidity ->
+  int ->
+  (specs * contract_id * contract_id step list) QCheck.arbitrary

src/proto_alpha/lib_protocol/test/liquidity_baking_pbt.ml

@@ -40,6 +40,25 @@ open Liquidity_baking_machine
       replayed against the {! ValidationMachine} to verify the same
       behavior is observed on-chain. *)
 
+let rec run_and_check check scenarios env state =
+  match scenarios with
+  | step :: rst ->
+      let state' = SymbolicMachine.step step env state in
+      assert (check state state') ;
+      run_and_check check rst env state'
+  | [] ->
+      state
+
+let one_balance_decreases c env state state' =
+  let xtz = SymbolicMachine.get_xtz_balance c state in
+  let tzbtc = SymbolicMachine.get_tzbtc_balance c env state in
+  let lqt = SymbolicMachine.get_liquidity_balance c env state in
+  let xtz' = SymbolicMachine.get_xtz_balance c state' in
+  let tzbtc' = SymbolicMachine.get_tzbtc_balance c env state' in
+  let lqt' = SymbolicMachine.get_liquidity_balance c env state' in
+  xtz' < xtz || tzbtc' < tzbtc || lqt' < lqt
+  || (xtz' = xtz && tzbtc' = tzbtc && lqt' = lqt)
+
 let tests =
   [ QCheck.Test.make
       ~count:5
@@ -50,6 +69,19 @@ let tests =
           ( ValidationMachine.build specs
           >>=? fun (state, env) ->
           ValidationMachine.run scenario env state >>=? fun _ -> return_unit ));
+    QCheck.Test.make
+      ~count:100
+      ~name:"arbitrary adversary scenarios"
+      (Liquidity_baking_generator.arb_adversary_scenario
+         1_000_000
+         1_000_000
+         100)
+      (fun (specs, attacker, scenario) ->
+        let (state, env) = SymbolicMachine.build ~subsidy:0L specs in
+        let _ =
+          run_and_check (one_balance_decreases attacker env) scenario env state
+        in
+        true);
     QCheck.Test.make
       ~count:100
       ~name:"liquidity_baking_subsidies"