From 2e6c3a58fc19800fd3ee033209728fd402bc39ef Mon Sep 17 00:00:00 2001 From: redshiftzero Date: Mon, 4 Mar 2024 18:00:34 -0500 Subject: [PATCH] spec: output invariants --- docs/protocol/src/protocol/invariants.md | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/docs/protocol/src/protocol/invariants.md b/docs/protocol/src/protocol/invariants.md index 5c0cb0743d..67f7c5ab38 100644 --- a/docs/protocol/src/protocol/invariants.md +++ b/docs/protocol/src/protocol/invariants.md @@ -1,5 +1,5 @@ -# System-Level +# System-Level #### Invariants @@ -13,9 +13,22 @@ ## Action-Level -### Community Pool Output +### Output -#### Global Violations +#### Local Invariants + +1. The created output note is spendable by the recipient if its nullifier has not been revealed. +1.1 The output note is bound to the recipient. +1.2 The output note can be spent only by the recipient. + +#### Local Justification + +1.1 The note commitment binds the note to the typed value and the address of the recipient. +1.2 Each note has a unique note commitment if the note blinding factor is unique for duplicate (recipient, typed value) pairs. Duplicate note commitments are allowed on chain since they commit to the same (recipient, typed value) pair. + +#### Global Justification + +1.1 This action contributes the value of the output note, which is summed as part of the transaction value balance. Value is not created due to system level invariant 1, which ensures that transactions contribute a 0 value balance. ### Spend