DEVX-564

docs/src/guide/index.md

@@ -16,6 +16,7 @@ The following guides are available:
 + @{seclink("guide-ctransfers")}
 + @{seclink("guide-assert")}
 + @{seclink("guide-loop-invs")}
++ @{seclink("guide-invariants")}
 + @{seclink("guide-timeout")}
 + @{seclink("guide-determ")}
 + @{seclink("guide-race")}

docs/src/guide/invariants/config.json

@@ -0,0 +1 @@
+{ "bookRank": 95 }

docs/xrefs.json

@@ -775,6 +775,10 @@
     "title": "Install VSCode",
     "path": "/guide/editor-support/#guide-install-VSCode"
   },
+  "guide-invariants": {
+    "title": "Writing Invariants",
+    "path": "/guide/invariants/#guide-invariants"
+  },
   "guide-lifecycle": {
     "title": "Contract Development Lifecycle and Best Practices for Building Reach DApps",
     "path": "/guide/lifecycle/#guide-lifecycle"

examples/point-of-sale/index-balinv.rsh

@@ -0,0 +1,58 @@
+'reach 0.1';
+
+export const main = Reach.App(() => {
+  const A = Participant('Admin', {
+    params: Object({
+      min: UInt,
+      tok: Token,
+      supply: UInt,
+    }),
+    launched: Fun([Contract], Null),
+  });
+  const B = API('Buyer', {
+    purchase: Fun([UInt], UInt),
+    refund: Fun([], UInt),
+  });
+  init();
+
+  A.only(() => {
+   const {min, tok, supply} = declassify(interact.params);
+  });
+  A.publish(min, tok, supply);
+  commit();
+  A.pay([[supply, tok]])
+  A.interact.launched(getContract());
+
+  const pMap = new Map(UInt);
+  const [tokensSold, total] = parallelReduce([0, 0])
+    .paySpec([tok])
+    .invariant(pMap.sum() == total, "tracking total wrong")
+    .invariant(balance(tok) == supply - tokensSold, "non-network token balance wrong")
+    .while(tokensSold < supply)
+    .api_(B.purchase, (purchasePrice) => {
+      check(tokensSold != supply, "sorry, out of tickets");
+      check(isNone(pMap[this]), "sorry, you are already in this list");
+      check(purchasePrice >= min, "sorry, amount too low");
+      return[[purchasePrice, [0, tok]], (ret) => {
+        pMap[this] = purchasePrice;
+        const sold = tokensSold + 1;
+        transfer(1, tok).to(this);
+        ret(sold);
+        return [sold, total + purchasePrice];
+      }];
+    })
+    .api_(B.refund, () => {
+      check(isSome(pMap[this]), "sorry, you are not in the list");
+      return[[0, [1, tok]], (ret) => {
+        const paid = fromSome(pMap[this], 0);
+        transfer(paid).to(this);
+        ret(paid);
+        delete pMap[this];
+        return[tokensSold - 1, total - paid]
+      }];
+    });
+  transfer(total).to(A);
+  commit();
+  exit();
+});
+

examples/point-of-sale/index-balinv.txt

@@ -0,0 +1,80 @@
+Verifying knowledge assertions
+Verifying for generic connector
+  Verifying when ALL participants are honest
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance sufficient for transfer"
+  at ./index-balinv.rsh:48:26:application
+  at /app/index-balinv.rsh:46:35:application call to [unknown function] (defined at: /app/index-balinv.rsh:46:35:function exp)
+
+  // Violation Witness
+
+  const UInt.max = 33037;
+
+  const map0_1/981 = <fresh Map>;
+  //    ^ could = <map: (Some(8026 ))>[<abstract address 0> <- None(null )]
+  //      from: ./index-balinv.rsh:27:45:while
+  const netBalance/679 = <loop variable>;
+  //    ^ could = 8025
+  //      from: ./index-balinv.rsh:27:45:while
+  const this/760 = <an honest join from "Buyer_refund">;
+  //    ^ could = <abstract address 1>
+  //      from: ./index-balinv.rsh:27:45:dot
+
+  // Theorem Formalization
+
+  const v945 = fromSome(map0_1/981[this/760], 0 ) <= netBalance/679;
+  //    ^ would be false
+  assert(v945);
+
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance sufficient for transfer"
+  at ./index-balinv.rsh:54:21:application
+
+  // Violation Witness
+
+  const UInt.max = 1;
+
+  const total/671 = <loop variable>;
+  //    ^ could = 1
+  //      from: ./index-balinv.rsh:27:45:while
+  const netBalance/679 = <loop variable>;
+  //    ^ could = 0
+  //      from: ./index-balinv.rsh:27:45:while
+
+  // Theorem Formalization
+
+  const v957 = total/671 <= netBalance/679;
+  //    ^ would be false
+  assert(v957);
+
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance zero at application exit"
+  at ./index-balinv.rsh:56:7:application
+
+  // Violation Witness
+
+  const UInt.max = 1;
+
+  const total/671 = <loop variable>;
+  //    ^ could = 0
+  //      from: ./index-balinv.rsh:27:45:while
+  const netBalance/679 = <loop variable>;
+  //    ^ could = 1
+  //      from: ./index-balinv.rsh:27:45:while
+
+  // Theorem Formalization
+
+  const v961 = 0 == (netBalance/679 - total/671);
+  //    ^ would be false
+  assert(v961);
+
+  Verifying when NO participants are honest
+Checked 68 theorems; 7 failures (and 4 omitted repeats) :'(
+
+For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures

examples/point-of-sale/index-mapinv.rsh

@@ -0,0 +1,58 @@
+'reach 0.1';
+
+export const main = Reach.App(() => {
+  const A = Participant('Admin', {
+    params: Object({
+      min: UInt,
+      tok: Token,
+      supply: UInt,
+    }),
+    launched: Fun([Contract], Null),
+  });
+  const B = API('Buyer', {
+    purchase: Fun([UInt], UInt),
+    refund: Fun([], UInt),
+  });
+  init();
+
+  A.only(() => {
+   const {min, tok, supply} = declassify(interact.params);
+  });
+  A.publish(min, tok, supply);
+  commit();
+  A.pay([[supply, tok]])
+  A.interact.launched(getContract());
+
+  const pMap = new Map(UInt);
+  const [tokensSold, total] = parallelReduce([0, 0])
+    .paySpec([tok])
+    .invariant(balance() == total, "network token balance wrong")
+    .invariant(balance(tok) == supply - tokensSold, "non-network token balance wrong")
+    .while(tokensSold < supply)
+    .api_(B.purchase, (purchasePrice) => {
+      check(tokensSold != supply, "sorry, out of tickets");
+      check(isNone(pMap[this]), "sorry, you are already in this list");
+      check(purchasePrice >= min, "sorry, amount too low");
+      return[[purchasePrice, [0, tok]], (ret) => {
+        pMap[this] = purchasePrice;
+        const sold = tokensSold + 1;
+        transfer(1, tok).to(this);
+        ret(sold);
+        return [sold, total + purchasePrice];
+      }];
+    })
+    .api_(B.refund, () => {
+      check(isSome(pMap[this]), "sorry, you are not in the list");
+      return[[0, [1, tok]], (ret) => {
+        const paid = fromSome(pMap[this], 0);
+        transfer(paid).to(this);
+        ret(paid);
+        delete pMap[this];
+        return[tokensSold - 1, total - paid]
+      }];
+    });
+  transfer(total).to(A);
+  commit();
+  exit();
+});
+

examples/point-of-sale/index-mapinv.txt

@@ -0,0 +1,34 @@
+Verifying knowledge assertions
+Verifying for generic connector
+  Verifying when ALL participants are honest
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance sufficient for transfer"
+  at ./index-mapinv.rsh:48:26:application
+  at /app/index-mapinv.rsh:46:35:application call to [unknown function] (defined at: /app/index-mapinv.rsh:46:35:function exp)
+
+  // Violation Witness
+
+  const UInt.max = 33037;
+
+  const map0_1/961 = <fresh Map>;
+  //    ^ could = <map: (None(null ))>[<abstract address 1> <- Some(30613 )]
+  //      from: ./index-mapinv.rsh:27:45:while
+  const netBalance/665 = <loop variable>;
+  //    ^ could = 30612
+  //      from: ./index-mapinv.rsh:27:45:while
+  const this/740 = <an honest join from "Buyer_refund">;
+  //    ^ could = <abstract address 1>
+  //      from: ./index-mapinv.rsh:27:45:dot
+
+  // Theorem Formalization
+
+  const v925 = fromSome(map0_1/961[this/740], 0 ) <= netBalance/665;
+  //    ^ would be false
+  assert(v925);
+
+  Verifying when NO participants are honest
+Checked 68 theorems; 3 failures (and 2 omitted repeats) :'(
+
+For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures

examples/point-of-sale/index-tokinv.rsh

@@ -0,0 +1,58 @@
+'reach 0.1';
+
+export const main = Reach.App(() => {
+  const A = Participant('Admin', {
+    params: Object({
+      min: UInt,
+      tok: Token,
+      supply: UInt,
+    }),
+    launched: Fun([Contract], Null),
+  });
+  const B = API('Buyer', {
+    purchase: Fun([UInt], UInt),
+    refund: Fun([], UInt),
+  });
+  init();
+
+  A.only(() => {
+   const {min, tok, supply} = declassify(interact.params);
+  });
+  A.publish(min, tok, supply);
+  commit();
+  A.pay([[supply, tok]])
+  A.interact.launched(getContract());
+
+  const pMap = new Map(UInt);
+  const [tokensSold, total] = parallelReduce([0, 0])
+    .paySpec([tok])
+    .invariant(pMap.sum() == total, "tracking total wrong")
+    .invariant(balance() == total, "network token balance wrong")
+    .while(tokensSold < supply)
+    .api_(B.purchase, (purchasePrice) => {
+      check(tokensSold != supply, "sorry, out of tickets");
+      check(isNone(pMap[this]), "sorry, you are already in this list");
+      check(purchasePrice >= min, "sorry, amount too low");
+      return[[purchasePrice, [0, tok]], (ret) => {
+        pMap[this] = purchasePrice;
+        const sold = tokensSold + 1;
+        transfer(1, tok).to(this);
+        ret(sold);
+        return [sold, total + purchasePrice];
+      }];
+    })
+    .api_(B.refund, () => {
+      check(isSome(pMap[this]), "sorry, you are not in the list");
+      return[[0, [1, tok]], (ret) => {
+        const paid = fromSome(pMap[this], 0);
+        transfer(paid).to(this);
+        ret(paid);
+        delete pMap[this];
+        return[tokensSold - 1, total - paid]
+      }];
+    });
+  transfer(total).to(A);
+  commit();
+  exit();
+});
+

examples/point-of-sale/index-tokinv.txt

@@ -0,0 +1,48 @@
+Verifying knowledge assertions
+Verifying for generic connector
+  Verifying when ALL participants are honest
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance sufficient for transfer"
+  at ./index-tokinv.rsh:39:28:application
+  at /app/index-tokinv.rsh:36:47:application call to [unknown function] (defined at: /app/index-tokinv.rsh:36:47:function exp)
+
+  // Violation Witness
+
+  const UInt.max = 73349;
+
+  const tokenInfos/676 = <loop variable>;
+  //    ^ could = Array.const(Tuple(UInt, UInt, Bool), [0, 8855, false ] )
+  //      from: ./index-tokinv.rsh:27:45:while
+
+  // Theorem Formalization
+
+  const v822 = 1 <= tokenInfos/676[0][0];
+  //    ^ would be false
+  assert(v822);
+
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance zero at application exit"
+  at ./index-tokinv.rsh:56:7:application
+
+  // Violation Witness
+
+  const UInt.max = 1;
+
+  const tokenInfos/676 = <loop variable>;
+  //    ^ could = Array.const(Tuple(UInt, UInt, Bool), [1, 11797, false ] )
+  //      from: ./index-tokinv.rsh:27:45:while
+
+  // Theorem Formalization
+
+  const v960 = 0 == tokenInfos/676[0][0];
+  //    ^ would be false
+  assert(v960);
+
+  Verifying when NO participants are honest
+Checked 68 theorems; 5 failures (and 3 omitted repeats) :'(
+
+For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures