Merge pull request #58 from freespek/andrey/reverse-reasoning

Monitor specs for Timelock using reverse reasoning

doc/case-studies/timelock/balance_record.tla

@@ -0,0 +1,41 @@
+(*
+ * Balance record effect monitor for the Timelock contract
+ *
+ * Andrey Kuprianov, 2024
+ *)
+---- MODULE balance_record ----
+
+EXTENDS timelock
+
+\* This trigger fires when the balance record is created or destroyed
+\* Notice that it doesn't track the record content
+MonitorTrigger_BalanceRecord_RecordChanged ==
+    instance_has("Balance") /= next_instance_has("Balance")
+
+\* This trigger fires when the balance record content changes
+\* Notice that it will panic (won't fire) if the record doesn't exist
+MonitorTrigger_BalanceRecord_ContentChanged ==
+    Balance /= Balance'
+
+\* Only deposit and claim methods are allowed to alter balances
+MonitorEffect_BalanceRecord_AllowedToChange ==
+    tx.status = TRUE => (
+        \/ tx.method_name = "deposit"
+        \/ tx.method_name = "claim"
+    )
+
+
+\* Everything below is deterministic, and will be generated automatically
+\* For now, we encode this manually
+
+MonitorTrigger_BalanceRecord ==
+    \/ MonitorTrigger_BalanceRecord_RecordChanged
+    \/ MonitorTrigger_BalanceRecord_ContentChanged
+
+MonitorEffect_BalanceRecord == 
+    /\ MonitorEffect_BalanceRecord_AllowedToChange
+
+Monitor_BalanceRecord ==
+    MonitorTrigger_BalanceRecord => MonitorEffect_BalanceRecord
+
+================================================

doc/case-studies/timelock/balance_record_test.tla

@@ -0,0 +1,113 @@
+(*
+ * Tests for the balance record effect monitor of the Timelock contract
+ *
+ * The concrete values will be fetched from blockchain transactions
+ * Here we manually create a few for testing purposes.
+ * 
+ * Andrey Kuprianov, 2024
+ *)
+
+---- MODULE balance_record_test ----
+
+EXTENDS balance_record
+
+\****************************************************************************************
+\*
+\* A monitor test N is validated via running
+\* apalache-mc check --length=1 --init=Init_N --next=Next_N balance_record_test.tla
+\* 
+\****************************************************************************************
+
+\* Success: Record updated by the claim call
+Init_1 == 
+    /\ env = [ current_contract_address |-> "this", ledger_timestamp |-> 10 ]
+    /\ tx = [ method_name |-> "claim", signatures |-> {"bob"}, status |-> TRUE ]
+    /\ instance_storage = { "Balance" }
+    /\ token_balances =  SetAsFun({
+        << "TOK", SetAsFun({ <<"alice", 100>>, <<"bob", 100>>, <<"this", 100>>}) >>
+       })
+    /\ Balance = [
+            token |-> "TOK", 
+            amount |-> 100, 
+            claimants |-> <<"alice", "bob">>,
+            time_bound |-> [kind |-> "Before", timestamp |-> 42]
+        ]
+
+Next_1 ==
+    /\ env' = env
+    /\ tx' = tx
+    /\ instance_storage' = {}
+    /\ token_balances' = SetAsFun({
+        << "TOK", SetAsFun({ <<"alice", 100>>, <<"bob", 200>>, <<"this", 0>>}) >>
+       })
+    /\ Balance' = [
+            token |-> "", 
+            amount |-> 0, 
+            claimants |-> <<>>,
+            time_bound |-> [kind |-> "", timestamp |-> 0]
+        ]
+    /\ Monitor_BalanceRecord
+
+\* Failure: balance record removed by another call
+\* Apalache should report a deadlock!
+Init_2 == 
+    /\ env = [ current_contract_address |-> "this", ledger_timestamp |-> 10 ]
+    /\ tx = [ method_name |-> "withdraw", signatures |-> {"bob"}, status |-> TRUE ]
+    /\ instance_storage = { "Balance" }
+    /\ token_balances =  SetAsFun({
+        << "TOK", SetAsFun({ <<"alice", 100>>, <<"bob", 100>>, <<"this", 100>>}) >>
+       })
+    /\ Balance = [
+            token |-> "TOK", 
+            amount |-> 100, 
+            claimants |-> <<"alice", "bob">>,
+            time_bound |-> [kind |-> "Before", timestamp |-> 42]
+        ]
+
+Next_2 ==
+    /\ env' = env
+    /\ tx' = tx
+    /\ instance_storage' = {}
+    /\ token_balances' = SetAsFun({
+        << "TOK", SetAsFun({ <<"alice", 100>>, <<"bob", 200>>, <<"this", 0>>}) >>
+       })
+    /\ Balance' = [
+            token |-> "", 
+            amount |-> 0, 
+            claimants |-> <<>>,
+            time_bound |-> [kind |-> "", timestamp |-> 0]
+        ]
+    /\ Monitor_BalanceRecord
+
+\* Failure: balance record changed by another call
+\* Apalache should report a deadlock!
+Init_3 == 
+    /\ env = [ current_contract_address |-> "this", ledger_timestamp |-> 10 ]
+    /\ tx = [ method_name |-> "claim_part", signatures |-> {"bob"}, status |-> TRUE ]
+    /\ instance_storage = { "Balance" }
+    /\ token_balances =  SetAsFun({
+        << "TOK", SetAsFun({ <<"alice", 100>>, <<"bob", 100>>, <<"this", 100>>}) >>
+       })
+    /\ Balance = [
+            token |-> "TOK", 
+            amount |-> 100, 
+            claimants |-> <<"alice", "bob">>,
+            time_bound |-> [kind |-> "Before", timestamp |-> 42]
+        ]
+
+Next_3 ==
+    /\ env' = env
+    /\ tx' = tx
+    /\ instance_storage' = { "Balance" }
+    /\ token_balances' = SetAsFun({
+        << "TOK", SetAsFun({ <<"alice", 100>>, <<"bob", 150>>, <<"this", 50>>}) >>
+       })
+    /\ Balance' = [
+            token |-> "TOK", 
+            amount |-> 50, 
+            claimants |-> <<"alice", "bob">>,
+            time_bound |-> [kind |-> "Before", timestamp |-> 42]
+        ]
+    /\ Monitor_BalanceRecord
+
+================================================

doc/case-studies/timelock/claim.tla

@@ -0,0 +1,108 @@
+(*
+ * Claim method monitors for the Timelock contract
+ *
+ * Andrey Kuprianov, 2024
+ *)
+---- MODULE claim ----
+
+EXTENDS timelock
+
+(*
+    @typeAlias: claimArgs = { 
+        claimant: $address
+    };
+*)
+claim_typedefs == TRUE
+
+
+\* @type: ($claimArgs) => Bool;
+MustFail_claim_Unauthorized(args) == 
+    ~authorized(args.claimant)
+
+MustFail_claim_NoBalanceRecord(args) == 
+    ~instance_has("Balance")
+
+\* @type: ($claimArgs) => Bool;
+MustFail_claim_NotClaimant(args) == 
+    \A i \in DOMAIN Balance.claimants: 
+        Balance.claimants[i] /= args.claimant
+
+\* One success condition: correctly claimed before time bound
+MustPass_claim_BeforeTimeBound(args) ==
+    /\ Balance.time_bound.kind = "Before" 
+    /\ env.ledger_timestamp <= Balance.time_bound.timestamp
+
+\* Another success condition: correctly claimed after time bound
+MustPass_claim_AfterTimeBound(args) ==
+    /\ Balance.time_bound.kind = "After" 
+    /\ env.ledger_timestamp >= Balance.time_bound.timestamp
+
+\* @type: ($claimArgs) => Bool;
+MustHold_claim_TokenTransferred(args) ==
+    token_transferred(
+        Balance.token, env.current_contract_address, args.claimant, Balance.amount)
+
+MustHold_claim_BalanceRecordRemoved(args) ==
+    ~next_instance_has("Balance")
+
+
+
+\* Everything below is deterministic, and will be generated automatically
+\* For now, we encode this manually
+
+\* Auxiliary predicate describing the failure condition
+\* (formed as a disjunction of all "MustFail" predicates)
+MustFail_claim(args) ==
+    \/ MustFail_claim_NoBalanceRecord(args)
+    \/ MustFail_claim_NotClaimant(args)
+    \* Checking of the condition(s) below is not yet supported 
+    \* \/ MustFail_claim_Unauthorized(args)
+
+\* Auxiliary predicate describing the success condition
+\* (formed as a disjunction of all "MustPass" predicates)
+MustPass_claim(args) ==
+    \/ MustPass_claim_BeforeTimeBound(args)
+    \/ MustPass_claim_AfterTimeBound(args)
+
+\* Auxiliary predicate describing the effect
+\* (formed as a conjunction of all "MustHold" predicates)
+MustHold_claim(args) ==
+    /\ MustHold_claim_BalanceRecordRemoved(args)
+    \* Checking of the condition(s) below is not yet supported 
+    \* /\ MustHold_claim_TokenTransferred(args)
+
+
+\* Monitor invariants to be checked
+\* (encode the expected interpretation of monitor predicates)
+Inv_MustFail_claim(args) ==
+    (   /\ tx.method_name = "claim" 
+        /\ MustFail_claim(args)
+    )   => tx.status = FALSE
+
+Inv_MustPass_claim(args) ==
+    (   /\ tx.method_name = "claim" 
+        /\ ~MustFail_claim(args)
+        /\ MustPass_claim(args)
+    )   => tx.status = TRUE
+
+Inv_MustHold_claim(args) ==
+    (   /\ tx.method_name = "claim"
+        /\ tx.status = TRUE
+    )   => MustHold_claim(args)
+
+
+\* The main invariant
+\* (formed as a conjunction of all auxiliary invariants)
+\* @type: ($claimArgs) => Bool;
+Inv_claim(args) ==
+    /\ Inv_MustFail_claim(args)
+    /\ Inv_MustPass_claim(args)
+    /\ Inv_MustHold_claim(args)
+
+claim(claimant) ==
+    LET args == [ 
+        claimant |-> claimant
+    ] IN 
+    Inv_claim(args)
+
+================================================

doc/case-studies/timelock/claim_test.tla

@@ -0,0 +1,99 @@
+(*
+ * Tests for the claim method of the Timelock contract
+ *
+ * The concrete values will be fetched from blockchain transactions
+ * Here we manually create a few for testing purposes.
+ * 
+ * Andrey Kuprianov, 2024
+ *)
+
+---- MODULE claim_test ----
+
+EXTENDS claim
+
+\****************************************************************************************
+\*
+\* A monitor test N is validated via running
+\* apalache-mc check --length=1 --init=Init_N --next=Next_N claim_test.tla
+\* 
+\****************************************************************************************
+
+\* Successful claim call
+Init_1 == 
+    /\ env = [ current_contract_address |-> "this", ledger_timestamp |-> 10 ]
+    /\ tx = [ method_name |-> "claim", signatures |-> {"bob"}, status |-> TRUE ]
+    /\ instance_storage = { "Balance" }
+    /\ token_balances =  SetAsFun({
+        << "TOK", SetAsFun({ <<"alice", 100>>, <<"bob", 100>>, <<"this", 100>>}) >>
+       })
+    /\ Balance = [
+            token |-> "TOK", 
+            amount |-> 100, 
+            claimants |-> <<"alice", "bob">>,
+            time_bound |-> [kind |-> "Before", timestamp |-> 42]
+        ]
+
+Next_1 ==
+    /\ env' = env
+    /\ tx' = tx
+    /\ instance_storage' = {}
+    /\ token_balances' = SetAsFun({
+        << "TOK", SetAsFun({ <<"alice", 100>>, <<"bob", 200>>, <<"this", 0>>}) >>
+       })
+    /\ Balance' = [
+            token |-> "", 
+            amount |-> 0, 
+            claimants |-> <<>>,
+            time_bound |-> [kind |-> "", timestamp |-> 0]
+        ]
+    /\ claim("bob")
+
+
+\* Failing claim call: no balance record
+Init_2 == 
+    /\ env = [ current_contract_address |-> "this", ledger_timestamp |-> 10 ]
+    /\ tx = [ method_name |-> "claim", signatures |-> {"bob"}, status |-> FALSE ]
+    /\ instance_storage = { }
+    /\ token_balances =  SetAsFun({
+        << "TOK", SetAsFun({ <<"alice", 100>>, <<"bob", 100>>, <<"this", 100>>}) >>
+       })
+    /\ Balance = [
+            token |-> "TOK", 
+            amount |-> 100, 
+            claimants |-> <<"alice", "bob">>,
+            time_bound |-> [kind |-> "Before", timestamp |-> 42]
+        ]
+
+Next_2 ==
+    /\ env' = env
+    /\ tx' = tx
+    /\ instance_storage' = instance_storage
+    /\ token_balances' = token_balances
+    /\ Balance' = Balance
+    /\ claim("bob")
+
+
+\* Failing claim call: not a claimant
+Init_3 == 
+    /\ env = [ current_contract_address |-> "this", ledger_timestamp |-> 10 ]
+    /\ tx = [ method_name |-> "claim", signatures |-> {"bob"}, status |-> FALSE ]
+    /\ instance_storage = { "Balance" }
+    /\ token_balances =  SetAsFun({
+        << "TOK", SetAsFun({ <<"alice", 100>>, <<"bob", 100>>, <<"this", 100>>}) >>
+       })
+    /\ Balance = [
+            token |-> "TOK", 
+            amount |-> 100, 
+            claimants |-> <<"alice", "bob">>,
+            time_bound |-> [kind |-> "Before", timestamp |-> 42]
+        ]
+
+Next_3 ==
+    /\ env' = env
+    /\ tx' = tx
+    /\ instance_storage' = instance_storage
+    /\ token_balances' = token_balances
+    /\ Balance' = Balance
+    /\ claim("carol")
+
+================================================