convert store cell to list

Pi-Squared-Inc · Sep 6, 2024 · 8dad932 · 8dad932
1 parent eea9f8c
commit 8dad932
Show file tree

Hide file tree

Showing 4 changed files with 37 additions and 37 deletions.
diff --git a/src/expression.md b/src/expression.md
@@ -13,7 +13,7 @@ module SOLIDITY-EXPRESSION
        <this> THIS => ADDR </this>
        <this-type> TYPE => X </this-type>
        <env> E => .Map </env>
-       <store> S => .Map </store>
+       <store> S => .List </store>
        <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
        <contract-id> X </contract-id>
        <contract-init> INIT </contract-init>
@@ -38,7 +38,7 @@ module SOLIDITY-EXPRESSION
        <this> THIS => ADDR </this>
        <this-type> TYPE => X </this-type>
        <env> E => .Map </env>
-       <store> S => .Map </store>
+       <store> S => .List </store>
        <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
        <contract-id> X </contract-id>
        <contract-init> INIT </contract-init>
@@ -53,10 +53,10 @@ module SOLIDITY-EXPRESSION
        <next-address> ADDR => ADDR +MInt 1p160 </next-address>
 
   // new array
-  rule <k> new T[](Len:Int) => lv(!I:Int, .List, T[]) ...</k>
-       <store> S => S [ !I:Int <- makeList(Len, default(T)) ] </store>
-  rule <k> new T[](v(Len:MInt{256}, _)) => lv(!I:Int, .List, T[]) ...</k>
-       <store> S => S [ !I:Int <- makeList(MInt2Unsigned(Len), default(T)) ] </store>
+  rule <k> new T[](Len:Int) => lv(size(S), .List, T[]) ...</k>
+       <store> S => S ListItem(makeList(Len, default(T))) </store>
+  rule <k> new T[](v(Len:MInt{256}, _)) => lv(size(S), .List, T[]) ...</k>
+       <store> S => S ListItem(makeList(MInt2Unsigned(Len), default(T))) </store>
 
   // literal assignment to state variable
   rule <k> X:Id = N:Int => X = v(convert(N, LT), LT) ...</k>
@@ -139,7 +139,7 @@ module SOLIDITY-EXPRESSION
   // local variable lookup
   rule <k> X:Id => v(V, T) ...</k>
        <env>... X |-> var(I, T) ...</env>
-       <store>... I |-> V ...</store>
+       <store> _ [ I <- V ] </store>
     requires notBool isAggregateType(T)
 
   rule <k> X:Id => lv(I, .List, T) ...</k>
@@ -150,10 +150,10 @@ module SOLIDITY-EXPRESSION
   context HOLE:Expression [ _:Expression ]
   context _:Expression [ HOLE:Expression ]
   rule <k> lv(I:Int, L, T []) [ Idx:Int ] => v(read(V, L ListItem(Idx), T[]), T) ...</k>
-       <store>... I |-> V ...</store>
+       <store> _ [ I <- V ] </store>
     requires notBool isAggregateType(T)
   rule <k> lv(I:Int, L, T []) [ v(Idx:MInt{256}, _) ] => v(read(V, L ListItem(MInt2Unsigned(Idx)), T[]), T) ...</k>
-       <store>... I |-> V ...</store>
+       <store> _ [ I <- V ] </store>
     requires notBool isAggregateType(T)
   rule <k> lv(X:Id, L, mapping(T1:ElementaryTypeName _ => T2)) [ v(Key, RT) ] => v(read({S [ X ] orDefault .Map}:>Value, L ListItem(convert(Key, RT, T1)), T), T2) ...</k>
        <this> THIS </this>
@@ -180,7 +180,7 @@ module SOLIDITY-EXPRESSION
   syntax Id ::= "length" [token]
   context HOLE . length
   rule <k> lv(I:Int, .List, T) . length => v(Int2MInt(size({read(V, .List, T)}:>List))::MInt{256}, uint) ...</k>
-       <store>... I |-> V ...</store>
+       <store> _ [ I <- V ] </store>
 
   // external call
   context HOLE . _ ( _:CallArgumentList )
@@ -191,7 +191,7 @@ module SOLIDITY-EXPRESSION
        <this> THIS => ADDR </this>
        <this-type> TYPE => TYPE' </this-type>
        <env> E => .Map </env>
-       <store> S => .Map </store>
+       <store> S => .List </store>
        <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
        <contract-id> TYPE' </contract-id>
        <contract-fn-id> F </contract-fn-id>
@@ -216,7 +216,7 @@ module SOLIDITY-EXPRESSION
        <this> THIS => ADDR </this>
        <this-type> TYPE => TYPE' </this-type>
        <env> E => .Map </env>
-       <store> S => .Map </store>
+       <store> S => .List </store>
        <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
        <contract-id> TYPE' </contract-id>
        <contract-fn-id> F </contract-fn-id>
@@ -310,10 +310,10 @@ module SOLIDITY-EXPRESSION
   // local increment and decrement
   rule <k> X:Id ++ => v(V, T) ...</k>
        <env>... X |-> var(I, T) ...</env>
-       <store>... I |-> (V => add(V, convert(1, T))) ...</store>
+       <store> _ [ I <- (V => add(V, convert(1, T))) ] </store>
   rule <k> X:Id -- => v(V, T) ...</k>
        <env>... X |-> var(I, T) ...</env>
-       <store>... I |-> (V => sub(V, convert(1, T))) ...</store>
+       <store> _ [ I <- (V => sub(V, convert(1, T))) ] </store>
 
   // equality and inequality
   rule v(V1:Value, T) == v(V2:Value, T) => v(eq(V1, V2), bool)
@@ -384,19 +384,19 @@ module SOLIDITY-EXPRESSION
 
   syntax KItem ::= var(Int, TypeName)
 
-  syntax KItem ::= bind(Map, List, List, CallArgumentList, List, List)
+  syntax KItem ::= bind(List, List, List, CallArgumentList, List, List)
   rule bind(_, .List, .List, .CallArgumentList, .List, .List) => .K
   rule bind(STORE, ListItem(noId) PARAMS, ListItem(_) TYPES, _, ARGS, L1:List, L2:List) => bind(STORE, PARAMS, TYPES, ARGS, L1, L2)
   rule bind(STORE, .List, .List, .CallArgumentList, ListItem(_) TYPES, ListItem(noId) NAMES) => bind(STORE, .List, .List, .CallArgumentList, TYPES, NAMES)
   rule <k> bind(STORE, ListItem(X:Id) PARAMS, ListItem(T:TypeName) TYPES, lv(I:Int, .List, T:TypeName), ARGS, L1:List, L2:List) => bind(STORE, PARAMS, TYPES, ARGS, L1, L2) ...</k>
-       <env> E => E [ X <- var(!I:Int, T) ] </env>
-       <store> S => S [ !I <- STORE [ I ] ] </store>
+       <env> E => E [ X <- var(size(S), T) ] </env>
+       <store> S => S ListItem(STORE [ I ]) </store>
   rule <k> bind(STORE, ListItem(X:Id) PARAMS, ListItem(LT:TypeName) TYPES, v(V:Value, RT:TypeName), ARGS, L1:List, L2:List) => bind(STORE, PARAMS, TYPES, ARGS, L1, L2) ...</k>
-       <env> E => E [ X <- var(!I:Int, LT) ] </env>
-       <store> S => S [ !I <- convert(V, RT, LT) ] </store>
+       <env> E => E [ X <- var(size(S), LT) ] </env>
+       <store> S => S ListItem(convert(V, RT, LT)) </store>
   rule <k> bind(STORE, .List, .List, .CallArgumentList, ListItem(LT:TypeName) TYPES, ListItem(X:Id) NAMES) => bind(STORE, .List, .List, .CallArgumentList, TYPES, NAMES) ...</k>
-       <env> E => E [ X <- var(!I:Int, LT) ] </env>
-       <store> S => S [ !I <- default(LT) ] </store>
+       <env> E => E [ X <- var(size(S), LT) ] </env>
+       <store> S => S ListItem(default(LT)) </store>
 
   syntax Value ::= convert(Value, from: TypeName, to: TypeName) [function]
   rule convert(V, T, T) => V

diff --git a/src/solidity.md b/src/solidity.md
@@ -67,7 +67,7 @@ module SOLIDITY-CONFIGURATION
         <this> 0p160 </this>
         <this-type> Id </this-type>
         <env> .Map </env>
-        <store> .Map </store>
+        <store> .List </store>
         <call-stack> .List </call-stack>
         <live-contracts>
           <live-contract multiplicity="*" type="Map">
@@ -163,7 +163,7 @@ module SOLIDITY-DATA
   rule isAggregateType(_) => false [owise]
 
   // external frame
-  syntax Frame ::= frame(continuation: K, env: Map, store: Map, from: MInt{160}, type: Id, value: MInt{256})
+  syntax Frame ::= frame(continuation: K, env: Map, store: List, from: MInt{160}, type: Id, value: MInt{256})
   // internal frame
                  | frame(continuation: K, env: Map)
   syntax Event ::= event(name: Id, args: TypedVals)

diff --git a/src/statement.md b/src/statement.md
@@ -29,27 +29,27 @@ module SOLIDITY-STATEMENT
        <call-stack>... ListItem(frame(K, E, S, FROM, TYPE, VALUE)) => .List </call-stack>
 
   rule <k> return lv(I:Int, .List, T) ; => return v(L, T) ; ...</k>
-       <store>... I |-> L ...</store>
+       <store> _ [ I <- L ] </store>
 
   rule <k> return V:TypedVal ; ~> _ => V ~> K </k>
        <env> _ => E </env>
        <call-stack>... ListItem(frame(K, E)) => .List </call-stack>
 
   // variable declaration
   rule <k> LT:TypeName X:Id = v(V, RT) ; => .K ...</k>
-       <env> E => E [ X <- var(!I:Int, LT) ] </env>
-       <store> S => S [ !I <- convert(V, RT, LT) ] </store>
+       <env> E => E [ X <- var(size(S), LT) ] </env>
+       <store> S => S ListItem(convert(V, RT, LT)) </store>
   rule <k> LT:TypeName X:Id = N:Int ; => .K ...</k>
-       <env> E => E [ X <- var(!I:Int, LT) ] </env>
-       <store> S => S [ !I <- convert(N, LT) ] </store>
+       <env> E => E [ X <- var(size(S), LT) ] </env>
+       <store> S => S ListItem(convert(N, LT)) </store>
   rule <k> LT:TypeName memory X:Id = v(V, RT) ; => .K ...</k>
-       <env> E => E [ X <- var(!I:Int, LT) ] </env>
-       <store> S => S [ !I <- convert(V, RT, LT) ] </store>
+       <env> E => E [ X <- var(size(S), LT) ] </env>
+       <store> S => S ListItem(convert(V, RT, LT)) </store>
   rule <k> T:TypeName memory X:Id = lv(I:Int, .List, T) ; => .K ...</k>
        <env> E => E [ X <- var(I, T) ] </env>
   rule <k> T:TypeName X:Id ;::VariableDeclarationStatement => .K ...</k>
-       <env> E => E [ X <- var(!I:Int, T) ] </env>
-       <store> S => S [ !I <- default(T) ] </store>
+       <env> E => E [ X <- var(size(S), T) ] </env>
+       <store> S => S ListItem(default(T)) </store>
 
   // emit statement
   rule <k> emit X:Id ( ARGS ) ; => .K ...</k>

diff --git a/src/transaction.md b/src/transaction.md
@@ -7,15 +7,15 @@ module SOLIDITY-TRANSACTION
   imports INT
   imports private SOLIDITY-EXPRESSION
 
-  rule <k> create(FROM, VALUE, NOW, CTOR, ARGS) => bind(.Map, PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ...</k>
+  rule <k> create(FROM, VALUE, NOW, CTOR, ARGS) => bind(.List, PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ...</k>
        <msg-sender> _ => Int2MInt(Number2Int(FROM)) </msg-sender>
        <msg-value> _ => Int2MInt(Number2Int(VALUE)) </msg-value>
        <tx-origin> _ => Int2MInt(Number2Int(FROM)) </tx-origin>
        <block-timestamp> _ => Int2MInt(Number2Int(NOW)) </block-timestamp>
        <this> _ => ADDR </this>
        <this-type> _ => CTOR </this-type>
        <env> _ => .Map </env>
-       <store> _ => .Map </store>
+       <store> _ => .List </store>
        <contract-id> CTOR </contract-id>
        <contract-init> INIT </contract-init>
        <contract-fn-id> constructor </contract-fn-id>
@@ -41,7 +41,7 @@ module SOLIDITY-TRANSACTION
        <this> _ => ADDR </this>
        <this-type> _ => CTOR </this-type>
        <env> _ => .Map </env>
-       <store> _ => .Map </store>
+       <store> _ => .List </store>
        <contract-id> CTOR </contract-id>
        <contract-init> INIT </contract-init>
        <live-contracts>
@@ -58,15 +58,15 @@ module SOLIDITY-TRANSACTION
   syntax Transaction ::= txn(from: Decimal, to: MInt{160}, value: Decimal, timestamp: Decimal, func: Id, args: CallArgumentList) [strict(6)]
   rule txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => txn(FROM, Int2MInt(Number2Int(TO)), VALUE, NOW, FUNC, ARGS)
 
-  rule <k> txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => bind(.Map, PARAMS, TYPES, ARGS, .List, .List) ~> BODY ...</k>
+  rule <k> txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => bind(.List, PARAMS, TYPES, ARGS, .List, .List) ~> BODY ...</k>
        <msg-sender> _ => Int2MInt(Number2Int(FROM)) </msg-sender>
        <msg-value> _ => Int2MInt(Number2Int(VALUE)) </msg-value>
        <tx-origin> _ => Int2MInt(Number2Int(FROM)) </tx-origin>
        <block-timestamp> _ => Int2MInt(Number2Int(NOW)) </block-timestamp>
        <this> _ => TO </this>
        <this-type> _ => TYPE </this-type>
        <env> _ => .Map </env>
-       <store> _ => .Map </store>
+       <store> _ => .List </store>
        <live-contracts>
          <contract-address> TO </contract-address>
          <contract-type> TYPE </contract-type>