Skip to content

Commit

Permalink
*.k: fix whitespace errors
Browse files Browse the repository at this point in the history
  • Loading branch information
Everett Hildenbrandt committed Nov 30, 2018
1 parent 28b083c commit 20abc5a
Show file tree
Hide file tree
Showing 6 changed files with 266 additions and 266 deletions.
92 changes: 46 additions & 46 deletions configuration.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,30 +10,30 @@ syntax START
configuration
<k> $PGM:START </k>
<exit-code exit=""> 0 </exit-code>
// ...
// ...

<ethereum>

// Solidity execution engine
// =========================
<solidity>

<solidity>

// Mutable during a single transaction
// -----------------------------------

<execEngine>
<output> .K </output>
<statusCode> .K </statusCode>
<callStack> .List </callStack>
<interimStates> .List </interimStates>
<touchedAccounts> .K </touchedAccounts>
<currentAccount> #account(-1, #Testing-Engine#) </currentAccount>
<result> .K </result>
<mode> .K </mode>
<result> .K </result>
<mode> .K </mode>

<callState>

// Should be loaded from <account>
<program> .K </program> // currently running <contract>

Expand All @@ -45,26 +45,26 @@ configuration

// \mu_*
// env: map from qualified name to either storage or local memory
// QName ::= Id | Id.Id /* struct member */ | ...
// QName ::= Id | Id.Id /* struct member */ | ...
// Reference ::= storage(Index, Offset) // Index, Offset are Word a.k.a. uint256
// | memory(Index, Offset)
<env> .Map </env> // Map of names to references

// tenv: map from qualified name to type
// where Type ::= uintXX ... | array | struct(members) | ...
<tenv> .Map </tenv> // Map names to types

// memory: same as evm!!
// exact allocation strategy may vary(unlike storage), but anyway semantics should be indentical
<localMem> .Map </localMem>
// Gas: not sure how, but I think we need it.
<localMem> .Map </localMem>

// Gas: not sure how, but I think we need it.
<gas> 0:Int </gas>
<memoryUsed> 0:Int </memoryUsed>
<previousGas> 0:Int </previousGas>

// Those are present in both KEVM and IELE.
// Not sure we need them, let's keep them around until figure it out.
// Those are present in both KEVM and IELE.
// Not sure we need them, let's keep them around until figure it out.
<static> false:Bool </static>
<callDepth> 0 </callDepth>

Expand All @@ -88,7 +88,7 @@ configuration
<origin> 0 </origin> // I_o

// I_H* (block information)
// Needed or not? It is part of KEEI, but not sure. Should discuss.
// Needed or not? It is part of KEEI, but not sure. Should discuss.
<block>
<hashes> .List </hashes>
<coinbase> 0 </coinbase> // H_c
Expand All @@ -99,40 +99,40 @@ configuration
<timestamp> 0 </timestamp> // H_s
</block>
</execEngine>
// This is the part of the "Solidity VM" where we keep the available contracts.

// This is the part of the "Solidity VM" where we keep the available contracts.
// Those are either obtained from source file (creation) or loaded from accounts (function call).

// When we parse Solidity source file we
// - desugar/preprocess modifiers, inheritance (?) etc.
// When we parse Solidity source file we
// - desugar/preprocess modifiers, inheritance (?) etc.
// - create one <contract> structure for each contract declared in the sources
// (let's not worry about those for now, and just stick to simple functions)

// From here, <contract>s can be either deployed or executed.
// When a contract is deployed we not only copy its <contract> cell into the <account>,
// but we also copy the other contracts that were present in the same source file,
// so that the deployed contract have access to them and can create and deploy them if needed.
// From here, <contract>s can be either deployed or executed.
// When a contract is deployed we not only copy its <contract> cell into the <account>,
// but we also copy the other contracts that were present in the same source file,
// so that the deployed contract have access to them and can create and deploy them if needed.
// (see the <account> cell below for more notes about this)

<contracts>
<Contract multiplicity = "*" type="Map">
<cname> .K </cname>

<functions>
<Function multiplicity="*" type="Map">
<fname> .K </fname>
<inputParams> .K </inputParams>
<inputParams> .K </inputParams>
<Returns> .K </Returns>
<quantifiers> .K </quantifiers>
<visibility> .K </visibility> // Visibility ::= public | privat
<body> .K </body>
</Function>
</functions>

<stateVar> .List </stateVar>
<Constructor> false </Constructor>
// ... more to be added later ...

</Contract>
</contracts>

Expand All @@ -147,31 +147,31 @@ configuration
// ---------------

<activeAccounts> .Set </activeAccounts>

// removed becuase we can get this number by size(activeAccounts).
//<numOfAccounts> 0:Int </numOfAccounts>

<accounts>
<account multiplicity="*" type="Map">

// Same as in KEVM / IELE

<acctID> .K </acctID>
<balance> 0 </balance>



// The <acctEnv> cell refers to the environment, mapping variable names to logical
// The <acctEnv> cell refers to the environment, mapping variable names to logical
// storage references. Actually, <acctEnv> is equivalent to the <env> cell in <execEngine>.

<acctEnv> .Map </acctEnv>
<acctEnv> .Map </acctEnv>

// When a contract is deployed, its <contract> data structure will be copied here.
// Because contracts can create other contracts (via "new") we need to also keep the
// Because contracts can create other contracts (via "new") we need to also keep the
// set of contract that this contract can create (i.e. the set of contracts that was
// available at creation time, like in IELE)

<code>
<code>
<associatedContract> .K </associatedContract> // contract deployed on this account
<availableContracts> .K </availableContracts> // contracts that can be created by this account's contract
</code>
Expand All @@ -182,11 +182,11 @@ configuration
// variable and I think these rules should be the part of Solidity semantics,
// so that the storage usage of solidity program and evm bytecode have
// the same effect on the storage.

<acctStorage> .Map </acctStorage>

// Q. Why include allocation rules in solidity semantics?
// A.
// A.
// * These rules are explained in the offical solidity docs
// https://solidity.readthedocs.io/en/v0.4.24/miscellaneous.html?highlight=pack#layout-of-state-variables-in-storage
// * AFAIK, allocation is not affected by optimization level.
Expand All @@ -196,7 +196,7 @@ configuration
//

<nonce> 0:Int </nonce>

</account>
</accounts>

Expand All @@ -207,8 +207,8 @@ configuration
<txPending> .List </txPending>

// Borrowed from IELE. Notice this is more high level than KEVM
// May need further tweaks, but that's the idea.
// May need further tweaks, but that's the idea.

<messages>
<message multiplicity="*">
<msgID> 0 </msgID> // Unique ID of transaction
Expand All @@ -220,7 +220,7 @@ configuration
<value> 0 </value> // Value in funds to transfer by transaction
<from> 0 </from> // Sender of transaction
<data> .K </data> // .WordStack Arguments to function called by transaction
<args> .K </args> //.Ints
<args> .K </args> //.Ints
</message>
</messages>

Expand Down
34 changes: 17 additions & 17 deletions contract.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,9 @@ rule [ContractDefinition]:
<k> contract C:Id { Cs:ContractParts } => #pcsContractParts(C,Cs) ... </k>
(.Bag =>
<Contract>
<cname> C </cname>
<functions> .Bag </functions>
<stateVar> .List </stateVar>
<cname> C </cname>
<functions> .Bag </functions>
<stateVar> .List </stateVar>
...
</Contract>
)
Expand All @@ -32,20 +32,20 @@ syntax SolidityItem

rule #pcsContractParts(Ct:Id, .ContractParts) => .
rule #pcsContractParts(Ct:Id, C:ContractPart Cs:ContractParts) =>
#pcsContractPart(Ct, C) ~> #pcsContractParts(Ct,Cs)
#pcsContractPart(Ct, C) ~> #pcsContractParts(Ct,Cs)

rule [StateVariableDeclaration]:
<k> #pcsContractPart(C:Id, T:TypeName F:FunQuantifiers V:Id;) =>
. ...</k>
. ...</k>
<Contract>
<cname> C </cname>
<stateVar> ... .List => ListItem(#varInfo(V, #undef_Value, T, #storage)) </stateVar>
...
</Contract>

rule
rule
<k> #pcsContractPart(C:Id, T:TypeName F:FunQuantifiers V:Id = E;) =>
. ...</k>
. ...</k>
<Contract>
<cname> C </cname>
<stateVar> ... .List => ListItem(#varInfo(V, E, T, #storage)) </stateVar>
Expand All @@ -61,7 +61,7 @@ rule
<currentAccount> #account(C:Int, CN:AccountId) </currentAccount>

syntax SolidityItem
::= #createStateVars(Int, Id, List)
::= #createStateVars(Int, Id, List)
| #exeConstructor(Id,Int,ExpressionList) [strict(3)]

rule [New-Contract-Instance]:
Expand All @@ -77,16 +77,16 @@ rule [New-Contract-Instance]:
...
(.Bag =>
<account>
<acctID> #account(size(AA),C) </acctID>
<balance> 0 </balance>
<acctID> #account(size(AA),C) </acctID>
<balance> 0 </balance>
<acctEnv> .Map </acctEnv>
<code>
<associatedContract> .K </associatedContract>
<availableContracts> .K </availableContracts>
<associatedContract> .K </associatedContract>
<availableContracts> .K </availableContracts>
</code>
<acctStorage> .Map </acctStorage>
<nonce> 0 </nonce>
...
<acctStorage> .Map </acctStorage>
<nonce> 0 </nonce>
...
</account>
)
</accounts>
Expand All @@ -95,15 +95,15 @@ rule #createStateVars(N:Int, CN:Id, ListItem(VInfo) L:List) => #allocate(N, CN,

rule #createStateVars(N:Int, CN:Id, .List) => .

rule
rule
<k> #exeConstructor(C:Id,N:Int,Es:Values) => functionCall(N;String2Id("constructor"); Es); ... </k>
<Contract>
<cname> C </cname>
<Constructor> true </Constructor>
...
</Contract>

rule
rule
<k> #exeConstructor(C:Id,N:Int,Es:Values) => . ... </k>
<Contract>
<cname> C </cname>
Expand Down
Loading

0 comments on commit 20abc5a

Please sign in to comment.