Skip to content

Commit

Permalink
Small fixes (#149)
Browse files Browse the repository at this point in the history
* Add labels for rules that change the call stack.

* Labels for symbols that work with the callstate

* Use < for adder comparisons instead of <=
  • Loading branch information
virgil-serbanuta authored Oct 3, 2023
1 parent ac1c286 commit 32108d9
Show file tree
Hide file tree
Showing 3 changed files with 13 additions and 10 deletions.
15 changes: 9 additions & 6 deletions elrond-node.md
Original file line number Diff line number Diff line change
Expand Up @@ -160,23 +160,26 @@ Storage maps byte arrays to byte arrays.
The `<callStack>` cell stores a list of previous contract execution states. These internal commands manages the callstack when calling and returning from a contract.

```k
syntax InternalCmd ::= "pushCallState"
syntax InternalCmd ::= "pushCallState" [klabel(pushCallState), symbol]
// ---------------------------------------
rule <commands> pushCallState => . ... </commands>
rule [pushCallState]:
<commands> pushCallState => . ... </commands>
<callStack> (.List => ListItem(CALLSTATE)) ... </callStack>
<callState> CALLSTATE </callState>
[priority(60)]
syntax InternalCmd ::= "popCallState"
syntax InternalCmd ::= "popCallState" [klabel(popCallState), symbol]
// --------------------------------------
rule <commands> popCallState => . ... </commands>
rule [popCallState]:
<commands> popCallState => . ... </commands>
<callStack> (ListItem(CALLSTATE) => .List) ... </callStack>
<callState> _ => CALLSTATE </callState>
[priority(60)]
syntax InternalCmd ::= "dropCallState"
syntax InternalCmd ::= "dropCallState" [klabel(dropCallState), symbol]
// ---------------------------------------
rule <commands> dropCallState => . ... </commands>
rule [dropCallState]:
<commands> dropCallState => . ... </commands>
<callStack> (ListItem(_) => .List) ... </callStack>
[priority(60)]
```
Expand Down
2 changes: 1 addition & 1 deletion foundry.md
Original file line number Diff line number Diff line change
Expand Up @@ -406,7 +406,7 @@ Only the `#foundryRunner` account can execute these commands/host functions.
<instrs> #assume(P) => #endFoundryImmediately ... </instrs>
requires P ==Int 0
syntax IternalInstr ::= "#endFoundryImmediately"
syntax InternalInstr ::= "#endFoundryImmediately"
[symbol, klabel(endFoundryImmediately)]
// ------------------------------------------------------
rule [endFoundryImmediately]:
Expand Down
6 changes: 3 additions & 3 deletions tests/contracts/foundrylike/src/test_adder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ pub trait TestAdder {
#[endpoint(test_call_add)]
fn test_call_add(&self, value: BigUint) {

testapi::assume(value <= 100u32);
testapi::assume(value < 100u32);

let adder = self.adder_address().get();

Expand All @@ -71,8 +71,8 @@ pub trait TestAdder {
#[endpoint(test_call_add_twice)]
fn test_call_add_twice(&self, value1: BigUint, value2: BigUint) {

testapi::assume(value1 <= 100u32);
testapi::assume(value2 <= 100u32);
testapi::assume(value1 < 100u32);
testapi::assume(value2 < 100u32);

let adder = self.adder_address().get();

Expand Down

0 comments on commit 32108d9

Please sign in to comment.