Skip to content

Commit

Permalink
Fix contract initialization
Browse files Browse the repository at this point in the history
  • Loading branch information
virgil-serbanuta committed Nov 4, 2024
1 parent 6a36e38 commit 9c2b363
Showing 1 changed file with 8 additions and 1 deletion.
9 changes: 8 additions & 1 deletion ulm-semantics/main/execution/dispatch.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,16 +10,18 @@ module ULM-EXECUTION-DISPATCH
imports private ULM-COMMON-TOOLS-SYNTAX
imports private ULM-EXECUTION-SYNTAX
imports private ULM-PREPROCESSING-CONFIGURATION
imports private ULM-SEMANTICS-HOOKS-STATE-CONFIGURATION
syntax UlmInstruction ::= ulmExecute(create: Bool, contract:Value, gas: ValueOrError)
| setContractOutput(Bytes)
rule
<k>
// TODO: For some reason, kompile rejects 'Create' as a variabler name below.
// Figure out why.
ulmExecute(Createy:Bool, Pgm:Bytes, _AccountId:Int, Gas:Int)
=> ulmExecute(Createy, struct(ContractTrait, .Map), integerToValue(Gas, u64))
~> #if Createy #then Pgm #else .K #fi
~> #if Createy #then setContractOutput(Pgm) #else .K #fi
...
</k>
<ulm-contract-trait>
Expand All @@ -38,6 +40,11 @@ module ULM-EXECUTION-DISPATCH
<values> Values:Map => Values[NVI <- Contract] </values>
<next-value-id> NVI:Int => NVI +Int 1 </next-value-id>
requires notBool NVI in_keys(Values)
rule
<k> _:PtrValue ~> setContractOutput(B:Bytes) => .K ... </k>
<ulm-output> _ => B </ulm-output>
endmodule
```

0 comments on commit 9c2b363

Please sign in to comment.