Skip to content

Add compiler-level box verification util functions (closes #1037) - #1176

Open
Ergologica wants to merge 1 commit into
ergoplatform:masterfrom
Ergologica:feature/predef-verify-functions-1037
Open

Add compiler-level box verification util functions (closes #1037)#1176
Ergologica wants to merge 1 commit into
ergoplatform:masterfrom
Ergologica:feature/predef-verify-functions-1037

Conversation

@Ergologica

Copy link
Copy Markdown

Add compiler-level utility functions for common box verification patterns

Closes #1037

Summary

This PR adds the 6 utility functions proposed in #1037 as predefined global functions of the ErgoScript frontend (SigmaPredef.scala). Each function is expanded at compile time into ErgoTree nodes that are already supported by the interpreter, so no changes to the consensus-critical ErgoTree level (serializers, opcodes, evaluator, SigmaDsl) are involved — addressing the review feedback that led to closing #1086.

Function Expands to
verifySameForBasicRequiredRegisters(inBox: Box, outBox: Box): Boolean inBox.value == outBox.value && inBox.propositionBytes == outBox.propositionBytes
verifySameForRequiredRegisters(inBox: Box, outBox: Box): Boolean the above && inBox.tokens == outBox.tokens
verifyUsedAdditionalRegisters(box: Box, used: Int): Boolean (used >= 1 || box.R4[Any].isEmpty) && ... && (used >= 6 || box.R9[Any].isEmpty)
verifyBoxHasMarkerToken(box: Box, token: Coll[Byte]): Boolean box.tokens.exists { t => t._1 == token && t._2 >= 1L }
verifyBoxHasNoMarkerToken(box: Box, token: Coll[Byte]): Boolean box.tokens.forall { t => t._1 != token }
verifySpentToken(inBox: Box, outBox: Box, token: Coll[Byte], amount: Long): Boolean inBox.tokens.forall { it => if (it._1 == token) outBox.tokens.exists { ot => it._1 == ot._1 && it._2 == ot._2 + amount } else outBox.tokens.exists { ot => it._1 == ot._1 && it._2 == ot._2 } }

The semantics follow the reference implementations given in #1037 (uncurried argument lists are used, consistently with the other predefined global functions).

Implementation notes

  • All functions are registered in globalFuncs of PredefinedFuncRegistry and are expanded by the typer via the existing PredefinedFuncApply mechanism (PredefFuncInfo.irBuilder), like allOf, xorOf, etc.
  • The produced trees only use existing operations (EQ, BinAnd/BinOr (lazy), Exists/ForAll, ExtractAmount, ExtractScriptBytes, ExtractRegisterAs, MethodCall(Box.tokens), SelectField, If, ArithOp.Plus), so the resulting ErgoTree serializes and evaluates in all script versions.
  • verifyUsedAdditionalRegisters — one behavioral caveat, documented in the function's OperationInfo: the emptiness check is expressed as R{i}[Any].isEmpty (as in the issue's reference code). When a register beyond the first used ones is defined, Box.getReg[Any] throws InvalidType instead of returning Some(_), so the script evaluation fails rather than returning false. Used as a guarding predicate this is the desired outcome (the spending attempt is rejected), but the value cannot be negated/composed to recover from the failing branch. As far as I can tell, current ErgoTree has no type-agnostic "register is defined" primitive that could avoid this.
  • verifySpentToken follows the reference semantics literally: it requires the remainder ot._2 == it._2 - amount to be present in the output box, therefore spending a token completely (down to zero) yields false by design (covered by a test).

Testing

New UtilFunctionsSpecification (in sc/shared/src/test/scala/sigmastate/utxo/) with 20 properties run across script versions via CompilerCrossVersionProps. Each function is covered with positive and negative cases; every script is compiled, wrapped into an ErgoTree, proven and verified through ContextEnrichingTestProvingInterpreter / ErgoLikeTestInterpreter against a real spending context (SELF + OUTPUTS(0) with configurable values, tokens and registers). The ErgoTree serialization roundtrip is exercised implicitly by proving/verification.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

compiler level util functions

1 participant