New storage format in compiled output by ElijahVlasov · Pull Request #63 · NethermindEth/horus-compile

ElijahVlasov · 2023-02-21T06:41:24Z

"storage_variables" field in the spec json contains storage variables with [arity, coarity] tuple
Any invocation of a storage variable member is translated into storage_name n ...args... where n is the deep index of the member

Warning: remove tracing code Warning: finish revising this commit messsage This commit makes changes to match the new `spec.json` format output by `horus-compile` in the following PR: NethermindEth/horus-compile#63 In particular, return types of storage variables which are `struct`s are flattened (deeply) into a tuple, and internally, we use an extra argument to index into this tuple. For example, the keys in the `storage_update` object in the `spec.json` file have been modified as follows: ```diff - "__main__.complex_var_1.s.x": [ + "__main__.complex_var_1 0": [ ``` The relevants bits of the source file are: ```cairo struct Point { x: felt, y: felt, } @storage_var func complex_var_1(arg: Uint256) -> (s: Point) { } ``` Note that instead of using dot-accessor notation, we use an index `0` to indicate the first member of the return tuple of `complex_var_1()`, which is identified with the field `x` of `Point`. In order to parse this index argument from the key in the JSON, as seen in the diff above, we change implicitly change the `FromJSON` of `FuncSpec`/`Storage`, and define `ScopedNameWithIdxArg` which is basically `"__main__.complex_var_1 0"`, as is obvious from its name. So instead of parsing a value of type `Storage` from the JSON, instead we parse a value of type `S +type Storage' = Map ScopedNameWithIdxArg [([Expr TFelt], Expr TFelt)] ``` ..... finish this later Miscellaneous changes ===================== * Update `display.sh` and `oneoff.sh` testing scripts. * Uncomment the command that cleans up temp files in `oneoff.sh`. * Add `FromJSON` instance for `ScopedNameWithIdxArg` * Add flattening example `ab.cairo` We use a `mergeFuncSpecs` function to nicely take the conjunction of the preconditions and postconditions, and take the union of the `Storage` maps.

Warning: remove tracing code This commit makes changes to match the new `spec.json` format output by `horus-compile` in the following PR: NethermindEth/horus-compile#63 In particular, return types of storage variables which are `struct`s are flattened (deeply) into a tuple, and internally, we use an extra argument to index into this tuple. Parsing the new JSON format =========================== For example, the keys in the `storage_update` object in the `spec.json` file have been modified as follows: ```diff - "__main__.complex_var_1.s.x": [ + "__main__.complex_var_1 0": [ ``` The relevants bits of the source file are: ```cairo struct Point { x: felt, y: felt, } @storage_var func complex_var_1(arg: Uint256) -> (s: Point) { } ``` Note that instead of using dot-accessor notation, we use an index `0` to indicate the first member of the return tuple of `complex_var_1()`, which is identified with the field `x` of `Point`. In order to parse this index argument from the key in the JSON, as seen in the diff above, we change implicitly change the `FromJSON` of `FuncSpec`/`Storage`, and define `ScopedNameWithIdxArg` which is basically `"__main__.complex_var_1 0"`, as is obvious from its name. So instead of parsing a value of type `Storage` from the JSON, we parse a value of type `Storage'`: ``` +type Storage' = Map ScopedNameWithIdxArg [([Expr TFelt], Expr TFelt)] ``` and then convert it to a map of type `Storage` with a `storage'ToStorage` function. Standard specs for `<storage>.read()` and `<storage>.write()` ============================================================= We refactor `storageVarsSpecs` heavily, folding over the `ContractDefinition` field: ```diff + , cd_storageVars :: Map ScopedName (Arity, Coarity) ``` which now includes the arity and coarity of each storage variable. In order to manage this, we add helper functions: ```diff +mkReadSpecs :: ScopedName -> (Int, Int) -> [(ScopedName, FuncSpec)] +mkWriteSpecs :: ScopedName -> (Int, Int) -> [(ScopedName, FuncSpec)] ``` which basically construct a separate `FuncSpec` for each element of the flattened return tuple. We use a `mergeFuncSpecs` function to nicely take the conjunction of the preconditions and postconditions, and take the union of the `Storage` maps. Miscellaneous changes ===================== * Update `display.sh` and `oneoff.sh` testing scripts. * Uncomment the command that cleans up temp files in `oneoff.sh`. * Add `FromJSON` instance for `ScopedNameWithIdxArg` * Add flattening example `ab.cairo`

This commit makes changes to match the new `spec.json` format in: NethermindEth/horus-compile#63 In particular, return types of storage variables which are `struct`s are flattened (deeply) into a tuple, and internally, we use an extra argument to index into this tuple. Parsing the new JSON format =========================== For example, the keys in the `storage_update` object in the `spec.json` file have been modified as follows: ```diff - "__main__.complex_var_1.s.x": [ + "__main__.complex_var_1 0": [ ``` The relevants bits of the source file are: ```cairo struct Point { x: felt, y: felt, } @storage_var func complex_var_1(arg: Uint256) -> (s: Point) { } ``` Note that instead of using dot-accessor notation, we use an index `0` to indicate the first member of the return tuple of `complex_var_1()`, which is identified with the field `x` of `Point`. In order to parse this index argument from the key in the JSON, as seen in the diff above, we change implicitly change the `FromJSON` of `FuncSpec`/`Storage`, and define `ScopedNameWithIdxArg` which is basically `"__main__.complex_var_1 0"`, as is obvious from its name. So instead of parsing a value of type `Storage` from the JSON, we parse a value of type `Storage'`: ``` +type Storage' = Map ScopedNameWithIdxArg [([Expr TFelt], Expr TFelt)] ``` and then convert it to a map of type `Storage` with a `storage'ToStorage` function. Standard specs for `<storage>.read()` and `<storage>.write()` ============================================================= We refactor `storageVarsSpecs` heavily, folding over the `ContractDefinition` field: ```diff + , cd_storageVars :: Map ScopedName (Arity, Coarity) ``` which now includes the arity and coarity of each storage variable. In order to manage this, we add helper functions: ```diff +mkReadSpecs :: ScopedName -> (Int, Int) -> [(ScopedName, FuncSpec)] +mkWriteSpecs :: ScopedName -> (Int, Int) -> [(ScopedName, FuncSpec)] ``` which basically construct a separate `FuncSpec` for each element of the flattened return tuple. We use a `mergeFuncSpecs` function to nicely take the conjunction of the preconditions and postconditions, and take the union of the `Storage` maps. Miscellaneous changes ===================== * Update `display.sh` and `oneoff.sh` testing scripts. * Uncomment the command that cleans up temp files in `oneoff.sh`. * Add `FromJSON` instance for `ScopedNameWithIdxArg` * Add flattening example `ab.cairo`

This commit makes changes to match the new `spec.json` format in: NethermindEth/horus-compile#63 In particular, return types of storage variables which are `struct`s are flattened (deeply) into a tuple, and internally, we use an extra argument to index into this tuple. Parsing the new JSON format =========================== For example, the keys in the `storage_update` object in the `spec.json` file have been modified as follows: ```diff - "__main__.complex_var_1.s.x": [ + "__main__.complex_var_1 0": [ ``` The relevants bits of the source file are: ```cairo struct Point { x: felt, y: felt, } @storage_var func complex_var_1(arg: Uint256) -> (s: Point) { } ``` Note that instead of using dot-accessor notation, we use an index `0` to indicate the first member of the return tuple of `complex_var_1()`, which is identified with the field `x` of `Point`. In order to parse this index argument from the key in the JSON, as seen in the diff above, we change implicitly change the `FromJSON` of `FuncSpec`/`Storage`, and define `ScopedNameWithIdxArg` which is basically `"__main__.complex_var_1 0"`, as is obvious from its name. So instead of parsing a value of type `Storage` from the JSON, we parse a value of type `Storage'`: ``` +type Storage' = Map ScopedNameWithIdxArg [([Expr TFelt], Expr TFelt)] ``` and then convert it to a map of type `Storage` with a `storage'ToStorage` function. Standard specs for `<storage>.read()` and `<storage>.write()` ============================================================= We refactor `storageVarsSpecs` heavily, folding over the `ContractDefinition` field: ```diff + , cd_storageVars :: Map ScopedName (Arity, Coarity) ``` which now includes the arity and coarity of each storage variable. In order to manage this, we add helper functions: ```diff +mkReadSpecs :: ScopedName -> (Int, Int) -> [(ScopedName, FuncSpec)] +mkWriteSpecs :: ScopedName -> (Int, Int) -> [(ScopedName, FuncSpec)] ``` which basically construct a separate `FuncSpec` for each element of the flattened return tuple. We use a `mergeFuncSpecs` function to nicely take the conjunction of the preconditions and postconditions, and take the union of the `Storage` maps. Miscellaneous changes ===================== * Add flattening example `ab.cairo`

This commit makes changes to match the new `spec.json` format in: NethermindEth/horus-compile#63 In particular, return types of storage variables which are `struct`s are flattened (deeply) into a tuple, and internally, we use an extra argument to index into this tuple. Parsing the new JSON format =========================== For example, the keys in the `storage_update` object in the `spec.json` file have been modified as follows: ```diff - "__main__.complex_var_1.s.x": [ + "__main__.complex_var_1 0": [ ``` The relevants bits of the source file are: ```cairo struct Point { x: felt, y: felt, } @storage_var func complex_var_1(arg: Uint256) -> (s: Point) { } ``` Note that instead of using dot-accessor notation, we use an index `0` to indicate the first member of the return tuple of `complex_var_1()`, which is identified with the field `x` of `Point`. In order to parse this index argument from the key in the JSON, as seen in the diff above, we implicitly change the `FromJSON` instance of `FuncSpec`/`Storage`, and define `ScopedNameWithIdxArg` which is basically `"__main__.complex_var_1 0"`, as is obvious from its name. So instead of parsing a value of type `Storage` from the JSON, we parse a value of type `Storage'`: ``` +type Storage' = Map ScopedNameWithIdxArg [([Expr TFelt], Expr TFelt)] ``` and then convert it to a map of type `Storage` with a `storage'ToStorage` function. Standard specs for `<storage>.read()` and `<storage>.write()` ============================================================= We refactor `storageVarsSpecs` heavily, folding over the `ContractDefinition` field: ```diff + , cd_storageVars :: Map ScopedName (Arity, Coarity) ``` which now includes the arity and coarity of each storage variable. In order to manage this, we add helper functions: ```diff +mkReadSpecs :: ScopedName -> (Int, Int) -> [(ScopedName, FuncSpec)] +mkWriteSpecs :: ScopedName -> (Int, Int) -> [(ScopedName, FuncSpec)] ``` which basically construct a separate `FuncSpec` for each element of the flattened return tuple. We use a `mergeFuncSpecs` function to nicely take the conjunction of the preconditions and postconditions, and take the union of the `Storage` maps.

This commit makes changes to match the new `spec.json` format in: NethermindEth/horus-compile#63 In particular, return types of storage variables which are `struct`s are flattened (deeply) into a tuple, and internally, we use an extra argument to index into this tuple. Parsing the new JSON format =========================== For example, the keys in the `storage_update` object in the `spec.json` file have been modified as follows: ```diff - "__main__.complex_var_1.s.x": [ + "__main__.complex_var_1 0": [ ``` The relevants bits of the source file are: ```cairo struct Point { x: felt, y: felt, } @storage_var func complex_var_1(arg: Uint256) -> (s: Point) { } ``` Note that instead of using dot-accessor notation, we use an index `0` to indicate the first member of the return tuple of `complex_var_1()`, which is identified with the field `x` of `Point`. In order to parse this index argument from the key in the JSON, as seen in the diff above, we implicitly change the `FromJSON` instance of `FuncSpec`/`Storage`, and define `StorageUpdateKey` which is basically `"__main__.complex_var_1 0"`, as is obvious from its name. So instead of parsing a value of type `Storage` from the JSON, we parse a value of type `IndexedStorage`: ``` +type IndexedStorage = Map StorageUpdateKey [([Expr TFelt], Expr TFelt)] ``` and then convert it to a map of type `Storage` with a `unindexStorage` function. Standard specs for `<storage>.read()` and `<storage>.write()` ============================================================= We refactor `storageVarsSpecs` heavily, folding over the `ContractDefinition` field: ```diff + , cd_storageVars :: Map ScopedName (Arity, Coarity) ``` which now includes the arity and coarity of each storage variable. In order to manage this, we add helper functions: ```diff +mkReadSpecs :: ScopedName -> (Int, Int) -> [(ScopedName, FuncSpec)] +mkWriteSpecs :: ScopedName -> (Int, Int) -> [(ScopedName, FuncSpec)] ``` which basically construct a separate `FuncSpec` for each element of the flattened return tuple. We use a `mergeFuncSpecs` function to nicely take the conjunction of the preconditions and postconditions, and take the union of the `Storage` maps.

ElijahVlasov changed the base branch from master to ElijahVlasov/flattening February 21, 2023 06:41

ElijahVlasov force-pushed the ElijahVlasov/flattening branch from 28c0254 to 770918f Compare February 21, 2023 06:44

ElijahVlasov force-pushed the ElijahVlasov/different-invocation-of-storage branch 4 times, most recently from c7d844b to 0047423 Compare February 21, 2023 10:34

Change format of storage variables in compiled annotations

db75277

ElijahVlasov force-pushed the ElijahVlasov/different-invocation-of-storage branch from 0047423 to db75277 Compare February 21, 2023 10:39

ElijahVlasov requested review from DomHenderson and langfield February 21, 2023 11:32

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

New storage format in compiled output#63

New storage format in compiled output#63
ElijahVlasov wants to merge 1 commit intoElijahVlasov/flatteningfrom
ElijahVlasov/different-invocation-of-storage

ElijahVlasov commented Feb 21, 2023 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

ElijahVlasov commented Feb 21, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

ElijahVlasov commented Feb 21, 2023 •

edited

Loading