From c600f036823666def78d8d67bc44a9e3436dc1e3 Mon Sep 17 00:00:00 2001 From: TheChronicMonster Date: Mon, 17 Oct 2022 09:48:12 -0500 Subject: [PATCH 01/11] feat: invariants guide --- docs/gen.log | 1062 +++++++++++++++++++++++++ docs/gen/package-lock.json | 2 +- docs/src/guide/index.md | 1 + docs/src/guide/invariants/config.json | 1 + docs/src/guide/invariants/index.md | 330 ++++++++ docs/xrefs.json | 4 + 6 files changed, 1399 insertions(+), 1 deletion(-) create mode 100644 docs/gen.log create mode 100644 docs/src/guide/invariants/config.json create mode 100644 docs/src/guide/invariants/index.md diff --git a/docs/gen.log b/docs/gen.log new file mode 100644 index 0000000000..d45a8bf6d5 --- /dev/null +++ b/docs/gen.log @@ -0,0 +1,1062 @@ +[ + { + "here": "", + "title": "Reach", + "isBook": true, + "rank": 0 + }, + { + "here": "cout", + "title": "Compiled Output", + "isBook": false, + "rank": 60 + }, + { + "here": "changelog", + "title": "Changelog", + "isBook": false, + "rank": 120 + }, + { + "here": "model", + "title": "Model", + "isBook": false, + "rank": 30 + }, + { + "here": "quickstart", + "title": "Quickstart", + "isBook": false, + "rank": 10 + }, + { + "here": "build", + "title": "Reach is for Builders", + "isBook": false, + "rank": 5 + }, + { + "here": "networks", + "title": "Networks", + "isBook": false, + "rank": 80 + }, + { + "here": "frontend", + "title": "Frontends", + "isBook": false, + "rank": 70 + }, + { + "here": "rsh", + "title": "Language", + "isBook": false, + "rank": 50 + }, + { + "here": "tool", + "title": "Tool", + "isBook": false, + "rank": 40 + }, + { + "here": "index", + "title": "Index", + "isBook": false, + "rank": 140 + }, + { + "here": "search", + "title": "Search", + "isBook": false, + "rank": 130 + }, + { + "here": "tut", + "title": "Tutorials", + "isBook": false, + "rank": 20 + }, + { + "here": "trouble", + "title": "Troubleshooting", + "isBook": false, + "rank": 115 + }, + { + "here": "rpc", + "title": "RPC Server", + "isBook": true, + "rank": 90 + }, + { + "here": "workshop", + "title": "Workshops", + "isBook": true, + "rank": 100 + }, + { + "here": "guide", + "title": "Guide", + "isBook": true, + "rank": 110 + }, + { + "here": "rsh/compute", + "title": "Computations", + "isBook": false, + "rank": 60 + }, + { + "here": "rsh/consensus", + "title": "Consensus Steps", + "isBook": false, + "rank": 50 + }, + { + "here": "rsh/appinit", + "title": "Application Initialization", + "isBook": false, + "rank": 20 + }, + { + "here": "rsh/local", + "title": "Local Steps", + "isBook": false, + "rank": 40 + }, + { + "here": "rsh/errors", + "title": "Error Codes", + "isBook": false, + "rank": 70 + }, + { + "here": "rsh/step", + "title": "Steps", + "isBook": false, + "rank": 30 + }, + { + "here": "tut/wfs", + "title": "Wisdom For Sale", + "isBook": false, + "rank": 18 + }, + { + "here": "rsh/module", + "title": "Modules", + "isBook": false, + "rank": 10 + }, + { + "here": "tut/overview", + "title": "Overview", + "isBook": false, + "rank": 10 + }, + { + "here": "tut/rps", + "title": "Rock, Paper, Scissors!", + "isBook": false, + "rank": 20 + }, + { + "here": "tut/rsvp", + "title": "Répondez S'il Vous Plaît", + "isBook": false, + "rank": 30 + }, + { + "here": "rpc/proto", + "title": "Specification", + "isBook": false, + "rank": 50 + }, + { + "here": "rpc/py", + "title": "Python", + "isBook": false, + "rank": 40 + }, + { + "here": "rpc/client", + "title": "Client Walkthrough", + "isBook": false, + "rank": 60 + }, + { + "here": "rpc/go", + "title": "Go", + "isBook": false, + "rank": 20 + }, + { + "here": "rpc/js", + "title": "JavaScript", + "isBook": false, + "rank": 30 + }, + { + "here": "workshop/relay", + "title": "Relay Account", + "isBook": false, + "rank": 20 + }, + { + "here": "workshop/fomo", + "title": "Fear of Missing Out", + "isBook": false, + "rank": 40 + }, + { + "here": "rpc/cs", + "title": "C#", + "isBook": false, + "rank": 10 + }, + { + "here": "guide/invariants", + "title": "Writing Invariants", + "isBook": false, + "rank": 95 + }, + { + "here": "guide/ctransfers", + "title": "What do the different kinds of consensus transfers mean? publish, pay, race, fork, parallelReduce?", + "isBook": false, + "rank": 70 + }, + { + "here": "workshop/trust-fund", + "title": "Trust Fund", + "isBook": false, + "rank": 30 + }, + { + "here": "guide/assert", + "title": "How and what to verify", + "isBook": false, + "rank": 80 + }, + { + "here": "workshop/fomo-generalized", + "title": "Fear of Missing Out+", + "isBook": false, + "rank": 50 + }, + { + "here": "guide/lifecycle", + "title": "Contract Development Lifecycle and Best Practices for Building Reach DApps", + "isBook": false, + "rank": 35 + }, + { + "here": "guide/determ", + "title": "Determinism, simultaneity, and choice in decentralized applications", + "isBook": false, + "rank": 110 + }, + { + "here": "guide/limits", + "title": "What are Reach's limitations?", + "isBook": false, + "rank": 180 + }, + { + "here": "guide/abstract", + "title": "Building decentralized abstractions", + "isBook": false, + "rank": 130 + }, + { + "here": "guide/ganache", + "title": "How to use Ganache with Reach", + "isBook": false, + "rank": 140 + }, + { + "here": "guide/race", + "title": "Racing non-determinism in decentralized applications", + "isBook": false, + "rank": 120 + }, + { + "here": "guide/windows", + "title": "Using Reach on Windows", + "isBook": false, + "rank": 10 + }, + { + "here": "guide/reach", + "title": "How does Reach work?", + "isBook": false, + "rank": 170 + }, + { + "here": "guide/roadmap", + "title": "Reach's Roadmap", + "isBook": false, + "rank": 190 + }, + { + "here": "guide/solidity", + "title": "How does Reach development compare to Solidity development?", + "isBook": false, + "rank": 30 + }, + { + "here": "guide/staking", + "title": "Example: Staking and Unstaking Tokens", + "isBook": false, + "rank": 135 + }, + { + "here": "guide/packages", + "title": "Sharing and discovering shared Reach packages", + "isBook": false, + "rank": 160 + }, + { + "here": "guide/rpc", + "title": "Do I have to use JavaScript to write my frontend? What about Python, Go, or other languages?", + "isBook": false, + "rank": 40 + }, + { + "here": "guide/loop-invs", + "title": "Finding and using loop invariants", + "isBook": false, + "rank": 90 + }, + { + "here": "guide/nntoks", + "title": "How do network and non-network tokens differ?", + "isBook": false, + "rank": 60 + }, + { + "here": "guide/testing", + "title": "How should I test a DApp?", + "isBook": false, + "rank": 51 + }, + { + "here": "guide/logging", + "title": "How do I add tracing logs to my Reach program?", + "isBook": false, + "rank": 50 + }, + { + "here": "guide/timeout", + "title": "Non-participation: What it is and how to protect against it", + "isBook": false, + "rank": 100 + }, + { + "here": "guide/editor-support", + "title": "IDE/Text Editor Support", + "isBook": false, + "rank": 150 + }, + { + "here": "guide/versions", + "title": "How does Reach use version numbers?", + "isBook": false, + "rank": 20 + }, + { + "here": "workshop/hash-lock", + "title": "Hash Lock", + "isBook": false, + "rank": 10 + }, + { + "here": "tut/rps/7-rpc", + "title": "Rock, Paper, Scissors in Python", + "isBook": false, + "rank": 10 + } +] +{ + "path": [], + "children": { + "cout": { + "path": [ + "cout" + ], + "children": {}, + "here": "cout", + "title": "Compiled Output", + "isBook": false, + "rank": 60 + }, + "changelog": { + "path": [ + "changelog" + ], + "children": {}, + "here": "changelog", + "title": "Changelog", + "isBook": false, + "rank": 120 + }, + "model": { + "path": [ + "model" + ], + "children": {}, + "here": "model", + "title": "Model", + "isBook": false, + "rank": 30 + }, + "quickstart": { + "path": [ + "quickstart" + ], + "children": {}, + "here": "quickstart", + "title": "Quickstart", + "isBook": false, + "rank": 10 + }, + "build": { + "path": [ + "build" + ], + "children": {}, + "here": "build", + "title": "Reach is for Builders", + "isBook": false, + "rank": 5 + }, + "networks": { + "path": [ + "networks" + ], + "children": {}, + "here": "networks", + "title": "Networks", + "isBook": false, + "rank": 80 + }, + "frontend": { + "path": [ + "frontend" + ], + "children": {}, + "here": "frontend", + "title": "Frontends", + "isBook": false, + "rank": 70 + }, + "rsh": { + "path": [ + "rsh" + ], + "children": { + "compute": { + "path": [ + "rsh", + "compute" + ], + "children": {}, + "here": "rsh/compute", + "title": "Computations", + "isBook": false, + "rank": 60 + }, + "consensus": { + "path": [ + "rsh", + "consensus" + ], + "children": {}, + "here": "rsh/consensus", + "title": "Consensus Steps", + "isBook": false, + "rank": 50 + }, + "appinit": { + "path": [ + "rsh", + "appinit" + ], + "children": {}, + "here": "rsh/appinit", + "title": "Application Initialization", + "isBook": false, + "rank": 20 + }, + "local": { + "path": [ + "rsh", + "local" + ], + "children": {}, + "here": "rsh/local", + "title": "Local Steps", + "isBook": false, + "rank": 40 + }, + "errors": { + "path": [ + "rsh", + "errors" + ], + "children": {}, + "here": "rsh/errors", + "title": "Error Codes", + "isBook": false, + "rank": 70 + }, + "step": { + "path": [ + "rsh", + "step" + ], + "children": {}, + "here": "rsh/step", + "title": "Steps", + "isBook": false, + "rank": 30 + }, + "module": { + "path": [ + "rsh", + "module" + ], + "children": {}, + "here": "rsh/module", + "title": "Modules", + "isBook": false, + "rank": 10 + } + }, + "here": "rsh", + "title": "Language", + "isBook": false, + "rank": 50 + }, + "tool": { + "path": [ + "tool" + ], + "children": {}, + "here": "tool", + "title": "Tool", + "isBook": false, + "rank": 40 + }, + "index": { + "path": [ + "index" + ], + "children": {}, + "here": "index", + "title": "Index", + "isBook": false, + "rank": 140 + }, + "search": { + "path": [ + "search" + ], + "children": {}, + "here": "search", + "title": "Search", + "isBook": false, + "rank": 130 + }, + "tut": { + "path": [ + "tut" + ], + "children": { + "wfs": { + "path": [ + "tut", + "wfs" + ], + "children": {}, + "here": "tut/wfs", + "title": "Wisdom For Sale", + "isBook": false, + "rank": 18 + }, + "overview": { + "path": [ + "tut", + "overview" + ], + "children": {}, + "here": "tut/overview", + "title": "Overview", + "isBook": false, + "rank": 10 + }, + "rps": { + "path": [ + "tut", + "rps" + ], + "children": { + "7-rpc": { + "path": [ + "tut", + "rps", + "7-rpc" + ], + "children": {}, + "here": "tut/rps/7-rpc", + "title": "Rock, Paper, Scissors in Python", + "isBook": false, + "rank": 10 + } + }, + "here": "tut/rps", + "title": "Rock, Paper, Scissors!", + "isBook": false, + "rank": 20 + }, + "rsvp": { + "path": [ + "tut", + "rsvp" + ], + "children": {}, + "here": "tut/rsvp", + "title": "Répondez S'il Vous Plaît", + "isBook": false, + "rank": 30 + } + }, + "here": "tut", + "title": "Tutorials", + "isBook": false, + "rank": 20 + }, + "trouble": { + "path": [ + "trouble" + ], + "children": {}, + "here": "trouble", + "title": "Troubleshooting", + "isBook": false, + "rank": 115 + }, + "rpc": { + "path": [ + "rpc" + ], + "children": { + "proto": { + "path": [ + "rpc", + "proto" + ], + "children": {}, + "here": "rpc/proto", + "title": "Specification", + "isBook": false, + "rank": 50 + }, + "py": { + "path": [ + "rpc", + "py" + ], + "children": {}, + "here": "rpc/py", + "title": "Python", + "isBook": false, + "rank": 40 + }, + "client": { + "path": [ + "rpc", + "client" + ], + "children": {}, + "here": "rpc/client", + "title": "Client Walkthrough", + "isBook": false, + "rank": 60 + }, + "go": { + "path": [ + "rpc", + "go" + ], + "children": {}, + "here": "rpc/go", + "title": "Go", + "isBook": false, + "rank": 20 + }, + "js": { + "path": [ + "rpc", + "js" + ], + "children": {}, + "here": "rpc/js", + "title": "JavaScript", + "isBook": false, + "rank": 30 + }, + "cs": { + "path": [ + "rpc", + "cs" + ], + "children": {}, + "here": "rpc/cs", + "title": "C#", + "isBook": false, + "rank": 10 + } + }, + "here": "rpc", + "title": "RPC Server", + "isBook": true, + "rank": 90 + }, + "workshop": { + "path": [ + "workshop" + ], + "children": { + "relay": { + "path": [ + "workshop", + "relay" + ], + "children": {}, + "here": "workshop/relay", + "title": "Relay Account", + "isBook": false, + "rank": 20 + }, + "fomo": { + "path": [ + "workshop", + "fomo" + ], + "children": {}, + "here": "workshop/fomo", + "title": "Fear of Missing Out", + "isBook": false, + "rank": 40 + }, + "trust-fund": { + "path": [ + "workshop", + "trust-fund" + ], + "children": {}, + "here": "workshop/trust-fund", + "title": "Trust Fund", + "isBook": false, + "rank": 30 + }, + "fomo-generalized": { + "path": [ + "workshop", + "fomo-generalized" + ], + "children": {}, + "here": "workshop/fomo-generalized", + "title": "Fear of Missing Out+", + "isBook": false, + "rank": 50 + }, + "hash-lock": { + "path": [ + "workshop", + "hash-lock" + ], + "children": {}, + "here": "workshop/hash-lock", + "title": "Hash Lock", + "isBook": false, + "rank": 10 + } + }, + "here": "workshop", + "title": "Workshops", + "isBook": true, + "rank": 100 + }, + "guide": { + "path": [ + "guide" + ], + "children": { + "invariants": { + "path": [ + "guide", + "invariants" + ], + "children": {}, + "here": "guide/invariants", + "title": "Writing Invariants", + "isBook": false, + "rank": 95 + }, + "ctransfers": { + "path": [ + "guide", + "ctransfers" + ], + "children": {}, + "here": "guide/ctransfers", + "title": "What do the different kinds of consensus transfers mean? publish, pay, race, fork, parallelReduce?", + "isBook": false, + "rank": 70 + }, + "assert": { + "path": [ + "guide", + "assert" + ], + "children": {}, + "here": "guide/assert", + "title": "How and what to verify", + "isBook": false, + "rank": 80 + }, + "lifecycle": { + "path": [ + "guide", + "lifecycle" + ], + "children": {}, + "here": "guide/lifecycle", + "title": "Contract Development Lifecycle and Best Practices for Building Reach DApps", + "isBook": false, + "rank": 35 + }, + "determ": { + "path": [ + "guide", + "determ" + ], + "children": {}, + "here": "guide/determ", + "title": "Determinism, simultaneity, and choice in decentralized applications", + "isBook": false, + "rank": 110 + }, + "limits": { + "path": [ + "guide", + "limits" + ], + "children": {}, + "here": "guide/limits", + "title": "What are Reach's limitations?", + "isBook": false, + "rank": 180 + }, + "abstract": { + "path": [ + "guide", + "abstract" + ], + "children": {}, + "here": "guide/abstract", + "title": "Building decentralized abstractions", + "isBook": false, + "rank": 130 + }, + "ganache": { + "path": [ + "guide", + "ganache" + ], + "children": {}, + "here": "guide/ganache", + "title": "How to use Ganache with Reach", + "isBook": false, + "rank": 140 + }, + "race": { + "path": [ + "guide", + "race" + ], + "children": {}, + "here": "guide/race", + "title": "Racing non-determinism in decentralized applications", + "isBook": false, + "rank": 120 + }, + "windows": { + "path": [ + "guide", + "windows" + ], + "children": {}, + "here": "guide/windows", + "title": "Using Reach on Windows", + "isBook": false, + "rank": 10 + }, + "reach": { + "path": [ + "guide", + "reach" + ], + "children": {}, + "here": "guide/reach", + "title": "How does Reach work?", + "isBook": false, + "rank": 170 + }, + "roadmap": { + "path": [ + "guide", + "roadmap" + ], + "children": {}, + "here": "guide/roadmap", + "title": "Reach's Roadmap", + "isBook": false, + "rank": 190 + }, + "solidity": { + "path": [ + "guide", + "solidity" + ], + "children": {}, + "here": "guide/solidity", + "title": "How does Reach development compare to Solidity development?", + "isBook": false, + "rank": 30 + }, + "staking": { + "path": [ + "guide", + "staking" + ], + "children": {}, + "here": "guide/staking", + "title": "Example: Staking and Unstaking Tokens", + "isBook": false, + "rank": 135 + }, + "packages": { + "path": [ + "guide", + "packages" + ], + "children": {}, + "here": "guide/packages", + "title": "Sharing and discovering shared Reach packages", + "isBook": false, + "rank": 160 + }, + "rpc": { + "path": [ + "guide", + "rpc" + ], + "children": {}, + "here": "guide/rpc", + "title": "Do I have to use JavaScript to write my frontend? What about Python, Go, or other languages?", + "isBook": false, + "rank": 40 + }, + "loop-invs": { + "path": [ + "guide", + "loop-invs" + ], + "children": {}, + "here": "guide/loop-invs", + "title": "Finding and using loop invariants", + "isBook": false, + "rank": 90 + }, + "nntoks": { + "path": [ + "guide", + "nntoks" + ], + "children": {}, + "here": "guide/nntoks", + "title": "How do network and non-network tokens differ?", + "isBook": false, + "rank": 60 + }, + "testing": { + "path": [ + "guide", + "testing" + ], + "children": {}, + "here": "guide/testing", + "title": "How should I test a DApp?", + "isBook": false, + "rank": 51 + }, + "logging": { + "path": [ + "guide", + "logging" + ], + "children": {}, + "here": "guide/logging", + "title": "How do I add tracing logs to my Reach program?", + "isBook": false, + "rank": 50 + }, + "timeout": { + "path": [ + "guide", + "timeout" + ], + "children": {}, + "here": "guide/timeout", + "title": "Non-participation: What it is and how to protect against it", + "isBook": false, + "rank": 100 + }, + "editor-support": { + "path": [ + "guide", + "editor-support" + ], + "children": {}, + "here": "guide/editor-support", + "title": "IDE/Text Editor Support", + "isBook": false, + "rank": 150 + }, + "versions": { + "path": [ + "guide", + "versions" + ], + "children": {}, + "here": "guide/versions", + "title": "How does Reach use version numbers?", + "isBook": false, + "rank": 20 + } + }, + "here": "guide", + "title": "Guide", + "isBook": true, + "rank": 110 + } + }, + "here": "", + "title": "Reach", + "isBook": true, + "rank": 0 +} diff --git a/docs/gen/package-lock.json b/docs/gen/package-lock.json index 30439f6f1b..704282a2ae 100644 --- a/docs/gen/package-lock.json +++ b/docs/gen/package-lock.json @@ -1,5 +1,5 @@ { - "name": "dev", + "name": "gen", "version": "0.0.1", "lockfileVersion": 2, "requires": true, diff --git a/docs/src/guide/index.md b/docs/src/guide/index.md index 117af76977..3c1c868a00 100644 --- a/docs/src/guide/index.md +++ b/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")} diff --git a/docs/src/guide/invariants/config.json b/docs/src/guide/invariants/config.json new file mode 100644 index 0000000000..50b434d351 --- /dev/null +++ b/docs/src/guide/invariants/config.json @@ -0,0 +1 @@ +{ "bookRank": 95 } \ No newline at end of file diff --git a/docs/src/guide/invariants/index.md b/docs/src/guide/invariants/index.md new file mode 100644 index 0000000000..01ede57c29 --- /dev/null +++ b/docs/src/guide/invariants/index.md @@ -0,0 +1,330 @@ +# {#guide-invariants} Writing Invariants + +Invariants are an essential feature when writing complex Reach DApps. +Our guide @{seclink("guide-loop-invs")} provides a deep theoretical understanding of loop invariants, and the @{seclink("tut")} and @{seclink("tut-rsvp")} tutorials both feature invariants. If you desire to create a complex Reach DApp, then you'll likely need to write your own invariants, as well. + +To help prepare you to write your own invariants, we'll review a few examples and break them to help understand the error messages. +At the end of the guide you'll have a respect for how important invariants are in Reach Applications and how important it is to have a complete understanding of your application before writing the codebase. + +First, a few basics about invariants. + +Invariant refers to something that is constant without variation. + +Loop invariants are required when writing Reach `{!rsh} while` loops. +They are established immediately before the loop begins. +You are allowed to write as many `{!rsh} invariant` statements as needed. +Inside a `{!rsh} parallelReduce`, use dot notation to place each `{!rsh} invariant` on its own line to easily distinguish each `{!rsh} invariant` from the other. + +The `{!rsh} while` loop condition and the body of the loop must uphold the `{!rsh} invariant`. +To expand, there are moments within the loop that the invariant may be invalidated, but by the end of the loop, the invariant must be true. + +The invariant establishes properties for the rest of the program after the loop ends. +So the invariants establish truth just before the loop, uphold that truth inside the loop, and remains true after the loop ends. + +Let's look at some examples of invariants and break them to understand their importance. + +``` rsh +load: /examples/rps-7-loops/index.rsh +md5: ee287e712cdfe8d91bbb038c383d25d3 +range: 59-61 +``` + +This is from the @{seclink("tut")} tutorial. +The while loop features two invariants. +The first controls the balance in relation to the wager amount and the second ensures that the outcome is one of the enumerated outcomes from the top of the program. + +In this example, if the balance ever becomes something other than double the amount of the wager then the verification engine will throw an error. +Alternatively, if the outcome of the game is anything other than `A_WINS`, `B_WINS`, or a `DRAW`, then a different error will be thrown. + +The `{!rsh} while` loop's condition is dependent on the `outcome` being equal to `DRAW`. + +The invariant indicates the importance of tracking the balance and the condition(s) of the loop. +In almost all cases, you'll want to track these items inside a `{!rsh} while` loop. + +Let's remove the balance from the invariant and observe the output when we execute a `{!cmd} $ reach compile`. + +Our snippet now looks like: + +``` rsh + var outcome = DRAW; + invariant( isOutcome(outcome) ); + while ( outcome == DRAW ) { +``` + +Without tracking the balance, instead of compiling successfully, the verification engine now outputs: + +``` +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.rsh:94:31:application + + // Violation Witness + + const UInt.max = 4; + + const wager/297 = "Alice".interact.wager; + // ^ could = 1 + // from: ./index.rsh:30:14:property binding + const netBalance/330 = ; + // ^ could = 0 + // from: ./index.rsh:61:5:while + + // Theorem Formalization + + const v452 = (2 * wager/297) <= netBalance/330; + // ^ would be false + assert(v452); + + Verification failed: + when ALL participants are honest + of theorem: assert + msg: "balance zero at application exit" + at ./index.rsh:27:30:compileDApp + + // Violation Witness + + const UInt.max = 6; + + const wager/297 = "Alice".interact.wager; + // ^ could = 0 + // from: ./index.rsh:30:14:property binding + const netBalance/330 = ; + // ^ could = 1 + // from: ./index.rsh:61:5:while + + // Theorem Formalization + + const v456 = 0 == (netBalance/330 - (2 * wager/297)); + // ^ would be false + assert(v456); + + Verifying when NO participants are honest +Checked 77 theorems; 4 failures (and 2 omitted repeats) :'( + +For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures +``` + +The error message indicates that the balance is not sufficient for a transfer on line 94. +This line is far from our `{!rsh} while` loop and invariant. + +Line 94 is where we transfer the winnings to Alice or Bob based on who won the round. + +``` rsh +load: /examples/rps-7-loops/index.rsh +md5: ee287e712cdfe8d91bbb038c383d25d3 +range: 93-95 +``` + +If you don't understand the flow of the balance within your application then this error may be confusing. +Even though the trouble begins at the loop invariant in line 60, the error is triggered at line 94 because this is the first time we try to move the balance out of the contract. + +Reading the Violation Witness may be more helpful in this situation. +(If you'd like to gain a better understanding of Violation Witnesses and Theorem Formalizations then read our guide, @{seclink("how-to-read-verification-failures")}). +The verification engine is showing two possible places where the insufficient balance could have first occurred. + +The first place could be from the `wager` property binding in the Participant Interact Interface. +The second indicates that the insufficient balance could be originating in the while loop in line 61. +The next thing we see is the Theorem Formalization where the verification engine is showing the math of how the program fails. + +If you didn't already know that the balance was failing in the while loop then you'd want to investigate the lines that the Violation Witness points to. + +We see a second verification failure that indicates that the balance is not zero when the application exits. +This verification fails at line 27, which is where the Participant Interact Interface begins. +The Violation Witness points to the same lines as the prior error. +Again, this indicates that something may be wrong in our `wager` property or in the `{!rsh} while` loop. + +If you can rule out an error in the Participant Interact Interface then consider what invariants may still need to be tracked. +If you haven't created an invariant for the balance and the condition(s) of the loop then it is possible that your current invariants may be insufficient for the verification engine to formally verify your application. + +Let's replace the balance invariant and remove the condition's invariant. + +Our code now looks like: + +``` rsh + var outcome = DRAW; + invariant( balance() == 2 * wager ); + while ( outcome == DRAW ) { +``` + +The output now reads: + +``` +Verifying knowledge assertions +Verifying for generic connector + Verifying when ALL participants are honest +Verification failed: + when ALL participants are honest + of theorem: assert + at ./index.rsh:93:15:application + + // Violation Witness + + const UInt.max = 6; + + const outcome/321 = ; + // ^ could = 3 + // from: ./index.rsh:61:5:while + + // Theorem Formalization + + const v446 = ((outcome/321 == 2) ? true : (outcome/321 == 0)); + // ^ would be false + assert(v446); + + Verifying when NO participants are honest +Checked 77 theorems; 2 failures (and 1 omitted repeats) :'( + +For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures +``` + +In this instance, the theorem fails on an `{!rsh} assert` on line 93. +We also read that there is one Violation Witness that points to the `{!rsh} while` loop. +The Theorem Formalization shows a failing ternary involving `outcome`. +Failing to write an invariant that tracks the loop's condition leaves the program open to violating static `{!rsh} assert`ions. + +Recall that the failure points to line 93 where we `{!rsh} assert` that `outcome` must be `A_WINS` or `B_WINS`. + +``` rsh +load: /examples/rps-7-loops/index.rsh +md5: ee287e712cdfe8d91bbb038c383d25d3 +range: 93-93 +``` + +The verification engine is only able to formally verify the things inside a while loop through invariants. +By establishing invariants for the condition and the balance the verification engine is able to formally verify the entire application. +Without proper invariants the application cannot be formally verified and will fail to properly compile. + +Let's look at the RSVP application. +This DApp is more complicated than the @{seclink("tut")} tutorial, but the same principles apply. +We'll write invariants for the conditions of the `{!rsh} while` loop and the balance. +The one difference in this application is that one of the conditions, `done`, will be verified with a `check`, which is a dynamic assertion, rather than an invariant. + +``` rsh +load: /examples/rsvp-6-vevt/index.rsh +md5: ed7d96413f2f23224d5ea6081ae4cc78 +range: 44-54 +``` + +In RSVP, the `{!rsh} parallelReduce` tracks two constants, `done` and `howMany`. +The first invariant ensures that the size of the `{!rsh} Map`, `Guests`, is equal to `howMany`. +If we remove this invariant, the compiler will not be able to verify that the size of the Guestbook is the same size as how many guests have reserved or checked in. + +Let's view the compiled output when this first invariant is removed: + +``` +Verification failed: + when ALL participants are honest + of theorem: assert + msg: "balance sufficient for transfer" + at ./index.rsh:69:33:application + at /app/index.rsh:66:25:application call to [unknown function] (defined at: /app/index.rsh:66:25:function exp) + + // Violation Witness + + const UInt.max = 1; + + const details/713 = "Admin".interact.details; + // ^ could = {deadline: 1, host: , name: "Bytes!val!1", reservation: 1 } + // from: ./index.rsh:13:12:property binding + const netBalance/744 = ; + // ^ could = 0 + // from: ./index.rsh:45:19:while + + // Theorem Formalization + + const v928 = details/713.reservation <= netBalance/744; + // ^ would be false + assert(v928); + + Verifying when NO participants are honest +Checked 38 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 +``` + +The verification engine fails because the balance may be insufficient for a `{!rsh} transfer`. +Similar to before, the theorem failure points further in the program when a `{!rsh} transfer` is attempted. +We also see that the Violation Witness points to the Admin's details property in the Participant Interact Interface and the start of the `{!rsh} while` loop. + +The Theorem Formalization shows a false relation to the reservation details and the balance. +If we didn't know the origination of this error then we would need to consider any static assertions that we may have overlooked. +Writing your assumptions about the application before crafting the code makes it easier to complete a `{!rsh} parallelReduce` + +Removing the second invariant outputs a similar balance transfer error, and an additional "balance zero at application exit" error. + +``` +Verification failed: + when ALL participants are honest + of theorem: assert + msg: "balance sufficient for transfer" + at ./index.rsh:69:33:application + at /app/index.rsh:66:25:application call to [unknown function] (defined at: /app/index.rsh:66:25:function exp) + + // Violation Witness + + const UInt.max = 2; + + const details/728 = "Admin".interact.details; + // ^ could = {deadline: 1, host: , name: "Bytes!val!1", reservation: 2 } + // from: ./index.rsh:13:12:property binding + const netBalance/759 = ; + // ^ could = 1 + // from: ./index.rsh:45:19:while + + // Theorem Formalization + + const v948 = details/728.reservation <= netBalance/759; + // ^ would be false + assert(v948); + +Verification failed: + when ALL participants are honest + of theorem: assert + msg: "balance zero at application exit" + at ./index.rsh:77:7:application + + // Violation Witness + + const UInt.max = 1; + + const netBalance/759 = ; + // ^ could = 1 + // from: ./index.rsh:45:19:while + + // Theorem Formalization + + const v962 = 0 == netBalance/759; + // ^ would be false + assert(v962); + + Verifying when NO participants are honest +Checked 38 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 +``` + +We saw the "balance zero at application exit" verification failure in our Rock, Paper, Scissors example when we removed the balance logic from the invariant. + +Again, we can see that the Violation Witnesses point to the Participant Interact Interface and the `{!rsh} while` loop. +The Theorem Formalizations show errors in calculating the balance. +If we saw these errors in our application then we might reconsider how we expect the balance to be calculated and identify missing assumptions based on our findings. +In this case, the balance is equal to the product of `howMany` guests completed a reservation and the reservation fee. + +At this point, we've examined four invariants and how their absence results in Violation Witness errors. +This demonstrates how important it is to fully understand your program before it is time to write `{!rsh} invariant`s. +If you'd like more practice before writing, continue this exercise of finding examples, removing invariants, and studying the resulting compile errors. + +If you'd like to experiment with invariants in additional examples then I recommend starting with the [NFT-Auction-API](https://github.com/reach-sh/reach-lang/blob/master/examples/nft-auction-api/index.rsh) and the [Chicken-Parallel](https://github.com/reach-sh/reach-lang/blob/master/examples/chicken-parallel/index.rsh) examples. + +This can be a good way of developing a sense of when and how to use invariants. +Common error messages you may see are "balance zero at application exit" and "balance sufficient for transfer". +If you see these errors in your applications, take time to consider the balance throughout the application. +Seek to identify a mathematical relationship between loop conditions and the balance. + +You should now have a better understanding of how to write invariants and their importance in developing secure Reach DApps. +If you need additional advice for your DApp, reach out in our [Discord](@{DISCORD}). \ No newline at end of file diff --git a/docs/xrefs.json b/docs/xrefs.json index 9b4e4ed0bd..1b3ae4db6e 100644 --- a/docs/xrefs.json +++ b/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" From e1977fc4a7d59ec5462b96ddfa3048d49ed9fedb Mon Sep 17 00:00:00 2001 From: TheChronicMonster Date: Wed, 19 Oct 2022 13:45:31 -0500 Subject: [PATCH 02/11] feat: fail files --- docs/src/guide/invariants/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/src/guide/invariants/index.md b/docs/src/guide/invariants/index.md index 01ede57c29..0a72e737c8 100644 --- a/docs/src/guide/invariants/index.md +++ b/docs/src/guide/invariants/index.md @@ -202,7 +202,7 @@ Without proper invariants the application cannot be formally verified and will f Let's look at the RSVP application. This DApp is more complicated than the @{seclink("tut")} tutorial, but the same principles apply. We'll write invariants for the conditions of the `{!rsh} while` loop and the balance. -The one difference in this application is that one of the conditions, `done`, will be verified with a `check`, which is a dynamic assertion, rather than an invariant. +The one difference in this application is that one of the conditions, `done`, will be verified with a `{!rsh} check`, which is a dynamic assertion, rather than an invariant. ``` rsh load: /examples/rsvp-6-vevt/index.rsh From 01a3cdf056551f9145803f348dcd6b10f58cf7a0 Mon Sep 17 00:00:00 2001 From: TheChronicMonster Date: Wed, 19 Oct 2022 13:47:01 -0500 Subject: [PATCH 03/11] tracking dirs --- examples/rps-7-balinv/.dockerignore | 1 + examples/rps-7-balinv/.gitignore | 2 + examples/rps-7-balinv/index.mjs | 58 +++++++++++++ examples/rps-7-balinv/index.rsh | 100 ++++++++++++++++++++++ examples/rps-7-balinv/index.txt | 5 ++ examples/rps-7-condinv/.dockerignore | 1 + examples/rps-7-condinv/.gitignore | 2 + examples/rps-7-condinv/index.mjs | 58 +++++++++++++ examples/rps-7-condinv/index.rsh | 100 ++++++++++++++++++++++ examples/rps-7-condinv/index.txt | 5 ++ examples/rsvp-6-balinv/index.mjs | 120 +++++++++++++++++++++++++++ examples/rsvp-6-balinv/index.rsh | 77 +++++++++++++++++ examples/rsvp-6-balinv/index.txt | 15 ++++ examples/rsvp-6-mapinv/index.mjs | 120 +++++++++++++++++++++++++++ examples/rsvp-6-mapinv/index.rsh | 77 +++++++++++++++++ examples/rsvp-6-mapinv/index.txt | 15 ++++ 16 files changed, 756 insertions(+) create mode 100644 examples/rps-7-balinv/.dockerignore create mode 100644 examples/rps-7-balinv/.gitignore create mode 100644 examples/rps-7-balinv/index.mjs create mode 100644 examples/rps-7-balinv/index.rsh create mode 100644 examples/rps-7-balinv/index.txt create mode 100644 examples/rps-7-condinv/.dockerignore create mode 100644 examples/rps-7-condinv/.gitignore create mode 100644 examples/rps-7-condinv/index.mjs create mode 100644 examples/rps-7-condinv/index.rsh create mode 100644 examples/rps-7-condinv/index.txt create mode 100644 examples/rsvp-6-balinv/index.mjs create mode 100644 examples/rsvp-6-balinv/index.rsh create mode 100644 examples/rsvp-6-balinv/index.txt create mode 100644 examples/rsvp-6-mapinv/index.mjs create mode 100644 examples/rsvp-6-mapinv/index.rsh create mode 100644 examples/rsvp-6-mapinv/index.txt diff --git a/examples/rps-7-balinv/.dockerignore b/examples/rps-7-balinv/.dockerignore new file mode 100644 index 0000000000..c2658d7d1b --- /dev/null +++ b/examples/rps-7-balinv/.dockerignore @@ -0,0 +1 @@ +node_modules/ diff --git a/examples/rps-7-balinv/.gitignore b/examples/rps-7-balinv/.gitignore new file mode 100644 index 0000000000..3e2e84b087 --- /dev/null +++ b/examples/rps-7-balinv/.gitignore @@ -0,0 +1,2 @@ +build/ +node_modules/ diff --git a/examples/rps-7-balinv/index.mjs b/examples/rps-7-balinv/index.mjs new file mode 100644 index 0000000000..17bed07a6a --- /dev/null +++ b/examples/rps-7-balinv/index.mjs @@ -0,0 +1,58 @@ +import { loadStdlib } from '@reach-sh/stdlib'; +import * as backend from './build/index.main.mjs'; +const stdlib = loadStdlib(process.env); + +const startingBalance = stdlib.parseCurrency(100); +const accAlice = await stdlib.newTestAccount(startingBalance); +const accBob = await stdlib.newTestAccount(startingBalance); + +const fmt = (x) => stdlib.formatCurrency(x, 4); +const getBalance = async (who) => fmt(await stdlib.balanceOf(who)); +const beforeAlice = await getBalance(accAlice); +const beforeBob = await getBalance(accBob); + +const ctcAlice = accAlice.contract(backend); +const ctcBob = accBob.contract(backend, ctcAlice.getInfo()); + +const HAND = ['Rock', 'Paper', 'Scissors']; +const OUTCOME = ['Bob wins', 'Draw', 'Alice wins']; +const Player = (Who) => ({ + ...stdlib.hasRandom, + getHand: async () => { // <-- async now + const hand = Math.floor(Math.random() * 3); + console.log(`${Who} played ${HAND[hand]}`); + if ( Math.random() <= 0.01 ) { + for ( let i = 0; i < 10; i++ ) { + console.log(` ${Who} takes their sweet time sending it back...`); + await stdlib.wait(1); + } + } + return hand; + }, + seeOutcome: (outcome) => { + console.log(`${Who} saw outcome ${OUTCOME[outcome]}`); + }, + informTimeout: () => { + console.log(`${Who} observed a timeout`); + }, +}); + +await Promise.all([ + ctcAlice.p.Alice({ + ...Player('Alice'), + wager: stdlib.parseCurrency(5), + deadline: 10, + }), + ctcBob.p.Bob({ + ...Player('Bob'), + acceptWager: (amt) => { + console.log(`Bob accepts the wager of ${fmt(amt)}.`); + }, + }), +]); + +const afterAlice = await getBalance(accAlice); +const afterBob = await getBalance(accBob); + +console.log(`Alice went from ${beforeAlice} to ${afterAlice}.`); +console.log(`Bob went from ${beforeBob} to ${afterBob}.`); diff --git a/examples/rps-7-balinv/index.rsh b/examples/rps-7-balinv/index.rsh new file mode 100644 index 0000000000..8d2654d424 --- /dev/null +++ b/examples/rps-7-balinv/index.rsh @@ -0,0 +1,100 @@ +'reach 0.1'; + +const [ isHand, ROCK, PAPER, SCISSORS ] = makeEnum(3); +const [ isOutcome, B_WINS, DRAW, A_WINS ] = makeEnum(3); + +const winner = (handAlice, handBob) => + ((handAlice + (4 - handBob)) % 3); + +assert(winner(ROCK, PAPER) == B_WINS); +assert(winner(PAPER, ROCK) == A_WINS); +assert(winner(ROCK, ROCK) == DRAW); + +forall(UInt, handAlice => + forall(UInt, handBob => + assert(isOutcome(winner(handAlice, handBob))))); + +forall(UInt, (hand) => + assert(winner(hand, hand) == DRAW)); + +const Player = { + ...hasRandom, + getHand: Fun([], UInt), + seeOutcome: Fun([UInt], Null), + informTimeout: Fun([], Null), +}; + +export const main = Reach.App(() => { + const Alice = Participant('Alice', { + ...Player, + wager: UInt, // atomic units of currency + deadline: UInt, // time delta (blocks/rounds) + }); + const Bob = Participant('Bob', { + ...Player, + acceptWager: Fun([UInt], Null), + }); + init(); + + const informTimeout = () => { + each([Alice, Bob], () => { + interact.informTimeout(); + }); + }; + + Alice.only(() => { + const wager = declassify(interact.wager); + const deadline = declassify(interact.deadline); + }); + Alice.publish(wager, deadline) + .pay(wager); + commit(); + + Bob.only(() => { + interact.acceptWager(wager); + }); + Bob.pay(wager) + .timeout(relativeTime(deadline), () => closeTo(Alice, informTimeout)); + + var outcome = DRAW; + invariant( isOutcome(outcome) ); + while ( outcome == DRAW ) { + commit(); + + Alice.only(() => { + const _handAlice = interact.getHand(); + const [_commitAlice, _saltAlice] = makeCommitment(interact, _handAlice); + const commitAlice = declassify(_commitAlice); + }); + Alice.publish(commitAlice) + .timeout(relativeTime(deadline), () => closeTo(Bob, informTimeout)); + commit(); + + unknowable(Bob, Alice(_handAlice, _saltAlice)); + Bob.only(() => { + const handBob = declassify(interact.getHand()); + }); + Bob.publish(handBob) + .timeout(relativeTime(deadline), () => closeTo(Alice, informTimeout)); + commit(); + + Alice.only(() => { + const saltAlice = declassify(_saltAlice); + const handAlice = declassify(_handAlice); + }); + Alice.publish(saltAlice, handAlice) + .timeout(relativeTime(deadline), () => closeTo(Bob, informTimeout)); + checkCommitment(commitAlice, saltAlice, handAlice); + + outcome = winner(handAlice, handBob); + continue; + } + + assert(outcome == A_WINS || outcome == B_WINS); + transfer(2 * wager).to(outcome == A_WINS ? Alice : Bob); + commit(); + + each([Alice, Bob], () => { + interact.seeOutcome(outcome); + }); +}); diff --git a/examples/rps-7-balinv/index.txt b/examples/rps-7-balinv/index.txt new file mode 100644 index 0000000000..e4336f7210 --- /dev/null +++ b/examples/rps-7-balinv/index.txt @@ -0,0 +1,5 @@ +Verifying knowledge assertions +Verifying for generic connector + Verifying when ALL participants are honest + Verifying when NO participants are honest +Checked 77 theorems; No failures! diff --git a/examples/rps-7-condinv/.dockerignore b/examples/rps-7-condinv/.dockerignore new file mode 100644 index 0000000000..c2658d7d1b --- /dev/null +++ b/examples/rps-7-condinv/.dockerignore @@ -0,0 +1 @@ +node_modules/ diff --git a/examples/rps-7-condinv/.gitignore b/examples/rps-7-condinv/.gitignore new file mode 100644 index 0000000000..3e2e84b087 --- /dev/null +++ b/examples/rps-7-condinv/.gitignore @@ -0,0 +1,2 @@ +build/ +node_modules/ diff --git a/examples/rps-7-condinv/index.mjs b/examples/rps-7-condinv/index.mjs new file mode 100644 index 0000000000..17bed07a6a --- /dev/null +++ b/examples/rps-7-condinv/index.mjs @@ -0,0 +1,58 @@ +import { loadStdlib } from '@reach-sh/stdlib'; +import * as backend from './build/index.main.mjs'; +const stdlib = loadStdlib(process.env); + +const startingBalance = stdlib.parseCurrency(100); +const accAlice = await stdlib.newTestAccount(startingBalance); +const accBob = await stdlib.newTestAccount(startingBalance); + +const fmt = (x) => stdlib.formatCurrency(x, 4); +const getBalance = async (who) => fmt(await stdlib.balanceOf(who)); +const beforeAlice = await getBalance(accAlice); +const beforeBob = await getBalance(accBob); + +const ctcAlice = accAlice.contract(backend); +const ctcBob = accBob.contract(backend, ctcAlice.getInfo()); + +const HAND = ['Rock', 'Paper', 'Scissors']; +const OUTCOME = ['Bob wins', 'Draw', 'Alice wins']; +const Player = (Who) => ({ + ...stdlib.hasRandom, + getHand: async () => { // <-- async now + const hand = Math.floor(Math.random() * 3); + console.log(`${Who} played ${HAND[hand]}`); + if ( Math.random() <= 0.01 ) { + for ( let i = 0; i < 10; i++ ) { + console.log(` ${Who} takes their sweet time sending it back...`); + await stdlib.wait(1); + } + } + return hand; + }, + seeOutcome: (outcome) => { + console.log(`${Who} saw outcome ${OUTCOME[outcome]}`); + }, + informTimeout: () => { + console.log(`${Who} observed a timeout`); + }, +}); + +await Promise.all([ + ctcAlice.p.Alice({ + ...Player('Alice'), + wager: stdlib.parseCurrency(5), + deadline: 10, + }), + ctcBob.p.Bob({ + ...Player('Bob'), + acceptWager: (amt) => { + console.log(`Bob accepts the wager of ${fmt(amt)}.`); + }, + }), +]); + +const afterAlice = await getBalance(accAlice); +const afterBob = await getBalance(accBob); + +console.log(`Alice went from ${beforeAlice} to ${afterAlice}.`); +console.log(`Bob went from ${beforeBob} to ${afterBob}.`); diff --git a/examples/rps-7-condinv/index.rsh b/examples/rps-7-condinv/index.rsh new file mode 100644 index 0000000000..39e720c225 --- /dev/null +++ b/examples/rps-7-condinv/index.rsh @@ -0,0 +1,100 @@ +'reach 0.1'; + +const [ isHand, ROCK, PAPER, SCISSORS ] = makeEnum(3); +const [ isOutcome, B_WINS, DRAW, A_WINS ] = makeEnum(3); + +const winner = (handAlice, handBob) => + ((handAlice + (4 - handBob)) % 3); + +assert(winner(ROCK, PAPER) == B_WINS); +assert(winner(PAPER, ROCK) == A_WINS); +assert(winner(ROCK, ROCK) == DRAW); + +forall(UInt, handAlice => + forall(UInt, handBob => + assert(isOutcome(winner(handAlice, handBob))))); + +forall(UInt, (hand) => + assert(winner(hand, hand) == DRAW)); + +const Player = { + ...hasRandom, + getHand: Fun([], UInt), + seeOutcome: Fun([UInt], Null), + informTimeout: Fun([], Null), +}; + +export const main = Reach.App(() => { + const Alice = Participant('Alice', { + ...Player, + wager: UInt, // atomic units of currency + deadline: UInt, // time delta (blocks/rounds) + }); + const Bob = Participant('Bob', { + ...Player, + acceptWager: Fun([UInt], Null), + }); + init(); + + const informTimeout = () => { + each([Alice, Bob], () => { + interact.informTimeout(); + }); + }; + + Alice.only(() => { + const wager = declassify(interact.wager); + const deadline = declassify(interact.deadline); + }); + Alice.publish(wager, deadline) + .pay(wager); + commit(); + + Bob.only(() => { + interact.acceptWager(wager); + }); + Bob.pay(wager) + .timeout(relativeTime(deadline), () => closeTo(Alice, informTimeout)); + + var outcome = DRAW; + invariant( balance() == 2 * wager ); + while ( outcome == DRAW ) { + commit(); + + Alice.only(() => { + const _handAlice = interact.getHand(); + const [_commitAlice, _saltAlice] = makeCommitment(interact, _handAlice); + const commitAlice = declassify(_commitAlice); + }); + Alice.publish(commitAlice) + .timeout(relativeTime(deadline), () => closeTo(Bob, informTimeout)); + commit(); + + unknowable(Bob, Alice(_handAlice, _saltAlice)); + Bob.only(() => { + const handBob = declassify(interact.getHand()); + }); + Bob.publish(handBob) + .timeout(relativeTime(deadline), () => closeTo(Alice, informTimeout)); + commit(); + + Alice.only(() => { + const saltAlice = declassify(_saltAlice); + const handAlice = declassify(_handAlice); + }); + Alice.publish(saltAlice, handAlice) + .timeout(relativeTime(deadline), () => closeTo(Bob, informTimeout)); + checkCommitment(commitAlice, saltAlice, handAlice); + + outcome = winner(handAlice, handBob); + continue; + } + + assert(outcome == A_WINS || outcome == B_WINS); + transfer(2 * wager).to(outcome == A_WINS ? Alice : Bob); + commit(); + + each([Alice, Bob], () => { + interact.seeOutcome(outcome); + }); +}); diff --git a/examples/rps-7-condinv/index.txt b/examples/rps-7-condinv/index.txt new file mode 100644 index 0000000000..e4336f7210 --- /dev/null +++ b/examples/rps-7-condinv/index.txt @@ -0,0 +1,5 @@ +Verifying knowledge assertions +Verifying for generic connector + Verifying when ALL participants are honest + Verifying when NO participants are honest +Checked 77 theorems; No failures! diff --git a/examples/rsvp-6-balinv/index.mjs b/examples/rsvp-6-balinv/index.mjs new file mode 100644 index 0000000000..9ba6c30661 --- /dev/null +++ b/examples/rsvp-6-balinv/index.mjs @@ -0,0 +1,120 @@ +import { loadStdlib, test } from '@reach-sh/stdlib'; +import * as backend from './build/index.main.mjs'; + +// Basics +const stdlib = loadStdlib({ REACH_NO_WARN: 'Y' }); +const err = { + 'ETH': 'transaction may fail', + 'ALGO': 'assert failed', + 'CFX': 'transaction is reverted', +}[stdlib.connector]; + +// Framework +const makeRSVP = async ({ hostLabel, name, reservation, timeLimit }) => { + const sbal = stdlib.parseCurrency(100); + const accHost = await stdlib.newTestAccount(sbal); + accHost.setDebugLabel(hostLabel); + + const stdPerson = (obj) => { + const { acc } = obj; + const getBalance = async () => { + const bal = await acc.balanceOf(); + return `${stdlib.formatCurrency(bal, 4)} ${stdlib.standardUnit}`; + }; + return { + ...obj, + getBalance, + }; + }; + + const Host = stdPerson({ + acc: accHost, + label: hostLabel, + }); + + const deadline = (await stdlib.getNetworkTime()).add(timeLimit); + const waitUntilDeadline = async () => { + console.log(`Waiting until ${deadline}`); + await stdlib.waitUntilTime(deadline); + }; + + const details = { + name, reservation, deadline, host: accHost, + }; + + const ctcHost = accHost.contract(backend); + const ctcInfo = await stdlib.withDisconnect(() => ctcHost.p.Admin({ + details, + launched: stdlib.disconnect, + })); + console.log(`${hostLabel} launched contract`); + ctcHost.e.register.monitor((evt) => { + const { when, what: [ who_ ] } = evt; + const who = stdlib.formatAddress(who_); + console.log(`${hostLabel} sees that ${who} registered at ${when}`); + }); + + const makeGuest = async (label) => { + const acc = await stdlib.newTestAccount(sbal); + acc.setDebugLabel(label); + + const willGo = async () => { + const ctcGuest = acc.contract(backend, ctcInfo); + const { reservation } = await ctcGuest.unsafeViews.Info.details(); + console.log(`${label} sees event reservation is ${stdlib.formatCurrency(reservation)} ${stdlib.standardUnit}`); + await ctcGuest.a.Guest.register(); + console.log(`${label} made reservation`); + }; + const doHost = async (showed) => { + console.log(`Checking in ${label}...`); + await ctcHost.a.Host.checkin(acc, showed); + console.log(`${label} did${showed ? '' : ' not'} show.`); + }; + const showUp = () => doHost(true); + const noShow = () => doHost(false); + + return stdPerson({ + acc, label, + willGo, showUp, noShow, + }); + }; + const makeGuests = (labels) => Promise.all(labels.map(makeGuest)); + + return { Host, makeGuest, makeGuests, waitUntilDeadline }; +}; + +// Test Scenarios +test.one('BBBB', async () => { + const Event = await makeRSVP({ + hostLabel: 'Buffy', + name: `Buffy's Birthday Bash at the Bronze`, + reservation: stdlib.parseCurrency(1), + timeLimit: 250, + }); + const Buffy = Event.Host; + const People = await Event.makeGuests([ + 'Xander', 'Willow', 'Cordelia', 'Giles', 'Oz', 'Angel', 'Jonathan', + ]); + const [ Xander, Willow, Cordelia, Giles, Oz, Angel, Jonathan ] = People; + const Scoobies = [ Xander, Willow, Cordelia, Giles, Oz ]; + await Promise.all( Scoobies.map((G) => G.willGo()) ); + await Event.waitUntilDeadline(); + await test.chkErr('Angel', err, async () => { + await Angel.willGo(); + }); + await Xander.showUp(); + await Willow.showUp(); + await Cordelia.showUp(); + await test.chkErr('Jonathan', 'no reservation', async () => { + await Jonathan.showUp(); + }); + await Giles.noShow(); + await Oz.noShow(); + + for ( const p of [ Buffy, ...People ] ) { + const bal = await p.getBalance(); + console.log(`${p.label} has ${bal}`); + } +}); + +await test.run({ noVarOutput: true }); diff --git a/examples/rsvp-6-balinv/index.rsh b/examples/rsvp-6-balinv/index.rsh new file mode 100644 index 0000000000..069e61fd05 --- /dev/null +++ b/examples/rsvp-6-balinv/index.rsh @@ -0,0 +1,77 @@ +'reach 0.1'; +'use strict'; + +const Details = Object({ + name: Bytes(128), + reservation: UInt, + deadline: UInt, + host: Address, +}); + +export const main = Reach.App(() => { + const Admin = Participant('Admin', { + details: Details, + launched: Fun([Contract], Null), + }); + const Guest = API('Guest', { + register: Fun([], Null), + }); + const Host = API('Host', { + checkin: Fun([Address, Bool], Null), + }); + const Info = View('Info', { + details: Details, + howMany: UInt, + reserved: Fun([Address], Bool), + }); + const Notify = Events({ + register: [Address], + checkin: [Address, Bool], + }); + init(); + + Admin.only(() => { + const details = declassify(interact.details); + }); + Admin.publish(details); + const { reservation, deadline, host } = details; + enforce( thisConsensusTime() < deadline, "too late" ); + Admin.interact.launched(getContract()); + Info.details.set(details); + + const Guests = new Map(Bool); + Info.reserved.set((who) => isSome(Guests[who])); + const [ done, howMany ] = + parallelReduce([ false, 0 ]) + .define(() => { + Info.howMany.set(howMany); + }) + .invariant( Guests.size() == howMany, "howMany accurate" ) + .while( ! ( done && howMany == 0 ) ) + .api_(Guest.register, () => { + check(! done, "event started"); + check(isNone(Guests[this]), "already registered"); + return [ reservation, (ret) => { + enforce( thisConsensusTime() < deadline, "too late" ); + Guests[this] = true; + Notify.register(this); + ret(null); + return [ false, howMany + 1 ]; + } ]; + }) + .api_(Host.checkin, (guest, showed) => { + check(this == host, "not the host"); + check(isSome(Guests[guest]), "no reservation"); + return [ 0, (ret) => { + enforce( thisConsensusTime() >= deadline, "too early" ); + delete Guests[guest]; + transfer(reservation).to(showed ? guest : host); + Notify.checkin(guest, showed); + ret(null); + return [ true, howMany - 1 ]; + } ]; + }); + commit(); + + exit(); +}); diff --git a/examples/rsvp-6-balinv/index.txt b/examples/rsvp-6-balinv/index.txt new file mode 100644 index 0000000000..08dc6135b8 --- /dev/null +++ b/examples/rsvp-6-balinv/index.txt @@ -0,0 +1,15 @@ +Verifying knowledge assertions +Verifying for generic connector + Verifying when ALL participants are honest + Verifying when NO participants are honest +Checked 48 theorems; No failures! +warning[RW0005]: The `Object` type's format is controlled by Reach; you may want to use `Struct` instead for external interfaces, so you can mandate and document the format. + + ./index.rsh:22:20:application + + 22| const Info = View('Info', { + +For further explanation of this warning, see: https://docs.reach.sh/rsh/errors/#RW0005 + +WARNING: Compiler instructed to emit for Algorand, but the conservative analysis found these potential problems: + * This program was compiled with trustworthy maps, but maps are not trustworthy on Algorand, because they are represented with local state. A user can delete their local state at any time, by sending a ClearState transaction. The only way to use local state properly on Algorand is to ensure that a user doing this can only 'hurt' themselves and not the entire system. diff --git a/examples/rsvp-6-mapinv/index.mjs b/examples/rsvp-6-mapinv/index.mjs new file mode 100644 index 0000000000..9ba6c30661 --- /dev/null +++ b/examples/rsvp-6-mapinv/index.mjs @@ -0,0 +1,120 @@ +import { loadStdlib, test } from '@reach-sh/stdlib'; +import * as backend from './build/index.main.mjs'; + +// Basics +const stdlib = loadStdlib({ REACH_NO_WARN: 'Y' }); +const err = { + 'ETH': 'transaction may fail', + 'ALGO': 'assert failed', + 'CFX': 'transaction is reverted', +}[stdlib.connector]; + +// Framework +const makeRSVP = async ({ hostLabel, name, reservation, timeLimit }) => { + const sbal = stdlib.parseCurrency(100); + const accHost = await stdlib.newTestAccount(sbal); + accHost.setDebugLabel(hostLabel); + + const stdPerson = (obj) => { + const { acc } = obj; + const getBalance = async () => { + const bal = await acc.balanceOf(); + return `${stdlib.formatCurrency(bal, 4)} ${stdlib.standardUnit}`; + }; + return { + ...obj, + getBalance, + }; + }; + + const Host = stdPerson({ + acc: accHost, + label: hostLabel, + }); + + const deadline = (await stdlib.getNetworkTime()).add(timeLimit); + const waitUntilDeadline = async () => { + console.log(`Waiting until ${deadline}`); + await stdlib.waitUntilTime(deadline); + }; + + const details = { + name, reservation, deadline, host: accHost, + }; + + const ctcHost = accHost.contract(backend); + const ctcInfo = await stdlib.withDisconnect(() => ctcHost.p.Admin({ + details, + launched: stdlib.disconnect, + })); + console.log(`${hostLabel} launched contract`); + ctcHost.e.register.monitor((evt) => { + const { when, what: [ who_ ] } = evt; + const who = stdlib.formatAddress(who_); + console.log(`${hostLabel} sees that ${who} registered at ${when}`); + }); + + const makeGuest = async (label) => { + const acc = await stdlib.newTestAccount(sbal); + acc.setDebugLabel(label); + + const willGo = async () => { + const ctcGuest = acc.contract(backend, ctcInfo); + const { reservation } = await ctcGuest.unsafeViews.Info.details(); + console.log(`${label} sees event reservation is ${stdlib.formatCurrency(reservation)} ${stdlib.standardUnit}`); + await ctcGuest.a.Guest.register(); + console.log(`${label} made reservation`); + }; + const doHost = async (showed) => { + console.log(`Checking in ${label}...`); + await ctcHost.a.Host.checkin(acc, showed); + console.log(`${label} did${showed ? '' : ' not'} show.`); + }; + const showUp = () => doHost(true); + const noShow = () => doHost(false); + + return stdPerson({ + acc, label, + willGo, showUp, noShow, + }); + }; + const makeGuests = (labels) => Promise.all(labels.map(makeGuest)); + + return { Host, makeGuest, makeGuests, waitUntilDeadline }; +}; + +// Test Scenarios +test.one('BBBB', async () => { + const Event = await makeRSVP({ + hostLabel: 'Buffy', + name: `Buffy's Birthday Bash at the Bronze`, + reservation: stdlib.parseCurrency(1), + timeLimit: 250, + }); + const Buffy = Event.Host; + const People = await Event.makeGuests([ + 'Xander', 'Willow', 'Cordelia', 'Giles', 'Oz', 'Angel', 'Jonathan', + ]); + const [ Xander, Willow, Cordelia, Giles, Oz, Angel, Jonathan ] = People; + const Scoobies = [ Xander, Willow, Cordelia, Giles, Oz ]; + await Promise.all( Scoobies.map((G) => G.willGo()) ); + await Event.waitUntilDeadline(); + await test.chkErr('Angel', err, async () => { + await Angel.willGo(); + }); + await Xander.showUp(); + await Willow.showUp(); + await Cordelia.showUp(); + await test.chkErr('Jonathan', 'no reservation', async () => { + await Jonathan.showUp(); + }); + await Giles.noShow(); + await Oz.noShow(); + + for ( const p of [ Buffy, ...People ] ) { + const bal = await p.getBalance(); + console.log(`${p.label} has ${bal}`); + } +}); + +await test.run({ noVarOutput: true }); diff --git a/examples/rsvp-6-mapinv/index.rsh b/examples/rsvp-6-mapinv/index.rsh new file mode 100644 index 0000000000..a5d9bc1183 --- /dev/null +++ b/examples/rsvp-6-mapinv/index.rsh @@ -0,0 +1,77 @@ +'reach 0.1'; +'use strict'; + +const Details = Object({ + name: Bytes(128), + reservation: UInt, + deadline: UInt, + host: Address, +}); + +export const main = Reach.App(() => { + const Admin = Participant('Admin', { + details: Details, + launched: Fun([Contract], Null), + }); + const Guest = API('Guest', { + register: Fun([], Null), + }); + const Host = API('Host', { + checkin: Fun([Address, Bool], Null), + }); + const Info = View('Info', { + details: Details, + howMany: UInt, + reserved: Fun([Address], Bool), + }); + const Notify = Events({ + register: [Address], + checkin: [Address, Bool], + }); + init(); + + Admin.only(() => { + const details = declassify(interact.details); + }); + Admin.publish(details); + const { reservation, deadline, host } = details; + enforce( thisConsensusTime() < deadline, "too late" ); + Admin.interact.launched(getContract()); + Info.details.set(details); + + const Guests = new Map(Bool); + Info.reserved.set((who) => isSome(Guests[who])); + const [ done, howMany ] = + parallelReduce([ false, 0 ]) + .define(() => { + Info.howMany.set(howMany); + }) + .invariant( balance() == howMany * reservation, "balance accurate" ) + .while( ! ( done && howMany == 0 ) ) + .api_(Guest.register, () => { + check(! done, "event started"); + check(isNone(Guests[this]), "already registered"); + return [ reservation, (ret) => { + enforce( thisConsensusTime() < deadline, "too late" ); + Guests[this] = true; + Notify.register(this); + ret(null); + return [ false, howMany + 1 ]; + } ]; + }) + .api_(Host.checkin, (guest, showed) => { + check(this == host, "not the host"); + check(isSome(Guests[guest]), "no reservation"); + return [ 0, (ret) => { + enforce( thisConsensusTime() >= deadline, "too early" ); + delete Guests[guest]; + transfer(reservation).to(showed ? guest : host); + Notify.checkin(guest, showed); + ret(null); + return [ true, howMany - 1 ]; + } ]; + }); + commit(); + + exit(); +}); diff --git a/examples/rsvp-6-mapinv/index.txt b/examples/rsvp-6-mapinv/index.txt new file mode 100644 index 0000000000..08dc6135b8 --- /dev/null +++ b/examples/rsvp-6-mapinv/index.txt @@ -0,0 +1,15 @@ +Verifying knowledge assertions +Verifying for generic connector + Verifying when ALL participants are honest + Verifying when NO participants are honest +Checked 48 theorems; No failures! +warning[RW0005]: The `Object` type's format is controlled by Reach; you may want to use `Struct` instead for external interfaces, so you can mandate and document the format. + + ./index.rsh:22:20:application + + 22| const Info = View('Info', { + +For further explanation of this warning, see: https://docs.reach.sh/rsh/errors/#RW0005 + +WARNING: Compiler instructed to emit for Algorand, but the conservative analysis found these potential problems: + * This program was compiled with trustworthy maps, but maps are not trustworthy on Algorand, because they are represented with local state. A user can delete their local state at any time, by sending a ClearState transaction. The only way to use local state properly on Algorand is to ensure that a user doing this can only 'hurt' themselves and not the entire system. From 065f6798b4aeb5cb02dcd33082bb1b9fc51c7d71 Mon Sep 17 00:00:00 2001 From: TheChronicMonster Date: Fri, 21 Oct 2022 08:58:11 -0500 Subject: [PATCH 04/11] refactor: major updates --- docs/gen.log | 1000 ++++++++--------- docs/src/guide/invariants/index.md | 361 +++--- examples/rps-7-balinv/.dockerignore | 1 - examples/rps-7-balinv/.gitignore | 2 - examples/rps-7-balinv/index.mjs | 58 - examples/rps-7-balinv/index.txt | 5 - examples/rps-7-condinv/.dockerignore | 1 - examples/rps-7-condinv/.gitignore | 2 - examples/rps-7-condinv/index.mjs | 58 - examples/rps-7-condinv/index.txt | 5 - .../index-balinv.rsh} | 0 examples/rps-7-loops/index-balinv.txt | 53 + .../index-condinv.rsh} | 0 examples/rps-7-loops/index-condinv.txt | 26 + examples/rsvp-6-balinv/index.mjs | 120 -- examples/rsvp-6-balinv/index.txt | 15 - examples/rsvp-6-mapinv/index.mjs | 120 -- examples/rsvp-6-mapinv/index.txt | 15 - .../index-balinv.rsh} | 0 examples/rsvp-6-vevt/index-balinv.txt | 59 + .../index-mapinv.rsh} | 0 examples/rsvp-6-vevt/index-mapinv.txt | 39 + hs/test/Reach/Test_Compiler.hs | 4 + 23 files changed, 846 insertions(+), 1098 deletions(-) delete mode 100644 examples/rps-7-balinv/.dockerignore delete mode 100644 examples/rps-7-balinv/.gitignore delete mode 100644 examples/rps-7-balinv/index.mjs delete mode 100644 examples/rps-7-balinv/index.txt delete mode 100644 examples/rps-7-condinv/.dockerignore delete mode 100644 examples/rps-7-condinv/.gitignore delete mode 100644 examples/rps-7-condinv/index.mjs delete mode 100644 examples/rps-7-condinv/index.txt rename examples/{rps-7-balinv/index.rsh => rps-7-loops/index-balinv.rsh} (100%) create mode 100644 examples/rps-7-loops/index-balinv.txt rename examples/{rps-7-condinv/index.rsh => rps-7-loops/index-condinv.rsh} (100%) create mode 100644 examples/rps-7-loops/index-condinv.txt delete mode 100644 examples/rsvp-6-balinv/index.mjs delete mode 100644 examples/rsvp-6-balinv/index.txt delete mode 100644 examples/rsvp-6-mapinv/index.mjs delete mode 100644 examples/rsvp-6-mapinv/index.txt rename examples/{rsvp-6-balinv/index.rsh => rsvp-6-vevt/index-balinv.rsh} (100%) create mode 100644 examples/rsvp-6-vevt/index-balinv.txt rename examples/{rsvp-6-mapinv/index.rsh => rsvp-6-vevt/index-mapinv.rsh} (100%) create mode 100644 examples/rsvp-6-vevt/index-mapinv.txt diff --git a/docs/gen.log b/docs/gen.log index d45a8bf6d5..64ff482d3e 100644 --- a/docs/gen.log +++ b/docs/gen.log @@ -12,22 +12,16 @@ "rank": 60 }, { - "here": "changelog", - "title": "Changelog", - "isBook": false, - "rank": 120 - }, - { - "here": "model", - "title": "Model", + "here": "index", + "title": "Index", "isBook": false, - "rank": 30 + "rank": 140 }, { - "here": "quickstart", - "title": "Quickstart", + "here": "rsh", + "title": "Language", "isBook": false, - "rank": 10 + "rank": 50 }, { "here": "build", @@ -36,40 +30,40 @@ "rank": 5 }, { - "here": "networks", - "title": "Networks", + "here": "tool", + "title": "Tool", "isBook": false, - "rank": 80 + "rank": 40 }, { - "here": "frontend", - "title": "Frontends", + "here": "search", + "title": "Search", "isBook": false, - "rank": 70 + "rank": 130 }, { - "here": "rsh", - "title": "Language", + "here": "frontend", + "title": "Frontends", "isBook": false, - "rank": 50 + "rank": 70 }, { - "here": "tool", - "title": "Tool", + "here": "trouble", + "title": "Troubleshooting", "isBook": false, - "rank": 40 + "rank": 115 }, { - "here": "index", - "title": "Index", + "here": "model", + "title": "Model", "isBook": false, - "rank": 140 + "rank": 30 }, { - "here": "search", - "title": "Search", + "here": "networks", + "title": "Networks", "isBook": false, - "rank": 130 + "rank": 80 }, { "here": "tut", @@ -78,22 +72,16 @@ "rank": 20 }, { - "here": "trouble", - "title": "Troubleshooting", + "here": "quickstart", + "title": "Quickstart", "isBook": false, - "rank": 115 - }, - { - "here": "rpc", - "title": "RPC Server", - "isBook": true, - "rank": 90 + "rank": 10 }, { - "here": "workshop", - "title": "Workshops", - "isBook": true, - "rank": 100 + "here": "changelog", + "title": "Changelog", + "isBook": false, + "rank": 120 }, { "here": "guide", @@ -102,16 +90,16 @@ "rank": 110 }, { - "here": "rsh/compute", - "title": "Computations", - "isBook": false, - "rank": 60 + "here": "workshop", + "title": "Workshops", + "isBook": true, + "rank": 100 }, { - "here": "rsh/consensus", - "title": "Consensus Steps", - "isBook": false, - "rank": 50 + "here": "rpc", + "title": "RPC Server", + "isBook": true, + "rank": 90 }, { "here": "rsh/appinit", @@ -125,12 +113,24 @@ "isBook": false, "rank": 40 }, + { + "here": "rsh/compute", + "title": "Computations", + "isBook": false, + "rank": 60 + }, { "here": "rsh/errors", "title": "Error Codes", "isBook": false, "rank": 70 }, + { + "here": "rsh/module", + "title": "Modules", + "isBook": false, + "rank": 10 + }, { "here": "rsh/step", "title": "Steps", @@ -138,16 +138,16 @@ "rank": 30 }, { - "here": "tut/wfs", - "title": "Wisdom For Sale", + "here": "rsh/consensus", + "title": "Consensus Steps", "isBook": false, - "rank": 18 + "rank": 50 }, { - "here": "rsh/module", - "title": "Modules", + "here": "tut/rps", + "title": "Rock, Paper, Scissors!", "isBook": false, - "rank": 10 + "rank": 20 }, { "here": "tut/overview", @@ -155,12 +155,6 @@ "isBook": false, "rank": 10 }, - { - "here": "tut/rps", - "title": "Rock, Paper, Scissors!", - "isBook": false, - "rank": 20 - }, { "here": "tut/rsvp", "title": "Répondez S'il Vous Plaît", @@ -168,52 +162,46 @@ "rank": 30 }, { - "here": "rpc/proto", - "title": "Specification", - "isBook": false, - "rank": 50 - }, - { - "here": "rpc/py", - "title": "Python", + "here": "tut/wfs", + "title": "Wisdom For Sale", "isBook": false, - "rank": 40 + "rank": 18 }, { - "here": "rpc/client", - "title": "Client Walkthrough", + "here": "guide/determ", + "title": "Determinism, simultaneity, and choice in decentralized applications", "isBook": false, - "rank": 60 + "rank": 110 }, { - "here": "rpc/go", - "title": "Go", + "here": "guide/ctransfers", + "title": "What do the different kinds of consensus transfers mean? publish, pay, race, fork, parallelReduce?", "isBook": false, - "rank": 20 + "rank": 70 }, { - "here": "rpc/js", - "title": "JavaScript", + "here": "guide/assert", + "title": "How and what to verify", "isBook": false, - "rank": 30 + "rank": 80 }, { - "here": "workshop/relay", - "title": "Relay Account", + "here": "guide/abstract", + "title": "Building decentralized abstractions", "isBook": false, - "rank": 20 + "rank": 130 }, { - "here": "workshop/fomo", - "title": "Fear of Missing Out", + "here": "guide/editor-support", + "title": "IDE/Text Editor Support", "isBook": false, - "rank": 40 + "rank": 150 }, { - "here": "rpc/cs", - "title": "C#", + "here": "guide/lifecycle", + "title": "Contract Development Lifecycle and Best Practices for Building Reach DApps", "isBook": false, - "rank": 10 + "rank": 35 }, { "here": "guide/invariants", @@ -222,70 +210,76 @@ "rank": 95 }, { - "here": "guide/ctransfers", - "title": "What do the different kinds of consensus transfers mean? publish, pay, race, fork, parallelReduce?", + "here": "guide/ganache", + "title": "How to use Ganache with Reach", "isBook": false, - "rank": 70 + "rank": 140 }, { - "here": "workshop/trust-fund", - "title": "Trust Fund", + "here": "guide/limits", + "title": "What are Reach's limitations?", "isBook": false, - "rank": 30 + "rank": 180 }, { - "here": "guide/assert", - "title": "How and what to verify", + "here": "guide/logging", + "title": "How do I add tracing logs to my Reach program?", "isBook": false, - "rank": 80 + "rank": 50 }, { - "here": "workshop/fomo-generalized", - "title": "Fear of Missing Out+", + "here": "guide/packages", + "title": "Sharing and discovering shared Reach packages", "isBook": false, - "rank": 50 + "rank": 160 }, { - "here": "guide/lifecycle", - "title": "Contract Development Lifecycle and Best Practices for Building Reach DApps", + "here": "guide/solidity", + "title": "How does Reach development compare to Solidity development?", "isBook": false, - "rank": 35 + "rank": 30 }, { - "here": "guide/determ", - "title": "Determinism, simultaneity, and choice in decentralized applications", + "here": "guide/loop-invs", + "title": "Finding and using loop invariants", "isBook": false, - "rank": 110 + "rank": 90 }, { - "here": "guide/limits", - "title": "What are Reach's limitations?", + "here": "guide/timeout", + "title": "Non-participation: What it is and how to protect against it", "isBook": false, - "rank": 180 + "rank": 100 }, { - "here": "guide/abstract", - "title": "Building decentralized abstractions", + "here": "guide/roadmap", + "title": "Reach's Roadmap", "isBook": false, - "rank": 130 + "rank": 190 }, { - "here": "guide/ganache", - "title": "How to use Ganache with Reach", + "here": "guide/versions", + "title": "How does Reach use version numbers?", "isBook": false, - "rank": 140 + "rank": 20 }, { - "here": "guide/race", - "title": "Racing non-determinism in decentralized applications", + "here": "guide/rpc", + "title": "Do I have to use JavaScript to write my frontend? What about Python, Go, or other languages?", "isBook": false, - "rank": 120 + "rank": 40 }, { - "here": "guide/windows", - "title": "Using Reach on Windows", + "here": "guide/staking", + "title": "Example: Staking and Unstaking Tokens", "isBook": false, - "rank": 10 + "rank": 135 + }, + { + "here": "guide/race", + "title": "Racing non-determinism in decentralized applications", + "isBook": false, + "rank": 120 }, { "here": "guide/reach", @@ -294,82 +288,88 @@ "rank": 170 }, { - "here": "guide/roadmap", - "title": "Reach's Roadmap", + "here": "guide/testing", + "title": "How should I test a DApp?", "isBook": false, - "rank": 190 + "rank": 51 }, { - "here": "guide/solidity", - "title": "How does Reach development compare to Solidity development?", + "here": "guide/nntoks", + "title": "How do network and non-network tokens differ?", "isBook": false, - "rank": 30 + "rank": 60 }, { - "here": "guide/staking", - "title": "Example: Staking and Unstaking Tokens", + "here": "guide/windows", + "title": "Using Reach on Windows", "isBook": false, - "rank": 135 + "rank": 10 }, { - "here": "guide/packages", - "title": "Sharing and discovering shared Reach packages", + "here": "workshop/relay", + "title": "Relay Account", "isBook": false, - "rank": 160 + "rank": 20 }, { - "here": "guide/rpc", - "title": "Do I have to use JavaScript to write my frontend? What about Python, Go, or other languages?", + "here": "workshop/fomo-generalized", + "title": "Fear of Missing Out+", "isBook": false, - "rank": 40 + "rank": 50 }, { - "here": "guide/loop-invs", - "title": "Finding and using loop invariants", + "here": "workshop/hash-lock", + "title": "Hash Lock", "isBook": false, - "rank": 90 + "rank": 10 }, { - "here": "guide/nntoks", - "title": "How do network and non-network tokens differ?", + "here": "workshop/trust-fund", + "title": "Trust Fund", "isBook": false, - "rank": 60 + "rank": 30 }, { - "here": "guide/testing", - "title": "How should I test a DApp?", + "here": "workshop/fomo", + "title": "Fear of Missing Out", "isBook": false, - "rank": 51 + "rank": 40 }, { - "here": "guide/logging", - "title": "How do I add tracing logs to my Reach program?", + "here": "rpc/cs", + "title": "C#", "isBook": false, - "rank": 50 + "rank": 10 }, { - "here": "guide/timeout", - "title": "Non-participation: What it is and how to protect against it", + "here": "rpc/js", + "title": "JavaScript", "isBook": false, - "rank": 100 + "rank": 30 }, { - "here": "guide/editor-support", - "title": "IDE/Text Editor Support", + "here": "rpc/client", + "title": "Client Walkthrough", "isBook": false, - "rank": 150 + "rank": 60 }, { - "here": "guide/versions", - "title": "How does Reach use version numbers?", + "here": "rpc/go", + "title": "Go", "isBook": false, "rank": 20 }, { - "here": "workshop/hash-lock", - "title": "Hash Lock", + "here": "rpc/py", + "title": "Python", "isBook": false, - "rank": 10 + "rank": 40 + }, + { + "here": "rpc/proto", + "title": "Specification", + "isBook": false, + "rank": 50 }, { "here": "tut/rps/7-rpc", @@ -391,93 +391,21 @@ "isBook": false, "rank": 60 }, - "changelog": { - "path": [ - "changelog" - ], - "children": {}, - "here": "changelog", - "title": "Changelog", - "isBook": false, - "rank": 120 - }, - "model": { - "path": [ - "model" - ], - "children": {}, - "here": "model", - "title": "Model", - "isBook": false, - "rank": 30 - }, - "quickstart": { - "path": [ - "quickstart" - ], - "children": {}, - "here": "quickstart", - "title": "Quickstart", - "isBook": false, - "rank": 10 - }, - "build": { - "path": [ - "build" - ], - "children": {}, - "here": "build", - "title": "Reach is for Builders", - "isBook": false, - "rank": 5 - }, - "networks": { - "path": [ - "networks" - ], - "children": {}, - "here": "networks", - "title": "Networks", - "isBook": false, - "rank": 80 - }, - "frontend": { + "index": { "path": [ - "frontend" + "index" ], "children": {}, - "here": "frontend", - "title": "Frontends", + "here": "index", + "title": "Index", "isBook": false, - "rank": 70 + "rank": 140 }, "rsh": { "path": [ "rsh" ], "children": { - "compute": { - "path": [ - "rsh", - "compute" - ], - "children": {}, - "here": "rsh/compute", - "title": "Computations", - "isBook": false, - "rank": 60 - }, - "consensus": { - "path": [ - "rsh", - "consensus" - ], - "children": {}, - "here": "rsh/consensus", - "title": "Consensus Steps", - "isBook": false, - "rank": 50 - }, "appinit": { "path": [ "rsh", @@ -500,6 +428,17 @@ "isBook": false, "rank": 40 }, + "compute": { + "path": [ + "rsh", + "compute" + ], + "children": {}, + "here": "rsh/compute", + "title": "Computations", + "isBook": false, + "rank": 60 + }, "errors": { "path": [ "rsh", @@ -511,6 +450,17 @@ "isBook": false, "rank": 70 }, + "module": { + "path": [ + "rsh", + "module" + ], + "children": {}, + "here": "rsh/module", + "title": "Modules", + "isBook": false, + "rank": 10 + }, "step": { "path": [ "rsh", @@ -522,16 +472,16 @@ "isBook": false, "rank": 30 }, - "module": { + "consensus": { "path": [ "rsh", - "module" + "consensus" ], "children": {}, - "here": "rsh/module", - "title": "Modules", + "here": "rsh/consensus", + "title": "Consensus Steps", "isBook": false, - "rank": 10 + "rank": 50 } }, "here": "rsh", @@ -539,25 +489,25 @@ "isBook": false, "rank": 50 }, - "tool": { + "build": { "path": [ - "tool" + "build" ], "children": {}, - "here": "tool", - "title": "Tool", + "here": "build", + "title": "Reach is for Builders", "isBook": false, - "rank": 40 + "rank": 5 }, - "index": { + "tool": { "path": [ - "index" + "tool" ], "children": {}, - "here": "index", - "title": "Index", + "here": "tool", + "title": "Tool", "isBook": false, - "rank": 140 + "rank": 40 }, "search": { "path": [ @@ -569,37 +519,55 @@ "isBook": false, "rank": 130 }, + "frontend": { + "path": [ + "frontend" + ], + "children": {}, + "here": "frontend", + "title": "Frontends", + "isBook": false, + "rank": 70 + }, + "trouble": { + "path": [ + "trouble" + ], + "children": {}, + "here": "trouble", + "title": "Troubleshooting", + "isBook": false, + "rank": 115 + }, + "model": { + "path": [ + "model" + ], + "children": {}, + "here": "model", + "title": "Model", + "isBook": false, + "rank": 30 + }, + "networks": { + "path": [ + "networks" + ], + "children": {}, + "here": "networks", + "title": "Networks", + "isBook": false, + "rank": 80 + }, "tut": { "path": [ "tut" ], "children": { - "wfs": { - "path": [ - "tut", - "wfs" - ], - "children": {}, - "here": "tut/wfs", - "title": "Wisdom For Sale", - "isBook": false, - "rank": 18 - }, - "overview": { + "rps": { "path": [ "tut", - "overview" - ], - "children": {}, - "here": "tut/overview", - "title": "Overview", - "isBook": false, - "rank": 10 - }, - "rps": { - "path": [ - "tut", - "rps" + "rps" ], "children": { "7-rpc": { @@ -620,6 +588,17 @@ "isBook": false, "rank": 20 }, + "overview": { + "path": [ + "tut", + "overview" + ], + "children": {}, + "here": "tut/overview", + "title": "Overview", + "isBook": false, + "rank": 10 + }, "rsvp": { "path": [ "tut", @@ -630,6 +609,17 @@ "title": "Répondez S'il Vous Plaît", "isBook": false, "rank": 30 + }, + "wfs": { + "path": [ + "tut", + "wfs" + ], + "children": {}, + "here": "tut/wfs", + "title": "Wisdom For Sale", + "isBook": false, + "rank": 18 } }, "here": "tut", @@ -637,251 +627,228 @@ "isBook": false, "rank": 20 }, - "trouble": { + "quickstart": { "path": [ - "trouble" + "quickstart" ], "children": {}, - "here": "trouble", - "title": "Troubleshooting", + "here": "quickstart", + "title": "Quickstart", "isBook": false, - "rank": 115 + "rank": 10 }, - "rpc": { + "changelog": { "path": [ - "rpc" + "changelog" + ], + "children": {}, + "here": "changelog", + "title": "Changelog", + "isBook": false, + "rank": 120 + }, + "guide": { + "path": [ + "guide" ], "children": { - "proto": { + "determ": { "path": [ - "rpc", - "proto" + "guide", + "determ" ], "children": {}, - "here": "rpc/proto", - "title": "Specification", + "here": "guide/determ", + "title": "Determinism, simultaneity, and choice in decentralized applications", "isBook": false, - "rank": 50 + "rank": 110 }, - "py": { + "ctransfers": { "path": [ - "rpc", - "py" + "guide", + "ctransfers" ], "children": {}, - "here": "rpc/py", - "title": "Python", + "here": "guide/ctransfers", + "title": "What do the different kinds of consensus transfers mean? publish, pay, race, fork, parallelReduce?", "isBook": false, - "rank": 40 + "rank": 70 }, - "client": { + "assert": { "path": [ - "rpc", - "client" + "guide", + "assert" ], "children": {}, - "here": "rpc/client", - "title": "Client Walkthrough", + "here": "guide/assert", + "title": "How and what to verify", "isBook": false, - "rank": 60 + "rank": 80 }, - "go": { + "abstract": { "path": [ - "rpc", - "go" + "guide", + "abstract" ], "children": {}, - "here": "rpc/go", - "title": "Go", + "here": "guide/abstract", + "title": "Building decentralized abstractions", "isBook": false, - "rank": 20 + "rank": 130 }, - "js": { + "editor-support": { "path": [ - "rpc", - "js" + "guide", + "editor-support" ], "children": {}, - "here": "rpc/js", - "title": "JavaScript", + "here": "guide/editor-support", + "title": "IDE/Text Editor Support", "isBook": false, - "rank": 30 + "rank": 150 }, - "cs": { + "lifecycle": { "path": [ - "rpc", - "cs" + "guide", + "lifecycle" ], "children": {}, - "here": "rpc/cs", - "title": "C#", + "here": "guide/lifecycle", + "title": "Contract Development Lifecycle and Best Practices for Building Reach DApps", "isBook": false, - "rank": 10 - } - }, - "here": "rpc", - "title": "RPC Server", - "isBook": true, - "rank": 90 - }, - "workshop": { - "path": [ - "workshop" - ], - "children": { - "relay": { + "rank": 35 + }, + "invariants": { "path": [ - "workshop", - "relay" + "guide", + "invariants" ], "children": {}, - "here": "workshop/relay", - "title": "Relay Account", + "here": "guide/invariants", + "title": "Writing Invariants", "isBook": false, - "rank": 20 + "rank": 95 }, - "fomo": { + "ganache": { "path": [ - "workshop", - "fomo" + "guide", + "ganache" ], "children": {}, - "here": "workshop/fomo", - "title": "Fear of Missing Out", + "here": "guide/ganache", + "title": "How to use Ganache with Reach", "isBook": false, - "rank": 40 + "rank": 140 }, - "trust-fund": { + "limits": { "path": [ - "workshop", - "trust-fund" + "guide", + "limits" ], "children": {}, - "here": "workshop/trust-fund", - "title": "Trust Fund", + "here": "guide/limits", + "title": "What are Reach's limitations?", "isBook": false, - "rank": 30 + "rank": 180 }, - "fomo-generalized": { + "logging": { "path": [ - "workshop", - "fomo-generalized" + "guide", + "logging" ], "children": {}, - "here": "workshop/fomo-generalized", - "title": "Fear of Missing Out+", + "here": "guide/logging", + "title": "How do I add tracing logs to my Reach program?", "isBook": false, "rank": 50 }, - "hash-lock": { - "path": [ - "workshop", - "hash-lock" - ], - "children": {}, - "here": "workshop/hash-lock", - "title": "Hash Lock", - "isBook": false, - "rank": 10 - } - }, - "here": "workshop", - "title": "Workshops", - "isBook": true, - "rank": 100 - }, - "guide": { - "path": [ - "guide" - ], - "children": { - "invariants": { + "packages": { "path": [ "guide", - "invariants" + "packages" ], "children": {}, - "here": "guide/invariants", - "title": "Writing Invariants", + "here": "guide/packages", + "title": "Sharing and discovering shared Reach packages", "isBook": false, - "rank": 95 + "rank": 160 }, - "ctransfers": { + "solidity": { "path": [ "guide", - "ctransfers" + "solidity" ], "children": {}, - "here": "guide/ctransfers", - "title": "What do the different kinds of consensus transfers mean? publish, pay, race, fork, parallelReduce?", + "here": "guide/solidity", + "title": "How does Reach development compare to Solidity development?", "isBook": false, - "rank": 70 + "rank": 30 }, - "assert": { + "loop-invs": { "path": [ "guide", - "assert" + "loop-invs" ], "children": {}, - "here": "guide/assert", - "title": "How and what to verify", + "here": "guide/loop-invs", + "title": "Finding and using loop invariants", "isBook": false, - "rank": 80 + "rank": 90 }, - "lifecycle": { + "timeout": { "path": [ "guide", - "lifecycle" + "timeout" ], "children": {}, - "here": "guide/lifecycle", - "title": "Contract Development Lifecycle and Best Practices for Building Reach DApps", + "here": "guide/timeout", + "title": "Non-participation: What it is and how to protect against it", "isBook": false, - "rank": 35 + "rank": 100 }, - "determ": { + "roadmap": { "path": [ "guide", - "determ" + "roadmap" ], "children": {}, - "here": "guide/determ", - "title": "Determinism, simultaneity, and choice in decentralized applications", + "here": "guide/roadmap", + "title": "Reach's Roadmap", "isBook": false, - "rank": 110 + "rank": 190 }, - "limits": { + "versions": { "path": [ "guide", - "limits" + "versions" ], "children": {}, - "here": "guide/limits", - "title": "What are Reach's limitations?", + "here": "guide/versions", + "title": "How does Reach use version numbers?", "isBook": false, - "rank": 180 + "rank": 20 }, - "abstract": { + "rpc": { "path": [ "guide", - "abstract" + "rpc" ], "children": {}, - "here": "guide/abstract", - "title": "Building decentralized abstractions", + "here": "guide/rpc", + "title": "Do I have to use JavaScript to write my frontend? What about Python, Go, or other languages?", "isBook": false, - "rank": 130 + "rank": 40 }, - "ganache": { + "staking": { "path": [ "guide", - "ganache" + "staking" ], "children": {}, - "here": "guide/ganache", - "title": "How to use Ganache with Reach", + "here": "guide/staking", + "title": "Example: Staking and Unstaking Tokens", "isBook": false, - "rank": 140 + "rank": 135 }, "race": { "path": [ @@ -894,17 +861,6 @@ "isBook": false, "rank": 120 }, - "windows": { - "path": [ - "guide", - "windows" - ], - "children": {}, - "here": "guide/windows", - "title": "Using Reach on Windows", - "isBook": false, - "rank": 10 - }, "reach": { "path": [ "guide", @@ -916,143 +872,187 @@ "isBook": false, "rank": 170 }, - "roadmap": { + "testing": { "path": [ "guide", - "roadmap" + "testing" ], "children": {}, - "here": "guide/roadmap", - "title": "Reach's Roadmap", + "here": "guide/testing", + "title": "How should I test a DApp?", "isBook": false, - "rank": 190 + "rank": 51 }, - "solidity": { + "nntoks": { "path": [ "guide", - "solidity" + "nntoks" ], "children": {}, - "here": "guide/solidity", - "title": "How does Reach development compare to Solidity development?", + "here": "guide/nntoks", + "title": "How do network and non-network tokens differ?", "isBook": false, - "rank": 30 + "rank": 60 }, - "staking": { + "windows": { "path": [ "guide", - "staking" + "windows" ], "children": {}, - "here": "guide/staking", - "title": "Example: Staking and Unstaking Tokens", + "here": "guide/windows", + "title": "Using Reach on Windows", "isBook": false, - "rank": 135 + "rank": 10 + } + }, + "here": "guide", + "title": "Guide", + "isBook": true, + "rank": 110 + }, + "workshop": { + "path": [ + "workshop" + ], + "children": { + "relay": { + "path": [ + "workshop", + "relay" + ], + "children": {}, + "here": "workshop/relay", + "title": "Relay Account", + "isBook": false, + "rank": 20 }, - "packages": { + "fomo-generalized": { "path": [ - "guide", - "packages" + "workshop", + "fomo-generalized" ], "children": {}, - "here": "guide/packages", - "title": "Sharing and discovering shared Reach packages", + "here": "workshop/fomo-generalized", + "title": "Fear of Missing Out+", "isBook": false, - "rank": 160 + "rank": 50 }, - "rpc": { + "hash-lock": { "path": [ - "guide", - "rpc" + "workshop", + "hash-lock" ], "children": {}, - "here": "guide/rpc", - "title": "Do I have to use JavaScript to write my frontend? What about Python, Go, or other languages?", + "here": "workshop/hash-lock", + "title": "Hash Lock", "isBook": false, - "rank": 40 + "rank": 10 }, - "loop-invs": { + "trust-fund": { "path": [ - "guide", - "loop-invs" + "workshop", + "trust-fund" ], "children": {}, - "here": "guide/loop-invs", - "title": "Finding and using loop invariants", + "here": "workshop/trust-fund", + "title": "Trust Fund", "isBook": false, - "rank": 90 + "rank": 30 }, - "nntoks": { + "fomo": { "path": [ - "guide", - "nntoks" + "workshop", + "fomo" ], "children": {}, - "here": "guide/nntoks", - "title": "How do network and non-network tokens differ?", + "here": "workshop/fomo", + "title": "Fear of Missing Out", "isBook": false, - "rank": 60 + "rank": 40 + } + }, + "here": "workshop", + "title": "Workshops", + "isBook": true, + "rank": 100 + }, + "rpc": { + "path": [ + "rpc" + ], + "children": { + "cs": { + "path": [ + "rpc", + "cs" + ], + "children": {}, + "here": "rpc/cs", + "title": "C#", + "isBook": false, + "rank": 10 }, - "testing": { + "js": { "path": [ - "guide", - "testing" + "rpc", + "js" ], "children": {}, - "here": "guide/testing", - "title": "How should I test a DApp?", + "here": "rpc/js", + "title": "JavaScript", "isBook": false, - "rank": 51 + "rank": 30 }, - "logging": { + "client": { "path": [ - "guide", - "logging" + "rpc", + "client" ], "children": {}, - "here": "guide/logging", - "title": "How do I add tracing logs to my Reach program?", + "here": "rpc/client", + "title": "Client Walkthrough", "isBook": false, - "rank": 50 + "rank": 60 }, - "timeout": { + "go": { "path": [ - "guide", - "timeout" + "rpc", + "go" ], "children": {}, - "here": "guide/timeout", - "title": "Non-participation: What it is and how to protect against it", + "here": "rpc/go", + "title": "Go", "isBook": false, - "rank": 100 + "rank": 20 }, - "editor-support": { + "py": { "path": [ - "guide", - "editor-support" + "rpc", + "py" ], "children": {}, - "here": "guide/editor-support", - "title": "IDE/Text Editor Support", + "here": "rpc/py", + "title": "Python", "isBook": false, - "rank": 150 + "rank": 40 }, - "versions": { + "proto": { "path": [ - "guide", - "versions" + "rpc", + "proto" ], "children": {}, - "here": "guide/versions", - "title": "How does Reach use version numbers?", + "here": "rpc/proto", + "title": "Specification", "isBook": false, - "rank": 20 + "rank": 50 } }, - "here": "guide", - "title": "Guide", + "here": "rpc", + "title": "RPC Server", "isBook": true, - "rank": 110 + "rank": 90 } }, "here": "", diff --git a/docs/src/guide/invariants/index.md b/docs/src/guide/invariants/index.md index 0a72e737c8..37ff1e508d 100644 --- a/docs/src/guide/invariants/index.md +++ b/docs/src/guide/invariants/index.md @@ -1,27 +1,33 @@ # {#guide-invariants} Writing Invariants Invariants are an essential feature when writing complex Reach DApps. -Our guide @{seclink("guide-loop-invs")} provides a deep theoretical understanding of loop invariants, and the @{seclink("tut")} and @{seclink("tut-rsvp")} tutorials both feature invariants. If you desire to create a complex Reach DApp, then you'll likely need to write your own invariants, as well. +If you're reading this guide then you've probably encountered `{!rsh} invariant`s in other parts of the documentation. +Our guide @{seclink("guide-loop-invs")} provides a deep theoretical understanding of loop invariants, and the @{seclink("tut")} and @{seclink("tut-rsvp")} tutorials both feature invariants. +Interesting Reach DApps require an intimate understanding of invariants. +This guide will strengthen your ability to identify what values need to be restricted inside a `{!rsh} while` loop and help you write your own invariants. -To help prepare you to write your own invariants, we'll review a few examples and break them to help understand the error messages. -At the end of the guide you'll have a respect for how important invariants are in Reach Applications and how important it is to have a complete understanding of your application before writing the codebase. +To understand their importance, we'll break working invariants and review the resulting error messages. +By the end of the guide you'll have a sense of the most common error messages that occur due to missing invariants. +You'll also gain a respect for how important invariants are in Reach applications and how important it is to understand your application before writing the codebase. -First, a few basics about invariants. +## Basics Invariant refers to something that is constant without variation. -Loop invariants are required when writing Reach `{!rsh} while` loops. -They are established immediately before the loop begins. +Invariants are required in Reach `{!rsh} while` loops and in `{!rsh} parallelReduce`. +They are written immediately before the loop begins. You are allowed to write as many `{!rsh} invariant` statements as needed. Inside a `{!rsh} parallelReduce`, use dot notation to place each `{!rsh} invariant` on its own line to easily distinguish each `{!rsh} invariant` from the other. The `{!rsh} while` loop condition and the body of the loop must uphold the `{!rsh} invariant`. -To expand, there are moments within the loop that the invariant may be invalidated, but by the end of the loop, the invariant must be true. +There are moments within the loop that the invariant may be invalidated, but by the end of the loop, the invariant must be true. The invariant establishes properties for the rest of the program after the loop ends. So the invariants establish truth just before the loop, uphold that truth inside the loop, and remains true after the loop ends. -Let's look at some examples of invariants and break them to understand their importance. +## Importance of Invariants + +Let's look at examples of invariants and break them to understand their importance. ``` rsh load: /examples/rps-7-loops/index.rsh @@ -31,95 +37,51 @@ range: 59-61 This is from the @{seclink("tut")} tutorial. The while loop features two invariants. -The first controls the balance in relation to the wager amount and the second ensures that the outcome is one of the enumerated outcomes from the top of the program. +The first (line 60) asserts the balance never changes and is always two times the wager. +The second invariant, also on line 60, ensures that the outcome is one of the enumerated outcomes from the top of the program (shown below). -In this example, if the balance ever becomes something other than double the amount of the wager then the verification engine will throw an error. -Alternatively, if the outcome of the game is anything other than `A_WINS`, `B_WINS`, or a `DRAW`, then a different error will be thrown. +``` rsh +load: /examples/rps-7-loops/index.rsh +md5: ee287e712cdfe8d91bbb038c383d25d3 +range: 4-4 +``` -The `{!rsh} while` loop's condition is dependent on the `outcome` being equal to `DRAW`. +In this example, if the engineer ever modified the program in a way that the balance wasn't guaranteed to be two times the wager amount then there would be an error. +Alternatively, if the outcome of the game is anything other than `A_WINS`, `B_WINS`, or a `DRAW`, then a different error will be thrown. The invariant indicates the importance of tracking the balance and the condition(s) of the loop. In almost all cases, you'll want to track these items inside a `{!rsh} while` loop. -Let's remove the balance from the invariant and observe the output when we execute a `{!cmd} $ reach compile`. +### Balance Invariant + +Let's remove the balance invariant and observe the output when we execute a `{!cmd} $ reach compile`. Our snippet now looks like: ``` rsh - var outcome = DRAW; - invariant( isOutcome(outcome) ); - while ( outcome == DRAW ) { +load: /examples/rps-7-loops/index-balinv.rsh +md5: 7e59eeb6efb5e26e97c4c1d4df6669c6 +range: 59-61 ``` -Without tracking the balance, instead of compiling successfully, the verification engine now outputs: +The verification engine outputs: -``` -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.rsh:94:31:application - - // Violation Witness - - const UInt.max = 4; - - const wager/297 = "Alice".interact.wager; - // ^ could = 1 - // from: ./index.rsh:30:14:property binding - const netBalance/330 = ; - // ^ could = 0 - // from: ./index.rsh:61:5:while - - // Theorem Formalization - - const v452 = (2 * wager/297) <= netBalance/330; - // ^ would be false - assert(v452); - - Verification failed: - when ALL participants are honest - of theorem: assert - msg: "balance zero at application exit" - at ./index.rsh:27:30:compileDApp - - // Violation Witness - - const UInt.max = 6; - - const wager/297 = "Alice".interact.wager; - // ^ could = 0 - // from: ./index.rsh:30:14:property binding - const netBalance/330 = ; - // ^ could = 1 - // from: ./index.rsh:61:5:while - - // Theorem Formalization - - const v456 = 0 == (netBalance/330 - (2 * wager/297)); - // ^ would be false - assert(v456); - - Verifying when NO participants are honest -Checked 77 theorems; 4 failures (and 2 omitted repeats) :'( - -For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures +``` txt +load: /examples/rps-7-loops/index-balinv.txt +md5: fa159888f678f8f5057e5564e8f319c1 ``` -The error message indicates that the balance is not sufficient for a transfer on line 94. -This line is far from our `{!rsh} while` loop and invariant. - -Line 94 is where we transfer the winnings to Alice or Bob based on who won the round. +The error message on line 7 indicates that the balance is not sufficient for the `{!rsh} transfer` on line 94. +This line is far from our `{!rsh} while` loop and invariant, which originates on line 49. ``` rsh -load: /examples/rps-7-loops/index.rsh -md5: ee287e712cdfe8d91bbb038c383d25d3 +load: /examples/rps-7-loops/index-balinv.rsh +md5: 7e59eeb6efb5e26e97c4c1d4df6669c6 range: 93-95 ``` +Line 94 is where we transfer the winnings to Alice or Bob based on who won the round. + If you don't understand the flow of the balance within your application then this error may be confusing. Even though the trouble begins at the loop invariant in line 60, the error is triggered at line 94 because this is the first time we try to move the balance out of the contract. @@ -127,80 +89,116 @@ Reading the Violation Witness may be more helpful in this situation. (If you'd like to gain a better understanding of Violation Witnesses and Theorem Formalizations then read our guide, @{seclink("how-to-read-verification-failures")}). The verification engine is showing two possible places where the insufficient balance could have first occurred. -The first place could be from the `wager` property binding in the Participant Interact Interface. +The first place could be from the `wager` property binding in the Participant Interact Interface on line 30. + +``` rsh +load: /examples/rps-7-loops/index-balinv.rsh +md5: 7e59eeb6efb5e26e97c4c1d4df6669c6 +range: 27-32 +``` + The second indicates that the insufficient balance could be originating in the while loop in line 61. -The next thing we see is the Theorem Formalization where the verification engine is showing the math of how the program fails. + +``` rsh +load: /examples/rps-7-loops/index-balinv.rsh +md5: 7e59eeb6efb5e26e97c4c1d4df6669c6 +range: 60-62 +``` + +The next thing we see is the Theorem Formalization. +The verification engine is showing the representation of the theorem "balance sufficient for transfer" as a program. + +``` txt +load: /examples/rps-7-loops/index-balinv.txt +md5: fa159888f678f8f5057e5564e8f319c1 +range: 21-25 +``` + +Essentially, this theorem representation shows that the balance would not be equal to two times the wager amount. For a deeper study on Theorem Formalization, read our guide, @{seclink("how-to-read-verification-failures")}). If you didn't already know that the balance was failing in the while loop then you'd want to investigate the lines that the Violation Witness points to. +``` txt +load: /examples/rps-7-loops/index-balinv.txt +md5: fa159888f678f8f5057e5564e8f319c1 +range: 27-48 +``` + We see a second verification failure that indicates that the balance is not zero when the application exits. This verification fails at line 27, which is where the Participant Interact Interface begins. + +``` rsh +load: /examples/rps-7-loops/index-balinv.rsh +md5: 7e59eeb6efb5e26e97c4c1d4df6669c6 +range: 27-32 +``` + The Violation Witness points to the same lines as the prior error. -Again, this indicates that something may be wrong in our `wager` property or in the `{!rsh} while` loop. +Again, this indicates that something may be wrong in our `wager` property on line 30 or in the `{!rsh} while` loop on line 61. + +``` rsh +load: /examples/rps-7-loops/index-balinv.rsh +md5: 7e59eeb6efb5e26e97c4c1d4df6669c6 +range: 59-62 +``` If you can rule out an error in the Participant Interact Interface then consider what invariants may still need to be tracked. If you haven't created an invariant for the balance and the condition(s) of the loop then it is possible that your current invariants may be insufficient for the verification engine to formally verify your application. +### Condition Invariant + Let's replace the balance invariant and remove the condition's invariant. Our code now looks like: ``` rsh - var outcome = DRAW; - invariant( balance() == 2 * wager ); - while ( outcome == DRAW ) { +load: /examples/rps-7-loops/index-condinv.rsh +md5: 607c8bd0c7fb7a49570946eb309c69df +range: 59-61 ``` The output now reads: ``` -Verifying knowledge assertions -Verifying for generic connector - Verifying when ALL participants are honest -Verification failed: - when ALL participants are honest - of theorem: assert - at ./index.rsh:93:15:application - - // Violation Witness - - const UInt.max = 6; - - const outcome/321 = ; - // ^ could = 3 - // from: ./index.rsh:61:5:while +load: /examples/rps-7-loops/index-condinv.txt +md5: addb49b7bdacdfad0fe4e9661c90b554 +``` - // Theorem Formalization +In this instance, the theorem fails on an `{!rsh} assert` on line 93. - const v446 = ((outcome/321 == 2) ? true : (outcome/321 == 0)); - // ^ would be false - assert(v446); +``` rsh +load: /examples/rps-7-loops/index-condinv.rsh +md5: 607c8bd0c7fb7a49570946eb309c69df +range: 93-93 +``` - Verifying when NO participants are honest -Checked 77 theorems; 2 failures (and 1 omitted repeats) :'( +We also read that there is one Violation Witness that points to the `{!rsh} while` loop on line 61. +The Theorem Formalization shows a failing ternary involving `outcome`. -For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures +``` +load: /examples/rps-7-loops/index-condinv.txt +md5: addb49b7bdacdfad0fe4e9661c90b554 +range: 17-21 ``` -In this instance, the theorem fails on an `{!rsh} assert` on line 93. -We also read that there is one Violation Witness that points to the `{!rsh} while` loop. -The Theorem Formalization shows a failing ternary involving `outcome`. -Failing to write an invariant that tracks the loop's condition leaves the program open to violating static `{!rsh} assert`ions. - -Recall that the failure points to line 93 where we `{!rsh} assert` that `outcome` must be `A_WINS` or `B_WINS`. +Failing to write an invariant that asserts the loop's condition leaves the program open to violating static `{!rsh} assert`ions, such as the one controlling the `outcome` on line 93. ``` rsh -load: /examples/rps-7-loops/index.rsh -md5: ee287e712cdfe8d91bbb038c383d25d3 +load: /examples/rps-7-loops/index-condinv.rsh +md5: 607c8bd0c7fb7a49570946eb309c69df range: 93-93 ``` +Line 93 `{!rsh} assert`s that `outcome` must be `A_WINS` or `B_WINS`, but the compiler cannot verify this assertion without an invariant in the `{!rsh} while` loop. + The verification engine is only able to formally verify the things inside a while loop through invariants. By establishing invariants for the condition and the balance the verification engine is able to formally verify the entire application. -Without proper invariants the application cannot be formally verified and will fail to properly compile. +Without proper invariants the application cannot be formally verified and will fail to compile. + +## Invariants in paralellReduce Let's look at the RSVP application. -This DApp is more complicated than the @{seclink("tut")} tutorial, but the same principles apply. +This DApp is more complicated than the @{seclink("tut")} DApp, but the same principles apply. We'll write invariants for the conditions of the `{!rsh} while` loop and the balance. The one difference in this application is that one of the conditions, `done`, will be verified with a `{!rsh} check`, which is a dynamic assertion, rather than an invariant. @@ -211,119 +209,90 @@ range: 44-54 ``` In RSVP, the `{!rsh} parallelReduce` tracks two constants, `done` and `howMany`. -The first invariant ensures that the size of the `{!rsh} Map`, `Guests`, is equal to `howMany`. -If we remove this invariant, the compiler will not be able to verify that the size of the Guestbook is the same size as how many guests have reserved or checked in. +The first invariant on line 49 asserts that the size of the `{!rsh} Map`, `Guests`, is equal to `howMany`. +If we remove this invariant, the compiler will not be able to verify that the size of the Guestbook is the same as how many guests have reserved or checked in. + +### Map Invariant Let's view the compiled output when this first invariant is removed: ``` -Verification failed: - when ALL participants are honest - of theorem: assert - msg: "balance sufficient for transfer" - at ./index.rsh:69:33:application - at /app/index.rsh:66:25:application call to [unknown function] (defined at: /app/index.rsh:66:25:function exp) - - // Violation Witness - - const UInt.max = 1; - - const details/713 = "Admin".interact.details; - // ^ could = {deadline: 1, host: , name: "Bytes!val!1", reservation: 1 } - // from: ./index.rsh:13:12:property binding - const netBalance/744 = ; - // ^ could = 0 - // from: ./index.rsh:45:19:while - - // Theorem Formalization - - const v928 = details/713.reservation <= netBalance/744; - // ^ would be false - assert(v928); +load: /examples/rsvp-6-vevt/index-mapinv.txt +md5: 86c5c2187f037fb785f347ab28ccefd6 +``` - Verifying when NO participants are honest -Checked 38 theorems; 3 failures (and 2 omitted repeats) :'( +The verification engine fails because the balance may be insufficient for a `{!rsh} transfer` (line 7). +Similar to before, on line 8, the theorem failure points further into the program when the `{!rsh} transfer` is attempted on line 68 (shown below). +Line 9 in the error message points to the DApp's return function that deletes `Guests` and controls the `{!rsh} transfer` logic (line 65). -For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures +``` rsh +load: /examples/rsvp-6-vevt/index-mapinv.rsh +md5: 94acafe2646ee59c45c89b6e1c7a6592 +range: 65-72 ``` -The verification engine fails because the balance may be insufficient for a `{!rsh} transfer`. -Similar to before, the theorem failure points further in the program when a `{!rsh} transfer` is attempted. -We also see that the Violation Witness points to the Admin's details property in the Participant Interact Interface and the start of the `{!rsh} while` loop. +The Violation Witness (lines 15-20) states that the Admin's details property in the Participant Interact Interface could be modified to result in an error. +It also shows that the start of the `{!rsh} while` loop could be erroneously modified by the programmer. The Theorem Formalization shows a false relation to the reservation details and the balance. If we didn't know the origination of this error then we would need to consider any static assertions that we may have overlooked. -Writing your assumptions about the application before crafting the code makes it easier to complete a `{!rsh} parallelReduce` +Writing your assumptions about the application before crafting the code makes it easier to complete a `{!rsh} parallelReduce`. + +### Balance Invariant Removing the second invariant outputs a similar balance transfer error, and an additional "balance zero at application exit" error. +``` txt +load: /examples/rsvp-6-vevt/index-balinv.txt +md5: ffa07ffcab3de8b2bb5ec92c161877e0 ``` -Verification failed: - when ALL participants are honest - of theorem: assert - msg: "balance sufficient for transfer" - at ./index.rsh:69:33:application - at /app/index.rsh:66:25:application call to [unknown function] (defined at: /app/index.rsh:66:25:function exp) - - // Violation Witness - - const UInt.max = 2; - - const details/728 = "Admin".interact.details; - // ^ could = {deadline: 1, host: , name: "Bytes!val!1", reservation: 2 } - // from: ./index.rsh:13:12:property binding - const netBalance/759 = ; - // ^ could = 1 - // from: ./index.rsh:45:19:while - - // Theorem Formalization - const v948 = details/728.reservation <= netBalance/759; - // ^ would be false - assert(v948); - -Verification failed: - when ALL participants are honest - of theorem: assert - msg: "balance zero at application exit" - at ./index.rsh:77:7:application - - // Violation Witness - - const UInt.max = 1; +We saw the "balance zero at application exit" verification failure in our Rock, Paper, Scissors example when we removed the balance logic from the invariant. - const netBalance/759 = ; - // ^ could = 1 - // from: ./index.rsh:45:19:while +Again, we can see that the Violation Witnesses (above in lines 15-20) point to the Participant Interact Interface and the `{!rsh} paralellReduce` (`index-balinv.rsh` lines 13 and 45, respectively). - // Theorem Formalization +``` +load: /examples/rsvp-6-vevt/index-balinv.rsh +md5: 5551e68590bad318743accb1a03639a4 +range: 45-50 +``` - const v962 = 0 == netBalance/759; - // ^ would be false - assert(v962); +The Participant Interact Interface violation reference is similar to before so we won't look at that again. +However, it's worth pointing out that the second violation points to the beginning of the `{!rsh} parallelReduce`. +This is because a `{!rsh} parallelReduce` creates a race in a loop. +When an `{!rsh} API` is involved, as in the RSVP application, invariants must make `{!rsh} assert`ions over the conditions of the `{!rsh} parallelReduce`. +Learn more about races and `{!rsh} parallelReduce` in our @{seclink("guide-ctransfers")} guide. - Verifying when NO participants are honest -Checked 38 theorems; 5 failures (and 3 omitted repeats) :'( +The Theorem Formalizations in lines 24-26 and 44-46 show a representation of the theorem "balance sufficient for transfer" and "balance zero at application exit" as programs, respectively. +It demonstrates how the program would error when calculating the balance. -For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures +``` txt +load: /examples/rsvp-6-vevt/index-balinv.txt +md5: ffa07ffcab3de8b2bb5ec92c161877e0 +range: 24-26 ``` -We saw the "balance zero at application exit" verification failure in our Rock, Paper, Scissors example when we removed the balance logic from the invariant. +``` txt +load: /examples/rsvp-6-vevt/index-balinv.txt +md5: ffa07ffcab3de8b2bb5ec92c161877e0 +range: 44-46 +``` -Again, we can see that the Violation Witnesses point to the Participant Interact Interface and the `{!rsh} while` loop. -The Theorem Formalizations show errors in calculating the balance. -If we saw these errors in our application then we might reconsider how we expect the balance to be calculated and identify missing assumptions based on our findings. +Balance errors indicate the need to recalculate the balance's formula or identify missing assumptions about the program. In this case, the balance is equal to the product of `howMany` guests completed a reservation and the reservation fee. +However, Reach cannot guarantee the efficacy of the program because we failed to `{!rsh} assert` the balance's formula in the invariant. + +## Invariably, We Have Learned At this point, we've examined four invariants and how their absence results in Violation Witness errors. -This demonstrates how important it is to fully understand your program before it is time to write `{!rsh} invariant`s. -If you'd like more practice before writing, continue this exercise of finding examples, removing invariants, and studying the resulting compile errors. +This demonstrates how important it is to understand your program before it is time to write `{!rsh} invariant`s. +For more practice, continue to find examples, remove the invariants, and study the resulting compile errors. If you'd like to experiment with invariants in additional examples then I recommend starting with the [NFT-Auction-API](https://github.com/reach-sh/reach-lang/blob/master/examples/nft-auction-api/index.rsh) and the [Chicken-Parallel](https://github.com/reach-sh/reach-lang/blob/master/examples/chicken-parallel/index.rsh) examples. This can be a good way of developing a sense of when and how to use invariants. Common error messages you may see are "balance zero at application exit" and "balance sufficient for transfer". -If you see these errors in your applications, take time to consider the balance throughout the application. +If you see these errors in your applications, take time to consider the formula of the balance in your application. Seek to identify a mathematical relationship between loop conditions and the balance. You should now have a better understanding of how to write invariants and their importance in developing secure Reach DApps. diff --git a/examples/rps-7-balinv/.dockerignore b/examples/rps-7-balinv/.dockerignore deleted file mode 100644 index c2658d7d1b..0000000000 --- a/examples/rps-7-balinv/.dockerignore +++ /dev/null @@ -1 +0,0 @@ -node_modules/ diff --git a/examples/rps-7-balinv/.gitignore b/examples/rps-7-balinv/.gitignore deleted file mode 100644 index 3e2e84b087..0000000000 --- a/examples/rps-7-balinv/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -build/ -node_modules/ diff --git a/examples/rps-7-balinv/index.mjs b/examples/rps-7-balinv/index.mjs deleted file mode 100644 index 17bed07a6a..0000000000 --- a/examples/rps-7-balinv/index.mjs +++ /dev/null @@ -1,58 +0,0 @@ -import { loadStdlib } from '@reach-sh/stdlib'; -import * as backend from './build/index.main.mjs'; -const stdlib = loadStdlib(process.env); - -const startingBalance = stdlib.parseCurrency(100); -const accAlice = await stdlib.newTestAccount(startingBalance); -const accBob = await stdlib.newTestAccount(startingBalance); - -const fmt = (x) => stdlib.formatCurrency(x, 4); -const getBalance = async (who) => fmt(await stdlib.balanceOf(who)); -const beforeAlice = await getBalance(accAlice); -const beforeBob = await getBalance(accBob); - -const ctcAlice = accAlice.contract(backend); -const ctcBob = accBob.contract(backend, ctcAlice.getInfo()); - -const HAND = ['Rock', 'Paper', 'Scissors']; -const OUTCOME = ['Bob wins', 'Draw', 'Alice wins']; -const Player = (Who) => ({ - ...stdlib.hasRandom, - getHand: async () => { // <-- async now - const hand = Math.floor(Math.random() * 3); - console.log(`${Who} played ${HAND[hand]}`); - if ( Math.random() <= 0.01 ) { - for ( let i = 0; i < 10; i++ ) { - console.log(` ${Who} takes their sweet time sending it back...`); - await stdlib.wait(1); - } - } - return hand; - }, - seeOutcome: (outcome) => { - console.log(`${Who} saw outcome ${OUTCOME[outcome]}`); - }, - informTimeout: () => { - console.log(`${Who} observed a timeout`); - }, -}); - -await Promise.all([ - ctcAlice.p.Alice({ - ...Player('Alice'), - wager: stdlib.parseCurrency(5), - deadline: 10, - }), - ctcBob.p.Bob({ - ...Player('Bob'), - acceptWager: (amt) => { - console.log(`Bob accepts the wager of ${fmt(amt)}.`); - }, - }), -]); - -const afterAlice = await getBalance(accAlice); -const afterBob = await getBalance(accBob); - -console.log(`Alice went from ${beforeAlice} to ${afterAlice}.`); -console.log(`Bob went from ${beforeBob} to ${afterBob}.`); diff --git a/examples/rps-7-balinv/index.txt b/examples/rps-7-balinv/index.txt deleted file mode 100644 index e4336f7210..0000000000 --- a/examples/rps-7-balinv/index.txt +++ /dev/null @@ -1,5 +0,0 @@ -Verifying knowledge assertions -Verifying for generic connector - Verifying when ALL participants are honest - Verifying when NO participants are honest -Checked 77 theorems; No failures! diff --git a/examples/rps-7-condinv/.dockerignore b/examples/rps-7-condinv/.dockerignore deleted file mode 100644 index c2658d7d1b..0000000000 --- a/examples/rps-7-condinv/.dockerignore +++ /dev/null @@ -1 +0,0 @@ -node_modules/ diff --git a/examples/rps-7-condinv/.gitignore b/examples/rps-7-condinv/.gitignore deleted file mode 100644 index 3e2e84b087..0000000000 --- a/examples/rps-7-condinv/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -build/ -node_modules/ diff --git a/examples/rps-7-condinv/index.mjs b/examples/rps-7-condinv/index.mjs deleted file mode 100644 index 17bed07a6a..0000000000 --- a/examples/rps-7-condinv/index.mjs +++ /dev/null @@ -1,58 +0,0 @@ -import { loadStdlib } from '@reach-sh/stdlib'; -import * as backend from './build/index.main.mjs'; -const stdlib = loadStdlib(process.env); - -const startingBalance = stdlib.parseCurrency(100); -const accAlice = await stdlib.newTestAccount(startingBalance); -const accBob = await stdlib.newTestAccount(startingBalance); - -const fmt = (x) => stdlib.formatCurrency(x, 4); -const getBalance = async (who) => fmt(await stdlib.balanceOf(who)); -const beforeAlice = await getBalance(accAlice); -const beforeBob = await getBalance(accBob); - -const ctcAlice = accAlice.contract(backend); -const ctcBob = accBob.contract(backend, ctcAlice.getInfo()); - -const HAND = ['Rock', 'Paper', 'Scissors']; -const OUTCOME = ['Bob wins', 'Draw', 'Alice wins']; -const Player = (Who) => ({ - ...stdlib.hasRandom, - getHand: async () => { // <-- async now - const hand = Math.floor(Math.random() * 3); - console.log(`${Who} played ${HAND[hand]}`); - if ( Math.random() <= 0.01 ) { - for ( let i = 0; i < 10; i++ ) { - console.log(` ${Who} takes their sweet time sending it back...`); - await stdlib.wait(1); - } - } - return hand; - }, - seeOutcome: (outcome) => { - console.log(`${Who} saw outcome ${OUTCOME[outcome]}`); - }, - informTimeout: () => { - console.log(`${Who} observed a timeout`); - }, -}); - -await Promise.all([ - ctcAlice.p.Alice({ - ...Player('Alice'), - wager: stdlib.parseCurrency(5), - deadline: 10, - }), - ctcBob.p.Bob({ - ...Player('Bob'), - acceptWager: (amt) => { - console.log(`Bob accepts the wager of ${fmt(amt)}.`); - }, - }), -]); - -const afterAlice = await getBalance(accAlice); -const afterBob = await getBalance(accBob); - -console.log(`Alice went from ${beforeAlice} to ${afterAlice}.`); -console.log(`Bob went from ${beforeBob} to ${afterBob}.`); diff --git a/examples/rps-7-condinv/index.txt b/examples/rps-7-condinv/index.txt deleted file mode 100644 index e4336f7210..0000000000 --- a/examples/rps-7-condinv/index.txt +++ /dev/null @@ -1,5 +0,0 @@ -Verifying knowledge assertions -Verifying for generic connector - Verifying when ALL participants are honest - Verifying when NO participants are honest -Checked 77 theorems; No failures! diff --git a/examples/rps-7-balinv/index.rsh b/examples/rps-7-loops/index-balinv.rsh similarity index 100% rename from examples/rps-7-balinv/index.rsh rename to examples/rps-7-loops/index-balinv.rsh diff --git a/examples/rps-7-loops/index-balinv.txt b/examples/rps-7-loops/index-balinv.txt new file mode 100644 index 0000000000..5b65e5d585 --- /dev/null +++ b/examples/rps-7-loops/index-balinv.txt @@ -0,0 +1,53 @@ +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:94:25:application + + // Violation Witness + + const UInt.max = 4; + + const wager/297 = "Alice".interact.wager; + // ^ could = 1 + // from: ./index-balinv.rsh:30:10:property binding + const netBalance/330 = ; + // ^ could = 0 + // from: ./index-balinv.rsh:61:3:while + + // Theorem Formalization + + const v452 = (2 * wager/297) <= netBalance/330; + // ^ would be false + assert(v452); + +Verification failed: + when ALL participants are honest + of theorem: assert + msg: "balance zero at application exit" + at ./index-balinv.rsh:27:30:compileDApp + + // Violation Witness + + const UInt.max = 6; + + const wager/297 = "Alice".interact.wager; + // ^ could = 0 + // from: ./index-balinv.rsh:30:10:property binding + const netBalance/330 = ; + // ^ could = 1 + // from: ./index-balinv.rsh:61:3:while + + // Theorem Formalization + + const v456 = 0 == (netBalance/330 - (2 * wager/297)); + // ^ would be false + assert(v456); + + Verifying when NO participants are honest +Checked 77 theorems; 4 failures (and 2 omitted repeats) :'( + +For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures diff --git a/examples/rps-7-condinv/index.rsh b/examples/rps-7-loops/index-condinv.rsh similarity index 100% rename from examples/rps-7-condinv/index.rsh rename to examples/rps-7-loops/index-condinv.rsh diff --git a/examples/rps-7-loops/index-condinv.txt b/examples/rps-7-loops/index-condinv.txt new file mode 100644 index 0000000000..5cf00f1d09 --- /dev/null +++ b/examples/rps-7-loops/index-condinv.txt @@ -0,0 +1,26 @@ +Verifying knowledge assertions +Verifying for generic connector + Verifying when ALL participants are honest +Verification failed: + when ALL participants are honest + of theorem: assert + at ./index-condinv.rsh:93:9:application + + // Violation Witness + + const UInt.max = 6; + + const outcome/321 = ; + // ^ could = 3 + // from: ./index-condinv.rsh:61:3:while + + // Theorem Formalization + + const v446 = ((outcome/321 == 2) ? true : (outcome/321 == 0)); + // ^ would be false + assert(v446); + + Verifying when NO participants are honest +Checked 77 theorems; 2 failures (and 1 omitted repeats) :'( + +For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures diff --git a/examples/rsvp-6-balinv/index.mjs b/examples/rsvp-6-balinv/index.mjs deleted file mode 100644 index 9ba6c30661..0000000000 --- a/examples/rsvp-6-balinv/index.mjs +++ /dev/null @@ -1,120 +0,0 @@ -import { loadStdlib, test } from '@reach-sh/stdlib'; -import * as backend from './build/index.main.mjs'; - -// Basics -const stdlib = loadStdlib({ REACH_NO_WARN: 'Y' }); -const err = { - 'ETH': 'transaction may fail', - 'ALGO': 'assert failed', - 'CFX': 'transaction is reverted', -}[stdlib.connector]; - -// Framework -const makeRSVP = async ({ hostLabel, name, reservation, timeLimit }) => { - const sbal = stdlib.parseCurrency(100); - const accHost = await stdlib.newTestAccount(sbal); - accHost.setDebugLabel(hostLabel); - - const stdPerson = (obj) => { - const { acc } = obj; - const getBalance = async () => { - const bal = await acc.balanceOf(); - return `${stdlib.formatCurrency(bal, 4)} ${stdlib.standardUnit}`; - }; - return { - ...obj, - getBalance, - }; - }; - - const Host = stdPerson({ - acc: accHost, - label: hostLabel, - }); - - const deadline = (await stdlib.getNetworkTime()).add(timeLimit); - const waitUntilDeadline = async () => { - console.log(`Waiting until ${deadline}`); - await stdlib.waitUntilTime(deadline); - }; - - const details = { - name, reservation, deadline, host: accHost, - }; - - const ctcHost = accHost.contract(backend); - const ctcInfo = await stdlib.withDisconnect(() => ctcHost.p.Admin({ - details, - launched: stdlib.disconnect, - })); - console.log(`${hostLabel} launched contract`); - ctcHost.e.register.monitor((evt) => { - const { when, what: [ who_ ] } = evt; - const who = stdlib.formatAddress(who_); - console.log(`${hostLabel} sees that ${who} registered at ${when}`); - }); - - const makeGuest = async (label) => { - const acc = await stdlib.newTestAccount(sbal); - acc.setDebugLabel(label); - - const willGo = async () => { - const ctcGuest = acc.contract(backend, ctcInfo); - const { reservation } = await ctcGuest.unsafeViews.Info.details(); - console.log(`${label} sees event reservation is ${stdlib.formatCurrency(reservation)} ${stdlib.standardUnit}`); - await ctcGuest.a.Guest.register(); - console.log(`${label} made reservation`); - }; - const doHost = async (showed) => { - console.log(`Checking in ${label}...`); - await ctcHost.a.Host.checkin(acc, showed); - console.log(`${label} did${showed ? '' : ' not'} show.`); - }; - const showUp = () => doHost(true); - const noShow = () => doHost(false); - - return stdPerson({ - acc, label, - willGo, showUp, noShow, - }); - }; - const makeGuests = (labels) => Promise.all(labels.map(makeGuest)); - - return { Host, makeGuest, makeGuests, waitUntilDeadline }; -}; - -// Test Scenarios -test.one('BBBB', async () => { - const Event = await makeRSVP({ - hostLabel: 'Buffy', - name: `Buffy's Birthday Bash at the Bronze`, - reservation: stdlib.parseCurrency(1), - timeLimit: 250, - }); - const Buffy = Event.Host; - const People = await Event.makeGuests([ - 'Xander', 'Willow', 'Cordelia', 'Giles', 'Oz', 'Angel', 'Jonathan', - ]); - const [ Xander, Willow, Cordelia, Giles, Oz, Angel, Jonathan ] = People; - const Scoobies = [ Xander, Willow, Cordelia, Giles, Oz ]; - await Promise.all( Scoobies.map((G) => G.willGo()) ); - await Event.waitUntilDeadline(); - await test.chkErr('Angel', err, async () => { - await Angel.willGo(); - }); - await Xander.showUp(); - await Willow.showUp(); - await Cordelia.showUp(); - await test.chkErr('Jonathan', 'no reservation', async () => { - await Jonathan.showUp(); - }); - await Giles.noShow(); - await Oz.noShow(); - - for ( const p of [ Buffy, ...People ] ) { - const bal = await p.getBalance(); - console.log(`${p.label} has ${bal}`); - } -}); - -await test.run({ noVarOutput: true }); diff --git a/examples/rsvp-6-balinv/index.txt b/examples/rsvp-6-balinv/index.txt deleted file mode 100644 index 08dc6135b8..0000000000 --- a/examples/rsvp-6-balinv/index.txt +++ /dev/null @@ -1,15 +0,0 @@ -Verifying knowledge assertions -Verifying for generic connector - Verifying when ALL participants are honest - Verifying when NO participants are honest -Checked 48 theorems; No failures! -warning[RW0005]: The `Object` type's format is controlled by Reach; you may want to use `Struct` instead for external interfaces, so you can mandate and document the format. - - ./index.rsh:22:20:application - - 22| const Info = View('Info', { - -For further explanation of this warning, see: https://docs.reach.sh/rsh/errors/#RW0005 - -WARNING: Compiler instructed to emit for Algorand, but the conservative analysis found these potential problems: - * This program was compiled with trustworthy maps, but maps are not trustworthy on Algorand, because they are represented with local state. A user can delete their local state at any time, by sending a ClearState transaction. The only way to use local state properly on Algorand is to ensure that a user doing this can only 'hurt' themselves and not the entire system. diff --git a/examples/rsvp-6-mapinv/index.mjs b/examples/rsvp-6-mapinv/index.mjs deleted file mode 100644 index 9ba6c30661..0000000000 --- a/examples/rsvp-6-mapinv/index.mjs +++ /dev/null @@ -1,120 +0,0 @@ -import { loadStdlib, test } from '@reach-sh/stdlib'; -import * as backend from './build/index.main.mjs'; - -// Basics -const stdlib = loadStdlib({ REACH_NO_WARN: 'Y' }); -const err = { - 'ETH': 'transaction may fail', - 'ALGO': 'assert failed', - 'CFX': 'transaction is reverted', -}[stdlib.connector]; - -// Framework -const makeRSVP = async ({ hostLabel, name, reservation, timeLimit }) => { - const sbal = stdlib.parseCurrency(100); - const accHost = await stdlib.newTestAccount(sbal); - accHost.setDebugLabel(hostLabel); - - const stdPerson = (obj) => { - const { acc } = obj; - const getBalance = async () => { - const bal = await acc.balanceOf(); - return `${stdlib.formatCurrency(bal, 4)} ${stdlib.standardUnit}`; - }; - return { - ...obj, - getBalance, - }; - }; - - const Host = stdPerson({ - acc: accHost, - label: hostLabel, - }); - - const deadline = (await stdlib.getNetworkTime()).add(timeLimit); - const waitUntilDeadline = async () => { - console.log(`Waiting until ${deadline}`); - await stdlib.waitUntilTime(deadline); - }; - - const details = { - name, reservation, deadline, host: accHost, - }; - - const ctcHost = accHost.contract(backend); - const ctcInfo = await stdlib.withDisconnect(() => ctcHost.p.Admin({ - details, - launched: stdlib.disconnect, - })); - console.log(`${hostLabel} launched contract`); - ctcHost.e.register.monitor((evt) => { - const { when, what: [ who_ ] } = evt; - const who = stdlib.formatAddress(who_); - console.log(`${hostLabel} sees that ${who} registered at ${when}`); - }); - - const makeGuest = async (label) => { - const acc = await stdlib.newTestAccount(sbal); - acc.setDebugLabel(label); - - const willGo = async () => { - const ctcGuest = acc.contract(backend, ctcInfo); - const { reservation } = await ctcGuest.unsafeViews.Info.details(); - console.log(`${label} sees event reservation is ${stdlib.formatCurrency(reservation)} ${stdlib.standardUnit}`); - await ctcGuest.a.Guest.register(); - console.log(`${label} made reservation`); - }; - const doHost = async (showed) => { - console.log(`Checking in ${label}...`); - await ctcHost.a.Host.checkin(acc, showed); - console.log(`${label} did${showed ? '' : ' not'} show.`); - }; - const showUp = () => doHost(true); - const noShow = () => doHost(false); - - return stdPerson({ - acc, label, - willGo, showUp, noShow, - }); - }; - const makeGuests = (labels) => Promise.all(labels.map(makeGuest)); - - return { Host, makeGuest, makeGuests, waitUntilDeadline }; -}; - -// Test Scenarios -test.one('BBBB', async () => { - const Event = await makeRSVP({ - hostLabel: 'Buffy', - name: `Buffy's Birthday Bash at the Bronze`, - reservation: stdlib.parseCurrency(1), - timeLimit: 250, - }); - const Buffy = Event.Host; - const People = await Event.makeGuests([ - 'Xander', 'Willow', 'Cordelia', 'Giles', 'Oz', 'Angel', 'Jonathan', - ]); - const [ Xander, Willow, Cordelia, Giles, Oz, Angel, Jonathan ] = People; - const Scoobies = [ Xander, Willow, Cordelia, Giles, Oz ]; - await Promise.all( Scoobies.map((G) => G.willGo()) ); - await Event.waitUntilDeadline(); - await test.chkErr('Angel', err, async () => { - await Angel.willGo(); - }); - await Xander.showUp(); - await Willow.showUp(); - await Cordelia.showUp(); - await test.chkErr('Jonathan', 'no reservation', async () => { - await Jonathan.showUp(); - }); - await Giles.noShow(); - await Oz.noShow(); - - for ( const p of [ Buffy, ...People ] ) { - const bal = await p.getBalance(); - console.log(`${p.label} has ${bal}`); - } -}); - -await test.run({ noVarOutput: true }); diff --git a/examples/rsvp-6-mapinv/index.txt b/examples/rsvp-6-mapinv/index.txt deleted file mode 100644 index 08dc6135b8..0000000000 --- a/examples/rsvp-6-mapinv/index.txt +++ /dev/null @@ -1,15 +0,0 @@ -Verifying knowledge assertions -Verifying for generic connector - Verifying when ALL participants are honest - Verifying when NO participants are honest -Checked 48 theorems; No failures! -warning[RW0005]: The `Object` type's format is controlled by Reach; you may want to use `Struct` instead for external interfaces, so you can mandate and document the format. - - ./index.rsh:22:20:application - - 22| const Info = View('Info', { - -For further explanation of this warning, see: https://docs.reach.sh/rsh/errors/#RW0005 - -WARNING: Compiler instructed to emit for Algorand, but the conservative analysis found these potential problems: - * This program was compiled with trustworthy maps, but maps are not trustworthy on Algorand, because they are represented with local state. A user can delete their local state at any time, by sending a ClearState transaction. The only way to use local state properly on Algorand is to ensure that a user doing this can only 'hurt' themselves and not the entire system. diff --git a/examples/rsvp-6-balinv/index.rsh b/examples/rsvp-6-vevt/index-balinv.rsh similarity index 100% rename from examples/rsvp-6-balinv/index.rsh rename to examples/rsvp-6-vevt/index-balinv.rsh diff --git a/examples/rsvp-6-vevt/index-balinv.txt b/examples/rsvp-6-vevt/index-balinv.txt new file mode 100644 index 0000000000..8093013b7f --- /dev/null +++ b/examples/rsvp-6-vevt/index-balinv.txt @@ -0,0 +1,59 @@ +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:68:33:application + at /app/index-balinv.rsh:65:25:application call to [unknown function] (defined at: /app/index-balinv.rsh:65:25:function exp) + + // Violation Witness + + const UInt.max = 2; + + const details/728 = "Admin".interact.details; + // ^ could = {deadline: 1, host: , name: "Bytes!val!1", reservation: 2 } + // from: ./index-balinv.rsh:13:12:property binding + const netBalance/759 = ; + // ^ could = 1 + // from: ./index-balinv.rsh:45:19:while + + // Theorem Formalization + + const v948 = details/728.reservation <= netBalance/759; + // ^ would be false + assert(v948); + +Verification failed: + when ALL participants are honest + of theorem: assert + msg: "balance zero at application exit" + at ./index-balinv.rsh:76:7:application + + // Violation Witness + + const UInt.max = 1; + + const netBalance/759 = ; + // ^ could = 1 + // from: ./index-balinv.rsh:45:19:while + + // Theorem Formalization + + const v962 = 0 == netBalance/759; + // ^ would be false + assert(v962); + + Verifying when NO participants are honest +Checked 38 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 +warning[RW0005]: The `Object` type's format is controlled by Reach; you may want to use `Struct` instead for external interfaces, so you can mandate and document the format. + + ./index-balinv.rsh:22:20:application + + 22| const Info = View('Info', { + +For further explanation of this warning, see: https://docs.reach.sh/rsh/errors/#RW0005 + diff --git a/examples/rsvp-6-mapinv/index.rsh b/examples/rsvp-6-vevt/index-mapinv.rsh similarity index 100% rename from examples/rsvp-6-mapinv/index.rsh rename to examples/rsvp-6-vevt/index-mapinv.rsh diff --git a/examples/rsvp-6-vevt/index-mapinv.txt b/examples/rsvp-6-vevt/index-mapinv.txt new file mode 100644 index 0000000000..5286d1395d --- /dev/null +++ b/examples/rsvp-6-vevt/index-mapinv.txt @@ -0,0 +1,39 @@ +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:68:33:application + at /app/index-mapinv.rsh:65:25:application call to [unknown function] (defined at: /app/index-mapinv.rsh:65:25:function exp) + + // Violation Witness + + const UInt.max = 1; + + const details/713 = "Admin".interact.details; + // ^ could = {deadline: 1, host: , name: "Bytes!val!1", reservation: 1 } + // from: ./index-mapinv.rsh:13:12:property binding + const netBalance/744 = ; + // ^ could = 0 + // from: ./index-mapinv.rsh:45:19:while + + // Theorem Formalization + + const v928 = details/713.reservation <= netBalance/744; + // ^ would be false + assert(v928); + + Verifying when NO participants are honest +Checked 38 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 +warning[RW0005]: The `Object` type's format is controlled by Reach; you may want to use `Struct` instead for external interfaces, so you can mandate and document the format. + + ./index-mapinv.rsh:22:20:application + + 22| const Info = View('Info', { + +For further explanation of this warning, see: https://docs.reach.sh/rsh/errors/#RW0005 + diff --git a/hs/test/Reach/Test_Compiler.hs b/hs/test/Reach/Test_Compiler.hs index 0913bb3db2..bcc336588a 100644 --- a/hs/test/Reach/Test_Compiler.hs +++ b/hs/test/Reach/Test_Compiler.hs @@ -106,8 +106,12 @@ test_examples = goldenTests "../examples" f , "./pkg/index-master.rsh" , "./rps-4-attack/index-bad.rsh" , "./rps-4-attack/index-fails.rsh" + , "./rps-7-loops/index-balinv.rsh" + , "./rps-7-loops/index-condinv.rsh" , "./overview/index-error.rsh" , "./rsvp-5-cede/index-fail.rsh" + , "./rsvp-6-vevt/index-balinv.rsh" + , "./rsvp-6-vevt/index-mapinv.rsh" ] f fp = case S.member fp fails of From 38a1dcb897ea5f165d0e13aa63e867a39dbaa68e Mon Sep 17 00:00:00 2001 From: TheChronicMonster Date: Mon, 31 Oct 2022 15:51:35 -0500 Subject: [PATCH 05/11] feat: ticket ex --- docs/src/guide/invariants/index.md | 89 +++++++++++++++++++++++++++++- 1 file changed, 86 insertions(+), 3 deletions(-) diff --git a/docs/src/guide/invariants/index.md b/docs/src/guide/invariants/index.md index 37ff1e508d..093d4fb8fd 100644 --- a/docs/src/guide/invariants/index.md +++ b/docs/src/guide/invariants/index.md @@ -49,8 +49,8 @@ range: 4-4 In this example, if the engineer ever modified the program in a way that the balance wasn't guaranteed to be two times the wager amount then there would be an error. Alternatively, if the outcome of the game is anything other than `A_WINS`, `B_WINS`, or a `DRAW`, then a different error will be thrown. -The invariant indicates the importance of tracking the balance and the condition(s) of the loop. -In almost all cases, you'll want to track these items inside a `{!rsh} while` loop. +The invariant indicates the importance of asserting the balance and the condition(s) of the loop. +In almost all cases, you'll want to constrain these items inside a `{!rsh} while` loop. ### Balance Invariant @@ -142,8 +142,15 @@ md5: 7e59eeb6efb5e26e97c4c1d4df6669c6 range: 59-62 ``` -If you can rule out an error in the Participant Interact Interface then consider what invariants may still need to be tracked. +If you can rule out an error in the Participant Interact Interface then consider what invariants may be required by the `{!rsh} while` loop. If you haven't created an invariant for the balance and the condition(s) of the loop then it is possible that your current invariants may be insufficient for the verification engine to formally verify your application. +A pattern will emerge as we progress through this guide. +We'll see that the `{!rsh} invariant` should `{!rsh} assert` the balance, loop condition, and `{!rsh} Map` size, if applicable. +`{!rsh} check`s within the `{!rsh} parallelReduce` relate to the invariants. + +We'll continue to explore this pattern for writing invariants. +We've examined an `{!rsh} invariant` for asserting the `balance`. +Now we'll review an `${!rsh} invariant` that asserts the loop's condition. ### Condition Invariant @@ -282,6 +289,82 @@ Balance errors indicate the need to recalculate the balance's formula or identif In this case, the balance is equal to the product of `howMany` guests completed a reservation and the reservation fee. However, Reach cannot guarantee the efficacy of the program because we failed to `{!rsh} assert` the balance's formula in the invariant. +## Track/Distribute Supply of Non-Network Tokens + +Sometimes you may want to write an `{!rsh} assert`ion regarding the supply of non-network tokens. +In the "Ticket Sale DApp" an Administrator issues non-network tokens and Buyer `{!rsh} API`s have the ability to buy the tokens, which are referred to as 'tickets', in this DApp. + +The `{!rsh} invariant` in this DApp is interesting because it makes `{!rsh} assert`s over the network token balance (line 34) and the non-network token balance (line 35). + +``` +load - ticket sales +md5 - +range - 33-44 + + const [ticketsSold] = parallelReduce([0]) + .invariant(balance() == amount * ticketsSold) + .invariant(balance(tok) == supply - ticketsSold)errors + .while(ticketsSold < supply) + .api_(B.buyTicket, () => { + return[amount, (ret) => { + transfer(1, tok).to(this); + ret(true); + return [ticketsSold + 1]; + }]; + }); + transfer(balance()).to(A); +``` + +The `{!rsh} parallelReduce` updates the value of `ticketsSold` and the condition is `true` as long as `ticketsSold` is less than the available `supply` of tickets. +The `{!rsh} API` calls on the `buyTicket` function, which increments the number of `ticketsSold` and returns the new value. + +This program doesn't break after removing the first balance invariant. +The `{!rsh} parallelReduce` is in a race to sell the non-network tokens. +Writing an invariant about the network token balance provides stronger defenses to the program, but is not required for the compiler to complete its formal verification. +However, removing the second invariant will cause a violation witness. + +The critical `{!rsh} invariant` on line 35 and `{!rsh} assert`s that the non-network token balance is equal to the difference of the supply and the number of tickets sold. + +Once removed, the compiler returns + +``` +load - +md5 - +range - + +Verification failed: + when ALL participants are honest + of theorem: assert + msg: "balance sufficient for transfer" + at ./index.rsh:39:28:application + at /app/index.rsh:38:28:application call to [unknown function] (defined at: /app/index.rsh:38:28:function exp) + + // Violation Witness + + const UInt.max = 1; + + const tokenInfos/169 = ; + // ^ could = Array.const(Tuple(UInt, UInt, Bool), [0, 0, false ] ) + // from: ./index.rsh:33:39:while + + // Theorem Formalization + + const v189 = 1 <= tokenInfos/169[0][0]; + // ^ would be false + assert(v189); +``` + +We see the `balance sufficient for transfer` error, once again. +However, instead of referring to a network token transfer, the message is referring to the transfer of a non-network token. +In this example, the message points to the `{!rsh} transfer` on line 39 and the `return` statement on line 38. + +The Violation Witness on line XX shows how the `{!rsh} parallelReduce` could fail, followed by the Theorem Formalization. + +The second verification failure, "balance zero at application exit" indicates that tokens could remain in the contract when it exits on line 45. +This Violation Witness also points to the `{!rsh} parallelReduce` with a similar example as before. + +This example shows that it is critical to understand a non-network token's balance, as well as, the network token's balance. + ## Invariably, We Have Learned At this point, we've examined four invariants and how their absence results in Violation Witness errors. From 6e2d9ae379ae47a1359adfdaa2c59bc10c1046e8 Mon Sep 17 00:00:00 2001 From: TheChronicMonster Date: Wed, 9 Nov 2022 01:27:07 -0600 Subject: [PATCH 06/11] feat: fail ex --- docs/src/guide/invariants/index.md | 148 +++++++++++++++++++++++- examples/point-of-sale/index-balinv.rsh | 58 ++++++++++ examples/point-of-sale/index-balinv.txt | 80 +++++++++++++ examples/point-of-sale/index-mapinv.rsh | 58 ++++++++++ examples/point-of-sale/index-mapinv.txt | 34 ++++++ examples/point-of-sale/index-tokinv.rsh | 58 ++++++++++ examples/point-of-sale/index-tokinv.txt | 48 ++++++++ 7 files changed, 482 insertions(+), 2 deletions(-) create mode 100644 examples/point-of-sale/index-balinv.rsh create mode 100644 examples/point-of-sale/index-balinv.txt create mode 100644 examples/point-of-sale/index-mapinv.rsh create mode 100644 examples/point-of-sale/index-mapinv.txt create mode 100644 examples/point-of-sale/index-tokinv.rsh create mode 100644 examples/point-of-sale/index-tokinv.txt diff --git a/docs/src/guide/invariants/index.md b/docs/src/guide/invariants/index.md index 093d4fb8fd..158db1baed 100644 --- a/docs/src/guide/invariants/index.md +++ b/docs/src/guide/invariants/index.md @@ -318,7 +318,7 @@ range - 33-44 The `{!rsh} parallelReduce` updates the value of `ticketsSold` and the condition is `true` as long as `ticketsSold` is less than the available `supply` of tickets. The `{!rsh} API` calls on the `buyTicket` function, which increments the number of `ticketsSold` and returns the new value. -This program doesn't break after removing the first balance invariant. +This program doesn't break after removing the first balance invariant because the network tokens aren't transferred within the `{!rsh} parallelReduce`. The `{!rsh} parallelReduce` is in a race to sell the non-network tokens. Writing an invariant about the network token balance provides stronger defenses to the program, but is not required for the compiler to complete its formal verification. However, removing the second invariant will cause a violation witness. @@ -365,11 +365,155 @@ This Violation Witness also points to the `{!rsh} parallelReduce` with a similar This example shows that it is critical to understand a non-network token's balance, as well as, the network token's balance. +## All Together Now + +Let's look at one more example that asserts `{!rsh} invariant`s over network tokens, non-network tokens, and a `{!rsh} Map`. + +``` rsh +load: /examples/point-of-sale/index.rsh +md5: 102ed2e3f3a0d59a4f1a5aa5084823cf +range: 26-44 +``` + +This is a point-of-sale Reach application that allows an `{!rsh} API` member to make a purchase or request a refund. +An interesting feature in the point-of-sale application is that it takes in varying cost amounts and stores the inputs in a `{!rsh} Map` which is available to be returned through the refund function. + +You should be able to identify that the `{!rsh} invariant`(s) assert network and, if applicable, non-network balances, the loop condition, and the `{!rsh} Map` size, if applicable. +We also can identify a relationship between the `{!rsh} Map` `{!rsh} invariant` and the `{!rsh} check`. +`{!rsh} Map`s with transfers inside a `{!rsh} parallelReduce` require an `{!rsh} invariant` and a `{!rsh} check`. + +The other two `{!rsh} check`s are defensive. +`check(tokensSold != supply)` on line 34 offers insurance against split-second API calls, and `check(purchasePrice > min)` on line 36 is like a `try catch` to ensure that purchase calls meet the minimum price. + +### Lost Without a Map + +Let's remove each of the invariants and observe the outputs. +First, we remove the `{!rsh} Map` `{!rsh} invariant`: + +``` rsh +load: /examples/point-of-sale/index-mapinv.rsh +md5: 76b0af6be62a70fe1ad5cca2f5f85307 +range: 27-31 +``` + +The verification fails because the compiler cannot confirm that the balance is sufficient for a transfer. + +``` rsh +load: /examples/point-of-sale/index-mapinv.txt +md5: f28ba47027648e7e39b34e44b73cc763 +range: 7-9 +``` + +Failures point to the `{!rsh} api_` refund return object on line 46 and the `{!rsh} transfer` on line 48. + +``` rsh +load: /examples/point-of-sale/index-mapinv.rsh +md5: 76b0af6be62a70fe1ad5cca2f5f85307 +range: 46-48 +``` + +Without the `{!rsh} invariant`, Reach is not able `{!rsh} assert` the size of the `{!rsh} Map`. +When an `{!rsh} API` member attempts to call a refund, the verification engine cannot guarantee that the balance will be sufficient to payout the transfer amount. +It is critical to know the size of a `{!rsh} Map` if it will be used in a `{!rsh} transfer`. + +### Out of Balance + +Removing the balance `{!rsh} invariant` has similar results: + +``` rsh +load: /examples/point-of-sale/index-balinv.rsh +md5: b2c319bf236e4d7ddade29937e162e39 +range: 27-31 +``` + +As we saw before, the verification engine is not able to ensure that the balance is sufficient for a transfer in the `{!rsh} api_`'s refund functionality. + +``` rsh +load: /examples/point-of-sale/index-balinv.txt +md5: 90ef94492eaaae686c052e46a29a9373 +range: 7-9 +``` + +Removing the balance `{!rsh} invariant` causes a second failure point at line 54 when the contract transfers the `total` to the Administrator. + +``` rsh +load: /examples/point-of-sale/index-balinv.txt +md5: 90ef94492eaaae686c052e46a29a9373 +range: 34-35 +``` + +``` rsh +load: /examples/point-of-sale/index-balinv.rsh +md5: b2c319bf236e4d7ddade29937e162e39 +range: 54 +``` + +The third and final error states that the verification engine cannot confirm that the network token balance is zero when the application exits on line 56. + +``` rsh +load: /examples/point-of-sale/index-balinv.txt +md5: 90ef94492eaaae686c052e46a29a9373 +range: 57-58 +``` + +``` rsh +load: /examples/point-of-sale/index-balinv.rsh +md5: b2c319bf236e4d7ddade29937e162e39 +range: 56 +``` + +`{!rsh} invariant`s are always required for balances that will be transferred inside a `{!rsh} parallelReduce`. +Failing to make an `{!rsh} assert`ion over the balance with an `{!rsh} invariant` creates a host of verification errors that could be difficult to resolve without properly understanding the application. + +### Tokens + +For our final example, we remove the non-network token balance `{!rsh} invariant`. + +``` rsh +load: /examples/point-of-sale/index-tokinv.rsh +md5: 2280bcf03c528e31b6c37104786dc927 +range: 27-31 +``` + +We observe that the verification failure message is the same, "balance sufficient for transfer". +However, it fails inside the `{!rsh} api_` purchase functionality. + +``` rsh +load: /examples/point-of-sale/index-tokinv.txt +md5: 557d91780cd2f51743d5b84eca1d7989 +range: 7-9 +``` + +Non-network tokens are transferred on line 39 and the non-network token balance is updated in line 36. + +``` rsh +load: /examples/point-of-sale/index-tokinv.rsh +md5: 2280bcf03c528e31b6c37104786dc927 +range: 36-40 +``` + +Similar to network tokens, transferring non-network tokens within a `{!rsh} parallelReduce` requires an `{!rsh} invariant`. + +Failing to provide the non-network token `{!rsh} invariant` also creates a "balance zero at application exit" error on line 56, which is where the application `{!rsh} exit`s. + +``` rsh +load: /examples/point-of-sale/index-tokinv.txt +md5: 557d91780cd2f51743d5b84eca1d7989 +range: 28-29 +``` + +All tokens must be accounted for when the application is ready to exit. +Reach is not able to confirm balances after exiting a `{!rsh} parallelReduce` without `{!rsh} invariant`s. +If the compiler fails with "balance zero at application exit" then ensure you've created `{!rsh} invariant`s that `{!rsh} assert` the correct equations for network and non-network tokens. + ## Invariably, We Have Learned At this point, we've examined four invariants and how their absence results in Violation Witness errors. This demonstrates how important it is to understand your program before it is time to write `{!rsh} invariant`s. -For more practice, continue to find examples, remove the invariants, and study the resulting compile errors. +You should be prepared to create `{!rsh} invariant`s as soon as you need a `{!rsh} parallelReduce`. + +Learn to quickly identify where your application needs a `{!rsh} parallelReduce` and what `{!rsh} invariant`(s) will be required to correctly `{!rsh} assert` the balance(s) and condition(s). +For more practice, continue to find examples, remove the invariants, and study the compile errors. If you'd like to experiment with invariants in additional examples then I recommend starting with the [NFT-Auction-API](https://github.com/reach-sh/reach-lang/blob/master/examples/nft-auction-api/index.rsh) and the [Chicken-Parallel](https://github.com/reach-sh/reach-lang/blob/master/examples/chicken-parallel/index.rsh) examples. diff --git a/examples/point-of-sale/index-balinv.rsh b/examples/point-of-sale/index-balinv.rsh new file mode 100644 index 0000000000..56ab93e326 --- /dev/null +++ b/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(); +}); + diff --git a/examples/point-of-sale/index-balinv.txt b/examples/point-of-sale/index-balinv.txt new file mode 100644 index 0000000000..43722694e0 --- /dev/null +++ b/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 = ; + // ^ could = [ <- None(null )] + // from: ./index-balinv.rsh:27:45:while + const netBalance/679 = ; + // ^ could = 8025 + // from: ./index-balinv.rsh:27:45:while + const this/760 = ; + // ^ could = + // 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 = ; + // ^ could = 1 + // from: ./index-balinv.rsh:27:45:while + const netBalance/679 = ; + // ^ 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 = ; + // ^ could = 0 + // from: ./index-balinv.rsh:27:45:while + const netBalance/679 = ; + // ^ 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 diff --git a/examples/point-of-sale/index-mapinv.rsh b/examples/point-of-sale/index-mapinv.rsh new file mode 100644 index 0000000000..44774e4b25 --- /dev/null +++ b/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(); +}); + diff --git a/examples/point-of-sale/index-mapinv.txt b/examples/point-of-sale/index-mapinv.txt new file mode 100644 index 0000000000..a4d000b470 --- /dev/null +++ b/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 = ; + // ^ could = [ <- Some(30613 )] + // from: ./index-mapinv.rsh:27:45:while + const netBalance/665 = ; + // ^ could = 30612 + // from: ./index-mapinv.rsh:27:45:while + const this/740 = ; + // ^ could = + // 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 diff --git a/examples/point-of-sale/index-tokinv.rsh b/examples/point-of-sale/index-tokinv.rsh new file mode 100644 index 0000000000..a054d7c383 --- /dev/null +++ b/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(); +}); + diff --git a/examples/point-of-sale/index-tokinv.txt b/examples/point-of-sale/index-tokinv.txt new file mode 100644 index 0000000000..4752ac96b5 --- /dev/null +++ b/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 = ; + // ^ 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 = ; + // ^ 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 From 447abb42e1e3494f851ae0f5749f464f8a46393b Mon Sep 17 00:00:00 2001 From: TheChronicMonster Date: Wed, 9 Nov 2022 02:04:38 -0600 Subject: [PATCH 07/11] docs: v2 guide complete --- docs/src/guide/invariants/index.md | 76 +++++++++----------------- examples/ticket-sales/index-tokinv.rsh | 40 ++++++++++++++ examples/ticket-sales/index-tokinv.txt | 48 ++++++++++++++++ 3 files changed, 113 insertions(+), 51 deletions(-) create mode 100644 examples/ticket-sales/index-tokinv.rsh create mode 100644 examples/ticket-sales/index-tokinv.txt diff --git a/docs/src/guide/invariants/index.md b/docs/src/guide/invariants/index.md index 158db1baed..f781063a5b 100644 --- a/docs/src/guide/invariants/index.md +++ b/docs/src/guide/invariants/index.md @@ -292,27 +292,14 @@ However, Reach cannot guarantee the efficacy of the program because we failed to ## Track/Distribute Supply of Non-Network Tokens Sometimes you may want to write an `{!rsh} assert`ion regarding the supply of non-network tokens. -In the "Ticket Sale DApp" an Administrator issues non-network tokens and Buyer `{!rsh} API`s have the ability to buy the tokens, which are referred to as 'tickets', in this DApp. +In "Ticket Sales" an Administrator issues non-network tokens and Buyer `{!rsh} API`s have the ability to buy the tokens, which are referred to as 'tickets', in this DApp. -The `{!rsh} invariant` in this DApp is interesting because it makes `{!rsh} assert`s over the network token balance (line 34) and the non-network token balance (line 35). +The `{!rsh} invariant` in this DApp is interesting because it makes `{!rsh} assert`s over the network token balance (line 26) and the non-network token balance (line 27). ``` -load - ticket sales -md5 - -range - 33-44 - - const [ticketsSold] = parallelReduce([0]) - .invariant(balance() == amount * ticketsSold) - .invariant(balance(tok) == supply - ticketsSold)errors - .while(ticketsSold < supply) - .api_(B.buyTicket, () => { - return[amount, (ret) => { - transfer(1, tok).to(this); - ret(true); - return [ticketsSold + 1]; - }]; - }); - transfer(balance()).to(A); +load: /examples/ticket-sales +md5: c425745032273893d106fe3de005f15e +range: 25-37 ``` The `{!rsh} parallelReduce` updates the value of `ticketsSold` and the condition is `true` as long as `ticketsSold` is less than the available `supply` of tickets. @@ -323,51 +310,38 @@ The `{!rsh} parallelReduce` is in a race to sell the non-network tokens. Writing an invariant about the network token balance provides stronger defenses to the program, but is not required for the compiler to complete its formal verification. However, removing the second invariant will cause a violation witness. -The critical `{!rsh} invariant` on line 35 and `{!rsh} assert`s that the non-network token balance is equal to the difference of the supply and the number of tickets sold. +The critical `{!rsh} invariant` on line 27 `{!rsh} assert`s that the non-network token balance is equal to the difference of the supply and the number of tickets sold. Once removed, the compiler returns ``` -load - -md5 - -range - - -Verification failed: - when ALL participants are honest - of theorem: assert - msg: "balance sufficient for transfer" - at ./index.rsh:39:28:application - at /app/index.rsh:38:28:application call to [unknown function] (defined at: /app/index.rsh:38:28:function exp) - - // Violation Witness - - const UInt.max = 1; - - const tokenInfos/169 = ; - // ^ could = Array.const(Tuple(UInt, UInt, Bool), [0, 0, false ] ) - // from: ./index.rsh:33:39:while - - // Theorem Formalization - - const v189 = 1 <= tokenInfos/169[0][0]; - // ^ would be false - assert(v189); +load: /examples/ticket-sales/index-tokinv.txt +md5: bcb528856342039ea775659891bc24d0 +range: 4-23 ``` -We see the `balance sufficient for transfer` error, once again. +We see the "balance sufficient for transfer" error, once again. However, instead of referring to a network token transfer, the message is referring to the transfer of a non-network token. -In this example, the message points to the `{!rsh} transfer` on line 39 and the `return` statement on line 38. +In this example, the message points to the `{!rsh} transfer` on line 31 and the `return` statement on line 30. + +The Violation Witness on line 15 shows how the `{!rsh} parallelReduce` could fail, followed by the Theorem Formalization. -The Violation Witness on line XX shows how the `{!rsh} parallelReduce` could fail, followed by the Theorem Formalization. +``` +load: /examples/ticket-sales/index-tokinv.txt +md5: bcb528856342039ea775659891bc24d0 +range: 25-37 +``` -The second verification failure, "balance zero at application exit" indicates that tokens could remain in the contract when it exits on line 45. +The second verification failure, "balance zero at application exit" indicates that tokens could remain in the contract when it exits on line 38. This Violation Witness also points to the `{!rsh} parallelReduce` with a similar example as before. This example shows that it is critical to understand a non-network token's balance, as well as, the network token's balance. +Failing to understand how to `{!rsh} assert` the `{!rsh} invariant`(s) will make it difficult to successfully compile the Reach application. ## All Together Now -Let's look at one more example that asserts `{!rsh} invariant`s over network tokens, non-network tokens, and a `{!rsh} Map`. +Let's look at one more example that asserts `{!rsh} invariant`s over network tokens, non-network tokens, and a `{!rsh} Map`. +At this point, we will have already discussed the error messages so we'll move at a faster pace. ``` rsh load: /examples/point-of-sale/index.rsh @@ -404,7 +378,7 @@ md5: f28ba47027648e7e39b34e44b73cc763 range: 7-9 ``` -Failures point to the `{!rsh} api_` refund return object on line 46 and the `{!rsh} transfer` on line 48. +Failures point to the `{!rsh} API` refund return object on line 46 and the `{!rsh} transfer` on line 48. ``` rsh load: /examples/point-of-sale/index-mapinv.rsh @@ -426,7 +400,7 @@ md5: b2c319bf236e4d7ddade29937e162e39 range: 27-31 ``` -As we saw before, the verification engine is not able to ensure that the balance is sufficient for a transfer in the `{!rsh} api_`'s refund functionality. +As we saw before, the verification engine is not able to ensure that the balance is sufficient for a transfer in the `{!rsh} API`'s refund functionality. ``` rsh load: /examples/point-of-sale/index-balinv.txt @@ -476,7 +450,7 @@ range: 27-31 ``` We observe that the verification failure message is the same, "balance sufficient for transfer". -However, it fails inside the `{!rsh} api_` purchase functionality. +However, it fails inside the `{!rsh} API` purchase functionality. ``` rsh load: /examples/point-of-sale/index-tokinv.txt diff --git a/examples/ticket-sales/index-tokinv.rsh b/examples/ticket-sales/index-tokinv.rsh new file mode 100644 index 0000000000..05f5e77399 --- /dev/null +++ b/examples/ticket-sales/index-tokinv.rsh @@ -0,0 +1,40 @@ +'reach 0.1'; + +export const main = Reach.App(() => { + const A = Participant('Admin', { + params: Object({ + cost: UInt, + tok: Token, + supply: UInt, + }), + launched: Fun([Contract], Null), + }); + const B = API('Buyer', { + buyTicket: Fun([], Null), + }); + init(); + + A.only(() => { + const {cost, tok, supply} = declassify(interact.params); + }); + A.publish(cost, tok, supply); + commit(); + A.pay([[supply, tok]]); + A.interact.launched(getContract()); + + const [ticketsSold] = parallelReduce([0]) + .invariant(balance() == cost * ticketsSold) + .while(ticketsSold < supply) + .api_(B.buyTicket, () => { + check(ticketsSold != supply, "sorry, out of tickets"); + return[cost, (ret) => { + transfer(1, tok).to(this); + ret(null); + return [ticketsSold + 1]; + }]; + }); + transfer(cost * ticketsSold).to(A); + commit(); + exit(); +}); + diff --git a/examples/ticket-sales/index-tokinv.txt b/examples/ticket-sales/index-tokinv.txt new file mode 100644 index 0000000000..bc2f6f4248 --- /dev/null +++ b/examples/ticket-sales/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:31:28:application + at /app/index-tokinv.rsh:30:26:application call to [unknown function] (defined at: /app/index-tokinv.rsh:30:26:function exp) + + // Violation Witness + + const UInt.max = 1; + + const tokenInfos/267 = ; + // ^ could = Array.const(Tuple(UInt, UInt, Bool), [0, 0, false ] ) + // from: ./index-tokinv.rsh:25:39:while + + // Theorem Formalization + + const v299 = 1 <= tokenInfos/267[0][0]; + // ^ would be false + assert(v299); + +Verification failed: + when ALL participants are honest + of theorem: assert + msg: "balance zero at application exit" + at ./index-tokinv.rsh:38:7:application + + // Violation Witness + + const UInt.max = 1; + + const tokenInfos/267 = ; + // ^ could = Array.const(Tuple(UInt, UInt, Bool), [1, 0, false ] ) + // from: ./index-tokinv.rsh:25:39:while + + // Theorem Formalization + + const v323 = 0 == tokenInfos/267[0][0]; + // ^ would be false + assert(v323); + + Verifying when NO participants are honest +Checked 23 theorems; 4 failures (and 2 omitted repeats) :'( + +For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures From 74c098e67a91b58cb823da9269c13b7651fb7eb2 Mon Sep 17 00:00:00 2001 From: TheChronicMonster Date: Wed, 9 Nov 2022 09:10:36 -0600 Subject: [PATCH 08/11] typo --- docs/src/guide/invariants/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/src/guide/invariants/index.md b/docs/src/guide/invariants/index.md index f781063a5b..994a1ed846 100644 --- a/docs/src/guide/invariants/index.md +++ b/docs/src/guide/invariants/index.md @@ -202,7 +202,7 @@ The verification engine is only able to formally verify the things inside a whil By establishing invariants for the condition and the balance the verification engine is able to formally verify the entire application. Without proper invariants the application cannot be formally verified and will fail to compile. -## Invariants in paralellReduce +## Invariants in parallelReduce Let's look at the RSVP application. This DApp is more complicated than the @{seclink("tut")} DApp, but the same principles apply. From 773865dd13cd6fb2881c62333bad3b3dbb23aa3d Mon Sep 17 00:00:00 2001 From: TheChronicMonster Date: Wed, 9 Nov 2022 09:47:37 -0600 Subject: [PATCH 09/11] small edits --- docs/gen.log | 972 ++++++++++++++--------------- docs/src/guide/invariants/index.md | 20 +- 2 files changed, 496 insertions(+), 496 deletions(-) diff --git a/docs/gen.log b/docs/gen.log index 64ff482d3e..2ec4141d83 100644 --- a/docs/gen.log +++ b/docs/gen.log @@ -5,24 +5,6 @@ "isBook": true, "rank": 0 }, - { - "here": "cout", - "title": "Compiled Output", - "isBook": false, - "rank": 60 - }, - { - "here": "index", - "title": "Index", - "isBook": false, - "rank": 140 - }, - { - "here": "rsh", - "title": "Language", - "isBook": false, - "rank": 50 - }, { "here": "build", "title": "Reach is for Builders", @@ -30,16 +12,10 @@ "rank": 5 }, { - "here": "tool", - "title": "Tool", - "isBook": false, - "rank": 40 - }, - { - "here": "search", - "title": "Search", + "here": "cout", + "title": "Compiled Output", "isBook": false, - "rank": 130 + "rank": 60 }, { "here": "frontend", @@ -48,10 +24,16 @@ "rank": 70 }, { - "here": "trouble", - "title": "Troubleshooting", + "here": "changelog", + "title": "Changelog", "isBook": false, - "rank": 115 + "rank": 120 + }, + { + "here": "index", + "title": "Index", + "isBook": false, + "rank": 140 }, { "here": "model", @@ -65,6 +47,24 @@ "isBook": false, "rank": 80 }, + { + "here": "search", + "title": "Search", + "isBook": false, + "rank": 130 + }, + { + "here": "tool", + "title": "Tool", + "isBook": false, + "rank": 40 + }, + { + "here": "rsh", + "title": "Language", + "isBook": false, + "rank": 50 + }, { "here": "tut", "title": "Tutorials", @@ -72,16 +72,16 @@ "rank": 20 }, { - "here": "quickstart", - "title": "Quickstart", + "here": "trouble", + "title": "Troubleshooting", "isBook": false, - "rank": 10 + "rank": 115 }, { - "here": "changelog", - "title": "Changelog", + "here": "quickstart", + "title": "Quickstart", "isBook": false, - "rank": 120 + "rank": 10 }, { "here": "guide", @@ -89,30 +89,48 @@ "isBook": true, "rank": 110 }, - { - "here": "workshop", - "title": "Workshops", - "isBook": true, - "rank": 100 - }, { "here": "rpc", "title": "RPC Server", "isBook": true, "rank": 90 }, + { + "here": "workshop", + "title": "Workshops", + "isBook": true, + "rank": 100 + }, { "here": "rsh/appinit", "title": "Application Initialization", "isBook": false, "rank": 20 }, + { + "here": "rsh/module", + "title": "Modules", + "isBook": false, + "rank": 10 + }, + { + "here": "rsh/consensus", + "title": "Consensus Steps", + "isBook": false, + "rank": 50 + }, { "here": "rsh/local", "title": "Local Steps", "isBook": false, "rank": 40 }, + { + "here": "rsh/step", + "title": "Steps", + "isBook": false, + "rank": 30 + }, { "here": "rsh/compute", "title": "Computations", @@ -126,41 +144,17 @@ "rank": 70 }, { - "here": "rsh/module", - "title": "Modules", - "isBook": false, - "rank": 10 - }, - { - "here": "rsh/step", - "title": "Steps", + "here": "tut/rsvp", + "title": "Répondez S'il Vous Plaît", "isBook": false, "rank": 30 }, - { - "here": "rsh/consensus", - "title": "Consensus Steps", - "isBook": false, - "rank": 50 - }, - { - "here": "tut/rps", - "title": "Rock, Paper, Scissors!", - "isBook": false, - "rank": 20 - }, { "here": "tut/overview", "title": "Overview", "isBook": false, "rank": 10 }, - { - "here": "tut/rsvp", - "title": "Répondez S'il Vous Plaît", - "isBook": false, - "rank": 30 - }, { "here": "tut/wfs", "title": "Wisdom For Sale", @@ -168,46 +162,46 @@ "rank": 18 }, { - "here": "guide/determ", - "title": "Determinism, simultaneity, and choice in decentralized applications", + "here": "tut/rps", + "title": "Rock, Paper, Scissors!", "isBook": false, - "rank": 110 + "rank": 20 }, { - "here": "guide/ctransfers", - "title": "What do the different kinds of consensus transfers mean? publish, pay, race, fork, parallelReduce?", + "here": "guide/editor-support", + "title": "IDE/Text Editor Support", "isBook": false, - "rank": 70 + "rank": 150 }, { - "here": "guide/assert", - "title": "How and what to verify", + "here": "guide/ctransfers", + "title": "What do the different kinds of consensus transfers mean? publish, pay, race, fork, parallelReduce?", "isBook": false, - "rank": 80 + "rank": 70 }, { - "here": "guide/abstract", - "title": "Building decentralized abstractions", + "here": "guide/logging", + "title": "How do I add tracing logs to my Reach program?", "isBook": false, - "rank": 130 + "rank": 50 }, { - "here": "guide/editor-support", - "title": "IDE/Text Editor Support", + "here": "guide/loop-invs", + "title": "Finding and using loop invariants", "isBook": false, - "rank": 150 + "rank": 90 }, { - "here": "guide/lifecycle", - "title": "Contract Development Lifecycle and Best Practices for Building Reach DApps", + "here": "guide/assert", + "title": "How and what to verify", "isBook": false, - "rank": 35 + "rank": 80 }, { - "here": "guide/invariants", - "title": "Writing Invariants", + "here": "guide/determ", + "title": "Determinism, simultaneity, and choice in decentralized applications", "isBook": false, - "rank": 95 + "rank": 110 }, { "here": "guide/ganache", @@ -222,34 +216,28 @@ "rank": 180 }, { - "here": "guide/logging", - "title": "How do I add tracing logs to my Reach program?", - "isBook": false, - "rank": 50 - }, - { - "here": "guide/packages", - "title": "Sharing and discovering shared Reach packages", + "here": "guide/race", + "title": "Racing non-determinism in decentralized applications", "isBook": false, - "rank": 160 + "rank": 120 }, { - "here": "guide/solidity", - "title": "How does Reach development compare to Solidity development?", + "here": "guide/nntoks", + "title": "How do network and non-network tokens differ?", "isBook": false, - "rank": 30 + "rank": 60 }, { - "here": "guide/loop-invs", - "title": "Finding and using loop invariants", + "here": "guide/reach", + "title": "How does Reach work?", "isBook": false, - "rank": 90 + "rank": 170 }, { - "here": "guide/timeout", - "title": "Non-participation: What it is and how to protect against it", + "here": "guide/packages", + "title": "Sharing and discovering shared Reach packages", "isBook": false, - "rank": 100 + "rank": 160 }, { "here": "guide/roadmap", @@ -257,18 +245,6 @@ "isBook": false, "rank": 190 }, - { - "here": "guide/versions", - "title": "How does Reach use version numbers?", - "isBook": false, - "rank": 20 - }, - { - "here": "guide/rpc", - "title": "Do I have to use JavaScript to write my frontend? What about Python, Go, or other languages?", - "isBook": false, - "rank": 40 - }, { "here": "guide/staking", "title": "Example: Staking and Unstaking Tokens", @@ -276,28 +252,22 @@ "rank": 135 }, { - "here": "guide/race", - "title": "Racing non-determinism in decentralized applications", - "isBook": false, - "rank": 120 - }, - { - "here": "guide/reach", - "title": "How does Reach work?", + "here": "guide/lifecycle", + "title": "Contract Development Lifecycle and Best Practices for Building Reach DApps", "isBook": false, - "rank": 170 + "rank": 35 }, { - "here": "guide/testing", - "title": "How should I test a DApp?", + "here": "guide/invariants", + "title": "Writing Invariants", "isBook": false, - "rank": 51 + "rank": 95 }, { - "here": "guide/nntoks", - "title": "How do network and non-network tokens differ?", + "here": "guide/solidity", + "title": "How does Reach development compare to Solidity development?", "isBook": false, - "rank": 60 + "rank": 30 }, { "here": "guide/windows", @@ -306,40 +276,64 @@ "rank": 10 }, { - "here": "workshop/relay", - "title": "Relay Account", + "here": "guide/timeout", + "title": "Non-participation: What it is and how to protect against it", "isBook": false, - "rank": 20 + "rank": 100 }, { - "here": "workshop/fomo-generalized", - "title": "Fear of Missing Out+", + "here": "guide/abstract", + "title": "Building decentralized abstractions", "isBook": false, - "rank": 50 + "rank": 130 }, { - "here": "workshop/hash-lock", - "title": "Hash Lock", + "here": "rpc/go", + "title": "Go", "isBook": false, - "rank": 10 + "rank": 20 }, { - "here": "workshop/trust-fund", - "title": "Trust Fund", + "here": "rpc/cs", + "title": "C#", "isBook": false, - "rank": 30 + "rank": 10 }, { - "here": "workshop/fomo", - "title": "Fear of Missing Out", + "here": "rpc/proto", + "title": "Specification", + "isBook": false, + "rank": 50 + }, + { + "here": "rpc/py", + "title": "Python", "isBook": false, "rank": 40 }, { - "here": "rpc/cs", - "title": "C#", + "here": "rpc/client", + "title": "Client Walkthrough", "isBook": false, - "rank": 10 + "rank": 60 + }, + { + "here": "guide/versions", + "title": "How does Reach use version numbers?", + "isBook": false, + "rank": 20 + }, + { + "here": "guide/rpc", + "title": "Do I have to use JavaScript to write my frontend? What about Python, Go, or other languages?", + "isBook": false, + "rank": 40 + }, + { + "here": "guide/testing", + "title": "How should I test a DApp?", + "isBook": false, + "rank": 51 }, { "here": "rpc/js", @@ -348,29 +342,35 @@ "rank": 30 }, { - "here": "rpc/client", - "title": "Client Walkthrough", + "here": "workshop/hash-lock", + "title": "Hash Lock", "isBook": false, - "rank": 60 + "rank": 10 }, { - "here": "rpc/go", - "title": "Go", + "here": "workshop/relay", + "title": "Relay Account", "isBook": false, "rank": 20 }, { - "here": "rpc/py", - "title": "Python", + "here": "workshop/fomo", + "title": "Fear of Missing Out", "isBook": false, "rank": 40 }, { - "here": "rpc/proto", - "title": "Specification", + "here": "workshop/fomo-generalized", + "title": "Fear of Missing Out+", "isBook": false, "rank": 50 }, + { + "here": "workshop/trust-fund", + "title": "Trust Fund", + "isBook": false, + "rank": 30 + }, { "here": "tut/rps/7-rpc", "title": "Rock, Paper, Scissors in Python", @@ -381,6 +381,16 @@ { "path": [], "children": { + "build": { + "path": [ + "build" + ], + "children": {}, + "here": "build", + "title": "Reach is for Builders", + "isBook": false, + "rank": 5 + }, "cout": { "path": [ "cout" @@ -391,6 +401,26 @@ "isBook": false, "rank": 60 }, + "frontend": { + "path": [ + "frontend" + ], + "children": {}, + "here": "frontend", + "title": "Frontends", + "isBook": false, + "rank": 70 + }, + "changelog": { + "path": [ + "changelog" + ], + "children": {}, + "here": "changelog", + "title": "Changelog", + "isBook": false, + "rank": 120 + }, "index": { "path": [ "index" @@ -401,6 +431,46 @@ "isBook": false, "rank": 140 }, + "model": { + "path": [ + "model" + ], + "children": {}, + "here": "model", + "title": "Model", + "isBook": false, + "rank": 30 + }, + "networks": { + "path": [ + "networks" + ], + "children": {}, + "here": "networks", + "title": "Networks", + "isBook": false, + "rank": 80 + }, + "search": { + "path": [ + "search" + ], + "children": {}, + "here": "search", + "title": "Search", + "isBook": false, + "rank": 130 + }, + "tool": { + "path": [ + "tool" + ], + "children": {}, + "here": "tool", + "title": "Tool", + "isBook": false, + "rank": 40 + }, "rsh": { "path": [ "rsh" @@ -417,71 +487,71 @@ "isBook": false, "rank": 20 }, - "local": { + "module": { "path": [ "rsh", - "local" + "module" ], "children": {}, - "here": "rsh/local", - "title": "Local Steps", + "here": "rsh/module", + "title": "Modules", "isBook": false, - "rank": 40 + "rank": 10 }, - "compute": { + "consensus": { "path": [ "rsh", - "compute" + "consensus" ], "children": {}, - "here": "rsh/compute", - "title": "Computations", + "here": "rsh/consensus", + "title": "Consensus Steps", "isBook": false, - "rank": 60 + "rank": 50 }, - "errors": { + "local": { "path": [ "rsh", - "errors" + "local" ], "children": {}, - "here": "rsh/errors", - "title": "Error Codes", + "here": "rsh/local", + "title": "Local Steps", "isBook": false, - "rank": 70 + "rank": 40 }, - "module": { + "step": { "path": [ "rsh", - "module" + "step" ], "children": {}, - "here": "rsh/module", - "title": "Modules", + "here": "rsh/step", + "title": "Steps", "isBook": false, - "rank": 10 + "rank": 30 }, - "step": { + "compute": { "path": [ "rsh", - "step" + "compute" ], "children": {}, - "here": "rsh/step", - "title": "Steps", + "here": "rsh/compute", + "title": "Computations", "isBook": false, - "rank": 30 + "rank": 60 }, - "consensus": { + "errors": { "path": [ "rsh", - "consensus" + "errors" ], "children": {}, - "here": "rsh/consensus", - "title": "Consensus Steps", + "here": "rsh/errors", + "title": "Error Codes", "isBook": false, - "rank": 50 + "rank": 70 } }, "here": "rsh", @@ -489,104 +559,21 @@ "isBook": false, "rank": 50 }, - "build": { - "path": [ - "build" - ], - "children": {}, - "here": "build", - "title": "Reach is for Builders", - "isBook": false, - "rank": 5 - }, - "tool": { - "path": [ - "tool" - ], - "children": {}, - "here": "tool", - "title": "Tool", - "isBook": false, - "rank": 40 - }, - "search": { - "path": [ - "search" - ], - "children": {}, - "here": "search", - "title": "Search", - "isBook": false, - "rank": 130 - }, - "frontend": { - "path": [ - "frontend" - ], - "children": {}, - "here": "frontend", - "title": "Frontends", - "isBook": false, - "rank": 70 - }, - "trouble": { - "path": [ - "trouble" - ], - "children": {}, - "here": "trouble", - "title": "Troubleshooting", - "isBook": false, - "rank": 115 - }, - "model": { - "path": [ - "model" - ], - "children": {}, - "here": "model", - "title": "Model", - "isBook": false, - "rank": 30 - }, - "networks": { - "path": [ - "networks" - ], - "children": {}, - "here": "networks", - "title": "Networks", - "isBook": false, - "rank": 80 - }, "tut": { "path": [ "tut" ], "children": { - "rps": { + "rsvp": { "path": [ "tut", - "rps" + "rsvp" ], - "children": { - "7-rpc": { - "path": [ - "tut", - "rps", - "7-rpc" - ], - "children": {}, - "here": "tut/rps/7-rpc", - "title": "Rock, Paper, Scissors in Python", - "isBook": false, - "rank": 10 - } - }, - "here": "tut/rps", - "title": "Rock, Paper, Scissors!", + "children": {}, + "here": "tut/rsvp", + "title": "Répondez S'il Vous Plaît", "isBook": false, - "rank": 20 + "rank": 30 }, "overview": { "path": [ @@ -599,17 +586,6 @@ "isBook": false, "rank": 10 }, - "rsvp": { - "path": [ - "tut", - "rsvp" - ], - "children": {}, - "here": "tut/rsvp", - "title": "Répondez S'il Vous Plaît", - "isBook": false, - "rank": 30 - }, "wfs": { "path": [ "tut", @@ -620,6 +596,30 @@ "title": "Wisdom For Sale", "isBook": false, "rank": 18 + }, + "rps": { + "path": [ + "tut", + "rps" + ], + "children": { + "7-rpc": { + "path": [ + "tut", + "rps", + "7-rpc" + ], + "children": {}, + "here": "tut/rps/7-rpc", + "title": "Rock, Paper, Scissors in Python", + "isBook": false, + "rank": 10 + } + }, + "here": "tut/rps", + "title": "Rock, Paper, Scissors!", + "isBook": false, + "rank": 20 } }, "here": "tut", @@ -627,41 +627,41 @@ "isBook": false, "rank": 20 }, - "quickstart": { + "trouble": { "path": [ - "quickstart" + "trouble" ], "children": {}, - "here": "quickstart", - "title": "Quickstart", + "here": "trouble", + "title": "Troubleshooting", "isBook": false, - "rank": 10 + "rank": 115 }, - "changelog": { + "quickstart": { "path": [ - "changelog" + "quickstart" ], "children": {}, - "here": "changelog", - "title": "Changelog", + "here": "quickstart", + "title": "Quickstart", "isBook": false, - "rank": 120 + "rank": 10 }, "guide": { "path": [ "guide" ], "children": { - "determ": { + "editor-support": { "path": [ "guide", - "determ" + "editor-support" ], "children": {}, - "here": "guide/determ", - "title": "Determinism, simultaneity, and choice in decentralized applications", + "here": "guide/editor-support", + "title": "IDE/Text Editor Support", "isBook": false, - "rank": 110 + "rank": 150 }, "ctransfers": { "path": [ @@ -674,6 +674,28 @@ "isBook": false, "rank": 70 }, + "logging": { + "path": [ + "guide", + "logging" + ], + "children": {}, + "here": "guide/logging", + "title": "How do I add tracing logs to my Reach program?", + "isBook": false, + "rank": 50 + }, + "loop-invs": { + "path": [ + "guide", + "loop-invs" + ], + "children": {}, + "here": "guide/loop-invs", + "title": "Finding and using loop invariants", + "isBook": false, + "rank": 90 + }, "assert": { "path": [ "guide", @@ -685,93 +707,126 @@ "isBook": false, "rank": 80 }, - "abstract": { + "determ": { "path": [ "guide", - "abstract" + "determ" ], "children": {}, - "here": "guide/abstract", - "title": "Building decentralized abstractions", + "here": "guide/determ", + "title": "Determinism, simultaneity, and choice in decentralized applications", "isBook": false, - "rank": 130 + "rank": 110 }, - "editor-support": { + "ganache": { "path": [ "guide", - "editor-support" + "ganache" ], "children": {}, - "here": "guide/editor-support", - "title": "IDE/Text Editor Support", + "here": "guide/ganache", + "title": "How to use Ganache with Reach", "isBook": false, - "rank": 150 + "rank": 140 }, - "lifecycle": { + "limits": { "path": [ "guide", - "lifecycle" + "limits" ], "children": {}, - "here": "guide/lifecycle", - "title": "Contract Development Lifecycle and Best Practices for Building Reach DApps", + "here": "guide/limits", + "title": "What are Reach's limitations?", "isBook": false, - "rank": 35 + "rank": 180 }, - "invariants": { + "race": { "path": [ "guide", - "invariants" + "race" ], "children": {}, - "here": "guide/invariants", - "title": "Writing Invariants", + "here": "guide/race", + "title": "Racing non-determinism in decentralized applications", "isBook": false, - "rank": 95 + "rank": 120 }, - "ganache": { + "nntoks": { "path": [ "guide", - "ganache" + "nntoks" ], "children": {}, - "here": "guide/ganache", - "title": "How to use Ganache with Reach", + "here": "guide/nntoks", + "title": "How do network and non-network tokens differ?", "isBook": false, - "rank": 140 + "rank": 60 }, - "limits": { + "reach": { + "path": [ + "guide", + "reach" + ], + "children": {}, + "here": "guide/reach", + "title": "How does Reach work?", + "isBook": false, + "rank": 170 + }, + "packages": { + "path": [ + "guide", + "packages" + ], + "children": {}, + "here": "guide/packages", + "title": "Sharing and discovering shared Reach packages", + "isBook": false, + "rank": 160 + }, + "roadmap": { + "path": [ + "guide", + "roadmap" + ], + "children": {}, + "here": "guide/roadmap", + "title": "Reach's Roadmap", + "isBook": false, + "rank": 190 + }, + "staking": { "path": [ "guide", - "limits" + "staking" ], "children": {}, - "here": "guide/limits", - "title": "What are Reach's limitations?", + "here": "guide/staking", + "title": "Example: Staking and Unstaking Tokens", "isBook": false, - "rank": 180 + "rank": 135 }, - "logging": { + "lifecycle": { "path": [ "guide", - "logging" + "lifecycle" ], "children": {}, - "here": "guide/logging", - "title": "How do I add tracing logs to my Reach program?", + "here": "guide/lifecycle", + "title": "Contract Development Lifecycle and Best Practices for Building Reach DApps", "isBook": false, - "rank": 50 + "rank": 35 }, - "packages": { + "invariants": { "path": [ "guide", - "packages" + "invariants" ], "children": {}, - "here": "guide/packages", - "title": "Sharing and discovering shared Reach packages", + "here": "guide/invariants", + "title": "Writing Invariants", "isBook": false, - "rank": 160 + "rank": 95 }, "solidity": { "path": [ @@ -784,16 +839,16 @@ "isBook": false, "rank": 30 }, - "loop-invs": { + "windows": { "path": [ "guide", - "loop-invs" + "windows" ], "children": {}, - "here": "guide/loop-invs", - "title": "Finding and using loop invariants", + "here": "guide/windows", + "title": "Using Reach on Windows", "isBook": false, - "rank": 90 + "rank": 10 }, "timeout": { "path": [ @@ -806,16 +861,16 @@ "isBook": false, "rank": 100 }, - "roadmap": { + "abstract": { "path": [ "guide", - "roadmap" + "abstract" ], "children": {}, - "here": "guide/roadmap", - "title": "Reach's Roadmap", + "here": "guide/abstract", + "title": "Building decentralized abstractions", "isBook": false, - "rank": 190 + "rank": 130 }, "versions": { "path": [ @@ -839,39 +894,6 @@ "isBook": false, "rank": 40 }, - "staking": { - "path": [ - "guide", - "staking" - ], - "children": {}, - "here": "guide/staking", - "title": "Example: Staking and Unstaking Tokens", - "isBook": false, - "rank": 135 - }, - "race": { - "path": [ - "guide", - "race" - ], - "children": {}, - "here": "guide/race", - "title": "Racing non-determinism in decentralized applications", - "isBook": false, - "rank": 120 - }, - "reach": { - "path": [ - "guide", - "reach" - ], - "children": {}, - "here": "guide/reach", - "title": "How does Reach work?", - "isBook": false, - "rank": 170 - }, "testing": { "path": [ "guide", @@ -882,28 +904,6 @@ "title": "How should I test a DApp?", "isBook": false, "rank": 51 - }, - "nntoks": { - "path": [ - "guide", - "nntoks" - ], - "children": {}, - "here": "guide/nntoks", - "title": "How do network and non-network tokens differ?", - "isBook": false, - "rank": 60 - }, - "windows": { - "path": [ - "guide", - "windows" - ], - "children": {}, - "here": "guide/windows", - "title": "Using Reach on Windows", - "isBook": false, - "rank": 10 } }, "here": "guide", @@ -911,87 +911,65 @@ "isBook": true, "rank": 110 }, - "workshop": { + "rpc": { "path": [ - "workshop" + "rpc" ], "children": { - "relay": { + "go": { "path": [ - "workshop", - "relay" + "rpc", + "go" ], "children": {}, - "here": "workshop/relay", - "title": "Relay Account", + "here": "rpc/go", + "title": "Go", "isBook": false, "rank": 20 }, - "fomo-generalized": { - "path": [ - "workshop", - "fomo-generalized" - ], - "children": {}, - "here": "workshop/fomo-generalized", - "title": "Fear of Missing Out+", - "isBook": false, - "rank": 50 - }, - "hash-lock": { + "cs": { "path": [ - "workshop", - "hash-lock" + "rpc", + "cs" ], "children": {}, - "here": "workshop/hash-lock", - "title": "Hash Lock", + "here": "rpc/cs", + "title": "C#", "isBook": false, "rank": 10 }, - "trust-fund": { + "proto": { "path": [ - "workshop", - "trust-fund" + "rpc", + "proto" ], "children": {}, - "here": "workshop/trust-fund", - "title": "Trust Fund", + "here": "rpc/proto", + "title": "Specification", "isBook": false, - "rank": 30 + "rank": 50 }, - "fomo": { + "py": { "path": [ - "workshop", - "fomo" + "rpc", + "py" ], "children": {}, - "here": "workshop/fomo", - "title": "Fear of Missing Out", + "here": "rpc/py", + "title": "Python", "isBook": false, "rank": 40 - } - }, - "here": "workshop", - "title": "Workshops", - "isBook": true, - "rank": 100 - }, - "rpc": { - "path": [ - "rpc" - ], - "children": { - "cs": { + }, + "client": { "path": [ "rpc", - "cs" + "client" ], "children": {}, - "here": "rpc/cs", - "title": "C#", + "here": "rpc/client", + "title": "Client Walkthrough", "isBook": false, - "rank": 10 + "rank": 60 }, "js": { "path": [ @@ -1003,56 +981,78 @@ "title": "JavaScript", "isBook": false, "rank": 30 - }, - "client": { + } + }, + "here": "rpc", + "title": "RPC Server", + "isBook": true, + "rank": 90 + }, + "workshop": { + "path": [ + "workshop" + ], + "children": { + "hash-lock": { "path": [ - "rpc", - "client" + "workshop", + "hash-lock" ], "children": {}, - "here": "rpc/client", - "title": "Client Walkthrough", + "here": "workshop/hash-lock", + "title": "Hash Lock", "isBook": false, - "rank": 60 + "rank": 10 }, - "go": { + "relay": { "path": [ - "rpc", - "go" + "workshop", + "relay" ], "children": {}, - "here": "rpc/go", - "title": "Go", + "here": "workshop/relay", + "title": "Relay Account", "isBook": false, "rank": 20 }, - "py": { + "fomo": { "path": [ - "rpc", - "py" + "workshop", + "fomo" ], "children": {}, - "here": "rpc/py", - "title": "Python", + "here": "workshop/fomo", + "title": "Fear of Missing Out", "isBook": false, "rank": 40 }, - "proto": { + "fomo-generalized": { "path": [ - "rpc", - "proto" + "workshop", + "fomo-generalized" ], "children": {}, - "here": "rpc/proto", - "title": "Specification", + "here": "workshop/fomo-generalized", + "title": "Fear of Missing Out+", "isBook": false, "rank": 50 + }, + "trust-fund": { + "path": [ + "workshop", + "trust-fund" + ], + "children": {}, + "here": "workshop/trust-fund", + "title": "Trust Fund", + "isBook": false, + "rank": 30 } }, - "here": "rpc", - "title": "RPC Server", + "here": "workshop", + "title": "Workshops", "isBook": true, - "rank": 90 + "rank": 100 } }, "here": "", diff --git a/docs/src/guide/invariants/index.md b/docs/src/guide/invariants/index.md index 994a1ed846..562921d9fa 100644 --- a/docs/src/guide/invariants/index.md +++ b/docs/src/guide/invariants/index.md @@ -114,7 +114,7 @@ md5: fa159888f678f8f5057e5564e8f319c1 range: 21-25 ``` -Essentially, this theorem representation shows that the balance would not be equal to two times the wager amount. For a deeper study on Theorem Formalization, read our guide, @{seclink("how-to-read-verification-failures")}). +Essentially, this theorem representation shows that the balance would not be equal to two times the wager amount. For a deeper study on Theorem Formalization, read our guide, @{seclink("how-to-read-verification-failures")}. If you didn't already know that the balance was failing in the while loop then you'd want to investigate the lines that the Violation Witness points to. @@ -150,7 +150,7 @@ We'll see that the `{!rsh} invariant` should `{!rsh} assert` the balance, loop c We'll continue to explore this pattern for writing invariants. We've examined an `{!rsh} invariant` for asserting the `balance`. -Now we'll review an `${!rsh} invariant` that asserts the loop's condition. +Now we'll review an `{!rsh} invariant` that asserts the loop's condition. ### Condition Invariant @@ -216,7 +216,7 @@ range: 44-54 ``` In RSVP, the `{!rsh} parallelReduce` tracks two constants, `done` and `howMany`. -The first invariant on line 49 asserts that the size of the `{!rsh} Map`, `Guests`, is equal to `howMany`. +The first invariant on line 49 asserts that the size of `{!rsh} Map` `Guests` is equal to `howMany`. If we remove this invariant, the compiler will not be able to verify that the size of the Guestbook is the same as how many guests have reserved or checked in. ### Map Invariant @@ -287,17 +287,17 @@ range: 44-46 Balance errors indicate the need to recalculate the balance's formula or identify missing assumptions about the program. In this case, the balance is equal to the product of `howMany` guests completed a reservation and the reservation fee. -However, Reach cannot guarantee the efficacy of the program because we failed to `{!rsh} assert` the balance's formula in the invariant. +However, Reach cannot guarantee the efficacy of the program because we failed to `{!rsh} assert` the balance's formula in the `{!rsh} invariant`. -## Track/Distribute Supply of Non-Network Tokens +## Distribute Supply of Non-Network Tokens Sometimes you may want to write an `{!rsh} assert`ion regarding the supply of non-network tokens. -In "Ticket Sales" an Administrator issues non-network tokens and Buyer `{!rsh} API`s have the ability to buy the tokens, which are referred to as 'tickets', in this DApp. +In _Ticket Sales_ an Administrator issues non-network tokens and Buyer `{!rsh} API`s have the ability to buy the tokens, which are referred to as 'tickets', in this DApp. The `{!rsh} invariant` in this DApp is interesting because it makes `{!rsh} assert`s over the network token balance (line 26) and the non-network token balance (line 27). ``` -load: /examples/ticket-sales +load: /examples/ticket-sales/index.rsh md5: c425745032273893d106fe3de005f15e range: 25-37 ``` @@ -433,7 +433,7 @@ range: 57-58 ``` rsh load: /examples/point-of-sale/index-balinv.rsh md5: b2c319bf236e4d7ddade29937e162e39 -range: 56 +range: 56-56 ``` `{!rsh} invariant`s are always required for balances that will be transferred inside a `{!rsh} parallelReduce`. @@ -491,10 +491,10 @@ For more practice, continue to find examples, remove the invariants, and study t If you'd like to experiment with invariants in additional examples then I recommend starting with the [NFT-Auction-API](https://github.com/reach-sh/reach-lang/blob/master/examples/nft-auction-api/index.rsh) and the [Chicken-Parallel](https://github.com/reach-sh/reach-lang/blob/master/examples/chicken-parallel/index.rsh) examples. -This can be a good way of developing a sense of when and how to use invariants. +This can be a good way of developing a sense of when and how to use `{!rsh} invariant`s. Common error messages you may see are "balance zero at application exit" and "balance sufficient for transfer". If you see these errors in your applications, take time to consider the formula of the balance in your application. Seek to identify a mathematical relationship between loop conditions and the balance. -You should now have a better understanding of how to write invariants and their importance in developing secure Reach DApps. +You should now have a better understanding of how to write `{!rsh} invariant`s and their importance in developing secure Reach DApps. If you need additional advice for your DApp, reach out in our [Discord](@{DISCORD}). \ No newline at end of file From 5672571d21b788f99b9d0be23b7eb6e311905e49 Mon Sep 17 00:00:00 2001 From: TheChronicMonster Date: Wed, 9 Nov 2022 11:15:30 -0600 Subject: [PATCH 10/11] refactor: failing tests --- hs/test/Reach/Test_Compiler.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/hs/test/Reach/Test_Compiler.hs b/hs/test/Reach/Test_Compiler.hs index bcc336588a..1a5abf6e07 100644 --- a/hs/test/Reach/Test_Compiler.hs +++ b/hs/test/Reach/Test_Compiler.hs @@ -104,6 +104,9 @@ test_examples = goldenTests "../examples" f [ "./pkg/index.rsh" , "./pkg/local.rsh" , "./pkg/index-master.rsh" + , "./point-of-sale/index-balinv.rsh" + , "./point-of-sale/index-mapinv.rsh" + , "./point-of-sale/index-tokinv.rsh" , "./rps-4-attack/index-bad.rsh" , "./rps-4-attack/index-fails.rsh" , "./rps-7-loops/index-balinv.rsh" @@ -112,6 +115,7 @@ test_examples = goldenTests "../examples" f , "./rsvp-5-cede/index-fail.rsh" , "./rsvp-6-vevt/index-balinv.rsh" , "./rsvp-6-vevt/index-mapinv.rsh" + , "./ticket-sales/index-tokinv.rsh" ] f fp = case S.member fp fails of From 2884acef1f1e03e22f2b2b5b70642db0d324baac Mon Sep 17 00:00:00 2001 From: TheChronicMonster Date: Wed, 16 Nov 2022 09:52:18 -0600 Subject: [PATCH 11/11] update: rps rpc index.txt --- examples/rps-7-rpc/server/index.txt | 1 - 1 file changed, 1 deletion(-) diff --git a/examples/rps-7-rpc/server/index.txt b/examples/rps-7-rpc/server/index.txt index 7a3562f458..17663cd197 100644 --- a/examples/rps-7-rpc/server/index.txt +++ b/examples/rps-7-rpc/server/index.txt @@ -1,4 +1,3 @@ -Compiling `main`... Verifying knowledge assertions Verifying for generic connector Verifying when ALL participants are honest