digital-asset/daml
1
1
Fork 0
mirror of https://github.com/digital-asset/daml.git synced 2024-09-20 01:07:18 +03:00
Code Issues Projects Releases Wiki Activity

Verification of the Contract State Machine in UCK mode (#17293) (#17312)

Browse Source 
PR of Andrea Gilot's work from #17293

---------

Co-authored-by: Andrea Gilot <126685183+andreagilot-da@users.noreply.github.com>
This commit is contained in:
Carl Pulley 2023-08-29 20:46:01 +01:00 committed by GitHub
parent 0fc92a34d3
commit 62c9864514
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
37 changed files with 16548 additions and 85 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
canton_dep.bzl
View File

@ -2,7 +2,7 @@
# SPDX-License-Identifier: Apache-2.0
canton = {
"sha": "bc2fd1611ffbc3b990909743f3d6dd9e98af071e5de00f6f54719b76c852fdbd",
"url": "https://www.canton.io/releases/canton-open-source-2.8.0-snapshot.20230828.11069.0.v0819eb02.tar.gz",
"sha": "9cf983138e0a579b9cc713c6b0cd971c76be9c34031c2218f0fcecf4678d7580",
"url": "https://www.canton.io/releases/canton-open-source-2.8.0-snapshot.20230829.11082.0.v69754d9b.tar.gz",
"local": False,
}

6
daml-lf/interpreter/src/main/scala/com/digitalasset/daml/lf/transaction/PartialTransaction.scala
View File

@ -187,7 +187,7 @@ private[lf] object PartialTransaction {
nodes = HashMap.empty,
actionNodeSeeds = BackStack.empty,
context = Context(initialSeeds, committers),
contractState = new ContractStateMachine[NodeId](contractKeyUniqueness).initial,
contractState = ContractStateMachine.initial[NodeId](contractKeyUniqueness),
actionNodeLocations = BackStack.empty,
authorizationChecker = authorizationChecker,
)
@ -221,7 +221,7 @@ private[speedy] case class PartialTransaction(
nodes: HashMap[NodeId, Node],
actionNodeSeeds: BackStack[crypto.Hash],
context: PartialTransaction.Context,
contractState: ContractStateMachine[NodeId]#State,
contractState: ContractStateMachine.State[NodeId],
actionNodeLocations: BackStack[Option[Location]],
authorizationChecker: AuthorizationChecker,
) {
@ -652,7 +652,7 @@ private[speedy] case class PartialTransaction(
node: Node.LeafOnlyAction,
version: TxVersion,
optLocation: Option[Location],
newContractState: ContractStateMachine[NodeId]#State,
newContractState: ContractStateMachine.State[NodeId],
): PartialTransaction = {
val _ = version
val nid = NodeId(nextNodeIdx)

121
daml-lf/transaction/src/main/scala/com/digitalasset/daml/lf/transaction/ContractStateMachine.scala
View File

@ -31,10 +31,7 @@ import com.daml.lf.value.Value.ContractId
* [[com.daml.lf.transaction.ContractKeyUniquenessMode.Strict]] and
* @see ContractStateMachineSpec.visitSubtree for iteration in all modes
*/
class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
import ContractStateMachine._
def initial: State = State.empty
object ContractStateMachine {
/** @param locallyCreated
* Tracks all contracts created by a node processed so far (including nodes under a rollback).
@ -82,11 +79,12 @@ class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
* keyset are in [[activeState]].[[ActiveLedgerState.keys]],
* and similarly for all [[ActiveLedgerState]]s in [[rollbackStack]].
*/
case class State private (
case class State[Nid] private[lf] (
locallyCreated: Set[ContractId],
globalKeyInputs: Map[GlobalKey, KeyInput],
activeState: ActiveLedgerState[Nid],
rollbackStack: List[ActiveLedgerState[Nid]],
activeState: ContractStateMachine.ActiveLedgerState[Nid],
rollbackStack: List[ContractStateMachine.ActiveLedgerState[Nid]],
mode: ContractKeyUniquenessMode,
) {
/** The return value indicates if the given contract is either consumed, inactive, or otherwise
@ -106,8 +104,6 @@ class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
}
}
def mode: ContractKeyUniquenessMode = ContractStateMachine.this.mode
/** Lookup the given key k. Returns
* - Some(KeyActive(cid)) if k maps to cid and cid is active.
* - Some(KeyInactive) if there is no active contract with the given key.
@ -124,13 +120,13 @@ class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
}
/** Visit a create node */
def handleCreate(node: Node.Create): Either[KeyInputError, State] =
def handleCreate(node: Node.Create): Either[KeyInputError, State[Nid]] =
visitCreate(node.coid, node.gkeyOpt).left.map(Right(_))
private[lf] def visitCreate(
contractId: ContractId,
mbKey: Option[GlobalKey],
): Either[DuplicateContractKey, State] = {
): Either[DuplicateContractKey, State[Nid]] = {
val me =
this.copy(
locallyCreated = locallyCreated + contractId,
@ -160,7 +156,7 @@ class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
}
}
def handleExercise(nid: Nid, exe: Node.Exercise): Either[KeyInputError, State] =
def handleExercise(nid: Nid, exe: Node.Exercise): Either[KeyInputError, State[Nid]] =
visitExercise(
nid,
exe.targetCoid,
@ -180,7 +176,7 @@ class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
mbKey: Option[GlobalKey],
byKey: Boolean,
consuming: Boolean,
): Either[InconsistentContractKey, State] = {
): Either[InconsistentContractKey, State[Nid]] = {
for {
state <-
if (byKey || mode == ContractKeyUniquenessMode.Strict)
@ -197,7 +193,7 @@ class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
/** Must be used to handle lookups iff in [[com.daml.lf.transaction.ContractKeyUniquenessMode.Strict]] mode
*/
def handleLookup(lookup: Node.LookupByKey): Either[KeyInputError, State] = {
def handleLookup(lookup: Node.LookupByKey): Either[KeyInputError, State[Nid]] = {
// If the key has not yet been resolved, we use the resolution from the lookup node,
// but this only makes sense if `activeState.keys` is updated by every node and not only by by-key nodes.
if (mode != ContractKeyUniquenessMode.Strict)
@ -221,7 +217,7 @@ class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
def handleLookupWith(
lookup: Node.LookupByKey,
keyInput: Option[ContractId],
): Either[KeyInputError, State] = {
): Either[KeyInputError, State[Nid]] = {
if (mode != ContractKeyUniquenessMode.Off)
throw new UnsupportedOperationException(
"handleLookupWith can only be used if only by-key nodes are considered"
@ -233,7 +229,7 @@ class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
gk: GlobalKey,
keyInput: Option[ContractId],
keyResolution: Option[ContractId],
): Either[InconsistentContractKey, State] = {
): Either[InconsistentContractKey, State[Nid]] = {
val (keyMapping, next) = resolveKey(gk) match {
case Right(result) => result
case Left(handle) => handle(keyInput)
@ -247,13 +243,13 @@ class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
private[lf] def resolveKey(
gkey: GlobalKey
): Either[Option[ContractId] => (KeyMapping, State), (KeyMapping, State)] = {
): Either[Option[ContractId] => (KeyMapping, State[Nid]), (KeyMapping, State[Nid])] = {
lookupActiveKey(gkey) match {
case Some(keyMapping) => Right(keyMapping -> this)
case None =>
// if we cannot find it here, send help, and make sure to update keys after
// that.
def handleResult(result: Option[ContractId]): (KeyMapping, State) = {
def handleResult(result: Option[ContractId]): (KeyMapping, State[Nid]) = {
// Update key inputs. Create nodes never call this method,
// so NegativeKeyLookup is the right choice for the global key input.
val keyInput = result match {
@ -273,23 +269,23 @@ class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
}
}
def handleFetch(node: Node.Fetch): Either[KeyInputError, State] =
def handleFetch(node: Node.Fetch): Either[KeyInputError, State[Nid]] =
visitFetch(node.coid, node.gkeyOpt, node.byKey).left.map(Left(_))
private[lf] def visitFetch(
contractId: ContractId,
mbKey: Option[GlobalKey],
byKey: Boolean,
): Either[InconsistentContractKey, State] =
): Either[InconsistentContractKey, State[Nid]] =
if (byKey || mode == ContractKeyUniquenessMode.Strict)
assertKeyMapping(contractId, mbKey)
else
Right(this)
private[this] def assertKeyMapping(
private[lf] def assertKeyMapping(
cid: Value.ContractId,
mbKey: Option[GlobalKey],
): Either[InconsistentContractKey, State] =
): Either[InconsistentContractKey, State[Nid]] =
mbKey match {
case None => Right(this)
case Some(gk) =>
@ -309,7 +305,7 @@ class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
id: Nid,
node: Node.Action,
keyInput: => Option[ContractId],
): Either[KeyInputError, State] = node match {
): Either[KeyInputError, State[Nid]] = node match {
case create: Node.Create => handleCreate(create)
case fetch: Node.Fetch => handleFetch(fetch)
case lookup: Node.LookupByKey =>
@ -324,13 +320,13 @@ class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
/** To be called when interpretation enters a try block or iteration enters a Rollback node
* Must be matched by [[endRollback]] or [[dropRollback]].
*/
def beginRollback(): State =
this.copy(rollbackStack = activeState +: rollbackStack)
def beginRollback(): State[Nid] =
this.copy(rollbackStack = activeState :: rollbackStack)
/** To be called when interpretation does insert a Rollback node or iteration leaves a Rollback node.
* Must be matched by a [[beginRollback]].
*/
def endRollback(): State = rollbackStack match {
def endRollback(): State[Nid] = rollbackStack match {
case Nil => throw new IllegalStateException("Not inside a rollback scope")
case headState :: tailStack => this.copy(activeState = headState, rollbackStack = tailStack)
}
@ -338,12 +334,12 @@ class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
/** To be called if interpretation notices that a try block did not lead to a Rollback node
* Must be matched by a [[beginRollback]].
*/
def dropRollback(): State = rollbackStack match {
def dropRollback(): State[Nid] = rollbackStack match {
case Nil => throw new IllegalStateException("Not inside a rollback scope")
case _ :: tailStack => this.copy(rollbackStack = tailStack)
}
private def withinRollbackScope: Boolean = rollbackStack.nonEmpty
private[lf] def withinRollbackScope: Boolean = rollbackStack.nonEmpty
/** Let `this` state be the result of iterating over a transaction `tx` until just before a node `n`.
* Let `substate` be the state obtained after fully iterating over the subtree rooted at `n`
@ -368,28 +364,32 @@ class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
* [[com.daml.lf.transaction.ContractKeyUniquenessMode.Strict]] and
* @see ContractStateMachineSpec.visitSubtree for iteration in all modes
*/
def advance(resolver: KeyResolver, substate: State): Either[KeyInputError, State] = {
def advance(resolver: KeyResolver, substate: State[Nid]): Either[KeyInputError, State[Nid]] = {
require(
!substate.withinRollbackScope,
"Cannot lift a state over a substate with unfinished rollback scopes",
)
// We want consistent key lookups within an action in any contract key mode.
def consistentGlobalKeyInputs: Either[KeyInputError, Unit] = {
def consistentGlobalKeyInputs: Either[KeyInputError, Unit] =
substate.globalKeyInputs
.collectFirst {
case (key, KeyCreate)
if lookupActiveKey(key).exists(_ != KeyInactive) &&
mode == ContractKeyUniquenessMode.Strict =>
Right(DuplicateContractKey(key))
case (key, NegativeKeyLookup) if lookupActiveKey(key).exists(_ != KeyInactive) =>
Left(InconsistentContractKey(key))
case (key, Transaction.KeyActive(cid))
if lookupActiveKey(key).exists(_ != KeyActive(cid)) =>
Left(InconsistentContractKey(key))
}
.toLeft(())
}
.find {
case (key, KeyCreate) =>
lookupActiveKey(key).exists(
_ != KeyInactive
) && mode == ContractKeyUniquenessMode.Strict
case (key, NegativeKeyLookup) => lookupActiveKey(key).exists(_ != KeyInactive)
case (key, Transaction.KeyActive(cid)) =>
lookupActiveKey(key).exists(_ != KeyActive(cid))
case _ => false
} match {
case Some((key, KeyCreate)) => Left[KeyInputError, Unit](Right(DuplicateContractKey(key)))
case Some((key, NegativeKeyLookup)) =>
Left[KeyInputError, Unit](Left(InconsistentContractKey(key)))
case Some((key, Transaction.KeyActive(_))) =>
Left[KeyInputError, Unit](Left(InconsistentContractKey(key)))
case _ => Right[KeyInputError, Unit](())
}
for {
_ <- consistentGlobalKeyInputs
@ -446,11 +446,16 @@ class ContractStateMachine[Nid](mode: ContractKeyUniquenessMode) {
}
object State {
val empty: State = new State(Set.empty, Map.empty, ActiveLedgerState.empty, List.empty)
def empty[Nid](mode: ContractKeyUniquenessMode): State[Nid] = new State(
Set.empty,
Map.empty,
ContractStateMachine.ActiveLedgerState.empty,
List.empty,
mode,
)
}
}
object ContractStateMachine {
def initial[Nid](mode: ContractKeyUniquenessMode): State[Nid] = State.empty(mode)
/** Represents the answers for [[com.daml.lf.engine.ResultNeedKey]] requests
* that may arise during Daml interpretation.
@ -479,12 +484,12 @@ object ContractStateMachine {
* was consumed or not. That information is stored in consumedBy.
* It also _only_ includes local contracts not global contracts.
*/
final case class ActiveLedgerState[+Nid](
final case class ActiveLedgerState[Nid](
locallyCreatedThisTimeline: Set[ContractId],
consumedBy: Map[ContractId, Nid],
private val localKeys: Map[GlobalKey, Value.ContractId],
private[lf] val localKeys: Map[GlobalKey, Value.ContractId],
) {
def consume[Nid2 >: Nid](contractId: ContractId, nodeId: Nid2): ActiveLedgerState[Nid2] =
def consume(contractId: ContractId, nodeId: Nid): ActiveLedgerState[Nid] =
this.copy(consumedBy = consumedBy.updated(contractId, nodeId))
def createKey(key: GlobalKey, cid: Value.ContractId): ActiveLedgerState[Nid] =
@ -492,16 +497,16 @@ object ContractStateMachine {
/** Equivalence relative to locallyCreatedThisTimeline, consumedBy & localActiveKeys.
*/
def isEquivalent[Nid2 >: Nid](other: ActiveLedgerState[Nid2]): Boolean =
def isEquivalent(other: ActiveLedgerState[Nid]): Boolean =
this.locallyCreatedThisTimeline == other.locallyCreatedThisTimeline &&
this.consumedBy == other.consumedBy &&
this.localActiveKeys == other.localActiveKeys
/** See docs of [[ContractStateMachine.advance]]
*/
private[ContractStateMachine] def advance[Nid2 >: Nid](
substate: ActiveLedgerState[Nid2]
): ActiveLedgerState[Nid2] =
private[lf] def advance(
substate: ActiveLedgerState[Nid]
): ActiveLedgerState[Nid] =
ActiveLedgerState(
locallyCreatedThisTimeline = this.locallyCreatedThisTimeline
.union(substate.locallyCreatedThisTimeline),
@ -512,9 +517,9 @@ object ContractStateMachine {
/** localKeys filter by whether contracts have been consumed already.
*/
def localActiveKeys: Map[GlobalKey, KeyMapping] =
localKeys.map { case (k, v) =>
k -> (if (consumedBy.contains(v)) KeyInactive else KeyActive(v))
}
localKeys.view
.mapValues((v: ContractId) => if (consumedBy.contains(v)) KeyInactive else KeyActive(v))
.toMap
/** Lookup in localActiveKeys.
*/
@ -527,9 +532,7 @@ object ContractStateMachine {
}
object ActiveLedgerState {
private val EMPTY: ActiveLedgerState[Nothing] =
ActiveLedgerState(Set.empty, Map.empty, Map.empty)
def empty[Nid]: ActiveLedgerState[Nid] = EMPTY
def empty[Nid]: ActiveLedgerState[Nid] = ActiveLedgerState(Set.empty, Map.empty, Map.empty)
}
}

5
daml-lf/transaction/src/main/scala/com/digitalasset/daml/lf/transaction/Transaction.scala
View File

@ -490,9 +490,8 @@ sealed abstract class HasTxNodes {
"If a contract key contains a contract id"
)
def contractKeyInputs: Either[KeyInputError, Map[GlobalKey, KeyInput]] = {
val machine = new ContractStateMachine[NodeId](mode = ContractKeyUniquenessMode.Strict)
foldInExecutionOrder[Either[KeyInputError, machine.State]](
Right(machine.initial)
foldInExecutionOrder[Either[KeyInputError, ContractStateMachine.State[NodeId]]](
Right(ContractStateMachine.initial[NodeId](ContractKeyUniquenessMode.Strict))
)(
exerciseBegin = (acc, nid, exe) =>
(acc.flatMap(_.handleExercise(nid, exe)), Transaction.ChildrenRecursion.DoRecurse),

40
daml-lf/transaction/src/test/scala/com/digitalasset/daml/lf/transaction/ContractStateMachineSpec.scala
View File

@ -162,7 +162,7 @@ class ContractStateMachineSpec extends AnyWordSpec with Matchers with TableDrive
val tx = builder.build()
val expected = Right(
Map(gkey("key1") -> KeyCreate) ->
ActiveLedgerState(Set(1), Map.empty, Map(gkey("key1") -> 1))
ActiveLedgerState[Unit](Set(1), Map.empty, Map(gkey("key1") -> 1))
)
TestCase(
"Create|Rb-Ex-LBK|LBK",
@ -331,7 +331,7 @@ class ContractStateMachineSpec extends AnyWordSpec with Matchers with TableDrive
val tx = builder.build()
val expectedOff = Right(
Map(gkey("key1") -> KeyCreate) ->
ActiveLedgerState(
ActiveLedgerState[Unit](
Set(2, 3),
Map.empty,
Map(
@ -358,7 +358,7 @@ class ContractStateMachineSpec extends AnyWordSpec with Matchers with TableDrive
val tx = builder.build()
val expected = Right(
Map(gkey("key1") -> NegativeKeyLookup) ->
ActiveLedgerState(Set.empty, Map.empty, Map.empty)
ActiveLedgerState[Unit](Set.empty, Map.empty, Map.empty)
)
TestCase(
"DivulgedLookup",
@ -427,7 +427,7 @@ class ContractStateMachineSpec extends AnyWordSpec with Matchers with TableDrive
val tx = builder.build()
val expected = Right(
Map(gkey("key1") -> KeyCreate) ->
ActiveLedgerState(Set(3), Map.empty, Map(gkey("key1") -> cid(3)))
ActiveLedgerState[Unit](Set(3), Map.empty, Map(gkey("key1") -> cid(3)))
)
TestCase(
"CreateAfterRbExercise",
@ -475,7 +475,7 @@ class ContractStateMachineSpec extends AnyWordSpec with Matchers with TableDrive
val tx = builder.build()
val expectedOff = Right(
Map(gkey("key1") -> KeyCreate, gkey("key2") -> KeyCreate) ->
ActiveLedgerState(
ActiveLedgerState[Unit](
Set(1, 3, 4, 5),
Map.empty,
Map(gkey("key1") -> cid(4), gkey("key2") -> cid(5)),
@ -561,10 +561,14 @@ class ContractStateMachineSpec extends AnyWordSpec with Matchers with TableDrive
expected.foreach { case (mode, expectedResult) =>
s"mode $mode" in {
// We use `Unit` instead of `NodeId` so that we don't have to fiddle with node ids
val ksm = new ContractStateMachine[Unit](mode)
val actualResolver: KeyResolver =
if (mode == ContractKeyUniquenessMode.Strict) Map.empty else resolver
val result = visitSubtrees(ksm)(tx.nodes, tx.roots.toSeq, actualResolver, ksm.initial)
val result = visitSubtrees(
tx.nodes,
tx.roots.toSeq,
actualResolver,
ContractStateMachine.initial[Unit](mode),
)
(result, expectedResult) match {
case (Left(err1), Left(err2)) => err1 shouldBe err2
@ -652,12 +656,12 @@ class ContractStateMachineSpec extends AnyWordSpec with Matchers with TableDrive
* for handling [[com.daml.lf.transaction.Node.LookupByKey]].
* Ignored in mode [[com.daml.lf.transaction.ContractKeyUniquenessMode.Strict]].
*/
private def visitSubtree(ksm: ContractStateMachine[Unit])(
private def visitSubtree(
nodes: Map[NodeId, Node],
root: NodeId,
resolver: KeyResolver,
state: ksm.State,
): Either[Transaction.KeyInputError, ksm.State] = {
state: ContractStateMachine.State[Unit],
): Either[Transaction.KeyInputError, ContractStateMachine.State[Unit]] = {
val node = nodes(root)
for {
next <- node match {
@ -667,7 +671,7 @@ class ContractStateMachineSpec extends AnyWordSpec with Matchers with TableDrive
Right(state.beginRollback())
}
afterChildren <- withClue(s"visiting children of $node") {
visitSubtrees(ksm)(nodes, children(node).toSeq, resolver, next)
visitSubtrees(nodes, children(node).toSeq, resolver, next)
}
exited = node match {
case _: Node.Rollback => afterChildren.endRollback()
@ -682,26 +686,26 @@ class ContractStateMachineSpec extends AnyWordSpec with Matchers with TableDrive
*
* @see visitSubtree for how visiting nodes updates the state
*/
private def visitSubtrees(ksm: ContractStateMachine[Unit])(
private def visitSubtrees(
nodes: Map[NodeId, Node],
roots: Seq[NodeId],
resolver: KeyResolver,
state: ksm.State,
): Either[Transaction.KeyInputError, ksm.State] = {
state: ContractStateMachine.State[Unit],
): Either[Transaction.KeyInputError, ContractStateMachine.State[Unit]] = {
roots match {
case Seq() => Right(state)
case root +: tail =>
val node = nodes(root)
val directVisit = visitSubtree(ksm)(nodes, root, resolver, state)
val directVisit = visitSubtree(nodes, root, resolver, state)
// Now project the resolver and visit the subtree from a fresh state and check whether we end up the same using advance
val fresh = ksm.initial
val fresh = ContractStateMachine.initial[Unit](state.mode)
val projectedResolver: KeyResolver =
if (state.mode == ContractKeyUniquenessMode.Strict) Map.empty
else state.projectKeyResolver(resolver)
withClue(
s"Advancing over subtree rooted at $node with projected resolver $projectedResolver; projection state=$state; original resolver=$resolver"
) {
val freshVisit = visitSubtree(ksm)(nodes, root, projectedResolver, fresh)
val freshVisit = visitSubtree(nodes, root, projectedResolver, fresh)
val advanced = freshVisit.flatMap(substate => state.advance(resolver, substate))
(directVisit, advanced) match {
@ -715,7 +719,7 @@ class ContractStateMachineSpec extends AnyWordSpec with Matchers with TableDrive
case _ => fail(s"$directVisit was knot equal to $advanced")
}
}
directVisit.flatMap(next => visitSubtrees(ksm)(nodes, tail, resolver, next))
directVisit.flatMap(next => visitSubtrees(nodes, tail, resolver, next))
}
}
}

62
daml-lf/verification/README.md Normal file
View File

@ -0,0 +1,62 @@
# Proof of the advance method of the Contract State Machine in UCK mode
Formal verification in [Stainless](https://stainless.epfl.ch/) of the advance method of the [ContractStateMachine](../transaction/src/main/scala/com/digitalasset/daml/lf/transaction/ContractStateMachine.scala) in strict mode.
More precisely, under reasonable assumptions, if $tr$ is a transaction, $init$ a State, and $\textup{traverse}(tr, \varepsilon)$ is well-defined then:
$$\textup{traverse}(tr, init) = init.\textup{advance}(\textup{traverse}(tr, \varepsilon))$$
where $\varepsilon$ is the empty State.
A pen and paper proof of the main component of the verification can be found [here](latex/proof.pdf).
## Components
- `latex` : the pen and paper proof.
- `scripts` : the verification scripts and its helpers.
- `transaction` : all the proofs related to how the CSM handles a node.
- `translation` : original file and proofs of the translation to a simplified version of it
- `tree` : all the proofs related to how the CSM handles a transaction.
- `utils` : helpers and theorems about collections.
## Developer Environment Setup
``` nix-shell ./stainless.nix -A stainlessEnv ```
## Build
To build the Stainless version used in the proof:
1. Clone [Stainless repo](https://github.com/epfl-lara/stainless)
2. Run sbt universal:stage
3. The generated binary can be found at the following location (in the following, this path is referred to as `<stainless_path>`):
`$STAINLESS_REPO_ROOT/frontends/dotty/target/universal/stage/bin/stainless-dotty`
4. The verification currently works with JDK 17
## Verification
The verification happens in 2 major steps:
- The translation from the original file to a [simplified version](transaction/ContractStateMachineAlt.scala) that is easy to work with in stainless and a proof of the soudness of this translation.
- The verification of the property
To verify the former you can execute the verification script with the following argument:
``` scripts/verification_script.sh <stainless_path> translate```
The scripts takes the original files and uses a regex to create a temporary copy of the file that modifies the imports,
removes the exceptions and in general features that are not yet supported in Stainless.
To verify the latter, you can either execute the following command:
```stainless utils/* transaction/* tree/* --watch=false --timeout=30 --vc-cache=false --compact=true --solvers=nativez3```
or execute the script with the following argument:
``` scripts/verification_script.sh <stainless_path> verify```
If in the first command you find that the timeout is too big you can reduce it as you wish (it is recommended to keep it above 10 if you don't want to have any suprises).

899
daml-lf/verification/latex/proof.tex Normal file
View File

@ -0,0 +1,899 @@
% Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
% SPDX-License-Identifier: Apache-2.0
\documentclass{article}
\usepackage[margin=2.5cm]{geometry}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{amsthm}
\usepackage{parskip}
\usepackage{hyperref}
\usepackage{cleveref}
\newtheorem{lemma}{Lemma}
\crefformat{lemma}{Lem.~#2#1#3}
\newtheorem{theorem}{Theorem}
\crefformat{theorem}{Thm.~#2#1#3}
\newtheorem{definition}[lemma]{Definition}
\crefformat{definition}{Def.~#2#1#3}
\newtheorem{claim}[lemma]{Claim}
\crefformat{claim}{Claim~#2#1#3}
\newtheorem{corollary}[lemma]{Corollary}
\crefformat{corollary}{Cor.~#2#1#3}
\newtheorem*{res}{Final result}
\newtheorem*{term}{Terminology}
\newcommand{\textfun}[1]{\textup{#1}}
\newcommand{\textcode}[1]{\texttt{#1}}
\newcommand{\bolddef}[1]{\textbf{\ensuremath{\mathbf{#1}}}}
\newcommand{\negat}[1]{\neg\,#1}
\newcommand{\fdown}[2]{\ensuremath{f_{down}(#1, #2)}}
\newcommand{\fup}[2]{\ensuremath{f_{up}(#1, #2)}}
\newcommand{\fone}[2]{\ensuremath{f_{1}(#1, #2)}}
\newcommand{\ftwo}[2]{\ensuremath{f_{2}(#1, #2)}}
\newcommand{\fcoll}[2]{\ensuremath{f_{collect}(#1, #2)}}
\newcommand{\emptyList}{\ensuremath{[\ ]}}
\newcommand{\concat}{{{\ ++\ }}}
% NODES %
\newcommand{\fetchNode}[2]{\textfun{Fetch} \ #1\ #2}
\newcommand{\lookupNode}[2]{\textfun{Lookup}\ #1\ #2}
\newcommand{\createNode}[2]{\textfun{Create}\ #1\ #2}
\newcommand{\exNode}[2]{\textfun{Exercise}\ #1\ #2}
%TREES
\newcommand{\nilNode}{\textfun{Endpoint}}
\newcommand{\contentNode}[2]{\textfun{ContentNode}\ #1\ #2}
\newcommand{\artNode}[2]{\textfun{ArticulationNode}\ #1\ #2}
\newcommand{\longtraverse}[4]{\textfun{traverse}\ #1\ #2\ #3 \ #4}
\newcommand{\traverse}[2]{\textfun{traverse}\ #1\ #2}
\newcommand{\longscan}[4]{\textfun{scan}\ #1\ #2\ #3 \ #4}
\newcommand{\scan}[2]{\textfun{scan}\ #1\ #2}
\newcommand{\collect}[1]{\textfun{collect}\ #1}
\newcommand{\collectTr}[1]{\textfun{collectTrace}\ #1}
\newcommand{\up}{\uparrow}
\newcommand{\down}{\downarrow}
\newcommand{\hNode}[2]{\textfun{handleNode}\ #1\ #2}
\newcommand{\beginRb}[1]{\textfun{beginRollback}\ #1}
\newcommand{\enRb}[1]{\textfun{endRollback}\ #1}
\newcommand{\defined}[1]{\textfun{defined}\ #1}
\newcommand{\get}[1]{\textfun{get}\ #1}
\newcommand{\mapping}[1]{\textfun{mapping}\ #1}
\newcommand{\size}[1]{\textfun{size}\ #1}
\newcommand{\fst}[1]{\textfun{proj}_1\ #1}
\newcommand{\snd}[1]{\textfun{proj}_2\ #1}
\newcommand{\trd}[1]{\textfun{proj}_3\ #1}
\newcommand{\keyAct}[1]{\textfun{KeyActive}\ #1}
\newcommand{\keyInact}{\textfun{KeyInactive}}
\newcommand{\state}{\textfun{State}}
\newcommand{\appfst}[2]{\textfun{app}_{#1} #2 = 1}
\newcommand{\actkey}[2]{\textfun{act}_{#1}\ #2}
\newcommand{\emptyState}[1]{\varepsilon_{#1}}
\title{\huge Proof of \texttt{advance} in the UCK State Machine}
\date{}
\author{}
\begin{document}
\maketitle
\begin{term}\
\begin{itemize}
\item A \textbf{well-defined state} is an instance of the type $\state$ or $\textfun{Right[KeyInputError, \state]}$
\item A \textbf{state} is an instance of the type $\textfun{Either[KeyInputError, \state]}$
\item A \textbf{node} is an instance of the type $\textfun{Node}$ or $\textfun{(Node, NodeId)}$.
\end{itemize}
When multiple interpretations are possible, the context will always make clear which one we are referring to.
In particular, depending on the situation, $\beginRb{s}$ and $\enRb{s}$ will return either a $\state$ or a $\textfun{Right[KeyInputError, \state]}$.
\end{term}
\begin{definition}
Let $s$ be a state, \bolddef{\defined{s}} is true if $s$ is a well-defined state.
When this is the case, \bolddef{\get{s}} yields the $\textfun{State}$ instance out of the option.
\end{definition}
\begin{definition}
Let $t := (v_1, v_2, v_3)$ a triple. The projections of the triple are $\bolddef{\fst{t}} := v_1$, $\bolddef{\snd{t}} := v_2$ and $\bolddef{\trd{t}} := v_3$.
\end{definition}
%TREES
\section*{Trees}
\begin{definition}[\textcode{Tree}]
A tree of nodes is a data structure defined inductively as either:
\begin{itemize}
\item $\nilNode$
\item $\contentNode{sub}{n}$, where $sub$ is a tree and $n$ a node.
\item $\artNode{l}{r}$, where $l$ and $r$ are both trees.
\end{itemize}
\end{definition}
Although this is not the most intuitive definition, it has the advantage of being able to represent forests
without running into measure decreaseness problems. In fact one can see content nodes as being trees and articulation nodes as forests.
\begin{definition}[\textcode{Tree.size}]
\label{size_def}
Let $tr$ be a tree of nodes, \bolddef{\size{tr}} is defined inductively as:
\begin{itemize}
\item $\size{\nilNode} := 0$
\item $\size{(\contentNode{sub}{n})} := (\size{sub}) + 1$
\item $\size{(\artNode{l}{r})} := (\size{l}) + (\size{r})$
\end{itemize}
\end{definition}
\begin{definition}[\textcode{Tree.traverse}]
\label{traverse_def}
Let $tr$ be a tree of nodes and $init$ a value, \bolddef{\longtraverse{tr}{init}{f_1}{f_2}} is defined inductively as:
\begin{itemize}
\item $\longtraverse{\nilNode}{init}{f_1}{f_2} := init$
\item $\longtraverse{(\contentNode{sub}{n})}{init}{f_1}{f_2} := \ftwo{\longtraverse{sub}{\fone{init}{n}}{f_1}{f_2}}{n}$
\item $\longtraverse{(\artNode{l}{r})}{init}{f_1}{f_2} := \longtraverse{r}{(\longtraverse{l}{init}{f_1}{f_2})}{f_1}{f_2}$
\end{itemize}
\end{definition}
\begin{definition}[\textcode{Tree.scan}]
\label{scan_def}
Let $tr$ be a tree of nodes and $init$ a value, \bolddef{\longscan{tr}{init}{f_1}{f_2}} is defined inductively as:
\begin{itemize}
\item $\longscan{\nilNode}{init}{f_1}{f_2} := \emptyList$
\item $\longscan{(\contentNode{sub}{n})}{init}{f_1}{f_2} :=$
\[ [(init, n,\,\down)] \concat \longscan{sub}{f_1(init, n)}{f_1}{f_2} \concat [(\longtraverse{sub}{f_1(init, n)}{f_1}{f_2}, n,\,\up)]\]
\item $\longscan{(\artNode{l}{r})}{init}{f_1}{f_2} :=$
\[\longscan{l}{init}{f_1}{f_2} \concat \longscan{r}{(\longtraverse{l}{init}{f_1}{f_2})}{f_1}{f_2}\]
\end{itemize}
\end{definition}
\begin{claim}[postcondition of \textcode{Tree.size}]
\label{size_pos}
Let $tr$ be a tree of nodes,
\[\size{tr} \geq 0 \]
\end{claim}
\begin{proof}
Straight induction on $tr$.
\end{proof}
\begin{claim}[postcondition of \textcode{Tree.scan}]
\label{scan_size}
For any tree of nodes $tr$, value $init$ and functions $f_1, f_2$
\[\size{(\longscan{tr}{init}{f_1}{f_2})} = 2 \cdot \size{tr}\]
\end{claim}
\begin{proof}
Straight induction on tr.
\end{proof}
\begin{lemma}[\textcode{scanIndexing}]
\label{scan_indexing}
For any tree of nodes $tr$, value $init$ and functions $f_1, f_2$
If $tr = \contentNode{sub}{n}$:
\[(\longscan{tr}{init}{f_1}{f_2})[i] =
\begin{cases}
(init, n,\,\down) & \text{if $i = 0$}\\
(\longtraverse{sub}{\fone{init}{n}}{f_1}{f_2}, n,\,\up) & \text{if $i = 2 \cdot \size{tr} - 1$}\\
(\longscan{sub}{\fone{init}{n}}{f_1}{f_2})[i - 1] & \text{otherwise}
\end{cases}\]
If $tr = \artNode{l}{r}$:
\[(\longscan{tr}{init}{f_1}{f_2})[i] =
\begin{cases}
(\longscan{l}{init}{f_1}{f_2})[i] & \text{if $i < 2\cdot \size{l}$}\\
(\longscan{r}{(\longtraverse{l}{init}{f_1}{f_2})}{f_1}{f_2})[i - 2 \cdot \size{l}] & \text{otherwise}
\end{cases}\]
\end{lemma}
\begin{proof}
Application of union indexing property in lists
\end{proof}
\begin{lemma}[\textcode{scanIndexingState}]
\label{scan_indexing_state}
Let $tr$ be a tree of nodes $tr$, $init$ a value, $f_1, f_2$ two functions and $i < 2 \cdot \size{tr}$ a non-negative integer. Let $l := \longscan{tr}{init}{f_1}{f_2}$:
\begin{align}
\fst{(l[i])} =& \begin{cases}
init & \text{if $i = 0$}\\
f_1(\fst{(l[i - 1])}, \snd{(l[i - 1])}) & \text{if $\trd{(l[i - 1])} = \, \down$} \\
f_2(\fst{(l[i - 1])}, \snd{(l[i - 1])}) & \text{if $\trd{(l[i - 1])} = \, \up$}
\end{cases}\\
\intertext{\hskip 25em and}
\longtraverse{tr}{init}{f_1}{f_2} =&
\begin{cases}
init &\text{if $\size{tr} = 0$} \\
f_2(\fst{(l[2 \cdot \size{tr} - 1])}, \snd{(l[2 \cdot \size{tr} - 1])}) &\text{otherwise}
\end{cases}
\end{align}
\end{lemma}
\begin{proof}
Induction on tr:
\begin{itemize}
\item If $tr = \nilNode$, then $\size{tr} = 0$.
\item If $tr = \contentNode{sub}{n}$:
\begin{itemize}
\item If $i = 0$ then by \cref{scan_indexing} $l[i] = (init, n, \down)$.
\item If $i = 2\, \cdot \, \size{tr} \, - \, 1$, then by \cref{scan_indexing} $l[i] = (\longtraverse{sub}{\fone{init}{n}}{f_1}{f_2}, n, \up)$.
Let $l_{sub} := \longscan{sub}{\fone{init}{n}}{f_1}{f_2}$.
If $\size{sub} = 0$, then $i = 1$:
\begin{align*}
\longtraverse{sub}{\fone{init}{n}}{f_1}{f_2} =& \fone{init}{n} & \text{by IH} \\
=& \fone{\fst{(l[0])}}{\snd{(l[0])}} & \text{by \cref{scan_indexing}} \\
=& \fone{\fst{(l[i - 1])}}{\snd{(l[i - 1])}}
\end{align*}
Moreover we know that $\trd{(l[0])} = \down$
Otherwise:
\begin{align*}
&\longtraverse{sub}{\fone{init}{n}}{f_1}{f_2} \\
=& \ftwo{\fst{(l_{sub}[2 \cdot \size{sub} - 1])}}{\snd{(l_{sub}[2 \cdot \size{sub} - 1])}} \\
=& \ftwo{\fst{(l_{sub}[2 \cdot \size{tr} - 3])}}{\snd{(l_{sub}[2 \cdot \size{tr} - 3])}} & \text{unfolding \cref{size_def}} \\
=& \ftwo{\fst{(l[2 \cdot \size{tr} - 2])}}{\snd{(l[2 \cdot \size{tr} - 2])}} & \text{by \cref{scan_indexing}} \\
=& \ftwo{\fst{(l[i - 1])}}{\snd{(l[i - 1])}}
\end{align*}
\item Else apply induction hypothesis with $sub$, $\fone{init}{n}$ and $i - 1$. Use \cref{scan_indexing} when $i > 1$.
\item To prove (2) we know by \cref{size_def} that $\size{tr} > 0$. The result is then immediate from \cref{scan_indexing}.
\end{itemize}
\item If $tr = \artNode{le}{ri}$:
\begin{itemize}
\item If $i < 2 \cdot \size{le}$, apply induction hypothesis with $le$, $init$ and $i$, and \cref{scan_indexing}.
\item If $i = 2 \cdot \size{le}$:
Let $l_{le} := (\longscan{le}{init}{f_1}{f_2})$ and $l_{ri} := (\longscan{ri}{(\longtraverse{le}{init}{f_1}{f_2})}{f_1}{f_2})$
\begin{align*}
\fst{(l_{ri}[0])} &= \longtraverse{le}{init}{f_1}{f_2}\: &\text{by IH on $ri$}\\
\fst{(l_{ri}[i - 2 \cdot \size{le}])} &= \longtraverse{le}{init}{f_1}{f_2} \\
\fst{(l[i])} &= \longtraverse{le}{init}{f_1}{f_2} &\text{by \cref{scan_indexing}} \\
&= \ftwo{\fst{(l_{le}[2 \cdot \size{le} - 1])}}{\snd{(l_{le}[2 \cdot \size{le} - 1])}} &\text{by IH on $le$} \\
&= \ftwo{\fst{(l_{le}[i - 1])}}{\snd{(l_{le}[i - 1])}}
\end{align*}
\item Else apply induction hypothesis with $ri$, $\longtraverse{le}{init}{f_1}{f_2}$ and $i - 2 \cdot \size{le}$ and \cref*{scan_indexing}.
\item If $\size{tr} = 0$ then by \cref{size_pos} and unfolding \cref{size_def}, $\size{le} = 0$ and $\size{ri} = 0$.
\begin{align*}
\longtraverse{tr}{init}{f_1}{f_2} &= \longtraverse{ri}{(\longtraverse{le}{init}{f_1}{f_2})}{f_1}{f_2} &\text{unfolding \cref{traverse_def}} \\
&= \longtraverse{le}{init}{f_1}{f_2} & \text{by IH on $ri$} \\
&= init & \text{by IH on $l$}
\end{align*}
Else if $\size{ri} = 0$:
\begin{align*}
\longtraverse{tr}{init}{f_1}{f_2}
=\ & \longtraverse{ri}{(\longtraverse{le}{init}{f_1}{f_2})}{f_1}{f_2} &\text{unfolding \cref{traverse_def}} \\
=\ & \longtraverse{le}{init}{f_1}{f_2} & \text{by IH on $ri$} \\
=\ & f_2(\fst{(l_{le}[2 \cdot \size{le} - 1])}, \snd{(l_{le}[2 \cdot \size{le} - 1])}) & \text{by IH on $le$} \\
=\ & f_2(\fst{(l[2 \cdot \size{le} - 1])}, \snd{(l[2 \cdot \size{le} - 1])}) & \text{by \cref{scan_indexing}} \\
=\ & f_2(\fst{(l[2 \cdot \size{tr} - 1])}, \snd{(l[2 \cdot \size{tr} - 1])}) & \text{by \cref{size_def}}
\end{align*}
When $\size{ri} > 0$:
\begin{align*}
&\longtraverse{tr}{init}{f_1}{f_2} \\
=\ & \longtraverse{ri}{(\longtraverse{le}{init}{f_1}{f_2})}{f_1}{f_2} &\text{unfolding \cref{traverse_def}} \\
=\ & f_2(\fst{(l_{ri}[2 \cdot \size{ri} - 1])}, \snd{(l_{ri}[2 \cdot \size{ri} - 1])}) & \text{by IH on $ri$} \\
=\ & f_2(\fst{(l[2 \cdot \size{ri} + 2 \cdot \size{le} - 1])}, \snd{(l[2 \cdot \size{ri} + 2 \cdot \size{le} - 1])}) & \text{by \cref{scan_indexing}} \\
=\ & f_2(\fst{(l[2 \cdot \size{tr} - 1])}, \snd{(l[2 \cdot \size{tr} - 1])}) & \text{by \cref{size_def}}
\end{align*}
\end{itemize}
\end{itemize}
\end{proof}
\begin{claim}[\textcode{scanIndexingNode}]
\label{scan_indexing_node}
For any tree of nodes $tr$, values $init_1,\, init_2$, functions $f^1_1, f^1_2, f^2_1, f^2_2$ and non-negative integer $i < 2\, \cdot\, \size{tr}$.
\[ \snd{((\longscan{tr}{init_1}{f^1_1}{f^1_2})[i])} = \snd{((\longscan{tr}{init_2}{f^2_1}{f^2_2})[i])}\]
\[\text{and}\]
\[ \trd{((\longscan{tr}{init_1}{f^1_1}{f^1_2})[i])} = \trd{((\longscan{tr}{init_2}{f^2_1}{f^2_2})[i])}\]
\end{claim}
\begin{proof}
Induction on tr using \cref{scan_indexing}.
\end{proof}
We now define the two functions we will be applying during a tree traversal.
\begin{definition}[\textcode{traverseInFun}, \textcode{traverseOutFun}]
Let $s$ be a state and $n$ be a node,
\[\fdown{s}{n} : =
\begin{cases}
\hNode{(\get{s})}{n}& \text{if $n$ is an Action node and $\defined{s}$} \\
\beginRb{(\get{s})} & \text{if $n$ is a Rollback node and $\defined{s}$} \\
s& \text{otherwise}
\end{cases} \]
\[\fup{s}{n} : =
\begin{cases}
\enRb{(\get{s})} & \text{if $n$ is a Rollback node and $\defined{s}$} \\
s& \text{otherwise}
\end{cases} \]
\end{definition}
In the rest of the document, unless stated otherwise, init will be a state and $\traverse{tr}{init}$ and $\scan{tr}{init}$ will be referring to as respectively
$\longtraverse{tr}{init}{f_{down}}{f_{up}}$ and $\longscan{tr}{init}{f_{down}}{f_{up}}$
\begin{claim}[\textcode{traverseTransactionProp}]
For any tree of nodes tr, state init, if $\defined{(\traverse{tr}{init})}$ then
\label{traverse_prop}
\[\defined{init} \land (\get{(\traverse{tr}{init})}).rollbackStack = (\get{init}).rollbackStack \ \land\]
\[(\get{(\traverse{tr}{init})}).globalKeys = (\get{init}).globalKeys\]
\end{claim}
\begin{proof}
Straight induction on tr.
\end{proof}
\begin{claim}[\textcode{scanTransactionProp}]
\label{defined_prop}
Let $tr$ be a tree of nodes, $init$ a state, $0 \leq i \leq j < 2 \cdot\, \size{tr} $ two integers and let $l:= \scan{tr}{init}$.
\[\defined (\fst{(l[j])}) \implies\, \defined (\fst{(l[i])})\]
\end{claim}
\begin{proof}
By induction on $j$: the base case is immediate and \cref{scan_indexing_state}
combined with the induction hypothesis concludes the proof.
\end{proof}
\begin{corollary}[\textcode{scanTransactionProp}]
\label{defined_traverse_prop}
Let $tr$ be a tree of nodes, $init$ a state, $0 \leq i < 2 \cdot\, \size{tr} $ an integer and let $l:= \scan{tr}{init}$.
\[\defined (\traverse{tr}{init}) \implies\, \defined (\fst{(l[i])})\]
\end{corollary}
\begin{proof}
By \cref{scan_indexing_state} and \cref{defined_prop} setting $j = 2 \cdot\, \size{tr} - 1$.
\end{proof}
\begin{lemma}
\label{defined_alt_def}
Let $tr$ be a tree of nodes, $init$ a state and $l := \scan{tr}{init}$ then
\[\defined{(\traverse{tr}{init})} \iff
\begin{cases}
\defined{init} \\
\forall\, 0 \leq i < 2 \cdot\, \size{tr} - 1, \, \defined{(\fst{(l[i])})} \implies \defined{(\fst{(l[i + 1])})} \,
\end{cases}\]
\end{lemma}
\begin{proof}
Let's first note that by \cref{scan_indexing_state}, $\fst{(l[0])} = init$.
If $\defined{(\traverse{tr}{init})}$ then by \cref{defined_traverse_prop}, $\defined{\fst{(l[i])}}$ for all $0 \leq i < 2 \cdot\, \size{tr}$.
If the right statement is true, then $\defined{(\fst{(l[2 \cdot \, \size{tr} - 1])})}$ and therefore by \cref{scan_indexing_state} we have $\defined{(\traverse{tr}{init})}$.
\end{proof}
\begin{claim}[\textcode{findBeginRollback}]
\label{find_two_begin_rb}
Let tr be a tree of nodes, $init_1, init_2$ be states and let $l_1 := \scan{tr}{init_1}$, $l_2 := \scan{tr}{init_2}$.
If there exists a non-negative integer $i < 2 \cdot (\size{tr})$, well-defined states $s^1_i$, $s^2_i$ and a Rollback node $n$ such that
$l_1[i] = (s^1_i, n, \up)$ and $l_2[i] = (s^2_i, n, \up)$, then there is an integer $j$, well-defined states $s^1_j, s^2_j$ and a tree $sub$ such that
\[0 \leq j < i \qquad l_1[j] = (s^1_j, n, \down) \qquad l_2[j] = (s^2_j, n, \down) \qquad \size{sub} < \size{tr}\]
\[s^1_i = \traverse{sub}{(\beginRb{(\get{s^1_j})})} \qquad s^2_i = \traverse{sub}{(\beginRb{(\get{s^2_j})})}\]
\end{claim}
\begin{proof}
Induction on $tr$:
\begin{itemize}
\item If $tr = \nilNode$, then $\size{tr} = 0$ which means the precondition is never met.
\item If $tr = \contentNode{str}{c}$:
\begin{itemize}
\item If $c \neq n$ then by \cref{scan_indexing}, $ 0 < i < 2 \cdot (\size{tr}) - 1$, $l_1[i] = (\scan{str}{\fdown{init_1}{n}})[i - 1]$ and
$l_2[i] = (\scan{str}{\fdown{init_2}{n}})[i - 1]$.
By induction hypothesis there is an integer $j$, well-defined state $s^1_j$, $s^2_j$ and a tree $sub$ such that:
\[(\scan{str}{\fdown{init_1}{n}})[j] = (s^1_j, n, \down) \qquad (\scan{str}{\fdown{init_2}{n}})[j] = (s^2_j, n, \down)\]
\[s^1_i = \traverse{sub}{(\beginRb{(\get{s^1_j})})} \qquad s^2_i = \traverse{sub}{(\beginRb{(\get{s^2_j})})}\]
\[0 \leq j < i - 1 \qquad \size{sub} < \size{tr} \qquad \]
Since $l_1[j + 1] = (\scan{str}{\fdown{init_1}{n}})[j]$ and $l_2[j + 1] = (\scan{str}{\fdown{init_2}{n}})[j]$, $j + 1$, $sub$, $s^1_j$ and $s^2_j$ satisfy the above conditions.
\item If $c = n$, then $i = 2\cdot (\size{tr}) - 1$ is valid and therefore $j = 0$, $s^1_j = init_1$, $s^2_j = init_2$ and $sub = str$.
\end{itemize}
\item If $tr = \artNode{left}{right}$:
\begin{itemize}
\item If $i < 2 \cdot \size{left}$, then by \cref{scan_indexing}, $l_1[i] = (\scan{left}{init_1})[i]$ and $l_2[i] = (\scan{left}{init_2})[i]$.
By induction hypothesis, there are $j$, well-defined $s^1_j$, $s^2_j$ and $sub$ such that.
\[(\scan{left}{init_1})[j] = (s^1_j, n, \down) \qquad\, (\scan{left}{init_2})[j] = (s^2_j, n, \down)\]
\[s^1_i = \traverse{sub}{(\beginRb{(\get{s^1_j})})} \qquad s^2_i = \traverse{sub}{(\beginRb{(\get{s^2_j})})}\]
\[0 \leq j < i \qquad \size{sub} < \size{left}\]
Since $l_1[j] = (\scan{left}{init_1})[j]$ and $l_2[j] = (\scan{left}{init_2})[j]$, $j$, $s^1_j$, $s^2_j$ and $sub$ satisfy the claim.
\item If $i \geq 2 \cdot \size{left}$, then by \cref{scan_indexing}, $l_1[i] = (\scan{right}{(\traverse{left}{init_1})})[i - 2 \cdot \size{left}]$ and $l_2[i] = (\scan{right}{(\traverse{left}{init_2})})[i - 2 \cdot \size{left}]$.
By induction hypothesis, there are $j$, well-defined $s^1_j$, $s^2_j$ and $sub$ such that.
\[(\scan{right}{(\traverse{left}{init_1})})[j] = (s^1_j, n, \down) \qquad (\scan{right}{(\traverse{left}{init_2})})[j] = (s^2_j, n, \down)\]
\[s^1_i = \traverse{sub}{(\beginRb{(\get{s^1_j})})} \qquad s^2_i = \traverse{sub}{(\beginRb{(\get{s^2_j})})}\]
\[ 0 \leq\, j < i - 2\cdot \size{left} \qquad \size{sub} < \size{right}\]
Since $l_1[j + 2 \cdot\, \size{left}] = (\scan{right}{(\traverse{left}{init_1})})[j] $ and $l_2[j + 2 \cdot \size{left}] = (\scan{right}{(\traverse{left}{init_2})})[j]$, $j + 2 \cdot \size{left}$, $s^1_j$, $s^2_j$ and $sub$ satisfy the claim.
\end{itemize}
\end{itemize}
\end{proof}
\begin{corollary}[\textcode{findBeginRollback}]
\label{find_begin_rb}
Let tr be a tree of nodes, $init$ a states and let $l := \scan{tr}{init}$.
If there exists a non-negative integer $i < 2 \cdot (\size{tr})$, a well-defined states $s_i$ and a rollback node $n$ such that
$l[i] = (s_i, n, \up)$, then there is an integer $j$, a well-defined states $s_j,$ and a tree $sub$ such that
\[0 \leq j < i \qquad l[j] = (s_j, n, \down) \qquad s_i = \traverse{sub}{(\beginRb{s_j})} \qquad \size{sub} < \size{tr}\]
\end{corollary}
\begin{proof}
By \cref{find_two_begin_rb} with $init_1 = init_2$.
\end{proof}
\newpage
\section*{Active Keys Lemmas}
\begin{definition}[\textcode{State.activeKeys.get}]
Let $s$ be a well-defined state and $k$ a key, \bolddef{\actkey{k}{s}} is the value associated to key in the active keys of the state
(i.e. we first look at the local keys, then the global ones filtering the consumed contracts).
\end{definition}
\begin{definition}[\textcode{nodeActionKeyMapping}]
Let $n$ be a node, \bolddef{\mapping{n}} is defined as:
\begin{itemize}
\item \mapping{(\createNode{id}{k})} := \keyInact
\item \mapping{(\fetchNode{id}{k})} := \keyAct{id}
\item \mapping{(\lookupNode{result}{k})} := result
\item \mapping{(\exNode{id}{k})} := \keyAct{id}
\end{itemize}
\end{definition}
\begin{lemma}[\textcode{handleNodeUndefined}]
\label{defined_def}
For any well-defined state s and Action node n,
\[\defined{(\hNode{s}{n})} \iff {\actkey{n.k}{s} = \mapping{n}}\]
\end{lemma}
\begin{corollary}[\textcode{handleSameNodeActiveKeys}]
\label{same_key_hnode}
For any well-defined states $s_1$, $s_2$ and Action node n, if $\defined{(\hNode{s_ 1}{n})}$ and $\defined{(\hNode{s_ 2}{n})}$
\[\actkey{n.k}{s_1} = \actkey{n.k}{s_2}\]
\end{corollary}
\begin{proof}
Direct consequence of \cref{defined_def}.
\end{proof}
\begin{lemma}[\textcode{handleNodeDifferentStatesActiveKeysGet}]
\label{same_key_after_hnode}
For any well-defined states $s_1$, $s_2$ and Action node n, if $\defined{(\hNode{s_ 1}{n})}$ and $\defined{(\hNode{s_ 2}{n})}$
\[\actkey{n.k}{(\get{(\hNode{s_1}{n})})} = \actkey{n.k}{(\get{(\hNode{s_2}{n})})}\]
\end{lemma}
\begin{lemma}[\textcode{handleNodeActiveKeysGet}]
\label{actkey_handle_node}
For any well-defined state $s$, Action node $n$, key $k_2$, if $n$ has no key or $k_2 \neq n.k$ and if $\defined{(\hNode{s}{n})}$,
\[\actkey{k_2}{(\get{(\hNode{s}{n})})} = \actkey{k_2}{s}\]
\end{lemma}
\begin{lemma}[\textcode{beginRollbackActiveKeysGet}]
\label{act_begin_rb}
For any well-defined state s, node n, key $k$,
\[\actkey{k}{(\beginRb{s})} = \actkey{k}{s}\]
\end{lemma}
\begin{lemma}[\textcode{activeKeysGetRollbackScope}]
\label{skip_rb}
For any well-defined state s, node n, key $k$, function $g: \state \rightarrow \state $ and:
\begin{itemize}
\item $g(\beginRb{s}).rollbackStack = (\beginRb{s}).rollbackStack$
\item $g(\beginRb{s}).globalKeys = (\beginRb{s}).globalKeys$
\end{itemize}
We have:
\[\actkey{k}{(\enRb{g(\beginRb{s})})} = \actkey{k}{s}\]
\end{lemma}
\newpage
\section*{The real deal}
\begin{definition}[\textcode{appearsAtIndex}, \textcode{doesNotAppearBefore}, \textcode{firstAppears}]
\label{appear_def}
Let tr be a tree of nodes, init a value, $k$ a key, $f_1, f_2$ two functions, $i < 2 \cdot \size{tr}$ a non-negative integer and let $l := \longscan{tr}{init}{f_1}{f_2}$.
We say that $k$ does not appear before $i$ if for all $0 \leq j < i,\ (\snd{l[j]}).k \neq k$ or $\trd{l[j]} =\, \up$
We say that $i$ is the first appearance of $k$ in $l$ if $(\snd{l[i]}).k = k$, $\trd{l[i]} = \ \down$ and $k$ does not appear before $i$.
\end{definition}
\begin{claim}[\textcode{doesNotAppearBeforeSame}, \textcode{firstAppearsSame}]
\label{appear_same}
Let tr be a tree of nodes, $init, init_2$ a state, $f^1_1, f^1_2, f^2_1, f^2_2$ functions, $k$ a key, $i$ a non-negative integer smaller than $2 \cdot \size{tr}$,
$l_1 := \longscan{tr}{init_1}{f^1_1}{f^1_2}$ and $l_2 := \longscan{tr}{init_2}{f^2_1}{f^2_2}$.
\begin{center}
$k$ does not appear before $i$ in $l_1$ $\iff$ $k$ does not appear before $i$ in $l_2$
\end{center}
and in particular
\begin{center}
$i$ is the first appearance of $k$ in $l_1$ $\iff$ $i$ is the first appearance of $k$ in $l_2$
\end{center}
\end{claim}
\begin{proof}
Consequence of \cref{scan_indexing_node}.
\end{proof}
\begin{claim}[\textcode{findFirstAppears}]
\label{find_first_appear}
Let tr be a tree of nodes, $init$ a state, $k$ a key, $0 \leq i_1 < i_2 < 2\cdot \size{tr}$ twos integers and
let $l := \scan{tr}{init}$. If $k$ appears before $i_2$ in $l$ but does not before $i_1$, then there exists an integer
$i_1 \leq j < i_2$ such that $j$ is the first appearance of $k$ in $l$.
\end{claim}
\begin{proof}
Immediate from \cref{appear_def}.
\end{proof}
\begin{claim}[\textcode{doesNotAppearBeforeSameActiveKeysGet}]
\label{actkey_not_appear}
Let tr be a tree of nodes, init a state, $k$ a key, $0 \leq j < i < 2\cdot\, \size{tr}$ two integers and let $l := \scan{tr}{init}$.
If $k$ does not appear before $i$ in $l$ and $\defined{(\fst{(l[i])})}$ (and $\defined{(\fst{(l[j])})}$ by \cref{defined_prop}) then
\[\actkey{k}{(\get{(\fst{(l[i])})})} = \actkey{k}{(\get{(\fst{(l[j])})})}\]
\end{claim}
\begin{proof}
By induction on $i$.
If $i = 0$ then the precondition is never met.
Else let $(s_{i -1}, n_{i - 1}, dir_{i - 1}) := l[i - 1]$ and $s_i := \fst{(l[i])}$. By \cref{defined_prop} $\defined{s_{i - 1}}$.
By \cref{scan_indexing_state} we either have:
\begin{itemize}
\item $s_i = \fdown{s_{i - 1}}{n_{i - 1}}$ and $dir_{i - 1} =\, \down$.
If $n_{i - 1}$ is an Action node, since $k$ does not appear before $i$, $k \neq n_{i - 1}.k$, then:
\begin{align*}
\actkey{k}{(\get{s_i})} &= \actkey{k}{(\get{(\hNode{(\get{s_{i - 1}})}{n_{i - 1}})})} \\
&= \actkey{k}{(\get{s_{i - 1}})} &\text{from \cref{actkey_handle_node}} \\
&= \actkey{k}{(\get{(\fst{(l[j])})})} &\text{for all $j < i - 1$ by IH}
\end{align*}
If $n_{i - 1}$ is a Rollback node then
\begin{align*}
\actkey{k}{(\get{s_i})} &= \actkey{k}{(\beginRb{(\get{s_{i - 1}})})}\\
&= \actkey{k}{(\get{s_{i - 1}})} &\text{by \cref{act_begin_rb}} \\
&= \actkey{k}{(\get{(\fst{(l[j])})})} &\text{for all $j < i - 1$ by IH }
\end{align*}
\item $s_i = \fup{s_{i - 1}}{n_{i - 1}}$ and $dir_{i - 1} =\, \up$.
If $n_{i - 1}$ is an Action node then
\begin{align*}
\actkey{k}{(\get{s_i})} &= \actkey{k}{(\get{s_{i - 1}})} \\
&=\actkey{k}{(\get{(\fst{(l[j])})})} &\text{\qquad \qquad for all $j < i - 1$ by IH }
\end{align*}
If $n_{i - 1}$ is a Rollback node then
\[\actkey{k}{(\get{s_i})} = \actkey{k}{(\enRb{(\get{s_{i - 1}})})} \]
By \cref{find_begin_rb} there exists an integer $0 \leq j' < i - 1$, a well-defined state $s_{j'} = \fst{(l[j'])}$ and a tree $sub$ such that $s_{i - 1} = \traverse{sub}{(\beginRb{(\get{s_{j'}})})}$. Therefore
\begin{align*}
\actkey{k}{(\get{s_i})} &= \actkey{k}{(\enRb{(\get{(\traverse{sub}{(\beginRb{(\get{s_j'})})})})})} \\
&= \actkey{k}{(\get{s_{j'}})} \text{\hskip 14.5em by \cref{skip_rb}} \\
&= \actkey{k}{(\get{(\fst{(l[j'])})})}
\end{align*}
In addition, by the induction hypothesis
\begin{align*}
\actkey{k}{(\get{s_{i - 1}})} &= \actkey{k}{(\get{(\fst{(l[j])})})} \text{\hskip 6em for all $j < i - 1$} \\
&= \actkey{k}{(\get{(\fst{(l[j'])})})} \\
&= \actkey{k}{(\get{s_i})}
\end{align*}
\end{itemize}
\end{proof}
\begin{corollary}[\textcode{firstAppearsSameActiveKeysGet}]
\label{actkey_first_appear}
Let tr be a tree of nodes, init a state, $k$ a key, $0 \leq j < i < 2\cdot \size{tr}$ two integers and let $l := \scan{tr}{init}$.
If $i$ is the first appearance of $k$ in $l$ and $\defined{(\fst{(l[i])})}$ (and $\defined{(\fst{(l[j])})}$ by \cref{defined_prop}), then
\[\actkey{k}{(\get{(\fst{(l[i])})})} = \actkey{k}{(\get{(\fst{(l[j])})})}\]
\end{corollary}
\begin{proof}
Direct consequence of \cref{actkey_not_appear}.
\end{proof}
\begin{corollary}[\textcode{firstAppearsHandleNodeUndefined}]
\label{defined_first_appear}
Let tr be a tree of nodes, init a state, $0 \leq i < 2\cdot \size{tr}$ an integer, let $l := \scan{tr}{init}$ and $(s, n, dir) := l[i]$.
If $n$ is an Action node with a well-defined key, $i$ is the first appearance of $n.k$ in $l$ and $\defined{s}$, then
\[\actkey{n.k}{(\get{init})} = \actkey{n.k}{(\get{s})}\]
\[\text{and in particular}\]
\[\defined{(\hNode{(\get{s})}{n})} \iff \actkey{n.k}{(\get{init})} = \mapping{n}\]
\end{corollary}
\begin{proof}
The first statement is a direct consequence of \cref{actkey_first_appear}. Applying \cref{defined_def} gives us the second statement.
\end{proof}
\begin{claim}[\textcode{appearsBeforeSameActiveKeysGet}]
\label{actkey_after_appear}
Let tr be a tree of nodes, $init_1$, $init_2$ two state, $k$ a key, $0 \leq i < 2\cdot \size{tr}$ an integer,
let $l_1 := \scan{tr}{init_1}$, $l_2 := \scan{tr}{init_2}$, $s^1_i := \fst{(l_1[i])}$ and $s^2_i := \fst{(l_2[i])}$.
If $k$ appears before $i$ in $l_1$ and $l_2$, $\defined{s^1_i}$ and $\defined{s^2_i}$, then
\[\actkey{k}{(\get{s^1_i})} = \actkey{k}{(\get{s^2_i})}\]
\end{claim}
\begin{proof}
By strong induction on i:
If $i = 0$ then the precondition is never met.
Else let $(s^1_{i -1}, n^1_{i - 1}, dir^1_{i - 1}) := l_1[i - 1]$, $(s^2_{i -1}, n^2_{i - 1}, dir^2_{i - 1}) := l_2[i - 1]$.
By \cref{scan_indexing_node}, $n_{i - 1} := n^1_{i - 1} = n^2_{i - 1}$ and $dir_{i - 1} := dir^1_{i - 1} = dir^2_{i - 1}$.
By \cref{scan_indexing_state} we either have:
\begin{itemize}
\item $s^1_i = \fdown{s^1_{i - 1}}{n_{i - 1}}$, $s^2_i = \fdown{s^2_{i - 1}}{n_{i - 1}}$ and $dir_{i - 1} =\, \down$
If $n_{i - 1}$ is an Action node then:
\begin{itemize}
\item If $n_{i - 1}.k = k$:
\begin{align*}
\actkey{n_{i - 1}.k}{(\get{s^1_i})} &= \actkey{n_{i - 1}.k}{(\get{(\hNode{(\get{s^1_{i - 1}})}{n_{i - 1}})})} \\
&= \actkey{n_{i - 1}.k}{(\get{(\hNode{(\get{s^2_{i - 1}})}{n_{i - 1}})})} & \text{by \cref{same_key_after_hnode}}\\
&= \actkey{n_{i - 1}.k}{(\get{s^2_{i}})} \\
\end{align*}
\item Otherwise, k appears before $i - 1$ in $l_1$ and $l_2$:
\begin{align*}
\actkey{k}{(\get{s^1_i})} &= \actkey{k}{(\get{(\hNode{(\get{s^1_{i - 1}})}{n_{i - 1}})})} \\
&= \actkey{k}{(\get{s^1_{i - 1}})} &\text{by \cref{actkey_handle_node}} \\
&= \actkey{k}{(\get{s^2_{i - 1}})} &\text{by IH} \\
&= \actkey{k}{(\get{(\hNode{(\get{s^2_{i - 1}})}{n_{i - 1}})})} &\text{by \cref{actkey_handle_node}} \\
&= \actkey{k}{(\get{s^2_i})}
\end{align*}
\end{itemize}
If $n_{i - 1}$ is a Rollback node then
\begin{align*}
\actkey{k}{(\get{s^1_i})} &= \actkey{k}{(\beginRb{(\get{s^1_{i - 1}})})}\\
&= \actkey{k}{(\get{s^1_{i - 1}})} &\text{by \cref{act_begin_rb}} \\
&= \actkey{k}{(\get{s^2_{i - 1}})} &\text{by IH} \\
&= \actkey{k}{(\beginRb{(\get{s^2_{i - 1}})})} &\text{by \cref{act_begin_rb}}\\
&= \actkey{k}{(\get{s^2_i})}
\end{align*}
\item $s^1_i = \fup{s^1_{i - 1}}{n_{i - 1}}$, $s^2_i = \fup{s^2_{i - 1}}{n_{i - 1}}$ and $dir_{i - 1} =\, \up$
If $n_{i - 1}$ is an Action node then
\begin{align*}
\actkey{k}{(\get{s^1_i})} &= \actkey{k}{(\get{s^1_{i - 1}})} \\
&= \actkey{k}{(\get{s^2_{i - 1}})} &\text{by IH}\\
&=\actkey{k}{(\get{s^2_i})}
\end{align*}
If $n_{i - 1}$ is a Rollback node then
\[\actkey{k}{(\get{s^1_i})} = \actkey{k}{(\enRb{(\get{s^1_{i - 1}})})} \]
By \cref{find_two_begin_rb} there exists an integer $0 \leq j < i - 1$ , well-defined states $s^1_{j}$, $s^2_{j}$ and tree $sub$ such that $s^1_{i - 1} = \traverse{sub}{(\beginRb{(\get{s^1_{j}})})}$,
$s^2_{i - 1} = \traverse{sub}{(\beginRb{(\get{s^2_{j}})})}$, $l_1[j] = (s^1_j, n_{i - 1}, \down)$, $l_2[j] = (s^2_j, n_{i - 1}, \down)$. Therefore
\begin{align*}
\actkey{k}{(\get{s^1_i})} &= \actkey{k}{(\enRb{(\get{(\traverse{sub}{(\beginRb{(\get{s^1_{j}})})})})})} \\
&= \actkey{k}{(\get{s^1_{j}})} &\text{by \cref{skip_rb}} \\
\intertext{If $k$ appears before $j$ in $l_1$ (and $l_2$ by \cref{appear_same}) then we can use the induction hypothesis and go backward.}
&= \actkey{k}{(\get{s^2_{j}})} &\text{by IH} \\
&= \actkey{k}{(\enRb{(\get{(\traverse{sub}{(\beginRb{(\get{s^2_{j}})})})})})} &\text{by \cref{skip_rb}}\\
&= \actkey{k}{(\get{s^2_i})}
\end{align*}
If $k$ does not appear before $j$ in $l_1$ and $l_2$, we can use \cref{find_first_appear} to obtain the index $j \leq j' < i$ such that $j'$ is the
first appearance of $k$ in $l_1$ and $l_2$.
Since $j' < i$ , by \cref{defined_prop}, $\defined{(\fst{(l_1[j'])})}$, $\defined{(\fst{(l_2[j'])})}$, $\defined{(\fst{(l_1[j' + 1])})}$ and $\defined{(\fst{(l_2[j' + 1])})}$.
By \cref{scan_indexing_state}, $\fst{(l_1[j' + 1])} = \hNode{(\get{(\fst{(l_1[j'])})})}{(\snd{(l_1[j'])})}$ and $(\snd{(l_1[j'])}).k = k$.
Similarly, $\fst{(l_2[j' + 1])} = \hNode{(\get{(\fst{(l_2[j'])})})}{(\snd{(l_2[j'])})}$ and $(\snd{(l_2[j'])}).k = k$.
Therefore:
\begin{align*}
\actkey{k}{s^1_{j}} &= \actkey{k}{(\get{(\fst{(l_1[j'])})})} &\text{by \cref{actkey_first_appear}} \\
&= \actkey{k}{(\get{(\fst{(l_2[j'])})})} &\text{by \cref{same_key_hnode}} \\
&= \actkey{k}{(\get{s^2_{j}})} &\text{by \cref{actkey_first_appear}} \\
&= \actkey{k}{(\enRb{(\get{(\traverse{sub}{(\beginRb{(\get{s^2_j})})})})})} &\text{by \cref{act_begin_rb}} \\
&= \actkey{k}{(\get{s^2_i})}
\end{align*}
\end{itemize}
\end{proof}
\begin{corollary}[\textcode{appearsBeforeSameUndefined}]
\label{same_defined_appear}
Let tr be a tree of nodes, $init_1, init_2$ states, $0 \leq i < 2\cdot \size{tr} - 1$ an integer, let $l_1 := \scan{tr}{init_1}$, $l_2 := \scan{tr}{init_2}$, $(s^1, n^1, dir^1) := l_1[i]$ and $(s^2, n^2, dir^2) := l_2[i]$.
By \cref{scan_indexing_node}, $n := n^1 = n^2$. If $n$ is an Action node, $n.k$ appears before $i$ in $l_1$ and $l_2$, $\defined{s^1}$ and $\defined{s^2}$, then
\[\defined{(\fst{(l_1[i + 1])})} \iff \defined{(\fst{(l_2[i + 1])})}\]
\end{corollary}
\begin{proof}
Consequence of \cref{actkey_after_appear} and \cref{defined_def}.
\end{proof}
\newpage
\section*{Empty state traversal}
\begin{definition}[\textcode{collect}]
Let $tr$ be a tree of nodes.
We respectively define the mapping \bolddef{\collect{tr}} as $\longtraverse{tr}{\emptyList}{f_{collect}}{id}$ and \bolddef{\collectTr{tr}} as
$\longscan{tr}{\emptyList}{f_{collect}}{id}$, where
\[\fcoll{m}{n} =
\begin{cases}
m + (n.k \to \mapping{n}) &\text{if $n$ is an Action node with a well-defined key and $n.k \notin m$} \\
m &\text{otherwise}
\end{cases} \]
\end{definition}
\begin{definition}[\textcode{emptyState}]
We define the empty state $\emptyState{tr}$ as the state whose rollback stack, locally created contracts set, consumed contracts set and local keys map are empty,
but whose global key map is $\collect{tr}$
\end{definition}
\begin{claim}[\textcode{collectTraceProp}]
\label{collect_submap}
Let tr be a tree of nodes and $0 \leq i < 2 \cdot \, \size{tr}$ an integer
\[\fst{((\collectTr{tr})[i])} \subseteq \collect{tr}\]
\end{claim}
\begin{proof}
By backward induction on $i$ and applying \cref{scan_indexing_state}.
\end{proof}
\begin{claim}[\textcode{collectTraceDoesNotAppear}, \textcode{collectDoesNotAppear}]
\label{collect_not_contains}
Let tr be a tree of nodes, $0 \leq i < 2 \cdot \, \size{tr}$ an integer and $k$ a key.
\[k \text{ does not appear before } i \text{ in } \collectTr{tr} \iff k \notin \fst{((\collectTr{tr})[i])}\]
In particular
\[k \text{ does not appear before } 2 \cdot \size{tr} - 1 \text{ in } \collectTr{tr} \iff k \notin \collect{tr}\]
\end{claim}
\begin{proof}
Induction on $i$, applying \cref{scan_indexing_state}.
\end{proof}
\begin{corollary}[\textcode{collectGet}]
\label{first_mapping}
Let tr be a tree of nodes, $0 \leq i < 2 \cdot \, \size{tr}$ an integer,
$n := \snd{((\collectTr{tr})[i])}$. If $n$ is an Action node with a well-defined key and $i$ is the first appearance of $n.k$ in $\collectTr{tr}$, then
\[(\collect{tr})[n.k] = \mapping{n}\]
\end{corollary}
\begin{proof}
By \cref{collect_not_contains}, $n.k \notin \fst{((\collectTr{tr})[i])}$. By applying \cref{scan_indexing_state} we have that $(n.k \to \mapping{n}) \in \fst{((\collectTr{tr})[i + 1])}$
if $i < 2 \cdot \, \size{tr} - 1$ and $(n.k \to \mapping{n}) \in \collect{tr}$ otherwise. In the first case we make use of \cref{collect_submap} to prove the claim.
\end{proof}
\begin{corollary}[\textcode{collectContains}]
\label{find_k_first_appear}
Let $tr$ be a tree of nodes and $k$ a key. If $k \in \collect{tr}$ then there exists an integer $0 \leq i < 2 \cdot \size{tr} - 1$ such that
$i$ is the first appearance of $k$ in $\collectTr{tr}$.
\end{corollary}
\begin{proof}
By \cref{collect_not_contains}, if $k \in \collect{tr}$ then $k$ does not appear before $2 \cdot \size{tr} - 1$. \cref{find_first_appear} concludes the proof.
\end{proof}
\begin{corollary}[\textcode{firstAppearsHandleNodeUndefinedEmpty}]
\label{defined_globalkeys_mapping}
Let tr be a tree of nodes, $init$ a state, $0 \leq i < 2\cdot \size{tr} - 1$ an integer, let $l := \scan{tr}{init}$, and $n := \snd{(l[i])}$.
If $n$ is an Action node with a well-defined key, $i$ is the first appearance of $n.k$ in $l$ and $\defined{(\fst{(l[i])})}$ then
\[\defined{(\fst{(l[i + 1])})} \iff \actkey{n.k}{(\get{init})} = (\emptyState{tr}.globalKeys)[n.k]\]
\end{corollary}
\begin{proof}
Let $l_{\varepsilon} = \scan{tr}{\emptyState{tr}}$. We know by \cref{scan_indexing_node} that $n = \snd{(l_{\varepsilon}[i])}$.
and $\fst{(l_\varepsilon[i + 1])} = \hNode{(\fst{(l_\varepsilon[i])})}{n}$.
Furthemore by \cref{appear_same}, $n.k$ does not appear before $i$ in $l_{\varepsilon}$. Finally by \cref{defined_traverse_prop}, if $\defined{(\traverse{tr}{\emptyState{tr}})}$ then $\defined{(\fst{(l_{\varepsilon}[i])})}$.
\begin{align*}
&\actkey{n.k}{(\get{init})} = (\emptyState{tr}.globalKeys)[n.k] \\
\iff &\actkey{n.k}{(\get{init})} = (\collect{tr})[n.k] \\
\iff &\actkey{n.k}{(\get{init})} =\, \mapping{n} &\text{by \cref{first_mapping}} \\
\iff &\defined{(\hNode{(\get{(\fst{(l[i])})})}{n})} &\text{by \cref{defined_first_appear}}\\
\iff &\defined{(\fst{(l[i + 1])})} &\text{by \cref{scan_indexing_state}}
\end{align*}
\end{proof}
\begin{corollary}
\label{defined_empty_traverse}
Let tr be a tree of nodes, $init$ a state, $0 \leq i < 2\cdot \size{tr} - 1$ an integer, let $l := \scan{tr}{init}$, and $n := \snd{(l[i])}$.
If $n$ is an Action node with a well-defined key, $\defined{(\traverse{tr}{\emptyState{tr}})}$, $n.k$ appears before $i$ in $l$ and $\defined{(\fst{(l[i])})}$ then
\[\defined{(\fst{(l[i + 1])})}\]
\end{corollary}
\begin{proof}
By \cref{defined_traverse_prop}, if $\defined{(\traverse{tr}{\emptyState{tr}})}$ then $\defined{(\fst{((\scan{tr}{\emptyState{tr}})[i])})}$ and \\
$\defined{(\fst{((\scan{tr}{\emptyState{tr}})[i + 1])})}$. Applying \cref{same_defined_appear} concludes the proof.
\end{proof}
\begin{res}[\textcode{traverseTransactionEmptyDefined}]
Let $tr$ be a tree of nodes and $init$ a well-defined state. If $\defined{(\traverse{tr}{\emptyState{tr}})}$, then
\[ (\forall (k \to m) \in \emptyState{tr}.globalKeys,\ \actkey{k}{(\get{init})} = m) \iff \defined{(\traverse{tr}{init})} \]
\end{res}
\begin{proof}
Let $l := \scan{tr}{init}$.
$(\Rightarrow)$ direction: By \cref{defined_alt_def}, we only need to prove that for an arbitrary $0 \leq i < 2 \cdot \, \size{tr} \, - 1$,\\
$\defined{(\fst{(l[i])})} \implies \defined{(\fst{(l[i + 1])})}$.
If $n := \snd{(l[i])}$ is a Rollback node, if $\trd{(l[i])} =\, \up$ or if $n$ is an Action node with no key, then by \cref{scan_indexing_state} (and \cref{actkey_handle_node} in the Action node case) this is automatically true.
If $n$ is an Action node then either:
\begin{itemize}
\item $i$ is the first appearance of $n.k$ in which case by \cref{defined_globalkeys_mapping} validates the claim
\item $n.k$ appears before $i$ in which case by \cref{defined_empty_traverse}, $\defined{(\fst{(l[i + 1])})}$
\end{itemize}
$(\Leftarrow)$ direction:
Assume there exists a key $k$ such that $k \in \emptyState{tr}.globalKeys$ and $\actkey{k}{(\get{init})} \neq (\emptyState{tr}.globalKeys)[k]$.
Then $k \in \collect{tr}$ and by \cref{find_k_first_appear}, there is a $0 \leq i < 2 \cdot \size{tr} - 1$ such that
$i$ is the first appearance of $k$ in $\collectTr{tr}$. In particular this means that $n := \snd{((\collectTr{tr})[i])}$ is an Action node with a well-defined
key and $k = n.k$. By \cref{defined_globalkeys_mapping} this means that either $\neg{\defined{(\fst{(l[i])})}}$ or $\neg{\defined{(\fst{(l[i + 1])})}}$, which both imply by \cref{defined_traverse_prop}
that $\neg{\defined{(\traverse{tr}{init})}}$.
\end{proof}
\end{document}

27
daml-lf/verification/scripts/stainless_imports.txt Normal file
View File

@ -0,0 +1,27 @@
package lf.verified
package translation
import stainless.lang._
import stainless.annotation._
import stainless.collection._
import utils.{
Either,
Map,
Set,
Value,
GlobalKey,
Transaction,
Unreachable,
Node,
ContractKeyUniquenessMode,
Option
}
import utils.Value.ContractId
import utils.Transaction.{
KeyCreate,
KeyInputError,
NegativeKeyLookup,
InconsistentContractKey,
DuplicateContractKey,
KeyInput
}

85
daml-lf/verification/scripts/verification_script.sh Executable file
View File

@ -0,0 +1,85 @@
#!/bin/bash
# Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
# SPDX-License-Identifier: Apache-2.0
cd scripts
STAINLESS=$1
ARGS="--watch=false --timeout=30 --vc-cache=false --compact=true --solvers=nativez3 --infer-measures=false"
#Running stainless, there are 3 modes:
# - translate: translate the original file to a simplified version and verifies only that
# the translation is correct
# - verification: verifies the proof
# - test: test that stainless is executed correctly; does not verify any file
# Finally returns the exit code of stainless:
# 0 : everything verifies
# 1 : something does not verify
# 2 : the files do not compile
if [[ $2 = "translate" ]]; then
DAML_ROOT=$(git rev-parse --show-toplevel);
FILE_LOCATION="$DAML_ROOT/daml-lf/transaction/src/main/scala/com/digitalasset/daml/lf/transaction/ContractStateMachine.scala";
#We first load the original file in a variable
FILE=$(cat $FILE_LOCATION)
#To be able to quickly double check the output we first remove comments and emptyLines
FILE=$(sed '/^\s*\/\*/d' <<<"$FILE");
FILE=$(sed '/^\s*\*/d' <<<"$FILE");
FILE=$(sed '/^\s*\/\//d' <<<"$FILE");
FILE=$(sed '/^$/d' <<<"$FILE");
#Replacing covariant options and lists by invariant ones
FILE=$(sed 's/\bNone\b/None()/g' <<<"$FILE");
FILE=$(sed 's/\([A-Za-z0-9_]*\)\s*::\s*\([A-Za-z0-9_]*\)/Cons(\1, \2)/g' <<<"$FILE");
FILE=$(sed 's/\(\([A-Za-z0-9_]\|\.\)*\).filterNot(\(\([A-Za-z0-9_]\|\.\)*\))/Option.filterNot(\1, \3)/g' <<<"$FILE");
FILE=$(sed 's/\bNil\b/Nil()/g' <<<"$FILE");
#Replacing KeyMapping with Option
FILE=$(sed '/^\s*val\s*KeyActive\s*=/d' <<<"$FILE");
FILE=$(sed '/^\s*val\s*KeyInactive\s*=/d' <<<"$FILE");
FILE=$(sed 's/\s\(ContractStateMachine\.\)\?KeyInactive\b/ None[ContractId]()/g' <<<"$FILE");
FILE=$(sed 's/\s\(ContractStateMachine\.\)\?KeyActive\b/ Some[ContractId]/g' <<<"$FILE");
FILE=$(sed '/^\s*val KeyActive/d' <<<"$FILE");
#Replacing exceptions with Unreachable
FILE=$(sed -z 's/throw\s*new\s*[A-Za-z0-9]\+(\s*\("\([A-Za-z0-9(),;:_]\|\s\|\[\|\]\|\-\|\.\|\/\)*"\)\?\s*)/Unreachable()/g' <<<"$FILE");
FILE=$(sed 's/throw\s*new\s*[A-Za-z0-9]\+(\("\([A-Za-z0-9(),;:_]\|\s\|\[\|\]\|\-\|\.\|\/\)*"\)\?)/Unreachable()/' <<<"$FILE");
#Replacing imports and package name by our own (located in $2) and writing the output in translation/ContractStateMachine.scala
FILE=$(sed '/^package/d' <<<"$FILE");
FILE=$(sed -z 's/\s*import\s*\([A-Za-z0-9]\|\.\)\+{\([A-Za-z0-9(),:;]\|\s\|\[\|\]\|\-\|\.\|\/\)*}//g' <<<"$FILE");
FILE=$(sed '/^\s*import\s*\([A-Za-z0-9]\|\.\)\+/d' <<<"$FILE");
FILE=$(sed 's/\(\s*\)\(case class State\)/\1@dropVCs\n\1\2/' <<<"$FILE");
ADD=$(cat stainless_imports.txt);
FILE_DESTINATION="../translation/ContractStateMachine.scala"
echo -e "${ADD}$FILE" > $FILE_DESTINATION;
$STAINLESS ../utils/* ../translation/* ../transaction/* $ARGS;
RES=$?
#Cleaning everything up
rm $FILE_DESTINATION
exit $RES
elif [[ $2 = "verify" ]]; then
$STAINLESS ../utils/* ../transaction/* ../tree/* $ARGS;
exit $?
elif [[ $2 = "test" ]]; then
$STAINLESS $ARGS;
exit $?
else
exit 3
fi

17
daml-lf/verification/stainless.nix Normal file
View File

@ -0,0 +1,17 @@
let
pkgs = import <nixpkgs> {};
stdenv = pkgs.stdenv;
in rec {
stainlessEnv = stdenv.mkDerivation rec {
name = "stainless-env";
shellHook = ''
alias cls=clear
'';
buildInputs = with pkgs; [
stdenv
sbt
openjdk17
z3
];
};
}

307
daml-lf/verification/transaction/CSMAdvance.scala Normal file
View File

@ -0,0 +1,307 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package transaction
import stainless.lang.{
unfold,
decreases,
BooleanDecorations,
Either,
Some,
None,
Option,
Right,
Left,
}
import stainless.annotation._
import scala.annotation.targetName
import stainless.collection._
import utils.Value.ContractId
import utils.Transaction.{DuplicateContractKey, InconsistentContractKey, KeyInputError}
import utils._
import ContractStateMachine._
import CSMEitherDef._
/** This file expresses the change of active state after handling a node as a call to [[ActiveLedgerState.advance]]
* with another state representing what is added.
*
* It also contains necessary properties of the advance methods that are needed in order to prove the above claim.
*/
object CSMAdvanceDef {
/** Express what is added to an active state after handling a node.
*
* @see [[CSMAdvance.handleNodeActiveState]] for an use case of this definition.
*/
@pure
@opaque
def actionActiveStateAddition(id: NodeId, n: Node.Action): ActiveLedgerState = {
n match {
case create: Node.Create =>
ActiveLedgerState(
Set(create.coid),
Map.empty[ContractId, NodeId],
(create.gkeyOpt match {
case None() => Map.empty[GlobalKey, ContractId]
case Some(k) => Map[GlobalKey, ContractId](k -> create.coid)
}),
)
case exe: Node.Exercise =>
ActiveLedgerState(
Set.empty[ContractId],
(if (exe.consuming) Map(exe.targetCoid -> id) else Map.empty[ContractId, NodeId]),
Map.empty[GlobalKey, ContractId],
)
case _ => ActiveLedgerState.empty
}
}
}
object CSMAdvance {
import CSMAdvanceDef._
/** [[ActiveLedgerState.empty]] is a neutral element wrt [[ActiveLedgerState.advance]].
*
* The set extensionality axiom is used here for the sake of simplicity.
*/
@pure
@opaque
def emptyAdvance(s: ActiveLedgerState): Unit = {
unfold(s.advance(ActiveLedgerState.empty))
unfold(ActiveLedgerState.empty.advance(s))
SetProperties.unionEmpty(s.locallyCreatedThisTimeline)
SetAxioms.extensionality(
s.locallyCreatedThisTimeline ++ Set.empty[ContractId],
s.locallyCreatedThisTimeline,
)
SetAxioms.extensionality(
Set.empty[ContractId] ++ s.locallyCreatedThisTimeline,
s.locallyCreatedThisTimeline,
)
MapProperties.concatEmpty(s.consumedBy)
MapAxioms.extensionality(s.consumedBy ++ Map.empty[ContractId, NodeId], s.consumedBy)
MapAxioms.extensionality(Map.empty[ContractId, NodeId] ++ s.consumedBy, s.consumedBy)
MapProperties.concatEmpty(s.localKeys)
MapAxioms.extensionality(s.localKeys ++ Map.empty[GlobalKey, ContractId], s.localKeys)
MapAxioms.extensionality(Map.empty[GlobalKey, ContractId] ++ s.localKeys, s.localKeys)
}.ensuring(
(s.advance(ActiveLedgerState.empty) == s) &&
(ActiveLedgerState.empty.advance(s) == s)
)
/** [[ActiveLedgerState.advance]] is an associative operation.
*
* The set extensionality axiom is used here for the sake of simplicity.
*/
@pure
@opaque
def advanceAssociativity(
s1: ActiveLedgerState,
s2: ActiveLedgerState,
s3: ActiveLedgerState,
): Unit = {
unfold(s1.advance(s2).advance(s3))
unfold(s1.advance(s2))
unfold(s1.advance(s2.advance(s3)))
unfold(s2.advance(s3))
SetProperties.unionAssociativity(
s1.locallyCreatedThisTimeline,
s2.locallyCreatedThisTimeline,
s3.locallyCreatedThisTimeline,
)
SetAxioms.extensionality(
(s1.locallyCreatedThisTimeline ++ s2.locallyCreatedThisTimeline) ++ s3.locallyCreatedThisTimeline,
s1.locallyCreatedThisTimeline ++ (s2.locallyCreatedThisTimeline ++ s3.locallyCreatedThisTimeline),
)
MapProperties.concatAssociativity(s1.consumedBy, s2.consumedBy, s3.consumedBy)
MapAxioms.extensionality(
(s1.consumedBy ++ s2.consumedBy) ++ s3.consumedBy,
s1.consumedBy ++ (s2.consumedBy ++ s3.consumedBy),
)
MapProperties.concatAssociativity(s1.localKeys, s2.localKeys, s3.localKeys)
MapAxioms.extensionality(
(s1.localKeys ++ s2.localKeys) ++ s3.localKeys,
s1.localKeys ++ (s2.localKeys ++ s3.localKeys),
)
}.ensuring(
s1.advance(s2).advance(s3) == s1.advance(s2.advance(s3))
)
/** Two states are equal if and only if one is the other after calling [[ActiveLedgerState.advance]] with
* [[ActiveLedgerState.empty]].
*/
@pure
@opaque
def sameActiveStateActiveState[T](s1: State, e2: Either[T, State]): Unit = {
require(sameActiveState(s1, e2))
unfold(sameActiveState(s1, e2))
e2 match {
case Right(s2) => emptyAdvance(s1.activeState)
case _ => Trivial()
}
}.ensuring(
sameActiveState(s1, e2) ==
e2.forall(
_.activeState ==
s1.activeState.advance(ActiveLedgerState.empty)
)
)
/** Express the [[State.activeState]] of a [[State]], after handling a [[Node.Create]], as a call to
* [[ActiveLedgerState.advance]].
*
* The set extensionality axiom is used here for the sake of simplicity.
*/
@pure
@opaque
def visitCreateActiveState(s: State, contractId: ContractId, mbKey: Option[GlobalKey]): Unit = {
unfold(s.visitCreate(contractId, mbKey))
unfold(
s.activeState.advance(
ActiveLedgerState(
Set(contractId),
Map.empty[ContractId, NodeId],
(mbKey match {
case None() => Map.empty[GlobalKey, ContractId]
case Some(k) => Map[GlobalKey, ContractId](k -> contractId)
}),
)
)
)
unfold(s.activeState.locallyCreatedThisTimeline.incl(contractId))
MapProperties.concatEmpty(s.activeState.consumedBy)
MapAxioms.extensionality(
s.activeState.consumedBy ++ Map.empty[ContractId, NodeId],
s.activeState.consumedBy,
)
mbKey match {
case None() =>
MapProperties.concatEmpty(s.activeState.localKeys)
MapAxioms.extensionality(
s.activeState.localKeys ++ Map.empty[GlobalKey, ContractId],
s.activeState.localKeys,
)
case Some(k) =>
unfold(s.activeState.localKeys.updated(k, contractId))
}
}.ensuring(
s.visitCreate(contractId, mbKey)
.forall(
_.activeState == s.activeState.advance(
ActiveLedgerState(
Set(contractId),
Map.empty[ContractId, NodeId],
(mbKey match {
case None() => Map.empty[GlobalKey, ContractId]
case Some(k) => Map[GlobalKey, ContractId](k -> contractId)
}),
)
)
)
)
/** Express the [[State.activeState]] of a [[State]], after handling a [[Node.Exercise]], as a call to
* [[ActiveLedgerState.advance]].
*
* The set extensionality axiom is used here for the sake of simplicity.
*/
@pure
@opaque
def visitExerciseActiveState(
s: State,
nodeId: NodeId,
targetId: ContractId,
mbKey: Option[GlobalKey],
byKey: Boolean,
consuming: Boolean,
): Unit = {
unfold(s.visitExercise(nodeId, targetId, mbKey, byKey, consuming))
unfold(
s.activeState.advance(
ActiveLedgerState(
Set.empty[ContractId],
(if (consuming) Map(targetId -> nodeId) else Map.empty[ContractId, NodeId]),
Map.empty[GlobalKey, ContractId],
)
)
)
unfold(sameActiveState(s, s.assertKeyMapping(targetId, mbKey)))
s.assertKeyMapping(targetId, mbKey) match {
case Right(state) =>
unfold(state.consume(targetId, nodeId))
unfold(state.activeState.consume(targetId, nodeId))
unfold(state.activeState.consumedBy.updated(targetId, nodeId))
MapProperties.concatEmpty(state.activeState.consumedBy)
MapAxioms.extensionality(
state.activeState.consumedBy ++ Map.empty[ContractId, NodeId],
state.activeState.consumedBy,
)
SetProperties.unionEmpty(state.activeState.locallyCreatedThisTimeline)
SetAxioms.extensionality(
state.activeState.locallyCreatedThisTimeline ++ Set.empty[ContractId],
state.activeState.locallyCreatedThisTimeline,
)
MapProperties.concatEmpty(state.activeState.localKeys)
MapAxioms.extensionality(
state.activeState.localKeys ++ Map.empty[GlobalKey, ContractId],
state.activeState.localKeys,
)
case _ => Trivial()
}
}.ensuring(
s.visitExercise(nodeId, targetId, mbKey, byKey, consuming)
.forall(
_.activeState == s.activeState.advance(
ActiveLedgerState(
Set.empty[ContractId],
(if (consuming) Map(targetId -> nodeId) else Map.empty[ContractId, NodeId]),
Map.empty[GlobalKey, ContractId],
)
)
)
)
/** Express the [[State.activeState]] of a [[State]], after handling a [[Node.Action]], as a call to
* [[ActiveLedgerState.advance]].
*/
@pure
@opaque
def handleNodeActiveState(s: State, nodeId: NodeId, n: Node.Action): Unit = {
unfold(s.handleNode(nodeId, n))
unfold(actionActiveStateAddition(nodeId, n))
n match {
case create: Node.Create => visitCreateActiveState(s, create.coid, create.gkeyOpt)
case fetch: Node.Fetch =>
sameActiveStateActiveState(s, s.assertKeyMapping(fetch.coid, fetch.gkeyOpt))
case lookup: Node.LookupByKey =>
sameActiveStateActiveState(s, s.visitLookup(lookup.gkey, lookup.result))
case exe: Node.Exercise =>
visitExerciseActiveState(s, nodeId, exe.targetCoid, exe.gkeyOpt, exe.byKey, exe.consuming)
}
}.ensuring(
s.handleNode(nodeId, n)
.forall(sf => sf.activeState == s.activeState.advance(actionActiveStateAddition(nodeId, n)))
)
}

673
daml-lf/verification/transaction/CSMEither.scala Normal file
View File

@ -0,0 +1,673 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package transaction
import stainless.lang.{
unfold,
decreases,
BooleanDecorations,
Either,
Some,
None,
Option,
Right,
Left,
}
import stainless.annotation._
import scala.annotation.targetName
import stainless.collection._
import utils.Value.ContractId
import utils.Transaction.{DuplicateContractKey, InconsistentContractKey, KeyInputError}
import utils._
import ContractStateMachine._
/** Having pattern matching inside ensuring or require clauses generates a lot of verification conditions
* and considerably slows down stainless. In order to avoid that, every pattern match in a postcondition
* or precondition should, if possible, be enclosed in an opaque function.
*
* This files gather all field equalities between a [[State]] and a Either[T, State], or between an Either[T, State]
* and an Either[U, State], where T and U are generic type.
* In practice T will be either [[KeyInputError]], [[InconsistentContractKey]] or [[DuplicateContractKey]]. Having a
* generic type avoids Stainless to spend time on what kind of type that is, making it sort of 'opaque'.
*
* It also describes error propagation, which happens when processing a transaction. The exact definitions of error
* propagation are described lower in the file.
*/
object CSMEitherDef {
/** Checks state equality. Equivalent to checking equality for every field.
*
* @param s1 A well-defined state
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1 is equal to s2 if s2 is well-defined, otherwise returns true
*/
@pure
@opaque
def sameState[T](s1: State, s2: Either[T, State]): Boolean = {
unfold(sameStack(s1, s2))
unfold(sameGlobalKeys(s1, s2))
unfold(sameActiveState(s1, s2))
unfold(sameLocallyCreated(s1, s2))
unfold(sameConsumed(s1, s2))
s2.forall((s: State) => s1 == s)
}.ensuring(
_ == (sameStack(s1, s2) && sameGlobalKeys(s1, s2) && sameActiveState(
s1,
s2,
) && sameLocallyCreated(s1, s2) && sameConsumed(s1, s2))
)
/** Checks state equality. Equivalent to checking equality for every field.
*
* @param s1 A state that can be either well-defined or erroneous
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1 is equal to s2 when both are well-defined, otherwise returns true
*/
@pure
@opaque
def sameState[U, T](s1: Either[U, State], s2: Either[T, State]): Boolean = {
unfold(sameStack(s1, s2))
unfold(sameGlobalKeys(s1, s2))
unfold(sameActiveState(s1, s2))
unfold(sameLocallyCreated(s1, s2))
unfold(sameConsumed(s1, s2))
s1.forall((s: State) => sameState(s, s2))
}.ensuring(
_ == (sameStack(s1, s2) && sameGlobalKeys(s1, s2) && sameActiveState(
s1,
s2,
) && sameLocallyCreated(s1, s2) && sameConsumed(s1, s2))
)
/** Checks that two states have the same [[State.locallyCreated]] field.
*
* @param s1 A well-defined state
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.locallyCreated is equal to s2.locallyCreated if s2 is well-defined, otherwise returns true
*/
@pure
@opaque
def sameLocallyCreated[T](s1: State, s2: Either[T, State]): Boolean = {
s2.forall((s: State) => s1.locallyCreated == s.locallyCreated)
}
/** Checks that two states have the same [[State.locallyCreated]] field.
*
* @param s1 A state that can be either well-defined or erroneous
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.locallyCreated is equal to s2.locallyCreated when both are well-defined,
* otherwise returns true
*/
@pure
@opaque
def sameLocallyCreated[U, T](s1: Either[U, State], s2: Either[T, State]): Boolean = {
s1.forall((s: State) => sameLocallyCreated(s, s2))
}
/** Checks that two states have the same [[State.consumed]] field.
*
* @param s1 A well-defined state
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.consumed is equal to s2.consumed if s2 is well-defined, otherwise returns true
*/
@pure
@opaque
def sameConsumed[T](s1: State, s2: Either[T, State]): Boolean = {
s2.forall((s: State) => s1.consumed == s.consumed)
}
/** Checks that two states have the same [[State.consumed]] field.
*
* @param s1 A state that can be either well-defined or erroneous
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.consumed is equal to s2.locallyCreated when both are well-defined,
* otherwise returns true
*/
@pure
@opaque
def sameConsumed[U, T](s1: Either[U, State], s2: Either[T, State]): Boolean = {
s1.forall((s: State) => sameConsumed(s, s2))
}
/** Checks that two states have the same [[State.activeState]] field.
*
* @param s1 A well-defined state
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.activeState is equal to s2.activeState if s2 is well-defined, otherwise returns true
*/
@pure
@opaque
def sameActiveState[T](s1: State, s2: Either[T, State]): Boolean = {
unfold(sameLocallyCreatedThisTimeline(s1, s2))
unfold(sameConsumedBy(s1, s2))
unfold(sameLocalKeys(s1, s2))
s2.forall((s: State) => s1.activeState == s.activeState)
}.ensuring(
_ == (sameLocallyCreatedThisTimeline(s1, s2) && sameConsumedBy(s1, s2) && sameLocalKeys(s1, s2))
)
/** Checks that two states have the same [[State.activeState]] field.
*
* @param s1 A state that can be either well-defined or erroneous
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.activeState is equal to s2.activeState when both are well-defined,
* otherwise returns true
*/
@pure
@opaque
def sameActiveState[U, T](s1: Either[U, State], s2: Either[T, State]): Boolean = {
unfold(sameLocallyCreatedThisTimeline(s1, s2))
unfold(sameConsumedBy(s1, s2))
unfold(sameLocalKeys(s1, s2))
s1.forall((s: State) => sameActiveState(s, s2))
}.ensuring(
_ == (sameLocallyCreatedThisTimeline(s1, s2) && sameConsumedBy(s1, s2) && sameLocalKeys(s1, s2))
)
/** Checks that two states have the same [[State.activeState.localKeys]] field.
*
* @param s1 A well-defined state
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.activeState.localKeys is equal to s2.activeState.localKeys if s2 is well-defined, otherwise returns true
*/
@pure
@opaque
def sameLocalKeys[T](s1: State, s2: Either[T, State]): Boolean = {
s2.forall((s: State) => s1.activeState.localKeys == s.activeState.localKeys)
}
/** Checks that two states have the same [[State.activeState.localKeys]] field.
*
* @param s1 A state that can be either well-defined or erroneous
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.activeState.localKeys is equal to s2.activeState.localKeys when both are well-defined,
* otherwise returns true
*/
@pure
@opaque
def sameLocalKeys[U, T](s1: Either[U, State], s2: Either[T, State]): Boolean = {
s1.forall((s: State) => sameLocalKeys(s, s2))
}
/** Checks that two states have the same [[State.activeState.locallyCreatedThisTimeline]] field.
*
* @param s1 A well-defined state
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.activeState.locallyCreatedThisTimeline is equal to s2.activeState.locallyCreatedThisTimeline
* if s2 is well-defined, otherwise returns true
*/
@pure
@opaque
def sameLocallyCreatedThisTimeline[T](s1: State, s2: Either[T, State]): Boolean = {
s2.forall((s: State) =>
s1.activeState.locallyCreatedThisTimeline == s.activeState.locallyCreatedThisTimeline
)
}
/** Checks that two states have the same [[State.activeState.locallyCreatedThisTimeline]] field.
*
* @param s1 A state that can be either well-defined or erroneous
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.activeState.locallyCreatedThisTimeline is equal to s2.activeState.locallyCreatedThisTimeline
* when both are well-defined, otherwise returns true
*/
@pure
@opaque
def sameLocallyCreatedThisTimeline[U, T](s1: Either[U, State], s2: Either[T, State]): Boolean = {
s1.forall((s: State) => sameLocallyCreatedThisTimeline(s, s2))
}
/** Checks that two states have the same [[State.activeState.consumedBy]] field.
*
* @param s1 A well-defined state
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.activeState.consumedBy is equal to s2.activeState.consumedBy if s2 is well-defined, otherwise
* returns true
*/
@pure
@opaque
def sameConsumedBy[T](s1: State, s2: Either[T, State]): Boolean = {
s2.forall((s: State) => s1.activeState.consumedBy == s.activeState.consumedBy)
}
/** Checks that two states have the same [[State.activeState.consumedBy]] field.
*
* @param s1 A state that can be either well-defined or erroneous
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.activeState.consumedBy is equal to s2.activeState.consumedBy when both are well-defined,
* otherwise returns true
*/
@pure
@opaque
def sameConsumedBy[U, T](s1: Either[U, State], s2: Either[T, State]): Boolean = {
s1.forall((s: State) => sameConsumedBy(s, s2))
}
/** Checks that two states have the same [[State.globalKeys]] field.
*
* @param s1 A well-defined state
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.globalKeys is equal to s2.globalKeys if s2 is well-defined, otherwise returns true
*/
@pure
@opaque
def sameGlobalKeys[T](s1: State, s2: Either[T, State]): Boolean = {
s2.forall((s: State) => s1.globalKeys == s.globalKeys)
}
/** Checks that two states have the same [[State.globalKeys]] field.
*
* @param s1 A state that can be either well-defined or erroneous
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.globalKeys is equal to s2.globalKeys when both are well-defined,
* otherwise returns true
*/
@pure
@opaque
def sameGlobalKeys[U, T](s1: Either[U, State], s2: Either[T, State]): Boolean = {
s1.forall((s: State) => sameGlobalKeys(s, s2))
}
/** Checks that two states have the same [[State.rollbackStack]] field.
*
* @param s1 A well-defined state
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.rollbackStack is equal to s2.rollbackStack if s2 is well-defined, otherwise returns true
*/
@pure
@opaque
def sameStack[T](s1: State, s2: Either[T, State]): Boolean = {
s2.forall((s: State) => s1.rollbackStack == s.rollbackStack)
}
/** Checks that two states have the same [[State.rollbackStack]] field.
*
* @param s1 A state that can be either well-defined or erroneous
* @param s2 A state that can be either well-defined or erroneous
* @return Whether s1.activeState.rollbackStack is equal to s2.rollbackStack when both are well-defined,
* otherwise returns true
*/
@pure
@opaque
def sameStack[U, T](s1: Either[U, State], s2: Either[T, State]): Boolean = {
s1.forall((s: State) => sameStack(s, s2))
}
/** Various definitions of error propagation
*
* @param s1
* The state or error before the operation
*
* @param s2
* The state or error after the operation
*
* 1. PropagatesError: if s1 is an error state then s2 will be an error as well. Both errors
* do not necessarily need to be the same.
*
* 2. PropagatesBothError: s1 is an error state if and only if s2 is an error state as well,
* although both errors do not necessarily need to be the same
*
* 3. PropagatesSameError: if s1 is an error state then s1 == s2
*
* 4. SameError: if s1 or s2 is an error state then s1 == s2
*
* Implications:
*
* SameError ==> PropagatesSameError ==> PropagatesError
* SameError ==> PropagatesBothError ==> PropagatesError
*/
/** Checks that if a state is erroneous than the other one is as well.
*
* @see above for further details
*/
@pure
@opaque
def propagatesError[U, T, V](s1: Either[U, V], s2: Either[T, V]): Boolean = {
s1.isLeft ==> s2.isLeft
}
/** Checks that a state is erroneous if and only if the other one is as well.
*
* @see above for further details
*/
@pure
def propagatesBothError[U, T, V](s1: Either[U, V], s2: Either[T, V]): Boolean = {
propagatesError(s1, s2) && propagatesError(s2, s1)
}
/** Checks that if a state is erroneous then the other one is erroneous has well and outputs the same result.
*
* @see above for further details
*/
@pure
@opaque
def propagatesSameError[T, V](s1: Either[T, V], s2: Either[T, V]): Boolean = {
unfold(propagatesError(s1, s2))
s1.isLeft ==> (s1 == s2)
}.ensuring(_ ==> propagatesError(s1, s2))
/** Checks that a state is erroneous if and only if the other one is erroneous. Moreover when this happens,
* both errors are the same.
*
* @see above for further details
*/
@pure
def sameError[T, V](s1: Either[T, V], s2: Either[T, V]): Boolean = {
propagatesSameError(s1, s2) && propagatesSameError(s2, s1)
}.ensuring(_ ==> propagatesBothError(s1, s2))
}
object CSMEither {
import CSMEitherDef._
/** Field equality extension is always reflexive. In order to be transitivity, we need error propagation
* on at least the second operation. In fact transitivity does not hold if we have s1 -> error -> s2
* with s1.field =/= s2.field.
*/
/** Reflexivity of [[State.rollbackStack]] field equality.
*/
@pure
@opaque
def sameStackReflexivity[T](s: Either[T, State]): Unit = {
unfold(sameStack(s, s))
s match {
case Left(_) => Trivial()
case Right(s2) => unfold(sameStack(s2, s))
}
}.ensuring(sameStack(s, s))
/** Transitivity of [[State.rollbackStack]] field equality. Holds only if error propagates between the
* second and the third state.
*/
@pure
@opaque
def sameStackTransitivity[V, W](s1: State, s2: Either[V, State], s3: Either[W, State]): Unit = {
require(sameStack(s1, s2))
require(sameStack(s2, s3))
require(propagatesError(s2, s3))
unfold(sameStack(s1, s2))
unfold(sameStack(s2, s3))
unfold(sameStack(s1, s3))
unfold(propagatesError(s2, s3))
s2 match {
case Left(_) => Trivial()
case Right(s) => unfold(sameStack(s, s3))
}
}.ensuring(sameStack(s1, s3))
/** Transitivity of [[State.rollbackStack]] field equality. Holds only if error propagates between the
* second and the third state.
*/
@pure
@opaque
def sameStackTransitivity[U, V, W](
s1: Either[U, State],
s2: Either[V, State],
s3: Either[W, State],
): Unit = {
require(sameStack(s1, s2))
require(sameStack(s2, s3))
require(propagatesError(s2, s3))
unfold(sameStack(s1, s2))
unfold(sameStack(s1, s3))
s1 match {
case Left(_) => Trivial()
case Right(s) => sameStackTransitivity(s, s2, s3)
}
}.ensuring(sameStack(s1, s3))
/** Reflexivity of [[State.globaKeys]] field equality. Holds only if error propagates between the
* second and the third state.
*/
@pure
@opaque
def sameGlobalKeysReflexivity[T](s: Either[T, State]): Unit = {
unfold(sameGlobalKeys(s, s))
s match {
case Left(_) => Trivial()
case Right(s2) => unfold(sameGlobalKeys(s2, s))
}
}.ensuring(sameGlobalKeys(s, s))
/** Transitivity of [[State.globalKeys]] field equality. Holds only if error propagates between the
* second and the third state.
*/
@pure
@opaque
def sameGlobalKeysTransitivity[V, W](
s1: State,
s2: Either[V, State],
s3: Either[W, State],
): Unit = {
require(sameGlobalKeys(s1, s2))
require(sameGlobalKeys(s2, s3))
require(propagatesError(s2, s3))
unfold(sameGlobalKeys(s1, s2))
unfold(sameGlobalKeys(s2, s3))
unfold(sameGlobalKeys(s1, s3))
unfold(propagatesError(s2, s3))
s2 match {
case Left(_) => Trivial()
case Right(s) => unfold(sameGlobalKeys(s, s3))
}
}.ensuring(sameGlobalKeys(s1, s3))
/** Transitivity of [[State.globalKeys]] field equality. Holds only if error propagates between the
* second and the third state.
*/
@pure
@opaque
def sameGlobalKeysTransitivity[U, V, W](
s1: Either[U, State],
s2: Either[V, State],
s3: Either[W, State],
): Unit = {
require(sameGlobalKeys(s1, s2))
require(sameGlobalKeys(s2, s3))
require(propagatesError(s2, s3))
unfold(sameGlobalKeys(s1, s2))
unfold(sameGlobalKeys(s1, s3))
s1 match {
case Left(_) => Trivial()
case Right(s) => sameGlobalKeysTransitivity(s, s2, s3)
}
}.ensuring(sameGlobalKeys(s1, s3))
/** Reflexivity of [[State.locallyCreated]] field equality. Holds only if error propagates between the
* second and the third state.
*/
@opaque
def sameLocallyCreatedReflexivity[T](s: Either[T, State]): Unit = {
unfold(sameLocallyCreated(s, s))
s match {
case Left(_) => Trivial()
case Right(s2) => unfold(sameLocallyCreated(s2, s))
}
}.ensuring(sameLocallyCreated(s, s))
/** Transitivity of [[State.locallyCreated]] field equality. Holds only if error propagates between the
* second and the third state.
*/
@pure
@opaque
def sameLocallyCreatedTransitivity[V, W](
s1: State,
s2: Either[V, State],
s3: Either[W, State],
): Unit = {
require(sameLocallyCreated(s1, s2))
require(sameLocallyCreated(s2, s3))
require(propagatesError(s2, s3))
unfold(sameLocallyCreated(s1, s2))
unfold(sameLocallyCreated(s2, s3))
unfold(sameLocallyCreated(s1, s3))
unfold(propagatesError(s2, s3))
s2 match {
case Left(_) => Trivial()
case Right(s) => unfold(sameLocallyCreated(s, s3))
}
}.ensuring(sameLocallyCreated(s1, s3))
/** Reflexivity of [[State.consumed]] field equality. Holds only if error propagates between the
* second and the third state.
*/
@pure
@opaque
def sameConsumedReflexivity[T](s: Either[T, State]): Unit = {
unfold(sameConsumed(s, s))
s match {
case Left(_) => Trivial()
case Right(s2) => unfold(sameConsumed(s2, s))
}
}.ensuring(sameConsumed(s, s))
/** Transitivity of [[State.consumed]] field equality. Holds only if error propagates between the
* second and the third state.
*/
@pure
@opaque
def sameConsumedTransitivity[V, W](
s1: State,
s2: Either[V, State],
s3: Either[W, State],
): Unit = {
require(sameConsumed(s1, s2))
require(sameConsumed(s2, s3))
require(propagatesError(s2, s3))
unfold(sameConsumed(s1, s2))
unfold(sameConsumed(s2, s3))
unfold(sameConsumed(s1, s3))
unfold(propagatesError(s2, s3))
s2 match {
case Left(_) => Trivial()
case Right(s) => unfold(sameConsumed(s, s3))
}
}.ensuring(sameConsumed(s1, s3))
/** Reflexivity of error propagation.
*/
@pure
@opaque
def propagatesErrorReflexivity[T, V](s: Either[T, V]): Unit = {
unfold(propagatesError(s, s))
}.ensuring(propagatesError(s, s))
/** Transitivity of error propagation.
*/
@pure
@opaque
def propagatesErrorTransitivity[T, V](
s1: Either[T, V],
s2: Either[T, V],
s3: Either[T, V],
): Unit = {
require(propagatesError(s1, s2))
require(propagatesError(s2, s3))
unfold(propagatesError(s1, s2))
unfold(propagatesError(s2, s3))
unfold(propagatesError(s1, s3))
}.ensuring(propagatesError(s1, s3))
/** Reflexivity of error propagation.
*/
@pure
@opaque
def propagatesSameErrorReflexivity[T, V](s: Either[T, V]): Unit = {
unfold(propagatesSameError(s, s))
}.ensuring(propagatesSameError(s, s))
/** Transitivity of error propagation.
*/
@pure
@opaque
def propagatesSameErrorTransitivity[T, V](
s1: Either[T, V],
s2: Either[T, V],
s3: Either[T, V],
): Unit = {
require(propagatesSameError(s1, s2))
require(propagatesSameError(s2, s3))
unfold(propagatesSameError(s1, s2))
unfold(propagatesSameError(s2, s3))
unfold(propagatesSameError(s1, s3))
}.ensuring(propagatesSameError(s1, s3))
/** Reflexivity of error propagation.
*/
@pure
@opaque
def sameErrorReflexivity[T, V](s: Either[T, V]): Unit = {
propagatesSameErrorReflexivity(s)
}.ensuring(sameError(s, s))
/** Transitivity of error propagation.
*/
@pure
@opaque
def sameErrorTransitivity[T, V](s1: Either[T, V], s2: Either[T, V], s3: Either[T, V]): Unit = {
require(sameError(s1, s2))
require(sameError(s2, s3))
propagatesSameErrorTransitivity(s1, s2, s3)
propagatesSameErrorTransitivity(s3, s2, s1)
}.ensuring(sameError(s1, s3))
/** Right map propagates error in both directions.
*/
@pure
@opaque
def propagatesSameErrorMap[T, V](e: Either[T, V], f: V => V): Unit = {
unfold(propagatesSameError(e, e.map(f)))
unfold(propagatesSameError(e.map(f), e))
}.ensuring(propagatesSameError(e, e.map(f)) && propagatesSameError(e.map(f), e))
/** Right map propagates error in both direction. Furthermore they are the same.
*/
@pure
@opaque
def sameErrorMap[T, V](e: Either[T, V], f: V => V): Unit = {
propagatesSameErrorMap(e, f)
}.ensuring(sameError(e, e.map(f)))
/** Left map propagates error in both directions. Furthermore the resulting state is equal to the input.
*/
@pure
@opaque
def sameStateLeftProj[U, T](s: Either[U, State], f: U => T): Unit = {
val lMap = s.left.map(f)
unfold(sameState(s, lMap))
unfold(propagatesError(s, lMap))
unfold(propagatesError(lMap, s))
s match {
case Left(_) => Trivial()
case Right(state) => unfold(sameState(state, lMap))
}
}.ensuring(
sameState(s, s.left.map(f)) &&
propagatesBothError(s, s.left.map(f))
)
}

174
daml-lf/verification/transaction/CSMHelpers.scala Normal file
View File

@ -0,0 +1,174 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package transaction
import stainless.lang.{
unfold,
decreases,
BooleanDecorations,
Either,
Some,
None,
Option,
Right,
Left,
}
import stainless.annotation._
import scala.annotation.targetName
import stainless.collection._
import utils.Value.ContractId
import utils.Transaction.{DuplicateContractKey, InconsistentContractKey, KeyInputError}
import utils._
import ContractStateMachine._
import CSMEitherDef._
import CSMEither._
/** Helpers definitions
*
* Definitions tightly related to ContractStateMachineAlt content. Most of them are extensions of already existing
* methods with Either arguments type instead of State.
*/
object CSMHelpers {
/** Extension of [[State.handleNode]] method to a union type argument. If e is defined calls handleNode otherwise returns
* the same error.
*/
@pure
def handleNode(
e: Either[KeyInputError, State],
id: NodeId,
node: Node.Action,
): Either[KeyInputError, State] = {
val res = e match {
case Left(e) => Left[KeyInputError, State](e)
case Right(s) => s.handleNode(id, node)
}
unfold(propagatesError(e, res))
unfold(sameGlobalKeys(e, res))
res
}.ensuring(res =>
propagatesError(e, res) &&
sameGlobalKeys(e, res)
)
/** Converts consumed active key mappings into an inactive key mappings.
*/
@pure
@opaque
def keyMappingToActiveMapping(consumedBy: Map[ContractId, NodeId]): KeyMapping => KeyMapping = {
case Some(cid) if !consumedBy.contains(cid) => KeyActive(cid)
case _ => KeyInactive
}
/** Converts the error of an union type argument (InconsistentContractKey or DuplicateContractkey) into the more
* generic error type KeyInputError.
*/
@pure
def toKeyInputError(e: Either[InconsistentContractKey, State]): Either[KeyInputError, State] = {
sameStateLeftProj(e, Left[InconsistentContractKey, DuplicateContractKey](_))
e.left.map(Left[InconsistentContractKey, DuplicateContractKey](_))
}.ensuring(res =>
propagatesBothError(e, res) &&
sameState(e, res)
)
@pure
@targetName("toKeyInputErrorDuplicateContractKey")
def toKeyInputError(e: Either[DuplicateContractKey, State]): Either[KeyInputError, State] = {
sameStateLeftProj(e, Right[InconsistentContractKey, DuplicateContractKey](_))
e.left.map(Right[InconsistentContractKey, DuplicateContractKey](_))
}.ensuring(res =>
propagatesBothError(e, res) &&
sameState(e, res)
)
/** Mapping that is added in the global keys when the n is handled.
*
* In the original ContractStateMachine, handleNode first adds the node's key with this mapping to the global keys
* and then process the node in the same way as ContractStateMachineAlt. In the simplified version, both operations
* are separated which brings the need for this function.
*
* @see mapping n, in the latex document
*/
@pure
@opaque
def nodeActionKeyMapping(n: Node.Action): KeyMapping = {
n match {
case create: Node.Create => KeyInactive
case fetch: Node.Fetch => KeyActive(fetch.coid)
case lookup: Node.LookupByKey => lookup.result
case exe: Node.Exercise => KeyActive(exe.targetCoid)
}
}
/** Extension of State.beginRollback() method to a union type argument. If e is defined calls beginRollback otherwise
* returns the same error.
*/
@pure
@opaque
def beginRollback[T](e: Either[T, State]): Either[T, State] = {
sameErrorMap(e, s => s.beginRollback())
val res = e.map(s => s.beginRollback())
unfold(sameGlobalKeys(e, res))
unfold(sameLocallyCreated(e, res))
unfold(sameConsumed(e, res))
e match {
case Left(t) => Trivial()
case Right(s) =>
unfold(s.beginRollback())
unfold(sameGlobalKeys(s, res))
unfold(sameLocallyCreated(s, res))
unfold(sameConsumed(s, res))
}
res
}.ensuring((res: Either[T, State]) =>
sameGlobalKeys[T, T](e, res) &&
sameLocallyCreated(e, res) &&
sameConsumed(e, res) &&
sameError(e, res)
)
/** Extension of State.endRollback() method to a union type argument. If e is defined calls endRollback otherwise
* returns the same error.
*
* Due to a bug in Stainless, writing the properties in the enduring clause of endRollback makes the JVM crash.
* Therefore, all of these are grouped in a different function endRollbackProp that often needs to be called
* separately when using endRollback with a union type argument.
*/
@pure
@opaque
def endRollback(e: Either[KeyInputError, State]): Either[KeyInputError, State] = {
e match {
case Left(t) => Left[KeyInputError, State](t)
case Right(s) => s.endRollback()
}
}
@pure @opaque
def endRollbackProp(e: Either[KeyInputError, State]): Unit = {
unfold(endRollback(e))
unfold(sameLocallyCreated(e, endRollback(e)))
unfold(sameConsumed(e, endRollback(e)))
unfold(sameGlobalKeys(e, endRollback(e)))
unfold(propagatesError(e, endRollback(e)))
}.ensuring(
sameLocallyCreated(e, endRollback(e)) &&
sameConsumed(e, endRollback(e)) &&
sameGlobalKeys(e, endRollback(e)) &&
propagatesError(e, endRollback(e))
)
@pure
@opaque
def advanceIsDefined(init: State, substate: State): Unit = {
require(!substate.withinRollbackScope)
}.ensuring(
init.advance(substate).isRight ==
substate.globalKeys.keySet.forall(k =>
init.activeKeys.get(k).forall(m => Some(m) == substate.globalKeys.get(k))
)
)
}

698
daml-lf/verification/transaction/CSMInconsistency.scala Normal file
View File

@ -0,0 +1,698 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package transaction
import stainless.lang.{
unfold,
decreases,
BooleanDecorations,
Either,
Some,
None,
Option,
Right,
Left,
}
import stainless.annotation._
import scala.annotation.targetName
import stainless.collection._
import utils.Value.ContractId
import utils.Transaction.{DuplicateContractKey, InconsistentContractKey, KeyInputError}
import utils._
import ContractStateMachine._
import CSMHelpers._
import CSMEitherDef._
import CSMKeysPropertiesDef._
import CSMKeysProperties._
/** File stating under which conditions a state is well defined after handling a node and how its active keys behave
* after that.
*/
object CSMInconsistencyDef {
/** *
* Alternative and general definition of an error in a transaction
*
* The objective of bringing this definition in are proving that:
* - s.handleNode(nid, node) leads to an error <=> inconsistencyCheck(s, node.gkeyOpt, node.m) is true
* - If node.gkeyOpt =/= Some(k2) then
* inconsistencyCheck(s, k2, m) == inconsistencyCheck(s.handleNode(nid, node), k2, m)
*
* @param s
* The current state
* @param k
* The key of the node we are handling. If the key is not defined then the transaction never fails, so
* the inconsistencyCheck is false
* @param m
* The key mapping that would have been added to the globalKeys if there was not an entry already for that key.
* This mapping (let denote it node.m) is:
* - KeyInactive for Node.Create
* - KeyActive(coid) for Node.Fetch
* - result for Node.Lookup
* - KeyActive(targetCoid) for Node.Exercise
*/
@pure
def inconsistencyCheck(s: State, k: GlobalKey, m: KeyMapping): Boolean = {
s.activeKeys.get(k).exists(_ != m)
}
@pure
def inconsistencyCheck(s: State, k: Option[GlobalKey], m: KeyMapping): Boolean = {
k.exists(gk => inconsistencyCheck(s, gk, m))
}
}
object CSMInconsistency {
import CSMInconsistencyDef._
import CSMInvariantDef._
import CSMInvariantDerivedProp._
/** The resulting state after handling a Create node is defined if any only if the inconsistencyCondition is not met
*/
@pure
@opaque
def visitCreateUndefined(s: State, contractId: ContractId, mbKey: Option[GlobalKey]): Unit = {
unfold(inconsistencyCheck(s, mbKey, KeyInactive))
unfold(s.visitCreate(contractId, mbKey))
mbKey match {
case None() => Trivial()
case Some(gk) => unfold(inconsistencyCheck(s, gk, KeyInactive))
}
}.ensuring(
(s.visitCreate(contractId, mbKey).isLeft == inconsistencyCheck(s, mbKey, KeyInactive))
)
/** The resulting state after handling a Fetch node is defined if any only if the inconsistencyCondition is not met
*/
@pure
@opaque
def assertKeyMappingUndefined(s: State, cid: ContractId, gkey: Option[GlobalKey]): Unit = {
require(containsOptionKey(s)(gkey))
unfold(containsOptionKey(s)(gkey))
unfold(inconsistencyCheck(s, gkey, KeyActive(cid)))
unfold(s.assertKeyMapping(cid, gkey))
gkey match {
case None() => Trivial()
case Some(gk) => visitLookupUndefined(s, gk, KeyActive(cid))
}
}.ensuring(s.assertKeyMapping(cid, gkey).isLeft == inconsistencyCheck(s, gkey, KeyActive(cid)))
/** The resulting state after handling an Exercise node is defined if any only if the inconsistencyCondition is not met
*/
@pure
@opaque
def visitExerciseUndefined(
s: State,
nodeId: NodeId,
targetId: ContractId,
gk: Option[GlobalKey],
byKey: Boolean,
consuming: Boolean,
): Unit = {
require(containsOptionKey(s)(gk))
unfold(s.visitExercise(nodeId, targetId, gk, byKey, consuming))
assertKeyMappingUndefined(s, targetId, gk)
}.ensuring(
s.visitExercise(nodeId, targetId, gk, byKey, consuming).isLeft == inconsistencyCheck(
s,
gk,
KeyActive(targetId),
)
)
/** The resulting state after handling a Lookup node is defined if any only if the inconsistencyCondition is not met
*/
@pure
@opaque
def visitLookupUndefined(s: State, gk: GlobalKey, keyResolution: Option[ContractId]): Unit = {
require(containsKey(s)(gk))
unfold(inconsistencyCheck(s, gk, keyResolution))
unfold(s.visitLookup(gk, keyResolution))
unfold(containsKey(s)(gk))
unfold(s.globalKeys.contains)
activeKeysGetOrElse(s, gk, KeyInactive)
activeKeysGet(s, gk)
}.ensuring(s.visitLookup(gk, keyResolution).isLeft == inconsistencyCheck(s, gk, keyResolution))
/** The resulting state after handling a node is defined if any only if the inconsistencyCondition is not met
*/
@pure
@opaque
def handleNodeUndefined(s: State, id: NodeId, node: Node.Action): Unit = {
require(containsActionKey(s)(node))
unfold(s.handleNode(id, node))
unfold(nodeActionKeyMapping(node))
unfold(containsActionKey(s)(node))
node match {
case create: Node.Create => visitCreateUndefined(s, create.coid, create.gkeyOpt)
case fetch: Node.Fetch => assertKeyMappingUndefined(s, fetch.coid, fetch.gkeyOpt)
case lookup: Node.LookupByKey =>
unfold(containsOptionKey(s)(node.gkeyOpt))
unfold(inconsistencyCheck(s, node.gkeyOpt, nodeActionKeyMapping(node)))
visitLookupUndefined(s, lookup.gkey, lookup.result)
case exe: Node.Exercise =>
visitExerciseUndefined(s, id, exe.targetCoid, exe.gkeyOpt, exe.byKey, exe.consuming)
}
}.ensuring(
s.handleNode(id, node).isLeft == inconsistencyCheck(s, node.gkeyOpt, nodeActionKeyMapping(node))
)
/** If two states are defined after handling a node then their activeKeys shared the same entry for the node's key
* before entering the node.
*/
@pure
@opaque
def handleSameNodeActiveKeys(s1: State, s2: State, id: NodeId, node: Node.Action): Unit = {
require(containsActionKey(s1)(node))
require(containsActionKey(s2)(node))
require(s1.handleNode(id, node).isRight)
require(s2.handleNode(id, node).isRight)
activeKeysContainsKey(s1, node)
activeKeysContainsKey(s2, node)
handleNodeUndefined(s1, id, node)
handleNodeUndefined(s2, id, node)
unfold(s1.activeKeys.contains)
unfold(s2.activeKeys.contains)
}.ensuring(node.gkeyOpt.forall(k => s1.activeKeys.get(k) == s2.activeKeys.get(k)))
/** If a state stay well defined after handling a Create node and if we are given a key different from the node's one,
* then the entry for that key in the activeKeys of the state did not change
*/
@opaque
@pure
def visitCreateActiveKeysGet(
s: State,
contractId: ContractId,
mbKey: Option[GlobalKey],
k2: GlobalKey,
): Unit = {
require(s.visitCreate(contractId, mbKey).isRight)
require(mbKey.forall(k1 => k1 != k2))
unfold(s.visitCreate(contractId, mbKey))
activeKeysGet(s, k2)
val me =
s.copy(
locallyCreated = s.locallyCreated + contractId,
activeState = s.activeState
.copy(locallyCreatedThisTimeline = s.activeState.locallyCreatedThisTimeline + contractId),
)
mbKey match {
case None() =>
activeKeysGet(me, k2)
case Some(gk) =>
activeKeysGet(me.copy(activeState = me.activeState.createKey(gk, contractId)), k2)
MapProperties.updatedGet(me.activeState.localKeys, gk, contractId, k2)
}
}.ensuring(s.visitCreate(contractId, mbKey).get.activeKeys.get(k2) == s.activeKeys.get(k2))
/** If a state stay well defined after handling a Lookup node and if we are given a key different from the node's one,
* then the entry for that key in the activeKeys of the state did not change
*/
@opaque
@pure
def visitLookupActiveKeysGet(
s: State,
gk: GlobalKey,
keyResolution: Option[ContractId],
k2: GlobalKey,
): Unit = {
require(s.visitLookup(gk, keyResolution).isRight)
unfold(sameState(s, s.visitLookup(gk, keyResolution)))
}.ensuring(s.visitLookup(gk, keyResolution).get.activeKeys.get(k2) == s.activeKeys.get(k2))
/** If a state stay well defined after handling a Fetch node and if we are given a key different from the node's one,
* then the entry for that key in the activeKeys of the state did not change
*/
@opaque
@pure
def assertKeyMappingActiveKeysGet(
s: State,
cid: ContractId,
mbKey: Option[GlobalKey],
k2: GlobalKey,
): Unit = {
require(s.assertKeyMapping(cid, mbKey).isRight)
unfold(sameState(s, s.assertKeyMapping(cid, mbKey)))
}.ensuring(s.assertKeyMapping(cid, mbKey).get.activeKeys.get(k2) == s.activeKeys.get(k2))
/** If a state stay well defined after handling an Exercise node and if we are given a key different from the node's one,
* then the entry for that key in the activeKeys of the state did not change
*/
@pure
@opaque
def visitExerciseActiveKeysGet(
s: State,
nodeId: NodeId,
targetId: ContractId,
gk: Option[GlobalKey],
byKey: Boolean,
consuming: Boolean,
k2: GlobalKey,
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(s.visitExercise(nodeId, targetId, gk, byKey, consuming).isRight)
require(containsOptionKey(s)(gk))
require(!gk.isDefined ==> unbound.contains(targetId))
require(gk.forall(k1 => k1 != k2))
require(stateInvariant(s)(unbound, lc))
unfold(s.visitExercise(nodeId, targetId, gk, byKey, consuming))
visitExerciseUndefined(s, nodeId, targetId, gk, byKey, consuming)
unfold(inconsistencyCheck(s, gk, KeyActive(targetId)))
unfold(containsOptionKey(s)(gk))
s.assertKeyMapping(targetId, gk) match {
case Left(_) => Trivial()
case Right(state) =>
keysGet(s, k2)
unfold(s.globalKeys.contains)
unfold(s.activeState.localKeys.contains)
gk match {
case Some(k) =>
// (s.globalKeys.get(k) == Some(KeyActive(targetId))) || (s.activeState.localKeys.get(k).map(KeyActive) == Some(KeyActive(targetId)))
activeKeysGet(s, k)
unfold(containsKey(s)(k))
unfold(keyMappingToActiveMapping(s.activeState.consumedBy))
if (s.globalKeys.get(k) == Some(KeyActive(targetId))) {
invariantGetGlobalKeys(s, k, k2, targetId, unbound, lc)
} else {
invariantGetLocalKeys(s, k, k2, targetId, unbound, lc)
}
case None() =>
SetProperties.mapContains(unbound, KeyActive, targetId)
SetProperties.disjointContains(
unbound.map(KeyActive),
s.globalKeys.values,
KeyActive(targetId),
)
if (s.globalKeys.get(k2) == Some(KeyActive(targetId))) {
MapAxioms.valuesContains(s.globalKeys, k2)
}
SetProperties.disjointContains(unbound, s.activeState.localKeys.values, targetId)
if (s.activeState.localKeys.get(k2) == Some(targetId)) {
MapAxioms.valuesContains(s.activeState.localKeys, k2)
}
}
unfold(sameState(s, s.assertKeyMapping(targetId, gk)))
unfold(state.consume(targetId, nodeId))
unfold(state.activeState.consume(targetId, nodeId))
activeKeysGet(state.consume(targetId, nodeId), k2)
activeKeysGet(state, k2)
unfold(keyMappingToActiveMapping(state.activeState.consumedBy))
unfold(keyMappingToActiveMapping(state.activeState.consumedBy.updated(targetId, nodeId)))
(s.activeState.localKeys.get(k2).map(KeyActive), s.globalKeys.get(k2)) match {
case (Some(Some(c1)), _) =>
MapProperties.updatedContains(state.activeState.consumedBy, targetId, nodeId, c1)
case (_, Some(Some(c2))) =>
MapProperties.updatedContains(state.activeState.consumedBy, targetId, nodeId, c2)
case _ => Trivial()
}
}
}.ensuring(
s.visitExercise(nodeId, targetId, gk, byKey, consuming).get.activeKeys.get(k2) == s.activeKeys
.get(k2)
)
/** If a state stay well defined after handling a node and if we are given a key different from the node's one,
* then the entry for that key in the activeKeys of the state did not change
*/
@pure
@opaque
def handleNodeActiveKeysGet(
s: State,
id: NodeId,
node: Node.Action,
k2: GlobalKey,
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(s.handleNode(id, node).isRight)
require(containsActionKey(s)(node))
require(node.gkeyOpt.forall(k1 => k1 != k2))
require(stateInvariant(s)(unbound, lc))
require(stateNodeCompatibility(s, node, unbound, lc, TraversalDirection.Down))
unfold(s.handleNode(id, node))
unfold(containsActionKey(s)(node))
node match {
case create: Node.Create => visitCreateActiveKeysGet(s, create.coid, create.gkeyOpt, k2)
case fetch: Node.Fetch => assertKeyMappingActiveKeysGet(s, fetch.coid, fetch.gkeyOpt, k2)
case lookup: Node.LookupByKey => visitLookupActiveKeysGet(s, lookup.gkey, lookup.result, k2)
case exe: Node.Exercise =>
unfold(stateNodeCompatibility(s, node, unbound, lc, TraversalDirection.Down))
visitExerciseActiveKeysGet(
s,
id,
exe.targetCoid,
exe.gkeyOpt,
exe.byKey,
exe.consuming,
k2,
unbound,
lc,
)
}
}.ensuring(s.handleNode(id, node).get.activeKeys.get(k2) == s.activeKeys.get(k2))
/** The entry for a given key in the activeKeys of the state does not change after entering a beginRollback
*/
@pure
@opaque
def beginRollbackActiveKeysGet(s: State, k: GlobalKey): Unit = {
unfold(s.beginRollback())
activeKeysGetSameFields(s.beginRollback(), s, k)
}.ensuring(s.beginRollback().activeKeys.get(k) == s.activeKeys.get(k))
/** If two states are defined after handling a Create node then they share the same mapping for the node's key entry in
* the activeKeys.
*/
@opaque
@pure
def visitCreateDifferentStatesActiveKeysGet(
s1: State,
s2: State,
contractId: ContractId,
mbKey: Option[GlobalKey],
): Unit = {
require(s1.visitCreate(contractId, mbKey).isRight)
require(s2.visitCreate(contractId, mbKey).isRight)
require(!s1.activeState.consumedBy.contains(contractId))
require(!s2.activeState.consumedBy.contains(contractId))
unfold(s1.visitCreate(contractId, mbKey))
unfold(s2.visitCreate(contractId, mbKey))
val me1 =
s1.copy(
locallyCreated = s1.locallyCreated + contractId,
activeState = s1.activeState
.copy(locallyCreatedThisTimeline = s1.activeState.locallyCreatedThisTimeline + contractId),
)
val me2 =
s2.copy(
locallyCreated = s2.locallyCreated + contractId,
activeState = s2.activeState
.copy(locallyCreatedThisTimeline = s2.activeState.locallyCreatedThisTimeline + contractId),
)
mbKey match {
case None() => Trivial()
case Some(gk) =>
val sf1 = me1.copy(activeState = me1.activeState.createKey(gk, contractId))
val sf2 = me2.copy(activeState = me2.activeState.createKey(gk, contractId))
activeKeysGet(sf1, gk)
activeKeysGet(sf2, gk)
unfold(me1.activeState.createKey(gk, contractId))
unfold(me2.activeState.createKey(gk, contractId))
unfold(keyMappingToActiveMapping(s1.activeState.consumedBy))
unfold(keyMappingToActiveMapping(s2.activeState.consumedBy))
}
}.ensuring(
mbKey.forall(k =>
s1.visitCreate(contractId, mbKey).get.activeKeys.get(k) == s2
.visitCreate(contractId, mbKey)
.get
.activeKeys
.get(k)
)
)
/** If two states are defined after handling a Lookup node then they share the same mapping for the node's key entry in
* the activeKeys.
*/
@opaque
@pure
def visitLookupDifferentStatesActiveKeysGet(
s1: State,
s2: State,
gk: GlobalKey,
keyResolution: Option[ContractId],
unbound1: Set[ContractId],
lc1: Set[ContractId],
unbound2: Set[ContractId],
lc2: Set[ContractId],
): Unit = {
require(s1.visitLookup(gk, keyResolution).isRight)
require(s2.visitLookup(gk, keyResolution).isRight)
require(
keyResolution.isDefined || (containsKey(s1)(gk) && containsKey(s2)(gk) && stateInvariant(s1)(
unbound1,
lc1,
) && stateInvariant(s2)(unbound2, lc2))
)
unfold(s1.visitLookup(gk, keyResolution))
unfold(s2.visitLookup(gk, keyResolution))
unfold(s1.activeKeys.getOrElse(gk, KeyInactive))
unfold(s2.activeKeys.getOrElse(gk, KeyInactive))
keyResolution match {
case None() =>
invariantContainsKey(s1, gk, unbound1, lc1)
invariantContainsKey(s2, gk, unbound2, lc2)
unfold(s1.activeKeys.contains)
unfold(s2.activeKeys.contains)
case Some(_) => Trivial()
}
}.ensuring(
(s1.visitLookup(gk, keyResolution).get.activeKeys.get(gk) == s2
.visitLookup(gk, keyResolution)
.get
.activeKeys
.get(gk)) &&
(s1.visitLookup(gk, keyResolution).get.activeKeys.get(gk) == Some(keyResolution))
)
/** If two states are defined after handling a Fetch node then they share the same mapping for the node's key entry in
* the activeKeys.
*/
@opaque
@pure
def assertKeyMappingDifferentStatesActiveKeysGet(
s1: State,
s2: State,
cid: ContractId,
mbKey: Option[GlobalKey],
): Unit = {
require(s1.assertKeyMapping(cid, mbKey).isRight)
require(s2.assertKeyMapping(cid, mbKey).isRight)
unfold(s1.assertKeyMapping(cid, mbKey))
unfold(s2.assertKeyMapping(cid, mbKey))
mbKey match {
case None() => Trivial()
case Some(k) =>
visitLookupDifferentStatesActiveKeysGet(
s1,
s2,
k,
Some(cid),
Set.empty[ContractId],
Set.empty[ContractId],
Set.empty[ContractId],
Set.empty[ContractId],
)
}
}.ensuring(
mbKey.forall(gk =>
(s1.assertKeyMapping(cid, mbKey).get.activeKeys.get(gk) == s2
.assertKeyMapping(cid, mbKey)
.get
.activeKeys
.get(gk)) &&
(s1.assertKeyMapping(cid, mbKey).get.activeKeys.get(gk) == Some(KeyActive(cid)))
)
)
/** If two states are defined after handling an Exercise node then they share the same mapping for the node's key entry in
* the activeKeys.
*/
@opaque
@pure
def visitExerciseDifferentStatesActiveKeysGet(
s1: State,
s2: State,
nodeId: NodeId,
targetId: ContractId,
mbKey: Option[GlobalKey],
byKey: Boolean,
consuming: Boolean,
): Unit = {
require(s1.visitExercise(nodeId, targetId, mbKey, byKey, consuming).isRight)
require(s2.visitExercise(nodeId, targetId, mbKey, byKey, consuming).isRight)
unfold(s1.visitExercise(nodeId, targetId, mbKey, byKey, consuming))
unfold(s2.visitExercise(nodeId, targetId, mbKey, byKey, consuming))
assertKeyMappingDifferentStatesActiveKeysGet(s1, s2, targetId, mbKey)
(s1.assertKeyMapping(targetId, mbKey), s2.assertKeyMapping(targetId, mbKey), mbKey) match {
case (Left(_), _, _) => Unreachable()
case (_, Left(_), _) => Unreachable()
case (Right(state1), Right(state2), Some(k)) =>
unfold(sameState(s1, s1.assertKeyMapping(targetId, mbKey)))
unfold(sameState(s2, s2.assertKeyMapping(targetId, mbKey)))
unfold(state1.consume(targetId, nodeId))
unfold(state1.activeState.consume(targetId, nodeId))
unfold(state2.consume(targetId, nodeId))
unfold(state2.activeState.consume(targetId, nodeId))
activeKeysGet(state1, k)
activeKeysGet(state2, k)
unfold(keyMappingToActiveMapping(state1.activeState.consumedBy))
unfold(keyMappingToActiveMapping(state2.activeState.consumedBy))
activeKeysGet(state1.consume(targetId, nodeId), k)
activeKeysGet(state2.consume(targetId, nodeId), k)
unfold(keyMappingToActiveMapping(state1.activeState.consumedBy.updated(targetId, nodeId)))
unfold(keyMappingToActiveMapping(state2.activeState.consumedBy.updated(targetId, nodeId)))
case _ => Trivial()
}
}.ensuring(
mbKey.forall(k =>
s1.visitExercise(nodeId, targetId, mbKey, byKey, consuming).get.activeKeys.get(k) ==
s2.visitExercise(nodeId, targetId, mbKey, byKey, consuming).get.activeKeys.get(k)
)
)
/** If two states are defined after handling a node then they share the same mapping for the node's key entry in
* the activeKeys.
*/
@opaque
@pure
def handleNodeDifferentStatesActiveKeysGet(
s1: State,
s2: State,
nid: NodeId,
node: Node.Action,
unbound1: Set[ContractId],
lc1: Set[ContractId],
unbound2: Set[ContractId],
lc2: Set[ContractId],
): Unit = {
require(s1.handleNode(nid, node).isRight)
require(s2.handleNode(nid, node).isRight)
require(containsActionKey(s1)(node))
require(containsActionKey(s2)(node))
require(stateInvariant(s1)(unbound1, lc1))
require(stateInvariant(s2)(unbound2, lc2))
require(stateNodeCompatibility(s1, node, unbound1, lc1, TraversalDirection.Down))
require(stateNodeCompatibility(s2, node, unbound2, lc2, TraversalDirection.Down))
unfold(s1.handleNode(nid, node))
unfold(s2.handleNode(nid, node))
unfold(containsActionKey(s1)(node))
unfold(containsActionKey(s2)(node))
unfold(stateNodeCompatibility(s1, node, unbound1, lc1, TraversalDirection.Down))
unfold(stateNodeCompatibility(s2, node, unbound2, lc2, TraversalDirection.Down))
node match {
case create: Node.Create =>
if (s1.activeState.consumedBy.contains(create.coid)) {
MapProperties.keySetContains(s1.activeState.consumedBy, create.coid)
SetProperties.subsetOfContains(s1.activeState.consumedBy.keySet, s1.consumed, create.coid)
Unreachable()
}
if (s2.activeState.consumedBy.contains(create.coid)) {
MapProperties.keySetContains(s2.activeState.consumedBy, create.coid)
SetProperties.subsetOfContains(s2.activeState.consumedBy.keySet, s2.consumed, create.coid)
Unreachable()
}
visitCreateDifferentStatesActiveKeysGet(s1, s2, create.coid, create.gkeyOpt)
case fetch: Node.Fetch =>
assertKeyMappingDifferentStatesActiveKeysGet(s1, s2, fetch.coid, fetch.gkeyOpt)
case lookup: Node.LookupByKey =>
unfold(containsOptionKey(s1)(node.gkeyOpt))
unfold(containsOptionKey(s2)(node.gkeyOpt))
visitLookupDifferentStatesActiveKeysGet(
s1,
s2,
lookup.gkey,
lookup.result,
unbound1,
lc1,
unbound2,
lc2,
)
case exe: Node.Exercise =>
visitExerciseDifferentStatesActiveKeysGet(
s1,
s2,
nid,
exe.targetCoid,
exe.gkeyOpt,
exe.byKey,
exe.consuming,
)
}
}.ensuring(
node.gkeyOpt.forall(k =>
s1.handleNode(nid, node).get.activeKeys.get(k) ==
s2.handleNode(nid, node).get.activeKeys.get(k)
)
)
/** If two states have the same activeState and the same globalKeys then their activeKeys are also the same.
*/
@pure @opaque
def activeKeysGetSameFields(s1: State, s2: State, k: GlobalKey): Unit = {
require(s1.activeState == s2.activeState)
require(s1.globalKeys == s2.globalKeys)
unfold(s1.activeKeys)
unfold(s2.activeKeys)
unfold(s1.keys)
unfold(s2.keys)
}.ensuring(s1.activeKeys.get(k) == s2.activeKeys.get(k))
/** beginRollback followed by a function that does not modify the rollbackStack and the globalKeys, followed by an
* endRollback does not change the activeKeys of a state.
*/
@opaque
@pure
def activeKeysGetRollbackScope(s: State, k: GlobalKey, f: State => State): Unit = {
require(f(s.beginRollback()).endRollback().isRight)
require(f(s.beginRollback()).rollbackStack == s.beginRollback().rollbackStack)
require(f(s.beginRollback()).globalKeys == s.beginRollback().globalKeys)
unfold(s.beginRollback())
unfold(f(s.beginRollback()).endRollback())
activeKeysGetSameFields(s, f(s.beginRollback()).endRollback().get, k)
}.ensuring(
f(s.beginRollback()).endRollback().get.activeKeys.get(k) ==
s.activeKeys.get(k)
)
}

825
daml-lf/verification/transaction/CSMInvariant.scala Normal file
View File

@ -0,0 +1,825 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package transaction
import stainless.lang.{
unfold,
decreases,
BooleanDecorations,
Either,
Some,
None,
Option,
Right,
Left,
}
import stainless.annotation._
import scala.annotation.targetName
import stainless.collection._
import utils.Value.ContractId
import utils.Transaction.{DuplicateContractKey, InconsistentContractKey, KeyInputError}
import utils._
import ContractStateMachine._
import CSMHelpers._
import CSMKeysPropertiesDef._
import CSMKeysProperties._
import CSMEitherDef._
object CSMInvariantDef {
/** *
* List of invariants that hold for well-defined transactions
*
* The following relationships tie together the various sets of ContractId.
* Let
* globalIds := globalKeys.values.filter(_.isDefined)
* act.localIds := act.localKeys.values
*
* a. unbound is disjoint from globalIds
*
* b. for every act in the rollbackStack and for the active state:
* act.localIds ⊆ locallyCreated ⊆ lc
*
* c. lc.map(KeyActive) is disjoint from globalIds
*
* d. for every act in the rollbackStack and for the active state:
* act.localIds is disjoint from unbound
*
* e. for every act in the rollbackStack and for the active state:
* act.consumedBy.values ⊆ consumed
*
* f. for every contractId v in globalIds:
* globalKeys.preimage(v).size <= 1
*
* g. for every contractId v in act.localIds
* act.localKeys.preimage(v).size <= 1
*
* Conditions e and f mean that both maps are injective, i.e. that no contract is assigned to two keys
* at the same time.
*
* Regarding the keys the only invariant is that local keys are a subset of global keys
*
* @param s
* The state for which those invariants hold
*
* @param lc
* Set of contracts contracted during the transaction, before executing
* @param unbound
* Set of contracts created throughout the transaction but not linked to any key
*/
@pure
def invariantWrtActiveState(
s: State
)(unbound: Set[ContractId], lc: Set[ContractId]): ActiveLedgerState => Boolean =
a =>
// point b.1.
a.localKeys.values.subsetOf(s.locallyCreated) &&
// point d.
unbound.disjoint(a.localKeys.values) &&
// point e.
a.consumedBy.keySet.subsetOf(s.consumed) &&
// point g.
(a.localKeys.values).forall(v => a.localKeys.preimage(v).size <= BigInt(1)) &&
// keySets
a.localKeys.keySet.subsetOf(s.globalKeys.keySet)
@pure
def invariantWrtList(s: State)(unbound: Set[ContractId], lc: Set[ContractId])(
l: List[ActiveLedgerState]
): Boolean = l.forall(invariantWrtActiveState(s)(unbound, lc))
@pure
def stateInvariant(s: State)(unbound: Set[ContractId], lc: Set[ContractId]): Boolean = {
val invariant: Boolean = {
// point a.
unbound.map[KeyMapping](KeyActive).disjoint(s.globalKeys.values) &&
// point b.2.
s.locallyCreated.subsetOf(lc) &&
// point c.
lc.map[KeyMapping](KeyActive).disjoint(s.globalKeys.values) &&
// point f.
(s.globalKeys.values
.filter(_.isDefined))
.forall(v => s.globalKeys.preimage(v).size <= BigInt(1)) &&
// the invariants hold for the active state
invariantWrtActiveState(s)(unbound, lc)(s.activeState) &&
// the invariants hold for all the states in the stack
invariantWrtList(s)(unbound, lc)(s.rollbackStack)
}
/** Properties that can be derived from the invariants:
* - globalKeys.keySet == activeKeys.keySet
*/
@opaque
def invariantProperties: Unit = {
require(invariant)
unfold(invariantWrtActiveState)
// globalKeys.keySet == activeKeys.keySet
unfold(s.activeKeys)
activeKeysKeySet(s)
SetProperties.unionAltDefinition(s.activeState.localKeys.keySet, s.globalKeys.keySet)
SetProperties.equalsTransitivityStrong(
s.globalKeys.keySet,
s.globalKeys.keySet ++ s.activeState.localKeys.keySet,
s.activeKeys.keySet,
)
// localKeys.values.subsetOf(lc)
SetProperties.subsetOfTransitivity(s.activeState.localKeys.values, s.locallyCreated, lc)
// localKeys.values.map(KeyActive).disjoint(s.globalKeys.values)
SetProperties.mapSubsetOf[ContractId, KeyMapping](
s.activeState.localKeys.values,
lc,
KeyActive,
)
SetProperties.disjointSubsetOf(
lc.map[KeyMapping](KeyActive),
s.activeState.localKeys.values.map[KeyMapping](KeyActive),
s.globalKeys.values,
)
}.ensuring(
(s.globalKeys.keySet === s.activeKeys.keySet) &&
s.activeState.localKeys.values.map[KeyMapping](KeyActive).disjoint(s.globalKeys.values)
)
if (invariant) {
invariantProperties
}
invariant
}
/** Properties that need to be true for any pair intermediate state - node during a transaction so that the invariants
* are preserved.
*/
@pure
@opaque
def stateNodeCompatibility(
s: State,
n: Node,
unbound: Set[ContractId],
lc: Set[ContractId],
dir: TraversalDirection,
): Boolean = {
(dir == TraversalDirection.Down) ==>
(n match {
case Node.Create(coid, mbKey) =>
lc.contains(coid) &&
(mbKey.isDefined == !unbound.contains(coid)) &&
!s.locallyCreated.contains(coid) &&
!s.consumed.contains(coid)
case exe: Node.Exercise => exe.gkeyOpt.isDefined == !unbound.contains(exe.targetCoid)
case _ => true
})
}
/** The invariants are considered true for an error state which means that they are preserved even when the transaction
* leads to an error
*/
@pure
def invariantWrtList[T](e: Either[T, State])(unbound: Set[ContractId], lc: Set[ContractId])(
l: List[ActiveLedgerState]
): Boolean =
e.forall(s => invariantWrtList(s)(unbound, lc)(l))
@pure
def stateInvariant[T](
e: Either[T, State]
)(unbound: Set[ContractId], lc: Set[ContractId]): Boolean = {
e.forall(s => stateInvariant(s)(unbound, lc))
}
}
/** The scope of this object is to prove that the invariants are preserved when traversing a transaction. This includes
* proving that they still hold:
* - after handling a node (given some conditions on the node that hold for well defined transactions)
* - after entering or exiting a rollback node
* - after adding a global mapping (given some conditions on the mapping)
*/
object CSMInvariant {
import CSMInvariantDef._
/** If a state fulfills the invariants then the state obtained after calling beginRollback also fulfills the invariants.
*/
@pure
@opaque
def stateInvariantBeginRollback(s: State, unbound: Set[ContractId], lc: Set[ContractId]): Unit = {
require(stateInvariant(s)(unbound, lc))
unfold(s.beginRollback())
}.ensuring(stateInvariant(s.beginRollback())(unbound, lc))
/** If a state fulfills the invariants then the state obtained after calling endRollback also fulfills the invariants.
*/
@pure
@opaque
def stateInvariantEndRollback(s: State, unbound: Set[ContractId], lc: Set[ContractId]): Unit = {
require(stateInvariant(s)(unbound, lc))
unfold(s.endRollback())
}.ensuring(stateInvariant(s.endRollback())(unbound, lc))
/** If a state fulfills the invariants and an other state has its same fields except for the locallyCreatedThisTimeline
* then it also fulfills the invariants.
*/
@pure
@opaque
def stateInvariantSameFields[T](
s1: State,
s2: Either[T, State],
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(s1)(unbound, lc))
require(sameLocalKeys(s1, s2))
require(sameConsumedBy(s1, s2))
require(sameGlobalKeys(s1, s2))
require(sameStack(s1, s2))
require(sameLocallyCreated(s1, s2))
require(sameConsumed(s1, s2))
unfold(sameLocalKeys(s1, s2))
unfold(sameConsumedBy(s1, s2))
unfold(sameGlobalKeys(s1, s2))
unfold(sameStack(s1, s2))
unfold(sameLocallyCreated(s1, s2))
unfold(sameConsumed(s1, s2))
}.ensuring(stateInvariant(s2)(unbound, lc))
/** If a state fulfills the invariants and an other state has its same fields except for the locallyCreatedThisTimeline
* then it also fulfills the invariants.
*/
@pure
@opaque
def stateInvariantSameFields[U, T](
s1: Either[U, State],
s2: Either[T, State],
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(s1)(unbound, lc))
require(sameLocalKeys(s1, s2))
require(sameConsumedBy(s1, s2))
require(sameGlobalKeys(s1, s2))
require(sameStack(s1, s2))
require(sameLocallyCreated(s1, s2))
require(sameConsumed(s1, s2))
require(propagatesError(s1, s2)) // we want to avoid the case s1.isLeft and s2.isRight
unfold(sameLocalKeys(s1, s2))
unfold(sameConsumedBy(s1, s2))
unfold(sameGlobalKeys(s1, s2))
unfold(sameStack(s1, s2))
unfold(sameLocallyCreated(s1, s2))
unfold(sameConsumed(s1, s2))
unfold(propagatesError(s1, s2))
s1 match {
case Right(s) => stateInvariantSameFields(s, s2, unbound, lc)
case Left(_) => Trivial()
}
}.ensuring(stateInvariant(s2)(unbound, lc))
/** If a state fulfills the invariants and an other state is equal to it then it also fulfills the invariants.
*/
@pure
@opaque
def stateInvariantSameState[T](
s1: State,
s2: Either[T, State],
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(s1)(unbound, lc))
require(sameState(s1, s2))
stateInvariantSameFields(s1, s2, unbound, lc)
}.ensuring(stateInvariant(s2)(unbound, lc))
/** If a state fulfills the invariants and an other state is equal to it then it also fulfills the invariants.
*/
@pure
@opaque
def stateInvariantSameState[U, T](
s1: Either[U, State],
s2: Either[T, State],
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(s1)(unbound, lc))
require(sameState(s1, s2))
require(propagatesError(s1, s2)) // we want to avoid the case s1.isLeft and s2.isRight
stateInvariantSameFields(s1, s2, unbound, lc)
}.ensuring(stateInvariant(s2)(unbound, lc))
/** If a state fulfills the invariants then the state obtained after calling assertKeyMapping also fulfills the invariants.
*/
@pure
@opaque
def stateInvariantAssertKeyMapping(
s: State,
cid: ContractId,
mbKey: Option[GlobalKey],
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(s)(unbound, lc))
stateInvariantSameState(s, s.assertKeyMapping(cid, mbKey), unbound, lc)
}.ensuring(stateInvariant(s.assertKeyMapping(cid, mbKey))(unbound, lc))
/** If a state fulfills the invariants then the state obtained after calling visitLookup also fulfills the invariants.
*/
@pure
@opaque
def stateInvariantVisitLookup(
s: State,
gk: GlobalKey,
keyResolution: Option[ContractId],
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(s)(unbound, lc))
stateInvariantSameState(s, s.visitLookup(gk, keyResolution), unbound, lc)
}.ensuring(stateInvariant(s.visitLookup(gk, keyResolution))(unbound, lc))
/** If a state fulfills the invariants then the state obtained after calling visitExercise also fulfills the invariants.
*/
@pure
@opaque
def stateInvariantVisitExercise(
s: State,
nodeId: NodeId,
targetId: ContractId,
mbKey: Option[GlobalKey],
byKey: Boolean,
consuming: Boolean,
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(s)(unbound, lc))
unfold(s.visitExercise(nodeId, targetId, mbKey, byKey, consuming))
s.assertKeyMapping(targetId, mbKey) match {
case Left(_) => Trivial()
case Right(state) =>
unfold(sameState(s, s.assertKeyMapping(targetId, mbKey)))
if (consuming) {
unfold(state.consume(targetId, nodeId))
unfold(state.activeState.consume(targetId, nodeId))
SetProperties.subsetOfIncl(s.activeState.consumedBy.keySet, s.consumed, targetId)
SetProperties.equalsSubsetOfTransitivity(
s.activeState.consumedBy.updated(targetId, nodeId).keySet,
s.activeState.consumedBy.keySet + targetId,
s.consumed + targetId,
)
val res = state.consume(targetId, nodeId)
if (!invariantWrtList(res)(unbound, lc)(s.rollbackStack)) {
val a = ListProperties.notForallWitness(
s.rollbackStack,
invariantWrtActiveState(res)(unbound, lc),
)
ListProperties.forallContains(
s.rollbackStack,
invariantWrtActiveState(s)(unbound, lc),
a,
)
SetProperties.subsetOfTransitivity(a.consumedBy.keySet, s.consumed, res.consumed)
Unreachable()
}
}
}
}.ensuring(
stateInvariant(s.visitExercise(nodeId, targetId, mbKey, byKey, consuming))(unbound, lc)
)
/** Invariants are preserved after a create node, given some conditions on the state and the node:
* - The key associated to the new contract has to appear in the global keys. This is always the case since
* we update all the globalKeys before traversing the transaction
* - lc has to contain contractId (since it is the set of all newly created contracts in the transaction)
* - if unbound contains the contract then it means that no key is given
* - The contract should not have been created previously in the transaction
*/
@pure
@opaque
def stateInvariantVisitCreate(
s: State,
contractId: ContractId,
mbKey: Option[GlobalKey],
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(s)(unbound, lc))
require(containsOptionKey(s)(mbKey))
require(lc.contains(contractId))
require(mbKey.isDefined ==> !unbound.contains(contractId))
require(!s.locallyCreated.contains(contractId))
unfold(s.visitCreate(contractId, mbKey))
val me =
s.copy(
locallyCreated = s.locallyCreated + contractId,
activeState = s.activeState
.copy(locallyCreatedThisTimeline = s.activeState.locallyCreatedThisTimeline + contractId),
)
/** STEP 1: the invariants still hold for every state in the rollback stack
*
* At this stage all the modifications relevant to the rollbackStack has already been done.
* In fact what remains is changing the active state. Therefore we can already prove that the
* invariants are preserved for every state in the rollback stack (by contradiction)
*/
if (!invariantWrtList(me)(unbound, lc)(me.rollbackStack)) {
val a =
ListProperties.notForallWitness(me.rollbackStack, invariantWrtActiveState(me)(unbound, lc))
ListProperties.forallContains(s.rollbackStack, invariantWrtActiveState(s)(unbound, lc), a)
SetProperties.subsetOfTransitivity(a.localKeys.values, s.locallyCreated, me.locallyCreated)
Unreachable()
}
/** STEP 2 locallyCreated + contractId ⊆ lc
*
* Here we need the fact that lc contains contractId
*/
SetProperties.subsetOfIncl(s.locallyCreated, lc, contractId)
mbKey match {
case None() =>
/** STEP 3.a localKeys.values ⊆ locallyCreated + contractId
*/
SetProperties.subsetOfTransitivity(
s.activeState.localKeys.values,
s.locallyCreated,
me.locallyCreated,
)
case Some(gk) =>
val ns = me.copy(activeState = me.activeState.createKey(gk, contractId))
unfold(me.activeState.createKey(gk, contractId))
MapProperties.updatedValues(s.activeState.localKeys, gk, contractId)
/** STEP 3.b localKeys.updated(gk, contractId).values ⊆ locallyCreated + contractId
*/
SetProperties.subsetOfIncl(s.activeState.localKeys.values, s.locallyCreated, contractId)
SetProperties.subsetOfTransitivity(
s.activeState.createKey(gk, contractId).localKeys.values,
s.activeState.localKeys.values + contractId,
s.locallyCreated + contractId,
)
/** STEP 4 unbound is disjoint from localKeys.updated(gk, contractId).values
*
* Here we need the fact that contractId is not in unbound if it is bound to some key
*/
SetProperties.disjointSubsetOf(
unbound,
s.activeState.localKeys.values + contractId,
s.activeState.createKey(gk, contractId).localKeys.values,
)
SetProperties.disjointIncl(unbound, s.activeState.localKeys.values, contractId)
/** STEP 5 (localKeys.updated(gk, contractId).values).forall(v => localKeys.updated(gk, contractId).preimage(v).size <= BigInt(1))
*
* We show that the statement is true for contractId and prove by contradiction that it remains true for
* the previous values. We will need the fact that locallyCreated and therefore localKeys.values do not
* contain contractId.
*/
val newF: ContractId => Boolean =
v => ns.activeState.localKeys.preimage(v).size <= BigInt(1)
SetProperties.forallIncl(s.activeState.localKeys.values, contractId, newF)
// STEP 5.1 localKeys.values do not contain contractId
if (s.activeState.localKeys.values.contains(contractId)) {
SetProperties.subsetOfContains(
s.activeState.localKeys.values,
s.locallyCreated,
contractId,
)
}
// STEP 5.2 newF(contractId)
{
// STEP 5.2.1 localKeys.preimage(contractId).size == 0
MapProperties.preimageIsEmpty(s.activeState.localKeys, contractId)
SetProperties.isEmptySize(s.activeState.localKeys.preimage(contractId))
// STEP 5.2.2 localKeys.updated(gk, contractId).preimage(contractId).size <= 1
MapProperties.inclPreimage(s.activeState.localKeys, gk, contractId, contractId)
SetProperties.subsetOfSize(
s.activeState.localKeys.updated(gk, contractId).preimage(contractId),
s.activeState.localKeys.preimage(contractId) + gk,
)
}
// STEP 5.3 localKeys.values.forall(v => localKeys.updated(gk, contractId).preimage(v).size <= BigInt(1))
if (!s.activeState.localKeys.values.forall(newF)) {
val w = SetProperties.notForallWitness(s.activeState.localKeys.values, newF)
SetProperties.forallContains(
s.activeState.localKeys.values,
v => s.activeState.localKeys.preimage(v).size <= BigInt(1),
w,
)
MapProperties.inclPreimage(s.activeState.localKeys, gk, contractId, w)
SetProperties.subsetOfSize(
s.activeState.localKeys.updated(gk, contractId).preimage(w),
s.activeState.localKeys.preimage(w),
)
Unreachable()
}
// STEP 5.4 Final calls
MapProperties.updatedValues(s.activeState.localKeys, gk, contractId)
SetProperties.forallSubsetOf(
s.activeState.localKeys.updated(gk, contractId).values,
s.activeState.localKeys.values + contractId,
newF,
)
/** STEP 6 localKeys.keySet ⊆ globalKeys.keySet
*
* For this, we will need the fact that the key is already in the global keys.
*/
unfold(containsOptionKey(s)(mbKey))
unfold(containsKey(s)(gk))
MapProperties.keySetContains(s.globalKeys, gk)
SetProperties.subsetOfIncl(s.activeState.localKeys.keySet, s.globalKeys.keySet, gk)
SetProperties.equalsSubsetOfTransitivity(
s.activeState.localKeys.updated(gk, contractId).keySet,
s.activeState.localKeys.keySet + gk,
s.globalKeys.keySet,
)
}
}.ensuring(stateInvariant(s.visitCreate(contractId, mbKey))(unbound, lc))
/** If a state fulfills the invariants and a node respects the [[CSMInvariantDef.stateNodeCompatibility]] conditions
* then the state obtained after handling it also fulfills the invariants.
*/
@pure
@opaque
def handleNodeInvariant(
s: State,
id: NodeId,
node: Node.Action,
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(s)(unbound, lc))
require(stateNodeCompatibility(s, node, unbound, lc, TraversalDirection.Down))
require(containsActionKey(s)(node))
unfold(s.handleNode(id, node))
unfold(stateNodeCompatibility(s, node, unbound, lc, TraversalDirection.Down))
unfold(containsActionKey(s)(node))
node match {
case create: Node.Create =>
stateInvariantVisitCreate(s, create.coid, create.gkeyOpt, unbound, lc)
case fetch: Node.Fetch =>
stateInvariantAssertKeyMapping(s, fetch.coid, fetch.gkeyOpt, unbound, lc)
case lookup: Node.LookupByKey =>
unfold(containsOptionKey(s)(node.gkeyOpt))
stateInvariantVisitLookup(s, lookup.gkey, lookup.result, unbound, lc)
case exe: Node.Exercise =>
stateInvariantVisitExercise(
s,
id,
exe.targetCoid,
exe.gkeyOpt,
exe.byKey,
exe.consuming,
unbound,
lc,
)
}
}.ensuring(stateInvariant(s.handleNode(id, node))(unbound, lc))
}
object CSMInvariantDerivedProp {
import CSMInvariantDef._
/** If a state fulfills the invariants then the activeKeys contains a key if and only if the globalKeys also do.
*/
@pure
@opaque
def invariantContainsKey(
s: State,
gk: GlobalKey,
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(s)(unbound, lc))
unfold(containsKey(s)(gk))
MapProperties.equalsKeySetContains(s.globalKeys, s.activeKeys, gk)
}.ensuring(containsKey(s)(gk) == s.activeKeys.contains(gk))
/** If a state fulfills the invariants and a key maps to a contract in the global keys, then no other key maps to the
* same contract in the global or local keys.
*/
@pure
@opaque
def invariantGetGlobalKeys(
s: State,
k: GlobalKey,
k2: GlobalKey,
c: ContractId,
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(s)(unbound, lc))
require(s.globalKeys.get(k) == Some(KeyActive(c)))
require(k != k2)
/** STEP 1: globalKeys.values.contains(KeyActive(c))
*/
unfold(s.globalKeys.contains)
MapAxioms.valuesContains(s.globalKeys, k)
/** STEP 2: localKeys.get(k2) != Some(c)
*/
if (s.activeState.localKeys.get(k2) == Some(c)) {
unfold(s.activeState.localKeys.contains)
MapAxioms.valuesContains(s.activeState.localKeys, k2)
SetProperties.mapContains[ContractId, KeyMapping](
s.activeState.localKeys.values,
KeyActive,
s.activeState.localKeys(k2),
)
SetProperties.disjointContains(
s.activeState.localKeys.values.map[KeyMapping](KeyActive),
s.globalKeys.values,
KeyActive(c),
)
Unreachable()
}
/** STEP 3: globalKeys.get(k2) != Some(KeyActive(c)
*/
if (s.globalKeys.get(k2) == Some(KeyActive(c))) {
// STEP 2.1: s.globalKeys.preimage(KeyActive(c)) contains k and k2
MapProperties.preimageGet(s.globalKeys, KeyActive(c), k)
MapProperties.preimageGet(s.globalKeys, KeyActive(c), k2)
// STEP 2.2: Set(k) ++ Set(k2) subsetOf s.globalKeys.preimage(KeyActive(c))
SetProperties.singletonSubsetOf(s.globalKeys.preimage(KeyActive(c)), k)
SetProperties.singletonSubsetOf(s.globalKeys.preimage(KeyActive(c)), k2)
SetProperties.unionSubsetOf(Set(k), Set(k2), s.globalKeys.preimage(KeyActive(c)))
// STEP 2.3: Set(k) ++ Set(k2) size == 2
SetAxioms.singletonSize(k)
SetAxioms.singletonSize(k2)
SetProperties.disjointTwoSingleton(k, k2)
SetAxioms.unionDisjointSize(Set(k), Set(k2))
// STEP 2.4: Final calls
SetProperties.subsetOfSize(Set(k) ++ Set(k2), s.globalKeys.preimage(KeyActive(c)))
SetProperties.filterContains(s.globalKeys.values, _.isDefined, KeyActive(c))
SetProperties.forallContains(
s.globalKeys.values.filter(_.isDefined),
v => s.globalKeys.preimage(v).size <= BigInt(1),
KeyActive(c),
)
Unreachable()
}
}.ensuring(
(s.globalKeys.get(k2) != Some(KeyActive(c))) && (s.activeState.localKeys.get(k2) != Some(c))
)
/** If a state fulfills the invariants and a key maps to a contract in the local keys, then no other key maps to the
* same contract in the global or local keys.
*/
@pure
@opaque
def invariantGetLocalKeys(
s: State,
k: GlobalKey,
k2: GlobalKey,
c: ContractId,
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(s)(unbound, lc))
require(s.activeState.localKeys.get(k) == Some(c))
require(k != k2)
/** STEP 1: localKeys.values.contains(KeyActive(c))
*/
unfold(s.activeState.localKeys.contains)
MapAxioms.valuesContains(s.activeState.localKeys, k)
/** STEP 2: globalKeys.get(k2) != Some(KeyActive(c))
*/
if (s.globalKeys.get(k2) == Some(KeyActive(c))) {
unfold(s.globalKeys.contains)
MapAxioms.valuesContains(s.globalKeys, k2)
SetProperties.mapContains[ContractId, KeyMapping](
s.activeState.localKeys.values,
KeyActive,
c,
)
SetProperties.disjointContains(
s.activeState.localKeys.values.map[KeyMapping](KeyActive),
s.globalKeys.values,
s.globalKeys(k2),
)
Unreachable()
}
/** STEP 3: localKeys.get(k2) != Some(c)
*/
if (s.activeState.localKeys.get(k2) == Some(c)) {
// STEP 2.1: s.activeState.localKeys.preimage(c) contains k and k2
MapProperties.preimageGet(s.activeState.localKeys, c, k)
MapProperties.preimageGet(s.activeState.localKeys, c, k2)
// STEP 2.2: Set(k) ++ Set(k2) subsetOf s.activeState.localKeys.preimage(c)
SetProperties.singletonSubsetOf(s.activeState.localKeys.preimage(c), k)
SetProperties.singletonSubsetOf(s.activeState.localKeys.preimage(c), k2)
SetProperties.unionSubsetOf(Set(k), Set(k2), s.activeState.localKeys.preimage(c))
// STEP 2.3: Set(k) ++ Set(k2) size == 2
SetAxioms.singletonSize(k)
SetAxioms.singletonSize(k2)
SetProperties.disjointTwoSingleton(k, k2)
SetAxioms.unionDisjointSize(Set(k), Set(k2))
// STEP 2.4: Final calls
SetProperties.subsetOfSize(Set(k) ++ Set(k2), s.activeState.localKeys.preimage(c))
SetProperties.forallContains(
s.activeState.localKeys.values,
v => s.activeState.localKeys.preimage(v).size <= BigInt(1),
c,
)
Unreachable()
}
}.ensuring(
(s.globalKeys.get(k2) != Some(KeyActive(c))) && (s.activeState.localKeys.get(k2) != Some(c))
)
/** The invariants are true for any state whose activeState is empty.
*/
@pure
@opaque
def emptyActiveStateInvariant(s: State, unbound: Set[ContractId], lc: Set[ContractId]): Unit = {
unfold(ActiveLedgerState.empty)
unfold(invariantWrtActiveState(s)(unbound, lc)(ActiveLedgerState.empty))
MapProperties.emptyValues[GlobalKey, ContractId]
SetProperties.isEmptySubsetOf(ActiveLedgerState.empty.localKeys.values, s.locallyCreated)
SetProperties.disjointIsEmpty(unbound, ActiveLedgerState.empty.localKeys.values)
SetProperties.forallIsEmpty(
ActiveLedgerState.empty.localKeys.values,
v => ActiveLedgerState.empty.localKeys.preimage(v).size <= BigInt(1),
)
MapProperties.emptyKeySet[GlobalKey, ContractId]
MapProperties.emptyKeySet[ContractId, NodeId]
SetProperties.isEmptySubsetOf(ActiveLedgerState.empty.consumedBy.keySet, s.consumed)
SetProperties.isEmptySubsetOf(ActiveLedgerState.empty.localKeys.keySet, s.globalKeys.keySet)
}.ensuring(
invariantWrtActiveState(s)(unbound, lc)(ActiveLedgerState.empty)
)
/** The list invariants are always true for the empty state.
*/
@pure
@opaque
def emptyListInvariant(s: State, unbound: Set[ContractId], lc: Set[ContractId]): Unit = {
unfold(State.empty)
unfold(invariantWrtList(State.empty)(unbound, lc)(State.empty.rollbackStack))
}.ensuring(
invariantWrtList(State.empty)(unbound, lc)(State.empty.rollbackStack)
)
}

1096
daml-lf/verification/transaction/CSMKeysProperties.scala Normal file
View File

File diff suppressed because it is too large Load Diff

198
daml-lf/verification/transaction/CSMLocallyCreatedProperties.scala Normal file
View File

@ -0,0 +1,198 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package transaction
import stainless.lang.{
unfold,
decreases,
BooleanDecorations,
Either,
Some,
None,
Option,
Right,
Left,
}
import stainless.annotation._
import scala.annotation.targetName
import stainless.collection._
import utils.Value.ContractId
import utils.Transaction.{DuplicateContractKey, InconsistentContractKey, KeyInputError}
import utils._
import ContractStateMachine._
import CSMHelpers._
import CSMEither._
import CSMEitherDef._
/** This file shows how the set of locallyCreated and consumed contracts of a state behave after handling a node.
*/
object CSMLocallyCreatedProperties {
/** The set of locally created contracts has the new contract added to it when the node is an instance of Create and
* otherwise remains the same
*/
@pure
@opaque
def handleNodeLocallyCreated(s: State, id: NodeId, node: Node.Action): Unit = {
unfold(s.handleNode(id, node))
val res = s.handleNode(id, node)
node match {
case create: Node.Create => Trivial()
case fetch: Node.Fetch =>
sameLocallyCreatedTransitivity(s, s.assertKeyMapping(fetch.coid, fetch.gkeyOpt), res)
unfold(sameLocallyCreated(s, res))
case lookup: Node.LookupByKey =>
sameLocallyCreatedTransitivity(s, s.visitLookup(lookup.gkey, lookup.result), res)
unfold(sameLocallyCreated(s, res))
case exe: Node.Exercise =>
sameLocallyCreatedTransitivity(
s,
s.visitExercise(id, exe.targetCoid, exe.gkeyOpt, exe.byKey, exe.consuming),
res,
)
unfold(sameLocallyCreated(s, res))
}
}.ensuring(
s.handleNode(id, node)
.forall(r =>
node match {
case Node.Create(coid, _) => r.locallyCreated == s.locallyCreated + coid
case _ => s.locallyCreated == r.locallyCreated
}
)
)
/** The set of locally created contracts has the new contract added to it when the node is an instance of Create and
* otherwise remains the same
*/
@pure
@opaque
def handleNodeLocallyCreated(
e: Either[KeyInputError, State],
id: NodeId,
node: Node.Action,
): Unit = {
unfold(handleNode(e, id, node))
e match {
case Left(_) => Trivial()
case Right(s) => handleNodeLocallyCreated(s, id, node)
}
}.ensuring(
handleNode(e, id, node).forall(r =>
e.forall(s =>
node match {
case Node.Create(coid, _) => r.locallyCreated == s.locallyCreated + coid
case _ => s.locallyCreated == r.locallyCreated
}
)
)
)
/** If two states propagates the error have the same set of locally created contracts then if the first is a subset of
* a third set then the second one also is.
*/
def sameLocallyCreatedSubsetOfTransivity[T, U](
e1: Either[T, State],
e2: Either[U, State],
lc: Set[ContractId],
): Unit = {
require(sameLocallyCreated(e1, e2))
require(propagatesError(e1, e2))
require(e1.forall(s1 => s1.locallyCreated.subsetOf(lc)))
unfold(propagatesError(e1, e2))
unfold(sameLocallyCreated(e1, e2))
e1 match {
case Left(_) => Trivial()
case Right(s1) => unfold(sameLocallyCreated(s1, e2))
}
}.ensuring(e2.forall(s2 => s2.locallyCreated.subsetOf(lc)))
/** The set of consumed contracts has the consumed contract added to it when the node is an instance of a consuming
* Exercise and otherwise remains the same
*/
@pure
@opaque
def handleNodeConsumed(s: State, id: NodeId, node: Node.Action): Unit = {
unfold(s.handleNode(id, node))
val res = s.handleNode(id, node)
node match {
case create: Node.Create =>
sameConsumedTransitivity(s, s.visitCreate(create.coid, create.gkeyOpt), res)
unfold(sameConsumed(s, res))
case fetch: Node.Fetch =>
sameConsumedTransitivity(s, s.assertKeyMapping(fetch.coid, fetch.gkeyOpt), res)
unfold(sameConsumed(s, res))
case lookup: Node.LookupByKey =>
sameConsumedTransitivity(s, s.visitLookup(lookup.gkey, lookup.result), res)
unfold(sameConsumed(s, res))
case exe: Node.Exercise =>
unfold(s.visitExercise(id, exe.targetCoid, exe.gkeyOpt, exe.byKey, exe.consuming))
for {
state <- s.assertKeyMapping(exe.targetCoid, exe.gkeyOpt)
} yield {
unfold(sameConsumed(s, s.assertKeyMapping(exe.targetCoid, exe.gkeyOpt)))
unfold(state.consume(exe.targetCoid, id))
}
()
}
}.ensuring(
s.handleNode(id, node)
.forall(r =>
node match {
case Node.Exercise(targetCoid, true, _, _, _) => r.consumed == s.consumed + targetCoid
case _ => s.consumed == r.consumed
}
)
)
/** The set of consumed contracts has the consumed contract added to it when the node is an instance of a consuming
* Exercise and otherwise remains the same
*/
@pure
@opaque
def handleNodeConsumed(e: Either[KeyInputError, State], id: NodeId, node: Node.Action): Unit = {
unfold(handleNode(e, id, node))
e match {
case Left(_) => Trivial()
case Right(s) => handleNodeConsumed(s, id, node)
}
}.ensuring(
handleNode(e, id, node).forall(r =>
e.forall(s =>
node match {
case Node.Exercise(targetCoid, true, _, _, _) => r.consumed == s.consumed + targetCoid
case _ => s.consumed == r.consumed
}
)
)
)
/** If two states propagates the error have the same set of consumed contracts then if the first is a subset of
* a third set then the second one also is.
*/
def sameConsumedSubsetOfTransivity[T, U](
e1: Either[T, State],
e2: Either[U, State],
lc: Set[ContractId],
): Unit = {
require(sameConsumed(e1, e2))
require(propagatesError(e1, e2))
require(e1.forall(s1 => s1.consumed.subsetOf(lc)))
unfold(propagatesError(e1, e2))
unfold(sameConsumed(e1, e2))
e1 match {
case Left(_) => Trivial()
case Right(s1) => unfold(sameConsumed(s1, e2))
}
}.ensuring(e2.forall(s2 => s2.consumed.subsetOf(lc)))
}

334
daml-lf/verification/transaction/ContractStateMachineAlt.scala Normal file
View File

@ -0,0 +1,334 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package transaction
import stainless.lang._
import stainless.annotation._
import stainless.collection._
import utils.{
Either,
Map,
Set,
Value,
GlobalKey,
Transaction,
Unreachable,
Node,
ContractKeyUniquenessMode,
NodeId,
MapProperties,
SetProperties,
}
import utils.Value.ContractId
import utils.Transaction.{
KeyCreate,
KeyInputError,
NegativeKeyLookup,
InconsistentContractKey,
DuplicateContractKey,
KeyInput,
}
import CSMHelpers._
import CSMEitherDef._
import CSMEither._
/** Simplified version of the contract state machine. All the implementations are simplified, and [[State.globalKeys]] are
* not updated anymore during [[State.handleNode]]. [[CSMKeysPropertiesDef.addKeyBeforeNode]] has to be called beforehand.
*/
case class State(
locallyCreated: Set[ContractId],
consumed: Set[ContractId],
globalKeys: Map[GlobalKey, ContractStateMachine.KeyMapping],
activeState: ContractStateMachine.ActiveLedgerState,
rollbackStack: List[ContractStateMachine.ActiveLedgerState],
) {
import ContractStateMachine._
@pure @opaque
def keys: Map[GlobalKey, KeyMapping] = {
MapProperties.mapValuesKeySet(activeState.localKeys, KeyActive)
SetProperties.unionEqualsRight(
globalKeys.keySet,
activeState.localKeys.keySet,
activeState.localKeys.mapValues(KeyActive).keySet,
)
MapProperties.concatKeySet(globalKeys, activeState.localKeys.mapValues(KeyActive))
SetProperties.equalsTransitivity(
(globalKeys ++ activeState.localKeys.mapValues(KeyActive)).keySet,
globalKeys.keySet ++ activeState.localKeys.mapValues(KeyActive).keySet,
globalKeys.keySet ++ activeState.localKeys.keySet,
)
globalKeys ++ activeState.localKeys.mapValues(KeyActive)
}.ensuring(res => res.keySet === globalKeys.keySet ++ activeState.localKeys.keySet)
@pure @opaque
def activeKeys: Map[GlobalKey, KeyMapping] = {
keys.mapValues(keyMappingToActiveMapping(activeState.consumedBy))
}
@pure @opaque
def consume(cid: ContractId, nid: NodeId): State = {
unfold(activeState.consume(cid, nid))
this.copy(activeState = activeState.consume(cid, nid), consumed = consumed + cid)
}.ensuring(res =>
(globalKeys == res.globalKeys) &&
(locallyCreated == res.locallyCreated) &&
(rollbackStack == res.rollbackStack) &&
(activeState.localKeys == res.activeState.localKeys)
)
@pure @opaque
def visitCreate(
contractId: ContractId,
mbKey: Option[GlobalKey],
): Either[DuplicateContractKey, State] = {
val me =
this.copy(
locallyCreated = locallyCreated + contractId,
activeState = this.activeState
.copy(locallyCreatedThisTimeline =
this.activeState.locallyCreatedThisTimeline + contractId
),
)
val res = mbKey match {
case None() => Right[DuplicateContractKey, State](me)
case Some(gk) =>
val conflict = activeKeys.get(gk).exists(_ != KeyInactive)
Either.cond(
!conflict,
me.copy(activeState = me.activeState.createKey(gk, contractId)),
DuplicateContractKey(gk),
)
}
unfold(sameGlobalKeys(this, res))
unfold(sameStack(this, res))
unfold(sameConsumed(this, res))
res
}.ensuring(res =>
sameGlobalKeys(this, res) &&
sameStack(this, res) &&
sameConsumed(this, res) &&
res.forall(r => r.locallyCreated == locallyCreated + contractId)
)
@pure @opaque
def visitExercise(
nodeId: NodeId,
targetId: ContractId,
mbKey: Option[GlobalKey],
byKey: Boolean,
consuming: Boolean,
): Either[InconsistentContractKey, State] = {
val res =
for {
state <- assertKeyMapping(targetId, mbKey)
} yield {
if (consuming)
state.consume(targetId, nodeId)
else state
}
unfold(sameGlobalKeys(this, assertKeyMapping(targetId, mbKey)))
unfold(sameStack(this, assertKeyMapping(targetId, mbKey)))
unfold(sameLocalKeys(this, assertKeyMapping(targetId, mbKey)))
unfold(sameLocallyCreated(this, assertKeyMapping(targetId, mbKey)))
unfold(sameGlobalKeys(this, res))
unfold(sameLocalKeys(this, res))
unfold(sameStack(this, res))
unfold(sameLocallyCreated(this, res))
res
}.ensuring(res =>
sameGlobalKeys(this, res) &&
sameStack(this, res) &&
sameLocalKeys(this, res) &&
sameLocallyCreated(this, res)
)
@pure @opaque
def visitLookup(
gk: GlobalKey,
keyResolution: Option[ContractId],
): Either[InconsistentContractKey, State] = {
val res = Either.cond(
activeKeys.getOrElse(gk, KeyInactive) == keyResolution,
this,
InconsistentContractKey(gk),
)
unfold(sameState(this, res))
res
}.ensuring(res => sameState(this, res))
@pure @opaque
def assertKeyMapping(
cid: ContractId,
mbKey: Option[GlobalKey],
): Either[InconsistentContractKey, State] = {
val res = mbKey match {
case None() => Right[InconsistentContractKey, State](this)
case Some(gk) => visitLookup(gk, KeyActive(cid))
}
unfold(sameState(this, res))
res
}.ensuring(res => sameState(this, res))
@pure @opaque
def handleNode(id: NodeId, node: Node.Action): Either[KeyInputError, State] = {
val res = node match {
case create: Node.Create => toKeyInputError(visitCreate(create.coid, create.gkeyOpt))
case fetch: Node.Fetch => toKeyInputError(assertKeyMapping(fetch.coid, fetch.gkeyOpt))
case lookup: Node.LookupByKey => toKeyInputError(visitLookup(lookup.gkey, lookup.result))
case exe: Node.Exercise =>
toKeyInputError(visitExercise(id, exe.targetCoid, exe.gkeyOpt, exe.byKey, exe.consuming))
}
@pure @opaque
def sameHandleNode: Unit = {
node match {
case create: Node.Create =>
sameGlobalKeysTransitivity(this, visitCreate(create.coid, create.gkeyOpt), res)
sameStackTransitivity(this, visitCreate(create.coid, create.gkeyOpt), res)
case fetch: Node.Fetch =>
sameGlobalKeysTransitivity(this, assertKeyMapping(fetch.coid, fetch.gkeyOpt), res)
sameStackTransitivity(this, assertKeyMapping(fetch.coid, fetch.gkeyOpt), res)
case lookup: Node.LookupByKey =>
sameGlobalKeysTransitivity(this, visitLookup(lookup.gkey, lookup.result), res)
sameStackTransitivity(this, visitLookup(lookup.gkey, lookup.result), res)
case exe: Node.Exercise =>
sameGlobalKeysTransitivity(
this,
visitExercise(id, exe.targetCoid, exe.gkeyOpt, exe.byKey, exe.consuming),
res,
)
sameStackTransitivity(
this,
visitExercise(id, exe.targetCoid, exe.gkeyOpt, exe.byKey, exe.consuming),
res,
)
}
}.ensuring(sameGlobalKeys(this, res) && sameStack(this, res))
sameHandleNode
res
}.ensuring(res =>
sameGlobalKeys(this, res) &&
sameStack(this, res)
)
@pure @opaque
def beginRollback(): State = {
val res = this.copy(rollbackStack = activeState :: rollbackStack)
unfold(res.withinRollbackScope)
res
}.ensuring(res =>
(globalKeys == res.globalKeys) &&
(locallyCreated == res.locallyCreated) &&
(consumed == res.consumed)
)
@pure @opaque
def endRollback(): Either[KeyInputError, State] = {
val res = rollbackStack match {
case Nil() =>
Left[KeyInputError, State](
Left[InconsistentContractKey, DuplicateContractKey](
InconsistentContractKey(GlobalKey(BigInt(0)))
)
)
case Cons(headState, tailStack) =>
Right[KeyInputError, State](this.copy(activeState = headState, rollbackStack = tailStack))
}
unfold(sameGlobalKeys(this, res))
unfold(sameLocallyCreated(this, res))
unfold(sameConsumed(this, res))
res
}.ensuring(res =>
sameGlobalKeys(this, res) &&
sameLocallyCreated(this, res) &&
sameConsumed(this, res)
)
@pure @opaque
def withinRollbackScope: Boolean = !rollbackStack.isEmpty
@pure
def advance(substate: State): Either[Unit, State] = {
require(!substate.withinRollbackScope)
if (
substate.globalKeys.keySet
.forall(k => activeKeys.get(k).forall(m => Some(m) == substate.globalKeys.get(k)))
) {
Right[Unit, State](
this.copy(
locallyCreated = locallyCreated ++ substate.locallyCreated,
consumed = consumed ++ substate.consumed,
globalKeys = substate.globalKeys ++ globalKeys,
activeState = activeState.advance(substate.activeState),
)
)
} else {
Left[Unit, State](())
}
}
}
object State {
def empty: State = new State(
Set.empty,
Set.empty,
Map.empty,
ContractStateMachine.ActiveLedgerState.empty,
List.empty,
)
}
object ContractStateMachine {
type KeyResolver = Map[GlobalKey, KeyMapping]
type KeyMapping = Option[ContractId]
val KeyInactive: KeyMapping = None[ContractId]()
val KeyActive: ContractId => KeyMapping = Some[ContractId](_)
final case class ActiveLedgerState(
locallyCreatedThisTimeline: Set[ContractId],
consumedBy: Map[ContractId, NodeId],
localKeys: Map[GlobalKey, ContractId],
) {
@pure @opaque
def consume(contractId: ContractId, nodeId: NodeId): ActiveLedgerState =
this.copy(consumedBy = consumedBy.updated(contractId, nodeId))
def createKey(key: GlobalKey, cid: ContractId): ActiveLedgerState =
this.copy(localKeys = localKeys.updated(key, cid))
@pure @opaque
def advance(substate: ActiveLedgerState): ActiveLedgerState =
ActiveLedgerState(
locallyCreatedThisTimeline =
locallyCreatedThisTimeline ++ substate.locallyCreatedThisTimeline,
consumedBy = consumedBy ++ substate.consumedBy,
localKeys = localKeys ++ substate.localKeys,
)
}
object ActiveLedgerState {
def empty: ActiveLedgerState = ActiveLedgerState(
Set.empty[ContractId],
Map.empty[ContractId, NodeId],
Map.empty[GlobalKey, ContractId],
)
}
}

626
daml-lf/verification/translation/CSMConversion.scala Normal file
View File

@ -0,0 +1,626 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package translation
import stainless.lang._
import stainless.annotation._
import stainless.collection._
import utils.{
Either,
Map,
Set,
Value,
GlobalKey,
Transaction,
Unreachable,
Node,
ContractKeyUniquenessMode,
MapProperties,
MapAxioms,
NodeId,
SetAxioms,
SetProperties,
Trivial,
}
import utils.Value.ContractId
import utils.Transaction.{
KeyCreate,
KeyInputError,
NegativeKeyLookup,
InconsistentContractKey,
DuplicateContractKey,
KeyInput,
}
import transaction.ContractStateMachine._
import transaction.CSMHelpers._
import transaction.CSMKeysPropertiesDef._
import transaction.CSMKeysProperties._
import transaction.CSMInvariantDerivedProp._
import transaction.CSMInvariantDef._
import transaction.State
import ContractStateMachine.{State => StateOriginal, ActiveLedgerState => ActiveLedgerStateOriginal}
object CSMConversion {
@pure
def toKeyMapping: KeyInput => KeyMapping = _.toKeyMapping
@pure
def toKeyInput: KeyMapping => KeyInput = {
case None() => NegativeKeyLookup
case Some(cid) => Transaction.KeyActive(cid)
}
@pure @opaque
def globalKeys(gki: Map[GlobalKey, KeyInput]): Map[GlobalKey, Option[ContractId]] = {
MapProperties.mapValuesKeySet(gki, toKeyMapping)
gki.mapValues(toKeyMapping)
}.ensuring(_.keySet === gki.keySet)
@pure
@opaque
def globalKeyInputs(gki: Map[GlobalKey, KeyMapping]): Map[GlobalKey, KeyInput] = {
MapProperties.mapValuesKeySet(gki, toKeyInput)
gki.mapValues(toKeyInput)
}.ensuring(_.keySet === gki.keySet)
@pure @opaque
def globalKeysGlobalKeyInputs(gki: Map[GlobalKey, KeyMapping]): Unit = {
unfold(globalKeyInputs(gki))
unfold(globalKeys(globalKeyInputs(gki)))
MapProperties.mapValuesAndThen(gki, toKeyInput, toKeyMapping)
if (gki =/= gki.mapValues(toKeyInput andThen toKeyMapping)) {
val k = MapProperties.notEqualsWitness(gki, gki.mapValues(toKeyInput andThen toKeyMapping))
MapProperties.mapValuesGet(gki, toKeyInput andThen toKeyMapping, k)
}
MapProperties.equalsTransitivity(
gki,
gki.mapValues(toKeyInput andThen toKeyMapping),
globalKeys(globalKeyInputs(gki)),
)
MapAxioms.extensionality(gki, globalKeys(globalKeyInputs(gki)))
}.ensuring(globalKeys(globalKeyInputs(gki)) == gki)
@pure
def toOriginal(s: ActiveLedgerState): ActiveLedgerStateOriginal[NodeId] = {
ActiveLedgerStateOriginal[NodeId](s.locallyCreatedThisTimeline, s.consumedBy, s.localKeys)
}
@pure
def toAlt(s: ActiveLedgerStateOriginal[NodeId]): ActiveLedgerState = {
ActiveLedgerState(s.locallyCreatedThisTimeline, s.consumedBy, s.localKeys)
}
@pure @opaque
def altOriginalInverse(s: ActiveLedgerState): Unit = {
unfold(toOriginal(s))
unfold(toAlt(toOriginal(s)))
}.ensuring(toAlt(toOriginal(s)) == s)
@pure
@opaque
def originalAltInverse(s: ActiveLedgerStateOriginal[NodeId]): Unit = {
unfold(toAlt(s))
unfold(toOriginal(toAlt(s)))
}.ensuring(toOriginal(toAlt(s)) == s)
@pure
def toOriginal(s: State): StateOriginal[NodeId] = {
StateOriginal[NodeId](
s.locallyCreated,
globalKeyInputs(s.globalKeys),
toOriginal(s.activeState),
s.rollbackStack.map(toOriginal),
ContractKeyUniquenessMode.Strict,
)
}
@pure
def toAlt(consumed: Set[ContractId])(s: StateOriginal[NodeId]): State = {
State(
s.locallyCreated,
consumed,
globalKeys(s.globalKeyInputs),
toAlt(s.activeState),
s.rollbackStack.map(toAlt),
)
}
@pure
def toAlt[T](consumed: Set[ContractId])(e: Either[T, StateOriginal[NodeId]]): Either[T, State] = {
e.map(toAlt(consumed))
}
@pure
def toOriginal[T](e: Either[T, State]): Either[T, StateOriginal[NodeId]] = {
e.map(toOriginal)
}
@pure
@opaque
def lookupActiveGlobalKeyInputToAlt(
s: StateOriginal[NodeId],
key: GlobalKey,
consumed: Set[ContractId],
) = {
unfold(toAlt(consumed)(s))
unfold(toAlt(s.activeState))
unfold(keyMappingToActiveMapping(toAlt(s.activeState).consumedBy))
unfold(globalKeys(s.globalKeyInputs))
MapProperties.mapValuesGet(s.globalKeyInputs, toKeyMapping, key)
MapProperties.mapValuesGet(
toAlt(consumed)(s).globalKeys,
keyMappingToActiveMapping(toAlt(consumed)(s).activeState.consumedBy),
key,
)
}.ensuring(
s.lookupActiveGlobalKeyInput(key) == (toAlt(consumed)(s)).globalKeys
.mapValues(keyMappingToActiveMapping(toAlt(consumed)(s).activeState.consumedBy))
.get(key)
)
@pure
@opaque
def getLocalActiveKeyToAlt(
s: ActiveLedgerStateOriginal[NodeId],
key: GlobalKey,
consumed: Set[ContractId],
): Unit = {
unfold(toAlt(s))
unfold(keyMappingToActiveMapping(toAlt(s).consumedBy))
MapProperties.mapValuesGet(
s.localKeys,
(v: ContractId) => if (s.consumedBy.contains(v)) KeyInactive else KeyActive(v),
key,
)
MapProperties.mapValuesGet(
toAlt(s).localKeys.mapValues(KeyActive),
keyMappingToActiveMapping(toAlt(s).consumedBy),
key,
)
MapProperties.mapValuesGet(toAlt(s).localKeys, KeyActive, key)
}.ensuring(
s.getLocalActiveKey(key) == toAlt(s).localKeys
.mapValues(KeyActive)
.mapValues(keyMappingToActiveMapping(toAlt(s).consumedBy))
.get(key)
)
@pure
@opaque
def lookupActiveKeyToAlt(
s: StateOriginal[NodeId],
key: GlobalKey,
consumed: Set[ContractId],
): Unit = {
unfold(toAlt(consumed)(s).activeKeys)
unfold(toAlt(consumed)(s).keys)
MapProperties.mapValuesConcat(
toAlt(consumed)(s).globalKeys,
toAlt(consumed)(s).activeState.localKeys.mapValues(KeyActive),
keyMappingToActiveMapping(toAlt(consumed)(s).activeState.consumedBy),
)
MapProperties.equalsGet(
toAlt(consumed)(s).activeKeys,
toAlt(consumed)(s).globalKeys
.mapValues(keyMappingToActiveMapping(toAlt(consumed)(s).activeState.consumedBy)) ++
toAlt(consumed)(s).activeState.localKeys
.mapValues(KeyActive)
.mapValues(keyMappingToActiveMapping(toAlt(consumed)(s).activeState.consumedBy)),
key,
)
MapAxioms.concatGet(
toAlt(consumed)(s).globalKeys
.mapValues(keyMappingToActiveMapping(toAlt(consumed)(s).activeState.consumedBy)),
toAlt(consumed)(s).activeState.localKeys
.mapValues(KeyActive)
.mapValues(keyMappingToActiveMapping(toAlt(consumed)(s).activeState.consumedBy)),
key,
)
getLocalActiveKeyToAlt(s.activeState, key, consumed)
lookupActiveGlobalKeyInputToAlt(s, key, consumed)
}.ensuring(
s.lookupActiveKey(key) == toAlt(consumed)(s).activeKeys.get(key)
)
@pure
@opaque
def consumeToAlt(
s: StateOriginal[NodeId],
cid: ContractId,
nid: NodeId,
consumed: Set[ContractId],
): Unit = {
unfold(toAlt(consumed)(s).consume(cid, nid))
}.ensuring(
toAlt(consumed + cid)(s.copy(activeState = s.activeState.consume(cid, nid))) == toAlt(consumed)(
s
).consume(cid, nid)
)
//
@pure @opaque
def globalKeyInputsContainsToAlt(
s: StateOriginal[NodeId],
gk: GlobalKey,
consumed: Set[ContractId],
): Unit = {
unfold(containsKey(toAlt(consumed)(s))(gk))
MapProperties.equalsKeySetContains(s.globalKeyInputs, globalKeys(s.globalKeyInputs), gk)
}.ensuring(s.globalKeyInputs.contains(gk) == containsKey(toAlt(consumed)(s))(gk))
@pure
@opaque
def globalKeyInputsUpdatedToAlt(
s: StateOriginal[NodeId],
gk: GlobalKey,
keyInput: KeyInput,
consumed: Set[ContractId],
): Unit = {
unfold(globalKeys(s.globalKeyInputs))
unfold(globalKeys(s.globalKeyInputs.updated(gk, keyInput)))
MapProperties.mapValuesUpdated(s.globalKeyInputs, gk, keyInput, toKeyMapping)
MapAxioms.extensionality(
s.globalKeyInputs.updated(gk, keyInput).mapValues(toKeyMapping),
s.globalKeyInputs.mapValues(toKeyMapping).updated(gk, keyInput.toKeyMapping),
)
}.ensuring(
globalKeys(s.globalKeyInputs.updated(gk, keyInput)) == globalKeys(s.globalKeyInputs)
.updated(gk, keyInput.toKeyMapping)
)
@pure
@opaque
def visitCreateToAlt(
s: StateOriginal[NodeId],
contractId: ContractId,
mbKey: Option[GlobalKey],
consumed: Set[ContractId],
): Unit = {
require(s.mode == ContractKeyUniquenessMode.Strict)
unfold(addKey(toAlt(consumed)(s), mbKey, KeyInactive))
unfold(addKey(toAlt(consumed)(s), mbKey, KeyInactive).visitCreate(contractId, mbKey))
mbKey match {
case None() => Trivial()
case Some(gk) =>
// STEP 1: conflicts match
lookupActiveKeyToAlt(s, gk, consumed)
activeKeysAddKey(toAlt(consumed)(s), gk, KeyInactive)
unfold(keyMappingToActiveMapping(toAlt(consumed)(s).activeState.consumedBy))
val newKeyInputs =
if (s.globalKeyInputs.contains(gk)) s.globalKeyInputs
else s.globalKeyInputs.updated(gk, KeyCreate)
// STEP 2: globalKeys(newKeyInputs) == toAlt(s).addKey(gk, KeyInactive).globalKeyInputs
unfold(addKey(toAlt(consumed)(s), gk, KeyInactive))
globalKeyInputsContainsToAlt(s, gk, consumed)
globalKeyInputsUpdatedToAlt(s, gk, KeyCreate, consumed)
}
}.ensuring(
addKey(toAlt(consumed)(s), mbKey, KeyInactive).visitCreate(contractId, mbKey) == toAlt(
consumed
)(s.visitCreate(contractId, mbKey))
)
@pure
def extractPair(
e: Either[Option[
ContractId
] => (KeyMapping, StateOriginal[NodeId]), (KeyMapping, StateOriginal[NodeId])],
result: Option[ContractId],
): (KeyMapping, StateOriginal[NodeId]) = {
e match {
case Left(handle) => handle(result)
case Right(p) => p
}
}
@pure
def extractState(
e: Either[Option[
ContractId
] => (KeyMapping, StateOriginal[NodeId]), (KeyMapping, StateOriginal[NodeId])],
result: Option[ContractId],
): StateOriginal[NodeId] = {
extractPair(e, result)._2
}
@pure
@opaque
def resolveKeyToAlt(
s: StateOriginal[NodeId],
result: Option[ContractId],
gkey: GlobalKey,
consumed: Set[ContractId],
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(toAlt(consumed)(s))(unbound, lc))
lookupActiveKeyToAlt(s, gkey, consumed)
invariantContainsKey(toAlt(consumed)(s), gkey, unbound, lc)
// globalKeyInputsContainsToAlt(s, gkey, consumed)
activeKeysAddKey(toAlt(consumed)(s), gkey, result)
unfold(addKey(toAlt(consumed)(s), gkey, result))
unfold(toAlt(consumed)(s).activeKeys.contains)
unfold(addKey(toAlt(consumed)(s), gkey, result))
globalKeyInputsUpdatedToAlt(
s,
gkey,
result match {
case None() => NegativeKeyLookup
case Some(cid) => Transaction.KeyActive(cid)
},
consumed,
)
unfold(
toAlt(consumed)(s).activeKeys.getOrElse(
gkey,
keyMappingToActiveMapping(toAlt(consumed)(s).activeState.consumedBy)(result),
)
)
unfold(keyMappingToActiveMapping(toAlt(consumed)(s).activeState.consumedBy))
}.ensuring(
(
addKey(toAlt(consumed)(s), gkey, result).activeKeys(gkey),
addKey(toAlt(consumed)(s), gkey, result),
) ==
(extractPair(s.resolveKey(gkey), result)._1, toAlt(consumed)(
extractState(s.resolveKey(gkey), result)
))
)
@pure
@opaque
def visitLookupToAlt(
s: StateOriginal[NodeId],
gk: GlobalKey,
keyInput: Option[ContractId],
keyResolution: Option[ContractId],
consumed: Set[ContractId],
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(toAlt(consumed)(s))(unbound, lc))
unfold(addKey(toAlt(consumed)(s), gk, keyInput).visitLookup(gk, keyResolution))
resolveKeyToAlt(s, keyInput, gk, consumed, unbound, lc)
unfold(addKey(toAlt(consumed)(s), gk, keyInput).activeKeys.getOrElse(gk, KeyInactive))
}.ensuring(
addKey(toAlt(consumed)(s), gk, keyInput).visitLookup(gk, keyResolution) ==
toAlt(consumed)(s.visitLookup(gk, keyInput, keyResolution))
)
@pure
@opaque
def assertKeyMappingToAlt(
s: StateOriginal[NodeId],
cid: ContractId,
gkey: Option[GlobalKey],
consumed: Set[ContractId],
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(toAlt(consumed)(s))(unbound, lc))
unfold(addKey(toAlt(consumed)(s), gkey, Some(cid)).assertKeyMapping(cid, gkey))
unfold(addKey(toAlt(consumed)(s), gkey, Some(cid)))
gkey match {
case None() => Trivial()
case Some(k) => visitLookupToAlt(s, k, Some(cid), Some(cid), consumed, unbound, lc)
}
}.ensuring(
addKey(toAlt(consumed)(s), gkey, Some(cid)).assertKeyMapping(cid, gkey) == toAlt(consumed)(
s.assertKeyMapping(cid, gkey)
)
)
@pure
@opaque
def visitExerciseToAlt(
s: StateOriginal[NodeId],
nodeId: NodeId,
targetId: ContractId,
gk: Option[GlobalKey],
byKey: Boolean,
consuming: Boolean,
consumed: Set[ContractId],
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(toAlt(consumed)(s))(unbound, lc))
require(s.mode == ContractKeyUniquenessMode.Strict)
unfold(
addKey(toAlt(consumed)(s), gk, Some(targetId))
.visitExercise(nodeId, targetId, gk, byKey, consuming)
)
assertKeyMappingToAlt(s, targetId, gk, consumed, unbound, lc)
s.assertKeyMapping(targetId, gk) match {
case Left(e) => Trivial()
case Right(state) => consumeToAlt(state, targetId, nodeId, consumed)
}
}.ensuring(
addKey(toAlt(consumed)(s), gk, Some(targetId))
.visitExercise(nodeId, targetId, gk, byKey, consuming) ==
toAlt(if (consuming) consumed + targetId else consumed)(
s.visitExercise(nodeId, targetId, gk, byKey, consuming)
)
)
@pure @opaque
def nodeConsumed(consumed: Set[ContractId], n: Node): Set[ContractId] = {
n match {
case exe: Node.Exercise if exe.consuming => consumed + exe.targetCoid
case _ => consumed
}
}
@pure
@opaque
def handleNodeOriginal(
e: Either[KeyInputError, StateOriginal[NodeId]],
nodeId: NodeId,
node: Node.Action,
keyInput: Option[ContractId],
): Either[KeyInputError, StateOriginal[NodeId]] = {
e match {
case Right(s) => s.handleNode(nodeId, node, keyInput)
case Left(_) => e
}
}
@pure @opaque
def handleNodeToAlt(
s: StateOriginal[NodeId],
nodeId: NodeId,
node: Node.Action,
keyInput: Option[ContractId],
consumed: Set[ContractId],
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(toAlt(consumed)(s))(unbound, lc))
require(s.mode == ContractKeyUniquenessMode.Strict)
unfold(nodeConsumed(consumed, node))
unfold(addKeyBeforeAction(toAlt(consumed)(s), node))
unfold(addKeyBeforeAction(toAlt(consumed)(s), node).handleNode(nodeId, node))
unfold(nodeActionKeyMapping(node))
node match {
case create: Node.Create => visitCreateToAlt(s, create.coid, create.gkeyOpt, consumed)
case fetch: Node.Fetch =>
assertKeyMappingToAlt(s, fetch.coid, fetch.gkeyOpt, consumed, unbound, lc)
case lookup: Node.LookupByKey =>
unfold(addKey(toAlt(consumed)(s), node.gkeyOpt, nodeActionKeyMapping(node)))
visitLookupToAlt(s, lookup.gkey, lookup.result, lookup.result, consumed, unbound, lc)
case exe: Node.Exercise =>
visitExerciseToAlt(
s,
nodeId,
exe.targetCoid,
exe.gkeyOpt,
exe.byKey,
exe.consuming,
consumed,
unbound,
lc,
)
}
}.ensuring(
addKeyBeforeAction(toAlt(consumed)(s), node).handleNode(nodeId, node) ==
toAlt(nodeConsumed(consumed, node))(s.handleNode(nodeId, node, keyInput))
)
@pure
@opaque
def handleNodeToAlt(
e: Either[KeyInputError, StateOriginal[NodeId]],
nodeId: NodeId,
node: Node.Action,
keyInput: Option[ContractId],
consumed: Set[ContractId],
unbound: Set[ContractId],
lc: Set[ContractId],
): Unit = {
require(stateInvariant(toAlt(consumed)(e))(unbound, lc))
require(e.forall(s => s.mode == ContractKeyUniquenessMode.Strict))
unfold(addKeyBeforeNode(toAlt(consumed)(e), node))
unfold(handleNodeOriginal(e, nodeId, node, keyInput))
e match {
case Right(s) =>
unfold(addKeyBeforeNode(toAlt(consumed)(s), node))
handleNodeToAlt(s, nodeId, node, keyInput, consumed, unbound, lc)
case Left(_) => Trivial()
}
}.ensuring(
handleNode(addKeyBeforeNode(toAlt(consumed)(e), node), nodeId, node) ==
toAlt(nodeConsumed(consumed, node))(handleNodeOriginal(e, nodeId, node, keyInput))
)
@pure
@opaque
def beginRollbackToAlt(s: StateOriginal[NodeId], consumed: Set[ContractId]): Unit = {
unfold(toAlt(consumed)(s).beginRollback())
}.ensuring(
toAlt(consumed)(s).beginRollback() ==
toAlt(consumed)(s.beginRollback())
)
@pure @opaque
def endRollbackOriginal(
s: StateOriginal[NodeId]
): Either[KeyInputError, StateOriginal[NodeId]] = {
if (s.withinRollbackScope) {
Right[KeyInputError, StateOriginal[NodeId]](s.endRollback())
} else {
Left[KeyInputError, StateOriginal[NodeId]](
Left[InconsistentContractKey, DuplicateContractKey](
InconsistentContractKey(GlobalKey(BigInt(0)))
)
)
}
}
@pure
@opaque
def endRollbackToAlt(s: StateOriginal[NodeId], consumed: Set[ContractId]): Unit = {
unfold(toAlt(consumed)(s).endRollback())
unfold(endRollbackOriginal(s))
}.ensuring(
toAlt(consumed)(s).endRollback() ==
toAlt(consumed)(endRollbackOriginal(s))
)
@pure
@opaque
def advanceToAlt(
s: ActiveLedgerStateOriginal[NodeId],
substate: ActiveLedgerStateOriginal[NodeId],
): Unit = {
unfold(toAlt(s).advance(toAlt(substate)))
}.ensuring(toAlt(s).advance(toAlt(substate)) == toAlt(s.advance(substate)))
/** Proof of only a part of advance equivalence. The other part is not here due to a Stainless bug.
*/
@pure @opaque
def advanceToAlt(
s: StateOriginal[NodeId],
substate: StateOriginal[NodeId],
resolver: KeyResolver,
consumed1: Set[ContractId],
consumed2: Set[ContractId],
): Unit = {
require(s.mode == ContractKeyUniquenessMode.Strict)
require(!substate.withinRollbackScope)
require(!toAlt(consumed2)(substate).withinRollbackScope)
require(toAlt(consumed1)(s).advance(toAlt(consumed2)(substate)).isRight)
require(s.advance(resolver, substate).isRight)
unfold(globalKeys(s.globalKeyInputs))
unfold(globalKeys(substate.globalKeyInputs))
unfold(globalKeys(substate.globalKeyInputs ++ s.globalKeyInputs))
MapProperties.mapValuesConcat(substate.globalKeyInputs, s.globalKeyInputs, toKeyMapping)
MapAxioms.extensionality(
globalKeys(substate.globalKeyInputs ++ s.globalKeyInputs),
globalKeys(substate.globalKeyInputs) ++ globalKeys(s.globalKeyInputs),
)
advanceToAlt(s.activeState, substate.activeState)
}.ensuring(
(toAlt(consumed1)(s).advance(toAlt(consumed2)(substate)).get ==
toAlt(consumed1 ++ consumed2)(s.advance(resolver, substate).get))
)
}

532
daml-lf/verification/tree/TransactionTree.scala Normal file
View File

@ -0,0 +1,532 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package tree
import stainless.lang.{
unfold,
decreases,
BooleanDecorations,
Either,
Some,
None,
Option,
Right,
Left,
}
import stainless.annotation._
import stainless.collection._
import utils.Value.ContractId
import utils.Transaction.{DuplicateContractKey, InconsistentContractKey, KeyInputError}
import utils._
import utils.TreeProperties._
import transaction.CSMHelpers._
import transaction.CSMEitherDef._
import transaction.CSMEither._
import transaction.{State}
/** Definitions and basic properties of simplified transaction traversal.
*
* In the contract state maching, handling a node comes in two major step:
* - Adding the node's key to the global keys with its corresponding mapping
* - Processing the node
* In the simplified version of the contract state machine, this behavior is respectively split in two different
* functions [[transaction.CSMKeysPropertiesDef.addKeyBeforeNode]] and [[transaction.State.handleNode]]
*
* A key property of transaction traversal is that one can first add the key-mapping pairs of every node in the
* globalKeys and then process the transaction. The proof of this claims lies in [[TransactionTreeFull]].
* We therefore define the processing part of a transaction assuming that the initial state already contains
* all the key mappings it needs.
*/
object TransactionTreeDef {
/** Function called when a node is entered for the first time ([[utils.TraversalDirection.Down]]).
* - If the node is an instance of [[transaction.Node.Action]] we handle it.
* - If it is a [[transaction.Node.Rollback]] node we call [[transaction.State.beginRollback]].
*
* Among the direct properties one can deduce we have that
* - the [[transaction.State.globalKeys]] are not modified (since we did before processing the transaction)
* - if the inital state is an error then the result is also an error
*
* @param s State before entering the node for the first time
* @param p Node and its id
* @see f,,down,, in the associated latex document
*/
@pure @opaque
def traverseInFun(
s: Either[KeyInputError, State],
p: (NodeId, Node),
): Either[KeyInputError, State] = {
p._2 match {
case r: Node.Rollback => beginRollback(s)
case a: Node.Action => handleNode(s, p._1, a)
}
}.ensuring(res =>
sameGlobalKeys(s, res) &&
propagatesError(s, res)
)
/** Function called when a node is entered for the second time ([[utils.TraversalDirection.Up]]).
* - If the node is an instance of [[transaction.Node.Action]] nothing happens
* - If it is a [[transaction.Node.Rollback]] node we call [[transaction.State.endRollback]]
*
* Among the direct properties one can deduce we have that
* - the [[transaction.State.globalKeys]] are not modified (since we did before processing the transaction)
* - the [[transaction.State.locallyCreated]] and [[transaction.State.consumed]] sets
* are not modified as well.
* - if the inital state is an error then the result is also an error
*
* @param s State before entering the node for the second time
* @param p Node and its id
* @see f,,up,, in the associated latex document
*/
@pure @opaque
def traverseOutFun(
s: Either[KeyInputError, State],
p: (NodeId, Node),
): Either[KeyInputError, State] = {
val res = p._2 match {
case r: Node.Rollback => endRollback(s)
case a: Node.Action => s
}
@pure @opaque
def traverseOutFunProperties: Unit = {
// case Rollback
endRollbackProp(s)
// case Action
sameGlobalKeysReflexivity(s)
sameLocallyCreatedReflexivity(s)
sameConsumedReflexivity(s)
propagatesErrorReflexivity(s)
}.ensuring(
sameGlobalKeys(s, res) &&
sameLocallyCreated(s, res) &&
sameConsumed(s, res) &&
propagatesError(s, res)
)
traverseOutFunProperties
res
}.ensuring(res =>
sameGlobalKeys(s, res) &&
sameLocallyCreated(s, res) &&
sameConsumed(s, res) &&
propagatesError(s, res)
)
/** List of triples whose respective entries are:
* - The state before the i-th step of the traversal
* - The pair node id - node that is handle during the i-th step
* - The direction i.e. if that's the first or the second time we enter the node
*
* @param tr The transaction that is being processed
* @param init The initial state (containing already all the necessary key-mapping pairs in the global keys)
*/
@pure
def scanTransaction(
tr: Tree[(NodeId, Node)],
init: Either[KeyInputError, State],
): List[(Either[KeyInputError, State], (NodeId, Node), TraversalDirection)] = {
tr.scan(init, traverseInFun, traverseOutFun)
}
/** Resulting state after a transaction traversal.
*
* @param tr The transaction that is being processed
* @param init The initial state (containing already all the necessary key-mapping pairs in the global keys)
*/
@pure
def traverseTransaction(
tr: Tree[(NodeId, Node)],
init: Either[KeyInputError, State],
): Either[KeyInputError, State] = {
tr.traverse(init, traverseInFun, traverseOutFun)
}
}
object TransactionTree {
import TransactionTreeDef._
/** Let i less or equal than j two integers.
* The states before the i-th and j-th step of the transaction traversal:
* - have the same [[transaction.State.globalKeys]]
* - are both erroneous if the state before the i-th step is erroneous
*
* @param tr The transaction that is being processed.
* @param init The initial state (containing already all the necessary key-mapping pairs in the global keys).
* @see The corresponding latex document for a pen and paper proof.
*/
@pure
@opaque
def scanTransactionProp(
tr: Tree[(NodeId, Node)],
init: Either[KeyInputError, State],
i: BigInt,
j: BigInt,
): Unit = {
decreases(j)
require(0 <= i)
require(i <= j)
require(j < 2 * tr.size)
val si = scanTransaction(tr, init)(i)._1
if (j == i) {
propagatesErrorReflexivity(si)
sameGlobalKeysReflexivity(si)
} else {
val sjm1 = scanTransaction(tr, init)(j - 1)._1
val sj = scanTransaction(tr, init)(j)._1
scanTransactionProp(tr, init, i, j - 1)
scanIndexingState(tr, init, traverseInFun, traverseOutFun, j)
propagatesErrorTransitivity(si, sjm1, sj)
sameGlobalKeysTransitivity(si, sjm1, sj)
}
}.ensuring(
propagatesError(scanTransaction(tr, init)(i)._1, scanTransaction(tr, init)(j)._1) &&
sameGlobalKeys(scanTransaction(tr, init)(i)._1, scanTransaction(tr, init)(j)._1)
)
/** Let i an integer. The inital state and the state before the i-th step of the transaction traversal:
* - have the same [[transaction.State.globalKeys]]
* - are both erroneous if the initial state is erroneous
*
* @param tr The transaction that is being processed.
* @param init The initial state (containing already all the necessary key-mapping pairs in the global keys).
* @see The corresponding latex document for a pen and paper proof.
*/
@pure
@opaque
def scanTransactionProp(
tr: Tree[(NodeId, Node)],
init: Either[KeyInputError, State],
i: BigInt,
): Unit = {
require(0 <= i)
require(i < 2 * tr.size)
scanTransactionProp(tr, init, 0, i)
scanIndexingState(tr, init, traverseInFun, traverseOutFun, 0)
}.ensuring(
propagatesError(init, scanTransaction(tr, init)(i)._1) &&
sameGlobalKeys(init, scanTransaction(tr, init)(i)._1)
)
/** Basic properties of transaction processing:
* - The [[transaction.State.globalKeys]] are not modified throughout the traversal
* - The [[transaction.State.rollbackStack]] is the same before and after the transaction
* - If the initial state is erroneous, so is the result of the traversal
*
* @param tr The transaction that is being processed.
* @param init The initial state (containing already all the necessary key-mapping pairs in the global keys).
*
* @note This is one of the only structural induction proof in the codebase. Whereas structural induction is
* not needed for the first and third property, it is for the second one. In fact, the property is not
* a local claim that is preserved every step. It is due to the symmetrical nature of the traversal (for
* rollbacks) and it would therefore not make sense finding a i such that the property is true at the
* i-th step but not the i+1-th one.
* Please also note that since we are working with opaqueness (almost) everywhere we will need to unfold
* many definition when proving such global properties.
*
* @see The corresponding latex document for a pen and paper proof.
* @see [[findBeginRollback]] and [[TransactionTreeChecks.traverseTransactionLC]] for other examples of
* structural induction proofs.
*/
@pure
@opaque
def traverseTransactionProp(
tr: Tree[(NodeId, Node)],
init: Either[KeyInputError, State],
): Unit = {
decreases(tr)
unfold(tr.traverse(init, traverseInFun, traverseOutFun))
tr match {
case Endpoint() =>
sameGlobalKeysReflexivity(init)
sameStackReflexivity(init)
propagatesErrorReflexivity(init)
case ContentNode(n, sub) =>
val e1 = traverseInFun(init, n)
val e2 = traverseTransaction(sub, e1)
val e3 = traverseTransaction(tr, init)
traverseTransactionProp(sub, e1)
// As the key property is a local one applying transitivity is sufficient
// we could have done the same with propagatesError but we need to unfold
// the latter to prove the stack equality property (which is global)
sameGlobalKeysTransitivity(init, e1, e2)
sameGlobalKeysTransitivity(init, e2, e3)
unfold(traverseInFun(init, n))
unfold(traverseOutFun(e2, n))
unfold(beginRollback(init))
unfold(endRollback(e2))
unfold(propagatesError(init, e1))
unfold(propagatesError(e1, e2))
unfold(propagatesError(e2, e3))
unfold(propagatesError(init, e3))
unfold(sameStack(init, e1))
unfold(sameStack(e1, e2))
unfold(sameStack(e2, e3))
unfold(sameStack(init, e3))
// If any of the intermediate states is not defined the result is immediate
// because of error propagation. Otherwise, we need to unfold the definition
// of beginRollback and endRollback as the result depends on the content of
// their body
(init, e1, e2) match {
case (Right(s0), Right(s1), Right(s2)) =>
unfold(s0.beginRollback())
unfold(s2.endRollback())
unfold(sameStack(s0, e1))
unfold(sameStack(s1, e2))
unfold(sameStack(s2, e3))
unfold(sameStack(s0, e3))
case (Right(s0), _, _) => unfold(sameStack(s0, e3))
case _ => Trivial()
}
case ArticulationNode(l, r) =>
val el = traverseTransaction(l, init)
val er = traverseTransaction(tr, init)
traverseTransactionProp(l, init)
traverseTransactionProp(r, el)
propagatesErrorTransitivity(init, el, er)
sameStackTransitivity(init, el, er)
sameGlobalKeysTransitivity(init, el, er)
}
}.ensuring(
sameGlobalKeys(init, traverseTransaction(tr, init)) &&
sameStack(init, traverseTransaction(tr, init)) &&
propagatesError(init, traverseTransaction(tr, init))
)
/** If any state of the transaction traversal is erroneous, then the result of the traversal is erroneous as well
*
* @param tr The transaction that is being processed.
* @param init The initial state (containing already all the necessary key-mapping pairs in the global keys).
* @param i The number of the step during the traversal
* @see The corresponding latex document for a pen and paper proof.
*/
@pure
@opaque
def traverseTransactionDefined(
tr: Tree[(NodeId, Node)],
init: Either[KeyInputError, State],
i: BigInt,
): Unit = {
require(0 <= i)
require(i < 2 * tr.size)
if (tr.size > 0) {
scanIndexingState(tr, init, traverseInFun, traverseOutFun, 0)
}
scanTransactionProp(tr, init, i, 2 * tr.size - 1)
propagatesErrorTransitivity(
scanTransaction(tr, init)(i)._1,
scanTransaction(tr, init)(2 * tr.size - 1)._1,
traverseTransaction(tr, init),
)
}.ensuring(
propagatesError(scanTransaction(tr, init)(i)._1, traverseTransaction(tr, init))
)
/** Given a step number in which [[transaction.Node.Rollback]] is entered for the second time, returns the step
* number in which it is has been entered for the first time. Also returns a subtree with the following convenient
* properties.
*
* If the result of the function is (j, sub) then:
* - The size of sub is strictly smaller than the size of the transaction tree.
* - Due to causality, j is strictly smaller than the step number given in argument.
* - The state before entering the node for the second time is the result of traversing sub. The
* inital state of the traversal is the state after step j.
*
* This version of findBeginRollback deals with two traversal simultaneously. This is due to the fact that the result
* only depends on the shape of the transaction and is independent of the initial state.
* For a simplified version cf. below.
*
* Please note that the claim is valid only if the tree is unique.
*
* @param tr The transaction that is being processed.
* @param init1 The initial state of the first traversal.
* @param init2 The initial state of the second traversal.
* @param i The step number during which the node is entered for the second time.
*
* @note This is one of the only structural induction proof in the codebase. Because the global nature of the property,
* it is not possible to prove a local claim that is preserved during every step. This is due to the symmetry
* of the traversal (for rollbacks) and it would therefore not make sense finding a i such that the
* property is true at the i-th step but not the i+1-th one.
*
* @see The corresponding latex document for a pen and paper proof.
* @see [[traverseTransactionProp]] and [[TransactionTreeChecks.traverseTransactionLC]] for other examples of
* structural induction proofs.
*/
@pure
@opaque
def findBeginRollback(
tr: Tree[(NodeId, Node)],
init1: Either[KeyInputError, State],
init2: Either[KeyInputError, State],
i: BigInt,
): (BigInt, Tree[(NodeId, Node)]) = {
decreases(tr)
require(tr.isUnique)
require(i >= 0)
require(i < 2 * tr.size)
require(scanTransaction(tr, init1)(i)._2._2.isInstanceOf[Node.Rollback])
require(scanTransaction(tr, init1)(i)._3 == TraversalDirection.Up)
unfold(tr.size)
unfold(tr.isUnique)
scanIndexingNode(
tr,
init1,
init2,
traverseInFun,
traverseOutFun,
traverseInFun,
traverseOutFun,
i,
)
tr match {
case Endpoint() => Unreachable()
case ContentNode(c, str) =>
scanIndexing(c, str, init1, traverseInFun, traverseOutFun, i)
scanIndexing(c, str, init2, traverseInFun, traverseOutFun, i)
if (c == scanTransaction(tr, init1)(i)._2) {
scanIndexing(c, str, init1, traverseInFun, traverseOutFun, 0)
scanIndexing(c, str, init2, traverseInFun, traverseOutFun, 0)
scanIndexing(c, str, init1, traverseInFun, traverseOutFun, 2 * tr.size - 1)
scanIndexing(c, str, init2, traverseInFun, traverseOutFun, 2 * tr.size - 1)
isUniqueIndexing(tr, init1, traverseInFun, traverseOutFun, i, 2 * tr.size - 1)
isUniqueIndexing(tr, init2, traverseInFun, traverseOutFun, i, 2 * tr.size - 1)
unfold(traverseInFun(init1, c))
unfold(traverseInFun(init2, c))
unfold(traverseOutFun(init1, c))
unfold(traverseOutFun(init2, c))
(BigInt(0), str)
} else {
val (j, sub) =
findBeginRollback(str, traverseInFun(init1, c), traverseInFun(init2, c), i - 1)
scanIndexing(c, str, init1, traverseInFun, traverseOutFun, j + 1)
scanIndexing(c, str, init2, traverseInFun, traverseOutFun, j + 1)
(j + 1, sub)
}
case ArticulationNode(l, r) =>
scanIndexing(l, r, init1, traverseInFun, traverseOutFun, i)
scanIndexing(l, r, init2, traverseInFun, traverseOutFun, i)
if (i < 2 * l.size) {
val (j, sub) = findBeginRollback(l, init1, init2, i)
scanIndexing(l, r, init1, traverseInFun, traverseOutFun, j)
scanIndexing(l, r, init2, traverseInFun, traverseOutFun, j)
// Required for performance (timeout: 2)
assert(
scanTransaction(tr, init1)(i)._1 == traverseTransaction(
sub,
beginRollback(scanTransaction(tr, init1)(j)._1),
)
)
assert(
scanTransaction(tr, init2)(i)._1 == traverseTransaction(
sub,
beginRollback(scanTransaction(tr, init2)(j)._1),
)
)
(j, sub)
} else {
val (j, sub) = findBeginRollback(
r,
traverseTransaction(l, init1),
traverseTransaction(l, init2),
i - 2 * l.size,
)
scanIndexing(l, r, init1, traverseInFun, traverseOutFun, j + 2 * l.size)
scanIndexing(l, r, init2, traverseInFun, traverseOutFun, j + 2 * l.size)
(j + 2 * l.size, sub)
}
}
}.ensuring((j, sub) =>
0 <= j && j < i && sub.size < tr.size &&
(scanTransaction(tr, init1)(j)._2 == scanTransaction(tr, init1)(i)._2) &&
(scanTransaction(tr, init2)(j)._2 == scanTransaction(tr, init2)(i)._2) &&
(scanTransaction(tr, init1)(j)._3 == TraversalDirection.Down) &&
(scanTransaction(tr, init2)(j)._3 == TraversalDirection.Down) &&
(scanTransaction(tr, init1)(i)._1 == traverseTransaction(
sub,
beginRollback(scanTransaction(tr, init1)(j)._1),
)) &&
(scanTransaction(tr, init2)(i)._1 == traverseTransaction(
sub,
beginRollback(scanTransaction(tr, init2)(j)._1),
))
)
/** Given a step number in which [[transaction.Node.Rollback]] is entered for the second time, returns the step
* number in which it is has been entered for the first time. Also returns a subtree with the following convenient
* properties.
*
* If the result of the function is (j, sub) then:
* - The size of sub is strictly smaller than the size of the transaction tree.
* - Due to causality, j is strictly smaller than the step number given in argument.
* - The state before entering the node for the second time is the result of traversing sub. The
* inital state of the traversal is the state after step j.
*
* This results only depends on the shape of the transaction and is independent of the initial state.
* For a version dealing with multiple transaction at the same time cf. the more complex version above.
*
* Please note that the claim is valid only if the tree is unique.
*
* @param tr The transaction that is being processed.
* @param init The initial state of the traversal.
* @param i The step number during which the node is entered for the second time.
* @see The corresponding latex document for a pen and paper proof.
*/
@pure
@opaque
def findBeginRollback(
tr: Tree[(NodeId, Node)],
init: Either[KeyInputError, State],
i: BigInt,
): (BigInt, Tree[(NodeId, Node)]) = {
require(tr.isUnique)
require(i >= 0)
require(i < 2 * tr.size)
require(scanTransaction(tr, init)(i)._2._2.isInstanceOf[Node.Rollback])
require(scanTransaction(tr, init)(i)._3 == TraversalDirection.Up)
findBeginRollback(tr, init, init, i)
}.ensuring((j, sub) =>
0 <= j && j < i && sub.size < tr.size &&
(scanTransaction(tr, init)(j)._2 == scanTransaction(tr, init)(i)._2) &&
(scanTransaction(tr, init)(j)._3 == TraversalDirection.Down) &&
(scanTransaction(tr, init)(i)._1 == traverseTransaction(
sub,
beginRollback(scanTransaction(tr, init)(j)._1),
))
)
}

480
daml-lf/verification/tree/TransactionTreeAdvance.scala Normal file
View File

@ -0,0 +1,480 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package tree
import stainless.lang.{
unfold,
decreases,
BooleanDecorations,
Either,
Some,
None,
Option,
Right,
Left,
}
import stainless.annotation._
import stainless.collection._
import utils.Value.ContractId
import utils.Transaction.{DuplicateContractKey, InconsistentContractKey, KeyInputError}
import utils._
import utils.TreeProperties._
import transaction.{State}
import transaction.CSMHelpers._
import transaction.CSMAdvanceDef._
import transaction.CSMAdvance._
import transaction.CSMEitherDef._
import transaction.ContractStateMachine._
import TransactionTreeDef._
import TransactionTree._
/** File stating how the activeState evolve while processing a transaction. We want to prove that the activeState of the
* resulting state of a traversal can be expressed in terms of the inital state active state and the advance method.
*/
object TransactionTreeAdvanceDef {
/** Function called when a node is entered for the first time ([[utils.TraversalDirection.Down]]).
* Compute the active state and the rollbackStack of a state after processing a node given only the rollbackStack
* and the active state of it behorehand.
*
* @param s rollbackStack and activeState of the state before the node
* @param p Node and its id
*/
@pure
@opaque
def activeStateInFun(
s: (ActiveLedgerState, List[ActiveLedgerState]),
p: (NodeId, Node),
): (ActiveLedgerState, List[ActiveLedgerState]) = {
p._2 match {
case a: Node.Action => (s._1.advance(actionActiveStateAddition(p._1, a)), s._2)
case r: Node.Rollback => (s._1, s._1 :: s._2)
}
}
/** Function called when a node is entered for the second time ([[utils.TraversalDirection.Up]]).
* Compute the active state and the rollbackStack of a state after processing a node given only the rollbackStack
* and the active state of it behorehand.
*
* @param s rollbackStack and activeState of the state before the node
* @param p Node and its id
*/
@pure
@opaque
def activeStateOutFun(
s: (ActiveLedgerState, List[ActiveLedgerState]),
p: (NodeId, Node),
): (ActiveLedgerState, List[ActiveLedgerState]) = {
p._2 match {
case a: Node.Action => s
case r: Node.Rollback =>
s._2 match {
case Nil() => s
case Cons(h, t) => (h, t)
}
}
}
/** List of triples whose respective entries are:
* - The activeState and the rollbackStack before the i-th step of the traversal
* - The pair node id - node that is handle during the i-th step
* - The direction i.e. if that's the first or the second time we enter the node
*
* @param tr The transaction that is being processed
* @param init The activeState and teh rollbackStack of the initial state of the traversal
*/
@pure
def scanActiveState(
tr: Tree[(NodeId, Node)],
init: (ActiveLedgerState, List[ActiveLedgerState]),
): List[((ActiveLedgerState, List[ActiveLedgerState]), (NodeId, Node), TraversalDirection)] = {
tr.scan(init, activeStateInFun, activeStateOutFun)
}
/** [[scanActiveState]] where the inital state is empty
*/
@pure
def scanActiveState(
tr: Tree[(NodeId, Node)]
): List[((ActiveLedgerState, List[ActiveLedgerState]), (NodeId, Node), TraversalDirection)] = {
scanActiveState(tr, (ActiveLedgerState.empty, Nil[ActiveLedgerState]()))
}
/** Computes the activeState and the rollbackStack of the state obtained after processing a transaction.
*
* @param tr The transaction that is being processed
* @param init The activeState and the rollbackStack of the initial state of the traversal
*/
@pure
def traverseActiveState(
tr: Tree[(NodeId, Node)],
init: (ActiveLedgerState, List[ActiveLedgerState]),
): (ActiveLedgerState, List[ActiveLedgerState]) = {
tr.traverse(init, activeStateInFun, activeStateOutFun)
}
/** [[traverseActiveState]] where the inital state is empty
*/
@pure
def traverseActiveState(
tr: Tree[(NodeId, Node)]
): (ActiveLedgerState, List[ActiveLedgerState]) = {
traverseActiveState(tr, (ActiveLedgerState.empty, Nil[ActiveLedgerState]()))
}
}
object TransactionTreeAdvance {
import TransactionTreeAdvanceDef._
/** The rollbackStack of the initial and final state of a transaction traversal are equal
*
* @param tr The transaction that is being processed
* @param init The initial state of the traversal
*
* @see [[TransactionTree.traverseTransactionProp]] for an alternative proof of the same concept.
*/
@pure
@opaque
def traverseActiveStateSameStack(
tr: Tree[(NodeId, Node)],
init: (ActiveLedgerState, List[ActiveLedgerState]),
): Unit = {
decreases(tr)
unfold(tr.traverse(init, activeStateInFun, activeStateOutFun))
tr match {
case Endpoint() => Trivial()
case ContentNode(n, sub) =>
val a1 = activeStateInFun(init, n)
traverseActiveStateSameStack(sub, a1)
unfold(activeStateInFun(init, n))
unfold(activeStateOutFun(traverseActiveState(sub, a1), n))
case ArticulationNode(l, r) =>
val al = traverseActiveState(l, init)
traverseActiveStateSameStack(l, init)
traverseActiveStateSameStack(r, al)
}
}.ensuring(
init._2 == traverseActiveState(tr, init)._2
)
/** The rollbackStacks of the state before entering a node for the first time and after having entered it for the second
* time are the same.
*
* @param tr The transaction that is being processed.
* @param init The activeState and the rollbackStack of the initial state of the transaction
* @param i The step number during which the node is entered for the first time.
* @param j The step number during which the node is entered for the second time.
*
* @note This is one of the only structural induction proof in the codebase. Because the global nature of the property,
* it is not possible to prove a local claim that is preserved during every step. This is due to the symmetry
* of the traversal (for rollbacks) and it would therefore not make sense finding a i such that the
* property is true at the i-th step but not the i+1-th one.
* @see [[TransactionTree.findBeginRollback]] for an alternative proof of the same concept.
*/
@pure
@opaque
def findBeginRollbackActiveState(
tr: Tree[(NodeId, Node)],
init: (ActiveLedgerState, List[ActiveLedgerState]),
i: BigInt,
j: BigInt,
): Unit = {
decreases(tr)
require(tr.isUnique)
require(i >= 0)
require(i <= j)
require(j < 2 * tr.size)
require(scanActiveState(tr, init)(i)._2 == scanActiveState(tr, init)(j)._2)
require(scanActiveState(tr, init)(i)._2._2.isInstanceOf[Node.Rollback])
require(scanActiveState(tr, init)(i)._3 == TraversalDirection.Down)
require(scanActiveState(tr, init)(j)._3 == TraversalDirection.Up)
unfold(tr.size)
unfold(tr.isUnique)
tr match {
case Endpoint() => Unreachable()
case ContentNode(c, str) =>
scanIndexing(c, str, init, activeStateInFun, activeStateOutFun, i)
scanIndexing(c, str, init, activeStateInFun, activeStateOutFun, j)
if ((i == 0) || (j == 2 * tr.size - 1)) {
scanIndexing(c, str, init, activeStateInFun, activeStateOutFun, 0)
scanIndexing(c, str, init, activeStateInFun, activeStateOutFun, 2 * tr.size - 1)
isUniqueIndexing(tr, init, activeStateInFun, activeStateOutFun, 0, i)
isUniqueIndexing(tr, init, activeStateInFun, activeStateOutFun, j, 2 * tr.size - 1)
traverseActiveStateSameStack(str, activeStateInFun(init, c))
unfold(activeStateInFun(init, c))
} else {
findBeginRollbackActiveState(str, activeStateInFun(init, c), i - 1, j - 1)
}
case ArticulationNode(l, r) =>
scanIndexing(l, r, init, activeStateInFun, activeStateOutFun, i)
scanIndexing(l, r, init, activeStateInFun, activeStateOutFun, j)
if (j < 2 * l.size) {
findBeginRollbackActiveState(l, init, i, j)
} else if (i >= 2 * l.size) {
findBeginRollbackActiveState(
r,
l.traverse(init, activeStateInFun, activeStateOutFun),
i - 2 * l.size,
j - 2 * l.size,
)
} else {
scanContains(l, init, activeStateInFun, activeStateOutFun, i)
scanContains(
r,
l.traverse(init, activeStateInFun, activeStateOutFun),
activeStateInFun,
activeStateOutFun,
j - 2 * l.size,
)
SetProperties.disjointContains(
l.content,
r.content,
tr.scan(init, activeStateInFun, activeStateOutFun)(i)._2,
)
SetProperties.disjointContains(
l.content,
r.content,
tr.scan(init, activeStateInFun, activeStateOutFun)(j)._2,
)
Unreachable()
}
}
}.ensuring(
scanActiveState(tr, init)(i)._1._1 :: scanActiveState(tr, init)(i)._1._2 == scanActiveState(
tr,
init,
)(j)._1._2
)
/** For any step in a transaction traversal, [[scanActiveState]] computes the activeState of the intermediate state
* of that step.
*
* @param tr The transaction that is being processed.
* @param init The initial state of the traversal.
* @param i The step number.
*/
@pure
@opaque
def scanActiveStateAdvance(
tr: Tree[(NodeId, Node)],
init: Either[KeyInputError, State],
i: BigInt,
): Unit = {
decreases(i)
require(i >= 0)
require(i < 2 * tr.size)
require(init.isRight)
require(scanTransaction(tr, init)(i)._1.isRight)
require(tr.isUnique)
scanIndexingState(tr, init, traverseInFun, traverseOutFun, i)
scanIndexingState(
tr,
(ActiveLedgerState.empty, Nil[ActiveLedgerState]()),
activeStateInFun,
activeStateOutFun,
i,
)
if (i == 0) {
emptyAdvance(init.get.activeState)
} else {
scanTransactionProp(tr, init, i - 1, i)
unfold(propagatesError(scanTransaction(tr, init)(i - 1)._1, scanTransaction(tr, init)(i)._1))
scanActiveStateAdvance(tr, init, i - 1)
scanIndexingNode(
tr,
(ActiveLedgerState.empty, Nil[ActiveLedgerState]()),
init,
activeStateInFun,
activeStateOutFun,
traverseInFun,
traverseOutFun,
i - 1,
)
val (si, n, dir) = scanTransaction(tr, init)(i - 1)
val ai = scanActiveState(tr)(i - 1)._1
if (dir == TraversalDirection.Down) {
unfold(traverseInFun(si, n))
unfold(activeStateInFun(ai, n))
n._2 match {
case a: Node.Action =>
unfold(handleNode(si, n._1, a))
handleNodeActiveState(si.get, n._1, a)
advanceAssociativity(init.get.activeState, ai._1, actionActiveStateAddition(n._1, a))
case r: Node.Rollback =>
unfold(beginRollback(si))
unfold(si.get.beginRollback())
}
} else {
unfold(traverseOutFun(si, n))
unfold(activeStateOutFun(ai, n))
n._2 match {
case a: Node.Action => Trivial()
case r: Node.Rollback =>
val (j, sub) = findBeginRollback(tr, init, i - 1)
val sj = scanTransaction(tr, init)(j)._1
traverseTransactionProp(sub, beginRollback(sj))
scanTransactionProp(tr, init, j, i)
unfold(propagatesError(sj, scanTransaction(tr, init)(i)._1))
unfold(sameStack(beginRollback(sj), si))
unfold(sameStack(sj.get.beginRollback(), si))
unfold(endRollback(si))
unfold(si.get.endRollback())
unfold(beginRollback(sj))
unfold(sj.get.beginRollback())
scanIndexingNode(
tr,
(ActiveLedgerState.empty, Nil[ActiveLedgerState]()),
init,
activeStateInFun,
activeStateOutFun,
traverseInFun,
traverseOutFun,
j,
)
findBeginRollbackActiveState(
tr,
(ActiveLedgerState.empty, Nil[ActiveLedgerState]()),
j,
i - 1,
)
scanActiveStateAdvance(tr, init, j)
}
}
}
}.ensuring(
(scanTransaction(tr, init)(i)._1.get.activeState ==
init.get.activeState.advance(scanActiveState(tr)(i)._1._1))
)
/** [[traverseActiveState]] computes the activeState of the resulting state of transaction traversal.
*
* @param tr The transaction that is being processed.
* @param init The initial state of the traversal.
*/
@pure
@opaque
def traverseActiveStateAdvance(
tr: Tree[(NodeId, Node)],
init: Either[KeyInputError, State],
): Unit = {
require(init.isRight)
require(traverseTransaction(tr, init).isRight)
require(tr.isUnique)
if (tr.size == 0) {
emptyAdvance(init.get.activeState)
} else {
scanIndexingState(tr, init, traverseInFun, traverseOutFun, 0)
scanIndexingState(
tr,
(ActiveLedgerState.empty, Nil[ActiveLedgerState]()),
activeStateInFun,
activeStateOutFun,
0,
)
traverseTransactionDefined(tr, init, 2 * tr.size - 1)
unfold(
propagatesError(
scanTransaction(tr, init)(2 * tr.size - 1)._1,
traverseTransaction(tr, init),
)
)
scanActiveStateAdvance(tr, init, 2 * tr.size - 1)
scanIndexingNode(
tr,
(ActiveLedgerState.empty, Nil[ActiveLedgerState]()),
init,
activeStateInFun,
activeStateOutFun,
traverseInFun,
traverseOutFun,
2 * tr.size - 1,
)
val (si, n, dir) = scanTransaction(tr, init)(2 * tr.size - 1)
val ai = scanActiveState(tr)(2 * tr.size - 1)._1
if (dir == TraversalDirection.Down) {
unfold(traverseInFun(si, n))
unfold(activeStateInFun(ai, n))
n._2 match {
case a: Node.Action =>
unfold(handleNode(si, n._1, a))
handleNodeActiveState(si.get, n._1, a)
advanceAssociativity(init.get.activeState, ai._1, actionActiveStateAddition(n._1, a))
case r: Node.Rollback =>
unfold(beginRollback(si))
unfold(si.get.beginRollback())
}
} else {
unfold(traverseOutFun(si, n))
unfold(activeStateOutFun(ai, n))
n._2 match {
case a: Node.Action => Trivial()
case r: Node.Rollback =>
val (j, sub) = findBeginRollback(tr, init, 2 * tr.size - 1)
val sj = scanTransaction(tr, init)(j)._1
traverseTransactionProp(sub, beginRollback(sj))
traverseTransactionDefined(tr, init, j)
unfold(propagatesError(sj, traverseTransaction(tr, init)))
unfold(sameStack(beginRollback(sj), si))
unfold(sameStack(sj.get.beginRollback(), si))
unfold(endRollback(si))
unfold(si.get.endRollback())
unfold(beginRollback(sj))
unfold(sj.get.beginRollback())
scanIndexingNode(
tr,
(ActiveLedgerState.empty, Nil[ActiveLedgerState]()),
init,
activeStateInFun,
activeStateOutFun,
traverseInFun,
traverseOutFun,
j,
)
findBeginRollbackActiveState(
tr,
(ActiveLedgerState.empty, Nil[ActiveLedgerState]()),
j,
2 * tr.size - 1,
)
scanActiveStateAdvance(tr, init, j)
}
}
}
}.ensuring(
(traverseTransaction(tr, init).get.activeState ==
init.get.activeState.advance(traverseActiveState(tr)._1))
)
}

1175
daml-lf/verification/tree/TransactionTreeChecks.scala Normal file
View File

File diff suppressed because it is too large Load Diff

1004
daml-lf/verification/tree/TransactionTreeFull.scala Normal file
View File

File diff suppressed because it is too large Load Diff

1086
daml-lf/verification/tree/TransactionTreeInconsistency.scala Normal file
View File

File diff suppressed because it is too large Load Diff

270
daml-lf/verification/tree/TransactionTreeInvariant.scala Normal file
View File

@ -0,0 +1,270 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package tree
import stainless.lang.{
unfold,
decreases,
BooleanDecorations,
Either,
Some,
None,
Option,
Right,
Left,
}
import stainless.annotation._
import stainless.collection._
import utils.Value.ContractId
import utils.Transaction.{DuplicateContractKey, InconsistentContractKey, KeyInputError}
import utils._
import utils.TreeProperties._
import transaction.CSMHelpers._
import transaction.CSMEitherDef._
import transaction.CSMEither._
import transaction.CSMLocallyCreatedProperties._
import transaction.{State}
import transaction.CSMKeysPropertiesDef._
import transaction.CSMInvariantDef._
import transaction.CSMInvariant._
import transaction.ContractStateMachine.{KeyMapping, ActiveLedgerState}
import TransactionTreeDef._
import TransactionTreeChecksDef._
import TransactionTreeChecks._
import TransactionTreeKeys._
import TransactionTreeKeysDef._
/** Properties on how invariants are preserved throughout transaction traversals.
*/
object TransactionTreeInvariant {
/** If the traversals in [[TransactionTreeChecks]] did not raise any error, then every pair intermediate state - node
* in the traversal respects the [[transaction.TransactioInvariantDef.stateNodeCompatibility]] condition.
*
* @param tr The tree that is being traversed
* @param init The initial state of the traversal
* @param i The step number during which the node is processed
*/
@pure @opaque
def scanStateNodeCompatibility(
tr: Tree[(NodeId, Node)],
init: Either[KeyInputError, State],
i: BigInt,
): Unit = {
require(i < 2 * tr.size)
require(0 <= i)
require(init.isRight)
require(traverseUnbound(tr)._3)
require(traverseLC(tr, init.get.locallyCreated, init.get.consumed, true)._3)
require(scanTransaction(tr, init)(i)._1.isRight)
val (si, n, dir) = scanTransaction(tr, init)(i)
val ilc = init.get.locallyCreated
val icons = init.get.consumed
unfold(
stateNodeCompatibility(
si.get,
n._2,
traverseUnbound(tr)._1,
traverseLC(tr, ilc, icons, true)._1,
dir,
)
)
dir match {
case TraversalDirection.Up => Trivial()
case TraversalDirection.Down =>
scanIndexingNode(
tr,
init,
(ilc, icons, true),
traverseInFun,
traverseOutFun,
buildLC,
(z, t) => z,
i,
)
scanIndexingNode(
tr,
init,
(Set.empty[ContractId], Set.empty[ContractId], true),
traverseInFun,
traverseOutFun,
unboundFun,
(z, t) => z,
i,
)
scanTraverseLCPropDown(tr, ilc, icons, true, i)
scanTraverseUnboundPropDown(tr, i)
scanTransactionLC(tr, init, true, i)
}
}.ensuring(
stateNodeCompatibility(
scanTransaction(tr, init)(i)._1.get,
scanTransaction(tr, init)(i)._2._2,
traverseUnbound(tr)._1,
traverseLC(tr, init.get.locallyCreated, init.get.consumed, true)._1,
scanTransaction(tr, init)(i)._3,
)
)
/** If the traversals in [[TransactionTreeChecks]] did not raise any error and if the initial state contains all the
* keys of the tree, then every intermediate state of the transaction traversal preserves the invariants.
*
* @param tr The tree that is being traversed
* @param init The initial state of the traversal
* @param i The step number of the intermediate state
*/
@pure @opaque
def scanInvariant(
tr: Tree[(NodeId, Node)],
init: Either[KeyInputError, State],
i: BigInt,
): Unit = {
require(i >= 0)
require(i < 2 * tr.size)
require(init.isRight)
require(traverseUnbound(tr)._3)
require(traverseLC(tr, init.get.locallyCreated, init.get.consumed, true)._3)
require(
stateInvariant(init)(
traverseUnbound(tr)._1,
traverseLC(tr, init.get.locallyCreated, init.get.consumed, true)._1,
)
)
require(containsAllKeys(tr, init))
val p: Either[KeyInputError, State] => Boolean = x =>
stateInvariant(x)(
traverseUnbound(tr)._1,
traverseLC(tr, init.get.locallyCreated, init.get.consumed, true)._1,
)
if (!p(scanTransaction(tr, init)(i)._1)) {
val j = scanNotProp(tr, init, traverseInFun, traverseOutFun, p, i)
scanIndexingState(tr, init, traverseInFun, traverseOutFun, j + 1)
val s = scanTransaction(tr, init)(j)._1
val n = scanTransaction(tr, init)(j)._2
val dir = scanTransaction(tr, init)(j)._3
s match {
case Left(_) =>
if (dir == TraversalDirection.Down) {
unfold(propagatesError(s, traverseInFun(s, n)))
} else {
unfold(propagatesError(s, traverseOutFun(s, n)))
}
case Right(state) =>
unfold(traverseInFun(s, n))
unfold(traverseOutFun(s, n))
n._2 match {
case a: Node.Action =>
if (dir == TraversalDirection.Down) {
containsAllKeysImpliesDown(tr, init, j)
unfold(containsKey(s)(n._2))
unfold(containsNodeKey(state)(n._2))
scanStateNodeCompatibility(tr, init, j)
handleNodeInvariant(
state,
n._1,
a,
traverseUnbound(tr)._1,
traverseLC(tr, init.get.locallyCreated, init.get.consumed, true)._1,
)
}
case r: Node.Rollback =>
if (dir == TraversalDirection.Down) {
unfold(beginRollback(s))
stateInvariantBeginRollback(
state,
traverseUnbound(tr)._1,
traverseLC(tr, init.get.locallyCreated, init.get.consumed, true)._1,
)
} else {
unfold(endRollback(s))
stateInvariantEndRollback(
state,
traverseUnbound(tr)._1,
traverseLC(tr, init.get.locallyCreated, init.get.consumed, true)._1,
)
}
}
}
}
}.ensuring(
stateInvariant(scanTransaction(tr, init)(i)._1)(
traverseUnbound(tr)._1,
traverseLC(tr, init.get.locallyCreated, init.get.consumed, true)._1,
)
)
/** If the traversals in [[TransactionTreeChecks]] did not raise any error and if the initial state contains all the
* keys of the tree, then the state obtained after processing the transaction preserves the invariants.
*
* @param tr The tree that is being traversed
* @param init The initial state of the traversal
*/
@pure
@opaque
def traverseInvariant(tr: Tree[(NodeId, Node)], init: Either[KeyInputError, State]): Unit = {
require(init.isRight)
require(traverseUnbound(tr)._3)
require(traverseLC(tr, init.get.locallyCreated, init.get.consumed, true)._3)
require(
stateInvariant(init)(
traverseUnbound(tr)._1,
traverseLC(tr, init.get.locallyCreated, init.get.consumed, true)._1,
)
)
require(containsAllKeys(tr, init))
if (tr.size == 0) {
Trivial()
} else {
scanIndexingState(tr, init, traverseInFun, traverseOutFun, 0)
scanInvariant(tr, init, 2 * tr.size - 1)
val s = scanTransaction(tr, init)(2 * tr.size - 1)._1
val n = scanTransaction(tr, init)(2 * tr.size - 1)._2
s match {
case Left(_) => unfold(propagatesError(s, traverseOutFun(s, n)))
case Right(state) =>
unfold(traverseOutFun(s, n))
n._2 match {
case a: Node.Action => Trivial()
case r: Node.Rollback =>
unfold(endRollback(s))
stateInvariantEndRollback(
state,
traverseUnbound(tr)._1,
traverseLC(tr, init.get.locallyCreated, init.get.consumed, true)._1,
)
}
}
}
}.ensuring(
stateInvariant(traverseTransaction(tr, init))(
traverseUnbound(tr)._1,
traverseLC(tr, init.get.locallyCreated, init.get.consumed, true)._1,
)
)
}

1109
daml-lf/verification/tree/TransactionTreeKeys.scala Normal file
View File

File diff suppressed because it is too large Load Diff

257
daml-lf/verification/utils/AxiomaticMap.scala Normal file
View File

@ -0,0 +1,257 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package utils
import stainless.lang.{unfold, Option, None, Some, BooleanDecorations}
import stainless.annotation._
import scala.annotation.targetName
import scala.collection.{Map => ScalaMap}
import MapProperties._
import SetProperties._
case class Map[K, V](@pure @extern toScala: ScalaMap[K, V]) {
import MapAxioms._
@pure @extern
def get(k: K): Option[V] = ???
@pure @opaque
def getOrElse(k: K, d: V): V = get(k).getOrElse(d)
@pure
def view: Map[K, V] = this
@pure
def toMap: Map[K, V] = this
@pure @extern
def preimage(s: Set[V]): Set[K] = ???
@pure
@extern
def find(f: ((K, V)) => Boolean): Option[(K, V)] = ???
@pure
@extern
def foldLeft[B](z: B)(op: (B, (K, V)) => B): B = ???
@pure @opaque
def preimage(v: V): Set[K] = preimage(Set(v))
@pure @extern
def submapOf(m2: Map[K, V]): Boolean = ???
@pure @opaque
def apply(k: K): V = {
require(contains(k))
unfold(contains)
get(k).get
}.ensuring(Some[V](_) == get(k))
@pure @opaque
def contains: K => Boolean = get(_).isDefined
@pure @extern
def concat(m2: Map[K, V]): Map[K, V] = Map(toScala ++ m2.toScala)
@pure @alias
def ++(s2: Map[K, V]): Map[K, V] = concat(s2)
@pure @opaque
def updated(k: K, v: V): Map[K, V] = {
val res = concat(Map(k -> v))
def updatedProperties: Unit = {
unfold(res.contains)
singletonGet(k, v, k)
concatGet(this, Map(k -> v), k)
// values
singletonValues(k, v)
concatValues(this, Map(k -> v))
unfold(values.incl(v))
unionEqualsRight(values, Map(k -> v).values, Set(v))
SetProperties.subsetOfEqualsTransitivity(
res.values,
values ++ Map(k -> v).values,
values ++ Set(v),
)
singletonKeySet(k, v)
concatKeySet(this, Map(k -> v))
unionEqualsRight(keySet, Map(k -> v).keySet, Set(k))
SetProperties.equalsTransitivity(res.keySet, keySet ++ Map(k -> v).keySet, keySet ++ Set(k))
unfold(keySet.incl(k))
if (!submapOf(res) && (!contains(k) || (get(k) == Some[V](v)))) {
val w = notSubmapOfWitness(this, res)
concatGet(this, Map(k -> v), w)
singletonGet(k, v, w)
}
if (submapOf(res) && contains(k) && (get(k) != Some[V](v))) {
submapOfGet(this, res, k)
}
}.ensuring(
res.contains(k) &&
res.get(k) == Some[V](v) &&
res.keySet === keySet + k &&
res.values.subsetOf(values + v) &&
(submapOf(res) == (!contains(k) || (get(k) == Some[V](v))))
)
updatedProperties
res
}.ensuring(res =>
res.contains(k) &&
res.get(k) == Some[V](v) &&
res.keySet === keySet + k &&
res.values.subsetOf(values + v) &&
(submapOf(res) == (!contains(k) || get(k) == Some[V](v)))
)
@pure @opaque
def keySet: Set[K] = preimage(values)
@pure @extern
def values: Set[V] = ???
@pure @targetName("mapValuesArgSingle")
def mapValues[V2](f: V => V2): Map[K, V2] = {
mapValues((k: K) => f)
}
@pure @opaque @targetName("mapValuesArgPair")
def mapValues[V2](f: K => V => V2): Map[K, V2] = {
map { case (k, v) => k -> f(k)(v) }
}
@pure
@extern
def map[K2, V2](f: ((K, V)) => (K2, V2)): Map[K2, V2] = Map(toScala.map(f))
@pure @extern
def filter(f: ((K, V)) => Boolean): Map[K, V] = Map(toScala.filter(f))
@pure
def ===(m2: Map[K, V]): Boolean = {
submapOf(m2) && m2.submapOf(this)
}
@pure
def =/=(m2: Map[K, V]): Boolean = !(this === m2)
}
object Map {
@pure @extern
def empty[K, V]: Map[K, V] = Map[K, V](ScalaMap[K, V]())
@pure @extern
def apply[K, V](p: (K, V)): Map[K, V] = Map[K, V](ScalaMap[K, V](p))
}
object MapAxioms {
/** Getting from a concatenation is equivalent to getting in the second map and in case of failure in the first one.
*/
@pure @extern
def concatGet[K, V](m1: Map[K, V], m2: Map[K, V], ks: K): Unit = {}.ensuring(
(m1 ++ m2).get(ks) == m2.get(ks).orElse(m1.get(ks))
)
/** Getting in an empty map will always result in a failure
*/
@pure
@extern
def emptyGet[K, V](ks: K): Unit = {}.ensuring(Map.empty[K, V].get(ks) == None[V]())
/** Getting from a singleton will be defined if and only if the query is the key of the pair. In this case the returned
* mapping is the value of the pair.
*/
@pure @extern
def singletonGet[K, V](k: K, v: V, ks: K): Unit = {}.ensuring(
Map(k -> v).get(ks) == (if (k == ks) Some(v) else None[V]())
)
/** Getting in a map after having mapped its value is the same as getting in the original map and afterward applying
* the function on the returned mapping
*/
@pure @extern
def mapValuesGet[K, V, V2](m: Map[K, V], f: K => V => V2, k: K): Unit = {}.ensuring(
m.mapValues(f).get(k) == m.get(k).map(f(k))
)
/** If a map is a submap of another one and it contains a given key, then that key is bound to the same mapping in both
* maps
*/
@pure @extern
def submapOfGet[K, V](m1: Map[K, V], m2: Map[K, V], k: K): Unit = {
require(m1.submapOf(m2))
require(m1.contains(k))
}.ensuring(m1.get(k) == m2.get(k))
/** If a map is not submap of another one then we can exhibit a key in the first map such that their mapping is different
*/
@pure
@extern
def notSubmapOfWitness[K, V](m1: Map[K, V], m2: Map[K, V]): K = {
require(!m1.submapOf(m2))
??? : K
}.ensuring(res => m1.contains(res) && (m1.get(res) != m2.get(res)))
@pure
@extern
def preimageGet[K, V](m: Map[K, V], s: Set[V], k: K): Unit = {}.ensuring(
m.preimage(s).contains(k) == (m.get(k).exists(s.contains))
)
/** If the values of a map contain a value then we can exhibit a key such that its mapping in the map is equal to the
* value
*/
@pure @extern
def valuesWitness[K, V](m: Map[K, V], v: V): K = {
require(m.values.contains(v))
(??? : K)
}.ensuring(res => m.get(res) == Some[V](v))
/** If map contains a key then the values of the map contain its mapping
*/
@pure
@extern
def valuesContains[K, V](m: Map[K, V], k: K): Unit = {
require(m.contains(k))
}.ensuring(m.values.contains(m(k)))
/** If find is defined then
*/
@pure
@extern
def findGet[K, V](m: Map[K, V], f: ((K, V)) => Boolean): Unit = {
require(m.find(f).isDefined)
}.ensuring(
m.get(m.find(f).get._1) == Some[V](m.find(f).get._2) && f((m.find(f).get))
)
/** If if there is a value in the map that satisfies a given predicate then find is defined.
*/
@pure
@extern
def findDefined[K, V](m: Map[K, V], f: ((K, V)) => Boolean, k: K, v: V): Unit = {
require(m.get(k) == Some[V](v))
require(f(k, v))
}.ensuring(
m.find(f).isDefined
)
/** Extensionality axiom
*
* If two maps are submap of each other then their are equal
*/
@pure @extern
def extensionality[K, V](m1: Map[K, V], m2: Map[K, V]): Unit = {
require(m1 === m2)
}.ensuring(m1 == m2)
}

287
daml-lf/verification/utils/AxiomaticSet.scala Normal file
View File

@ -0,0 +1,287 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package utils
import stainless.lang._
import stainless.annotation._
import scala.collection.{Set => ScalaSet}
import SetProperties._
case class Set[T](@pure @extern toScala: ScalaSet[T]) {
import SetAxioms._
@pure @opaque
def isEmpty: Boolean = this === Set.empty[T]
@pure @extern
def size: BigInt = toScala.size
@pure @opaque
def contains: T => Boolean = e => exists(_ == e)
@pure @alias
def apply(e: T): Boolean = contains(e)
@pure @extern
def forall(f: T => Boolean): Boolean = toScala.forall(f)
@pure @extern
def exists(f: T => Boolean): Boolean = toScala.exists(f)
@pure @opaque
def subsetOf(s2: Set[T]): Boolean = forall(s2.contains)
@pure @extern
def union(s2: Set[T]): Set[T] = Set(toScala ++ s2.toScala)
@pure @alias
def ++(s2: Set[T]): Set[T] = union(s2)
@pure @opaque
def incl(e: T): Set[T] = {
val res = union(Set(e))
@pure @opaque
def inclProp: Unit = {
unionContains(this, Set(e), e)
singletonContains(e)
subsetOfUnion(this, Set(e))
singletonSize(e)
if (contains(e)) {
intersectSingleton(this, e)
unionSize(this, Set(e))
sizeEquals(intersect(Set(e)), Set(e))
} else {
disjointSingleton(this, e)
unionDisjointSize(this, Set(e))
}
if (res.isEmpty) {
isEmptyContains(res, e)
}
}.ensuring(
res.contains(e) &&
subsetOf(res) &&
(res.size == (if (contains(e)) size else size + 1)) &&
!res.isEmpty
)
inclProp
res
}.ensuring { res =>
res.contains(e) &&
subsetOf(res) &&
(res.size == (if (contains(e)) size else size + 1)) &&
!res.isEmpty
}
@pure @alias
def +(e: T): Set[T] = incl(e)
@pure @extern
def filter(f: T => Boolean): Set[T] = Set(toScala.filter(f))
@pure
@extern
def map[V](f: T => V): Set[V] = Set(toScala.map(f))
@pure
@opaque
def diff(s2: Set[T]): Set[T] = {
filterSubsetOf(this, x => !s2.contains(x))
filter(!s2.contains(_))
}.ensuring(res => res.subsetOf(this))
@pure @alias
def &~(s2: Set[T]): Set[T] = diff(s2)
@pure @opaque
def remove(e: T): Set[T] = {
diff(Set[T](e))
}.ensuring(res => res.subsetOf(this))
@pure @alias
def -(e: T): Set[T] = remove(e)
@pure
@opaque
def symDiff(s2: Set[T]): Set[T] = diff(s2) ++ s2.diff(this)
@pure @opaque
def intersect(s2: Set[T]): Set[T] = union(s2) &~ symDiff(s2)
@pure @opaque
def disjoint(s2: Set[T]): Boolean = intersect(s2).isEmpty
@pure @alias
def &(s2: Set[T]): Set[T] = intersect(s2)
@pure @extern
def witness(f: T => Boolean): T = {
require(exists(f))
??? : T
}.ensuring(w => contains(w) && f(w))
/** Extensional equality for finite sets
*
* Should not be opaque in order to have automatic symmetry
*/
@pure @nopaque
def ===(s2: Set[T]): Boolean = subsetOf(s2) && s2.subsetOf(this)
@pure @alias
def =/=(s2: Set[T]): Boolean = !(this === s2)
}
object Set {
@pure @extern
def empty[T]: Set[T] = Set[T](ScalaSet[T]())
@pure @extern
def apply[T](e: T): Set[T] = Set[T](ScalaSet[T](e))
@pure
def range(a: BigInt, b: BigInt): Set[BigInt] = {
decreases(b - a)
require(a <= b)
if (a == b) {
Set.empty[BigInt]
} else {
Set.range(a + 1, b) + a
}
}
}
object SetAxioms {
/** Size nonnegativity axiom
*
* The size of any set is always non negative
*/
@pure
@extern
def sizePositive[T](s: Set[T]): Unit = {}.ensuring(s.size >= BigInt(0))
/** Singleton size axiom
*
* The size of a singleton is 1
*/
@pure @extern
def singletonSize[T](e: T): Unit = {}.ensuring(Set(e).size == BigInt(1))
/** Disjoint union size axiom
*
* The size of a disjoint union is the sum of the sizes of the set
*/
@pure
@extern
def unionDisjointSize[T](s1: Set[T], s2: Set[T]): Unit = {
require(s1.disjoint(s2))
}.ensuring((s1 ++ s2).size == s1.size + s2.size)
/** Congruence size axiom
*
* If two sets are equal then their size is also equal
*/
@pure
@extern
def sizeEquals[T](s1: Set[T], s2: Set[T]): Unit = {
require(s1 === s2)
}.ensuring(s1.size == s2.size)
/** De Morgan's laws for quantifiers
*
* The second one should not be an axiom if we assume that !!f == f
* which Stainless is not able to prove.
*/
@pure @extern @inlineOnce
def notForallExists[T](s: Set[T], f: T => Boolean): Unit = {}.ensuring(
!s.forall(f) == s.exists(!f(_))
)
@pure
@extern
@inlineOnce
def forallNotExists[T](s: Set[T], f: T => Boolean): Unit = {}.ensuring(
!s.forall(!f(_)) == s.exists(f)
)
/** Existential quantifier definition
*
* Should not be an axiom if we assume some properties on lambdas that
* Stainless is not able to prove
*/
@pure @extern
def witnessExists[T](s: Set[T], f: T => Boolean, w: T): Unit = {
require(s.contains(w))
require(f(w))
}.ensuring(s.exists(f))
/** Axiom of empty set
*
* Empty introduction axiom: any predicate on the empty set is valid. Equivalent
* to the ZF empty set axiom stating that there exists an empty such that it
* contains no element.
*/
@pure
@extern
def forallEmpty[T](f: T => Boolean): Unit = {}.ensuring(Set.empty.forall(f))
/** Axiom of union
*
* Union introduction axiom: any predicate is true on the union of two sets if
* and only if it is true for both.
*/
@pure @extern
def forallUnion[T](s1: Set[T], s2: Set[T], f: T => Boolean): Unit = {}.ensuring(
(s1 ++ s2).forall(f) == (s1.forall(f) && s2.forall(f))
)
/** Axiom of filter
*
* Filter introduction axiom: if a set is filtered by a predicate then all the element
* of the set verify this predicate.
*/
@pure
@extern
@inlineOnce
def forallFilter[T](s: Set[T], f: T => Boolean, p: T => Boolean): Unit = {}.ensuring(
s.filter(f).forall(p) == s.forall(x => f(x) ==> p(x))
)
/** Axiom of map
*
* Map introduction axiom: if a set is filtered by a predicate then all the element
* of the set verify this predicate.
*/
@pure
@extern
@inlineOnce
def forallMap[T, V](s: Set[T], f: T => V, p: V => Boolean): Unit = {}.ensuring(
s.map(f).forall(p) == s.forall(f andThen p)
)
/** Axiom of singleton
*
* Singleton introduction axiom: a predicate is true on a singleton if and only if
* it is valid for its unique element. Equivalent to an axiom for incl.
*/
@pure @extern
def forallSingleton[T](e: T, f: T => Boolean): Unit = {}.ensuring(Set(e).forall(f) == f(e))
/** Extensionality axiom
*
* If two sets are subset of each other then their are equal
*/
@pure
@extern
def extensionality[T](s1: Set[T], s2: Set[T]): Unit = {
require(s1 === s2)
}.ensuring(s1 == s2)
}

14
daml-lf/verification/utils/GlobalKey.scala Normal file
View File

@ -0,0 +1,14 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package utils
case class GlobalKey(hash: BigInt)
sealed abstract class ContractKeyUniquenessMode extends Product with Serializable
object ContractKeyUniquenessMode {
case object Off extends ContractKeyUniquenessMode
case object Strict extends ContractKeyUniquenessMode
}

45
daml-lf/verification/utils/Helpers.scala Normal file
View File

@ -0,0 +1,45 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package utils
import stainless.annotation._
import stainless.lang._
import scala.annotation.{Annotation}
object Unreachable {
@opaque
def apply(): Nothing = {
require(false)
???
}
}
object Trivial {
def apply(): Unit = ()
}
@ignore
class nopaque extends Annotation
@ignore
class alias extends Annotation
object Either {
@pure
def cond[A, B](test: Boolean, right: B, left: A): Either[A, B] = {
if (test) Right[A, B](right) else Left[A, B](left)
}.ensuring((res: Either[A, B]) => res.isInstanceOf[Right[A, B]] == test)
}
object Option {
def filterNot[T](o: Option[T], p: T => Boolean): Option[T] =
o match {
case Some(v) if !p(v) => o
case _ => None[T]()
}
}

184
daml-lf/verification/utils/InvListProperties.scala Normal file
View File

@ -0,0 +1,184 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package utils
import stainless.collection._
import stainless.lang._
import stainless.annotation._
object ListProperties {
extension[T](l: List[T]) {
def bindexOf(e: T): BigInt = l.indexOf(e)
def blength: BigInt = l.length
def bapply(i: BigInt): T = {
require(i >= 0)
require(i < l.length)
l(i)
}
}
@pure @opaque
def notForallWitness[T](l: List[T], f: T => Boolean): T = {
decreases(l)
require(!l.forall(f))
l match {
case Nil() => Unreachable()
case Cons(h, t) => if (!f(h)) h else notForallWitness(t, f)
}
}.ensuring(res => l.contains(res) && !f(res))
@pure
@opaque
def concatContains[T](@induct l1: List[T], l2: List[T], e: T): Unit = {}.ensuring(
(l1 ++ l2).contains(e) == (l1.contains(e) || l2.contains(e))
)
@pure
@opaque
def forallConcat[T](l1: List[T], l2: List[T], p: T => Boolean): Unit = {
if ((l1 ++ l2).forall(p)) {
if (!l1.forall(p)) {
val w = notForallWitness(l1, p)
concatContains(l1, l2, w)
forallContains(l1 ++ l2, p, w)
}
if (!l2.forall(p)) {
val w = notForallWitness(l2, p)
concatContains(l1, l2, w)
forallContains(l1 ++ l2, p, w)
}
}
if (l1.forall(p) && l2.forall(p) && !(l1 ++ l2).forall(p)) {
val w = notForallWitness(l1 ++ l2, p)
concatContains(l1, l2, w)
if (l1.contains(w)) forallContains(l1, p, w) else forallContains(l2, p, w)
}
}.ensuring((l1 ++ l2).forall(p) == (l1.forall(p) && l2.forall(p)))
@pure @opaque
def forallContains[T](l: List[T], f: T => Boolean, e: T): Unit = {
if (l.forall(f) && l.contains(e)) {
ListSpecs.forallContained(l, f, e)
}
}.ensuring((l.forall(f) && l.contains(e)) ==> f(e))
@pure
@opaque
def bapplyContains[T](tr: List[T], i: BigInt): Unit = {
decreases(tr)
require(i >= 0)
require(i < tr.blength)
tr match {
case Nil() => Trivial()
case Cons(h, t) =>
if (i == 0) {
Trivial()
} else {
bapplyContains(t, i - 1)
}
}
}.ensuring(tr.contains(tr.bapply(i)))
def isUnique[T](tr: List[T]): Boolean = {
decreases(tr)
tr match {
case Nil() => true
case Cons(h, t) => !t.contains(h) && isUnique(t)
}
}
@pure
@opaque
def isUniqueIndex[T](tr: List[T], i1: BigInt, i2: BigInt): Unit = {
require(i1 >= 0)
require(i2 >= 0)
require(i1 < tr.blength)
require(i2 < tr.blength)
require(isUnique(tr))
decreases(tr)
tr match {
case Nil() => Trivial()
case Cons(h, t) =>
if ((i1 == 0) && (i2 == 0)) {
Trivial()
} else if (i1 == 0) {
bapplyContains(t, i2 - 1)
} else if (i2 == 0) {
bapplyContains(t, i1 - 1)
} else {
isUniqueIndex(t, i1 - 1, i2 - 1)
}
}
}.ensuring((tr.bapply(i1) == tr.bapply(i2)) == (i1 == i2))
@pure @opaque
def bapplyBindexOf[T](l: List[T], e: T): Unit = {
decreases(l)
require(l.contains(e))
l match {
case Nil() => Unreachable()
case Cons(h, t) =>
if (h == e) {
Trivial()
} else {
bapplyBindexOf(t, e)
}
}
}.ensuring(
l.bapply(l.bindexOf(e)) == e
)
@pure
@opaque
def bindexOfLast[T](l: List[T], e: T): Unit = {
require(l.bindexOf(e) >= l.blength - 1)
require(!l.isEmpty)
decreases(l)
require(l.contains(e))
l match {
case Nil() => Unreachable()
case Cons(h, t) =>
if (t.isEmpty) {
Trivial()
} else {
bindexOfLast(t, e)
}
}
}.ensuring(
e == l.last
)
@pure
def next[T](l: List[T], e: T): T = {
require(l.contains(e))
require(e != l.last)
if (l.bindexOf(e) >= l.blength - 1) {
bindexOfLast(l, e)
}
l.bapply(l.bindexOf(e) + 1)
}.ensuring(l.contains)
@pure
@opaque
def concatIndex[T](l1: List[T], l2: List[T], i: BigInt): Unit = {
decreases(l1)
require(i >= 0)
require(i < l1.size + l2.size)
l1 match {
case Nil() => Trivial()
case Cons(h1, t1) =>
if (i == 0) {
Trivial()
} else {
concatIndex(t1, l2, i - 1)
}
}
}.ensuring(
(l1 ++ l2)(i) == (if (i < l1.size) l1(i) else l2(i - l1.size))
)
}

1104
daml-lf/verification/utils/MapProperties.scala Normal file
View File

File diff suppressed because it is too large Load Diff

57
daml-lf/verification/utils/Node.scala Normal file
View File

@ -0,0 +1,57 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package utils
import stainless.lang._
import stainless.annotation._
import stainless.proof._
import stainless.collection._
import Value.ContractId
/** Generic transaction node type for both update transactions and the
* transaction graph.
*/
sealed trait Node
object Node {
sealed trait Action extends Node {
def gkeyOpt: Option[GlobalKey]
def byKey: Boolean
}
sealed trait LeafOnlyAction extends Action
final case class Create(coid: ContractId, override val gkeyOpt: Option[GlobalKey])
extends LeafOnlyAction {
override def byKey: Boolean = false
}
final case class Fetch(
coid: ContractId,
override val gkeyOpt: Option[GlobalKey],
override val byKey: Boolean,
) extends LeafOnlyAction
final case class Exercise(
targetCoid: ContractId,
consuming: Boolean,
children: List[NodeId],
override val gkeyOpt: Option[GlobalKey],
override val byKey: Boolean,
) extends Action
final case class LookupByKey(gkey: GlobalKey, result: Option[ContractId]) extends LeafOnlyAction {
override def gkeyOpt: Option[GlobalKey] = Some(gkey)
override def byKey: Boolean = true
}
final case class Rollback(children: List[NodeId]) extends Node
}
final case class NodeId(index: BigInt)

2106
daml-lf/verification/utils/SetProperties.scala Normal file
View File

File diff suppressed because it is too large Load Diff

57
daml-lf/verification/utils/Transaction.scala Normal file
View File

@ -0,0 +1,57 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package utils
import stainless.lang._
import stainless.annotation._
import scala.annotation.nowarn
import stainless.proof._
import stainless.collection._
import Value.ContractId
object Transaction {
/** The state of a key at the beginning of the transaction.
*/
sealed trait KeyInput extends Product with Serializable {
def toKeyMapping: Option[ContractId]
def isActive: Boolean
}
/** No active contract with the given key.
*/
sealed trait KeyInactive extends KeyInput {
override def toKeyMapping: Option[ContractId] = None[ContractId]()
override def isActive: Boolean = false
}
/** A contract with the key will be created so the key must be inactive.
*/
@nowarn
final case object KeyCreate extends KeyInactive
/** Negative key lookup so the key mus tbe inactive.
*/
@nowarn
final case object NegativeKeyLookup extends KeyInactive
/** Key must be mapped to this active contract.
*/
final case class KeyActive(cid: ContractId) extends KeyInput {
override def toKeyMapping: Option[ContractId] = Some(cid)
override def isActive: Boolean = true
}
sealed abstract class TransactionError
final case class DuplicateContractKey(key: GlobalKey) extends TransactionError
final case class InconsistentContractKey(key: GlobalKey)
type KeyInputError = Either[InconsistentContractKey, DuplicateContractKey]
}

655
daml-lf/verification/utils/Tree.scala Normal file
View File

@ -0,0 +1,655 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package utils
import stainless.collection._
import stainless.lang.{unfold, decreases, BooleanDecorations}
import stainless.annotation._
import SetProperties._
import ListProperties._
import SetAxioms._
/** Type class representing forests in manner to avoid measure problems. In the rest of the file and the package we will
* make no distinction between a tree and a forest.
*
* A forest can either be:
* - A content node: a forest with a node on top of it, that is a tree
* - An articulation node: the union between a tree (on the left) and a forest (on the right)
* - The empty forest which does not contain any node.
*
* It can be therefore seen as a linear sequence of trees.
*/
sealed trait Tree[T] {
/** Numbers of node in the tree
*/
@pure
@opaque
def size: BigInt = {
decreases(this)
this match {
case Endpoint() => BigInt(0)
case ArticulationNode(l, r) => l.size + r.size
case ContentNode(n, sub) => sub.size + 1
}
}.ensuring(res =>
res >= 0 &&
((res == 0) ==> (this == Endpoint[T]()))
)
/** Whether the tree contains every node at most once
*/
@pure
@opaque
def isUnique: Boolean = {
decreases(this)
this match {
case Endpoint() => true
case ArticulationNode(l, r) => l.isUnique && r.isUnique && l.content.disjoint(r.content)
case ContentNode(n, sub) => sub.isUnique && !sub.contains(n)
}
}
/** Set of nodes
*/
@pure @opaque
def content: Set[T] = {
decreases(this)
this match {
case Endpoint() => Set.empty[T]
case ArticulationNode(l, r) => l.content ++ r.content
case ContentNode(n, sub) => sub.content + n
}
}
/** Checks if the tree contains a node
*/
@pure
def contains(e: T): Boolean = {
decreases(this)
unfold(content)
this match {
case ArticulationNode(l, r) =>
SetProperties.unionContains(l.content, r.content, e)
l.contains(e) || r.contains(e)
case Endpoint() =>
SetProperties.emptyContains(e)
false
case ContentNode(n, sub) =>
SetProperties.inclContains(sub.content, n, e)
sub.contains(e) || (e == n)
}
}.ensuring(res => (res == content.contains(e)))
/** Inorder traversal where each node is visited twice. When entering a node we apply a given function and when exiting
* the node we apply an other function. While doing this we update a state and return it at the end of the traversal.
* @param init The initial state of the traversal
* @param f1 The function that is applied everytime we visit a node for the first time (i.e. we are entering it)
* @param f2 The function that is applied everytime we visit a node for the second time (i.e. we are exiting it)
*/
@pure @opaque
def traverse[Z](init: Z, f1: (Z, T) => Z, f2: (Z, T) => Z): Z = {
decreases(this)
unfold(size)
this match {
case ArticulationNode(l, r) =>
r.traverse(l.traverse(init, f1, f2), f1, f2)
case Endpoint() => init
case ContentNode(n, sub) => f2(sub.traverse(f1(init, n), f1, f2), n)
}
}.ensuring(res => (size == 0) ==> (res == init))
/** In order traversal where each node is visited twice. When entering a node we apply a given function and when exiting
* the node we apply an other function. While doing this we update a state and return a list of triple whose entries
* are:
* - Each intermediate state
* - The node we have visited at each step
* - The traversal direction of the step, i.e. if that's the first or the second time we are visiting it
*
* @param init The initial state of the traversal
* @param f1 The function that is applied everytime we visit a node for the first time (i.e. we are entering it)
* @param f2 The function that is applied everytime we visit a node for the second time (i.e. we are exiting it)
*/
@pure
@opaque
def scan[Z](init: Z, f1: (Z, T) => Z, f2: (Z, T) => Z): List[(Z, T, TraversalDirection)] = {
decreases(this)
unfold(size)
this match {
case ArticulationNode(l, r) =>
concatIndex(l.scan(init, f1, f2), r.scan(l.traverse(init, f1, f2), f1, f2), 2 * size - 1)
l.scan(init, f1, f2) ++ r.scan(l.traverse(init, f1, f2), f1, f2)
case Endpoint() => Nil[(Z, T, TraversalDirection)]()
case ContentNode(n, sub) =>
concatIndex(
sub.scan(f1(init, n), f1, f2),
List((sub.traverse(f1(init, n), f1, f2), n, TraversalDirection.Up)),
2 * size - 2,
)
(init, n, TraversalDirection.Down) :: (sub.scan(f1(init, n), f1, f2) ++ List(
(sub.traverse(f1(init, n), f1, f2), n, TraversalDirection.Up)
))
}
}.ensuring(res =>
(res.size == 2 * size) &&
((size > 0) ==> (res(2 * size - 1)._3 == TraversalDirection.Up))
)
}
sealed trait StructuralNode[T] extends Tree[T]
case class ArticulationNode[T](left: ContentNode[T], right: StructuralNode[T])
extends StructuralNode[T]
case class Endpoint[T]() extends StructuralNode[T]
case class ContentNode[T](nodeContent: T, sub: StructuralNode[T]) extends Tree[T]
/** Trait describing if the node of a tree is being visited for the first time (Down) or the second time (Up)
*/
sealed trait TraversalDirection
object TraversalDirection {
case object Up extends TraversalDirection
case object Down extends TraversalDirection
}
object TreeProperties {
/** Express an intermediate state of a tree traversal in function of the one of the subtree when the tree is a [[ContentNode]]
*
* @param n The node of the content tree
* @param sub The subtree of the content tree
* @param init The initial state of the traversal
* @param f1 The function that is used when visiting the nodes for the first time
* @param f2 The function that is used when visiting the nodes for the second time
* @param i The step number of the intermediate state
*/
@pure @opaque
def scanIndexing[T, Z](
n: T,
sub: StructuralNode[T],
init: Z,
f1: (Z, T) => Z,
f2: (Z, T) => Z,
i: BigInt,
): Unit = {
require(i >= 0)
require(i < 2 * ContentNode(n, sub).size)
unfold(ContentNode(n, sub).size)
unfold(ContentNode(n, sub).scan(init, f1, f2))
if (i != 0) {
concatIndex(
sub.scan(f1(init, n), f1, f2),
List((sub.traverse(f1(init, n), f1, f2), n, TraversalDirection.Up)),
i - 1,
)
}
}.ensuring(
ContentNode(n, sub).scan(init, f1, f2)(i) ==
(
if (i == BigInt(0)) (init, n, TraversalDirection.Down)
else if (i == 2 * (ContentNode(n, sub).size) - 1)
(sub.traverse(f1(init, n), f1, f2), n, TraversalDirection.Up)
else (sub.scan(f1(init, n), f1, f2))(i - 1)
)
)
/** Express an intermediate state of a tree traversal in function of the one of the left or the right subtree
* when the tree is am [[ArticulationNode]]
*
* @param l The left subtree
* @param r The right subtree
* @param init The initial state of the traversal
* @param f1 The function that is used when visiting the nodes for the first time
* @param f2 The function that is used when visiting the nodes for the second time
* @param i The step number of the intermediate state
*/
@pure
@opaque
def scanIndexing[T, Z](
l: ContentNode[T],
r: StructuralNode[T],
init: Z,
f1: (Z, T) => Z,
f2: (Z, T) => Z,
i: BigInt,
): Unit = {
require(i >= 0)
require(i < 2 * ArticulationNode(l, r).size)
unfold(ArticulationNode(l, r).size)
unfold(ArticulationNode(l, r).scan(init, f1, f2))
concatIndex(l.scan(init, f1, f2), r.scan(l.traverse(init, f1, f2), f1, f2), i)
}.ensuring(
ArticulationNode(l, r).scan(init, f1, f2)(i) ==
(
if (i < 2 * l.size) l.scan(init, f1, f2)(i)
else r.scan(l.traverse(init, f1, f2), f1, f2)(i - 2 * l.size)
)
)
/** Express an intermediate state of a tree traversal in function of the one before
*
* @param n The node of the content tree
* @param sub The subtree of the content tree
* @param init The initial state of the traversal
* @param init The initial state of the traversal
* @param f1 The function that is used when visiting the nodes for the first time
* @param f2 The function that is used when visiting the nodes for the second time
* @param i The step number of the intermediate state
*/
@pure @opaque
def scanIndexingState[T, Z](
tr: Tree[T],
init: Z,
f1: (Z, T) => Z,
f2: (Z, T) => Z,
i: BigInt,
): Unit = {
decreases(tr)
require(i >= 0)
require(i < 2 * tr.size)
require(tr.size > 0)
unfold(tr.scan(init, f1, f2))
unfold(tr.traverse(init, f1, f2))
unfold(tr.size)
tr match {
case Endpoint() => Trivial()
case ContentNode(n, sub) =>
scanIndexing(n, sub, init, f1, f2, i)
scanIndexing(n, sub, init, f1, f2, 2 * tr.size - 1)
if (i == 0) {
Trivial()
} else if (i == 2 * tr.size - 1) {
if (sub.size > 0) {
scanIndexingState(sub, f1(init, n), f1, f2, 0)
scanIndexing(n, sub, init, f1, f2, i - 1)
}
} else {
scanIndexingState(sub, f1(init, n), f1, f2, i - 1)
scanIndexing(n, sub, init, f1, f2, i - 1)
}
case ArticulationNode(le, ri) =>
scanIndexing(le, ri, init, f1, f2, 2 * tr.size - 1)
scanIndexingState(le, init, f1, f2, 0) // traverse
if (ri.size == 0) {
scanIndexing(le, ri, init, f1, f2, 2 * le.size - 1)
} else {
scanIndexingState(ri, le.traverse(init, f1, f2), f1, f2, 0) // traverse
}
scanIndexing(le, ri, init, f1, f2, i)
if (i == 0) {
scanIndexingState(le, init, f1, f2, i)
} else {
scanIndexing(le, ri, init, f1, f2, i - 1)
if (i < 2 * le.size) {
scanIndexingState(le, init, f1, f2, i)
} else {
scanIndexingState(ri, le.traverse(init, f1, f2), f1, f2, i - 2 * le.size)
scanIndexing(le, ri, init, f1, f2, 2 * le.size - 1)
}
}
}
}.ensuring(
(tr.scan(init, f1, f2)(i)._1 == (
if (i == 0) init
else if (tr.scan(init, f1, f2)(i - 1)._3 == TraversalDirection.Down) {
f1(tr.scan(init, f1, f2)(i - 1)._1, tr.scan(init, f1, f2)(i - 1)._2)
} else {
f2(tr.scan(init, f1, f2)(i - 1)._1, tr.scan(init, f1, f2)(i - 1)._2)
}
)) &&
(tr.traverse(init, f1, f2) == f2(
tr.scan(init, f1, f2)(2 * tr.size - 1)._1,
tr.scan(init, f1, f2)(2 * tr.size - 1)._2,
))
)
/** The nodes and the directions of traversal are only dependent of the tree. That is they are independent of the initial
* state and of which functions are used to traverse it.
*
* @param tr The tree that is being traversed
* @param init1 The initial state of the first traversal
* @param init2 The initial state of the second traversal
* @param f11 The functions that is used when visiting the nodes for the first time in the first traversal
* @param f12 The functions that is used when visiting the nodes for the secondS time in the first traversal
* @param f21 The functions that is used when visiting the nodes for the first time in the second traversal
* @param f22 The functions that is used when visiting the nodes for the second time in the second traversal
* @param i The place in which the node appears
*/
@pure
@opaque
def scanIndexingNode[T, Z1, Z2](
tr: Tree[T],
init1: Z1,
init2: Z2,
f11: (Z1, T) => Z1,
f12: (Z1, T) => Z1,
f21: (Z2, T) => Z2,
f22: (Z2, T) => Z2,
i: BigInt,
): Unit = {
decreases(tr)
require(i >= 0)
require(i < 2 * tr.size)
unfold(tr.scan(init1, f11, f12))
unfold(tr.scan(init2, f21, f22))
unfold(tr.size)
tr match {
case Endpoint() => Trivial()
case ContentNode(n, sub) =>
scanIndexing(n, sub, init1, f11, f12, i)
scanIndexing(n, sub, init2, f21, f22, i)
if ((i == 0) || (i == 2 * tr.size - 1)) {
Trivial()
} else {
scanIndexingNode(sub, f11(init1, n), f21(init2, n), f11, f12, f21, f22, i - 1)
}
case ArticulationNode(l, r) =>
scanIndexing(l, r, init1, f11, f12, i)
scanIndexing(l, r, init2, f21, f22, i)
if (i < 2 * l.size) {
scanIndexingNode(l, init1, init2, f11, f12, f21, f22, i)
} else {
scanIndexingNode(
r,
l.traverse(init1, f11, f12),
l.traverse(init2, f21, f22),
f11,
f12,
f21,
f22,
i - 2 * l.size,
)
}
}
}.ensuring(
(tr.scan(init1, f11, f12)(i)._2 == tr.scan(init2, f21, f22)(i)._2) &&
(tr.scan(init1, f11, f12)(i)._3 == tr.scan(init2, f21, f22)(i)._3)
)
/** If an intermediate state of a tree traversal does not satisfy a property but the initial state does, then there
* is an intermediate state before that does satisfy this property but whose the next one does not.
*
* @param tr The tree that is being traversed
* @param init The initial state of the traversal
* @param f1 The function that is used when visiting the nodes for the first time
* @param f2 The function that is used when visiting the nodes for the second time
* @param p The propery that is fulfilled by the initial state but not the intermediate one
* @param i The step number of the state that does not satisfy p
*/
@pure
@opaque
def scanNotProp[T, Z](
tr: Tree[T],
init: Z,
f1: (Z, T) => Z,
f2: (Z, T) => Z,
p: Z => Boolean,
i: BigInt,
): BigInt = {
decreases(i)
require(i >= 0)
require(i < 2 * tr.size)
require(p(init))
require(!p(tr.scan(init, f1, f2)(i)._1))
if (i == 0) {
scanIndexingState(tr, init, f1, f2, 0)
Unreachable()
} else if (p(tr.scan(init, f1, f2)(i - 1)._1)) {
i - 1
} else {
scanNotProp(tr, init, f1, f2, p, i - 1)
}
}.ensuring(j =>
j >= 0 && j < i && p(tr.scan(init, f1, f2)(j)._1) && !p(tr.scan(init, f1, f2)(j + 1)._1)
)
/** If an intermediate state of a tree traversal does not satisfy a property but the final state does, then there
* is an intermediate state after that one that does not satisfy this property but whose the next one does.
*
* @param tr The tree that is being traversed
* @param init The initial state of the traversal
* @param f1 The function that is used when visiting the nodes for the first time
* @param f2 The function that is used when visiting the nodes for the second time
* @param p The propery that is fulfilled by the final state but not the intermediate one
* @param i The step number of the state that does not satisfy p
*/
@pure
@opaque
def scanNotPropRev[T, Z](
tr: Tree[T],
init: Z,
f1: (Z, T) => Z,
f2: (Z, T) => Z,
p: Z => Boolean,
i: BigInt,
): BigInt = {
decreases(2 * tr.size - i)
require(i >= 0)
require(i < 2 * tr.size)
require(p(tr.traverse(init, f1, f2)))
require(!p(tr.scan(init, f1, f2)(i)._1))
scanIndexingState(tr, init, f1, f2, i)
if (i == 2 * tr.size - 1) {
i
} else if (p(tr.scan(init, f1, f2)(i + 1)._1)) {
i
} else {
scanNotPropRev(tr, init, f1, f2, p, i + 1)
}
}.ensuring(j =>
(j >= i && j < 2 * tr.size - 1 && !p(tr.scan(init, f1, f2)(j)._1) && p(
tr.scan(init, f1, f2)(j + 1)._1
)) ||
((j == 2 * tr.size - 1) && !p(tr.scan(init, f1, f2)(j)._1) && p(tr.traverse(init, f1, f2)))
)
/** If the state obtained after traversing a tree does not satisfy a property but the initial state does, then there
* is an intermediate state of the traversal such that it does satisfy this property but the next one does not.
*
* @param tr The tree that is being traversed
* @param init The initial state of the traversal
* @param f1 The function that is used when visiting the nodes for the first time
* @param f2 The function that is used when visiting the nodes for the second time
* @param p The propery that is fulfilled by the initial state but not the final one
*/
@pure
@opaque
def traverseNotProp[T, Z](
tr: Tree[T],
init: Z,
f1: (Z, T) => Z,
f2: (Z, T) => Z,
p: Z => Boolean,
): BigInt = {
require(p(init))
require(!p(tr.traverse(init, f1, f2)))
scanIndexingState(tr, init, f1, f2, 0)
if (p(tr.scan(init, f1, f2)(2 * tr.size - 1)._1)) {
2 * tr.size - 1
} else {
scanNotProp(tr, init, f1, f2, p, 2 * tr.size - 1)
}
}.ensuring(i =>
i >= 0 && ((i < 2 * tr.size - 1 && p(tr.scan(init, f1, f2)(i)._1) && !p(
tr.scan(init, f1, f2)(i + 1)._1
))
|| (i == 2 * tr.size - 1 && p(tr.scan(init, f1, f2)(i)._1)))
)
/** If a node appears in a tree traversal then the tree contains it.
*
* @param tr The tree that is being traversed
* @param init The initial state of the traversal
* @param f1 The function that is used when visiting the nodes for the first time
* @param f2 The function that is used when visiting the nodes for the second time
* @param i The step during which the node appears
*/
@pure @opaque
def scanContains[T, Z](
tr: Tree[T],
init: Z,
f1: (Z, T) => Z,
f2: (Z, T) => Z,
i: BigInt,
): Unit = {
decreases(tr)
require(0 <= i)
require(i < 2 * tr.size)
unfold(tr.size)
unfold(tr.contains(tr.scan(init, f1, f2)(i)._2))
tr match {
case Endpoint() => Unreachable()
case ContentNode(n, sub) =>
scanIndexing(n, sub, init, f1, f2, i)
if (i > 0 && i < 2 * tr.size - 1) {
scanContains(sub, f1(init, n), f1, f2, i - 1)
}
case ArticulationNode(l, r) =>
scanIndexing(l, r, init, f1, f2, i)
if (i < 2 * l.size) {
scanContains(l, init, f1, f2, i)
} else {
scanContains(r, l.traverse(init, f1, f2), f1, f2, i - 2 * l.size)
}
}
}.ensuring(tr.contains(tr.scan(init, f1, f2)(i)._2))
/** If a tree is unique and a node is visited at two locations in the same [[TraversalDirection]], then those two locations
* are the same.
*
* @param tr The tree that is being traversed
* @param init The initial state of the traversal
* @param f1 The function that is used when visiting the nodes for the first time
* @param f2 The function that is used when visiting the nodes for the second time
* @param i The first locationof the node
* @param j The second location of the node
*/
@pure @opaque
def isUniqueIndexing[T, Z](
tr: Tree[T],
init: Z,
f1: (Z, T) => Z,
f2: (Z, T) => Z,
i: BigInt,
j: BigInt,
): Unit = {
decreases(tr)
require(tr.isUnique)
require(0 <= i)
require(i < 2 * tr.size)
require(0 <= j)
require(j < 2 * tr.size)
require(tr.scan(init, f1, f2)(i)._2 == tr.scan(init, f1, f2)(j)._2)
require(tr.scan(init, f1, f2)(i)._3 == tr.scan(init, f1, f2)(j)._3)
unfold(tr.size)
unfold(tr.isUnique)
tr match {
case Endpoint() => Unreachable()
case ContentNode(n, sub) =>
scanIndexing(n, sub, init, f1, f2, i)
scanIndexing(n, sub, init, f1, f2, j)
if ((i == 0) && ((j == 0) || (j == 2 * tr.size - 1))) {
Trivial()
} else if ((i == 2 * tr.size - 1) && ((j == 0) || (j == 2 * tr.size - 1))) {
Trivial()
} else if ((i == 0) || (i == 2 * tr.size - 1)) {
scanContains(sub, f1(init, n), f1, f2, j - 1)
} else if ((j == 0) || (j == 2 * tr.size - 1)) {
scanContains(sub, f1(init, n), f1, f2, i - 1)
} else {
isUniqueIndexing(sub, f1(init, n), f1, f2, i - 1, j - 1)
}
case ArticulationNode(l, r) =>
scanIndexing(l, r, init, f1, f2, i)
scanIndexing(l, r, init, f1, f2, j)
if ((i < 2 * l.size) && (j < 2 * l.size)) {
isUniqueIndexing(l, init, f1, f2, i, j)
} else if ((i >= 2 * l.size) && (j >= 2 * l.size)) {
isUniqueIndexing(r, l.traverse(init, f1, f2), f1, f2, i - 2 * l.size, j - 2 * l.size)
} else if (i < 2 * l.size) {
scanContains(l, init, f1, f2, i)
scanContains(r, l.traverse(init, f1, f2), f1, f2, j - 2 * l.size)
disjointContains(l.content, r.content, tr.scan(init, f1, f2)(i)._2)
disjointContains(l.content, r.content, tr.scan(init, f1, f2)(j)._2)
} else {
scanContains(l, init, f1, f2, j)
scanContains(r, l.traverse(init, f1, f2), f1, f2, i - 2 * l.size)
disjointContains(l.content, r.content, tr.scan(init, f1, f2)(j)._2)
disjointContains(l.content, r.content, tr.scan(init, f1, f2)(i)._2)
}
}
}.ensuring(i == j)
/** Given a node that has been visited for the second time in a traversal, returns when it has been visited for the
* first time.
* @param tr The tree that is being traversed
* @param init The initial state of the traversal
* @param f1 The function that is used when visiting the nodes for the first time
* @param f2 The function that is used when visiting the nodes for the second time
* @param i The step number during whch the node is visited for the second time.
*/
@pure @opaque
def findDown[T, Z](tr: Tree[T], init: Z, f1: (Z, T) => Z, f2: (Z, T) => Z, i: BigInt): BigInt = {
decreases(tr)
require(i >= 0)
require(i < 2 * tr.size)
require(tr.scan(init, f1, f2)(i)._3 == TraversalDirection.Up)
unfold(tr.scan(init, f1, f2))
unfold(tr.size)
tr match {
case Endpoint() => Unreachable()
case ContentNode(c, sub) =>
scanIndexing(c, sub, init, f1, f2, i)
if (i == 2 * tr.size - 1) {
scanIndexing(c, sub, init, f1, f2, 0)
BigInt(0)
} else {
val j = findDown(sub, f1(init, c), f1, f2, i - 1)
scanIndexing(c, sub, init, f1, f2, j + 1)
j + 1
}
case ArticulationNode(l, r) =>
scanIndexing(l, r, init, f1, f2, i)
if (i < 2 * l.size) {
val j = findDown(l, init, f1, f2, i)
scanIndexing(l, r, init, f1, f2, j)
j
} else {
val j = findDown(r, l.traverse(init, f1, f2), f1, f2, i - 2 * l.size)
scanIndexing(l, r, init, f1, f2, j + 2 * l.size)
j + 2 * l.size
}
}
}.ensuring(j =>
(j < i) &&
(tr.scan(init, f1, f2)(j)._3 == TraversalDirection.Down) &&
(tr.scan(init, f1, f2)(i)._2 == tr.scan(init, f1, f2)(j)._2)
)
}

14
daml-lf/verification/utils/Value.scala Normal file
View File

@ -0,0 +1,14 @@
// Copyright (c) 2023 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
// SPDX-License-Identifier: Apache-2.0
package lf.verified
package utils
import stainless.lang._
import stainless.annotation._
import stainless.proof._
import stainless.collection._
object Value {
case class ContractId(coid: String)
}