diff --git a/.DS_Store b/.DS_Store
new file mode 100644
index 00000000..ec97ada9
Binary files /dev/null and b/.DS_Store differ
diff --git a/packages/web/package.json b/packages/web/package.json
index 855ec092..0092d237 100644
--- a/packages/web/package.json
+++ b/packages/web/package.json
@@ -22,6 +22,7 @@
"@fortawesome/free-brands-svg-icons": "^6.5.1",
"@fortawesome/free-solid-svg-icons": "^6.5.1",
"@fortawesome/react-fontawesome": "^0.2.0",
+ "@hyperjump/json-schema": "1.6.7",
"@mdx-js/react": "^3.0.0",
"clsx": "^1.2.1",
"docusaurus-json-schema-plugin": "^1.11.0",
diff --git a/packages/web/spec/operation/concepts.mdx b/packages/web/spec/operation/concepts.mdx
new file mode 100644
index 00000000..ebff224c
--- /dev/null
+++ b/packages/web/spec/operation/concepts.mdx
@@ -0,0 +1,11 @@
+---
+sidebar_position: 2
+---
+
+import SchemaViewer from "@site/src/components/SchemaViewer";
+
+# Key concepts
+
+## Operations do not represent runtime
+
+##
diff --git a/packages/web/spec/operation/overview.mdx b/packages/web/spec/operation/overview.mdx
index 5bc69319..0b04ea9a 100644
--- a/packages/web/spec/operation/overview.mdx
+++ b/packages/web/spec/operation/overview.mdx
@@ -3,3 +3,48 @@ sidebar_position: 1
---
# Overview
+
+:::warning
+
+This schema is **very incomplete** and is missing subschemas for
+several essential kinds of operations.
+
+:::
+
+:::tip
+
+**ethdebug/format/operation** is a JSON schema for describing things that
+happen in high-level languages, such as the beginning of a function call or
+a variable's declaration as some type.
+
+Debuggers observe machine execution at the low-level and present a view of
+the changing machine state using the semantics of the high-level language.
+Doing this requires debuggers to keep track of the state of the machine in
+high-level terms and identify when machine instructions modify this state.
+
+This schema provides a means for compilers to represent high-level language
+operations as part of the annotation for individual machine instructions.
+Because of this, this schema inherently lacks a certain runtime completeness
+that might be desirable: e.g., compilers cannot indicate "this instruction
+is where we recurse into this function the first time", because that
+instruction might be used for the first recursion, the second recursion, and
+all the recursions.
+
+:::
+
+
+This format defines a schema for representing state transitions in high-level
+language models of computation.
+
+JSON values in this schema represent the point at which some high-level state
+change has definitely occurred. Values in this schema are designed for
+compilers to include as part of the broader schemas for annotating a specific
+machine instruction.
+
+## Reading this schema
+
+The **ethdebug/format/operation** schema is a root schema that composes
+other related schemas in the ethdebug/format/operation/* namespace.
+
+These schemas (like all schemas in this format) are specified as
+[JSON Schema](https://json-schema.org), draft 2020-12.
diff --git a/packages/web/spec/operation/schema.mdx b/packages/web/spec/operation/schema.mdx
index ffd8bfd8..87ce875b 100644
--- a/packages/web/spec/operation/schema.mdx
+++ b/packages/web/spec/operation/schema.mdx
@@ -9,3 +9,7 @@ import SchemaViewer from "@site/src/components/SchemaViewer";
+
+
diff --git a/packages/web/spec/operation/scope/_category_.json b/packages/web/spec/operation/scope/_category_.json
new file mode 100644
index 00000000..e1f9965b
--- /dev/null
+++ b/packages/web/spec/operation/scope/_category_.json
@@ -0,0 +1,8 @@
+{
+ "label": "Scope operations",
+ "position": 4,
+ "link": {
+ "type": "generated-index",
+ "description": "Work-in-progress formal schema for ethdebug format"
+ }
+}
diff --git a/packages/web/spec/operation/scope/actions.mdx b/packages/web/spec/operation/scope/actions.mdx
new file mode 100644
index 00000000..239987aa
--- /dev/null
+++ b/packages/web/spec/operation/scope/actions.mdx
@@ -0,0 +1,52 @@
+---
+sidebar_position: 6
+---
+
+import SchemaViewer from "@site/src/components/SchemaViewer";
+
+# Variable actions
+
+
+
+## Declaration actions
+
+### Declare variable as type {#declare}
+
+
+
+### Undeclare variable {#undeclare}
+
+
+
+## Allocation actions
+
+### Allocate variable at pointer {#allocate}
+
+
+
+### Deallocate variable {#deallocate}
+
+
+
+## Assignment action
+
+### Assign variable {#assign}
+
+
diff --git a/packages/web/spec/operation/base.mdx b/packages/web/spec/operation/scope/begin.mdx
similarity index 56%
rename from packages/web/spec/operation/base.mdx
rename to packages/web/spec/operation/scope/begin.mdx
index 0f8fd6f2..2f5c3690 100644
--- a/packages/web/spec/operation/base.mdx
+++ b/packages/web/spec/operation/scope/begin.mdx
@@ -4,8 +4,8 @@ sidebar_position: 3
import SchemaViewer from "@site/src/components/SchemaViewer";
-# Base schema
+# Begin a new scope
diff --git a/packages/web/spec/operation/scope/end.mdx b/packages/web/spec/operation/scope/end.mdx
new file mode 100644
index 00000000..666dd1d7
--- /dev/null
+++ b/packages/web/spec/operation/scope/end.mdx
@@ -0,0 +1,11 @@
+---
+sidebar_position: 5
+---
+
+import SchemaViewer from "@site/src/components/SchemaViewer";
+
+# End a scope
+
+
diff --git a/packages/web/spec/operation/scope/modify.mdx b/packages/web/spec/operation/scope/modify.mdx
new file mode 100644
index 00000000..fa247c13
--- /dev/null
+++ b/packages/web/spec/operation/scope/modify.mdx
@@ -0,0 +1,11 @@
+---
+sidebar_position: 4
+---
+
+import SchemaViewer from "@site/src/components/SchemaViewer";
+
+# Modify an existing scope
+
+
diff --git a/packages/web/spec/operation/scope/scope.mdx b/packages/web/spec/operation/scope/scope.mdx
new file mode 100644
index 00000000..c0c6c1b5
--- /dev/null
+++ b/packages/web/spec/operation/scope/scope.mdx
@@ -0,0 +1,11 @@
+---
+sidebar_position: 2
+---
+
+import SchemaViewer from "@site/src/components/SchemaViewer";
+
+# Scope operation schema
+
+
diff --git a/packages/web/spec/operation/scope/semantics.mdx b/packages/web/spec/operation/scope/semantics.mdx
new file mode 100644
index 00000000..e6729098
--- /dev/null
+++ b/packages/web/spec/operation/scope/semantics.mdx
@@ -0,0 +1,5 @@
+---
+sidebar_position: 1
+---
+
+# Semantics of scopes
diff --git a/packages/web/src/schemas.ts b/packages/web/src/schemas.ts
index 0216b3fc..d59d78b4 100644
--- a/packages/web/src/schemas.ts
+++ b/packages/web/src/schemas.ts
@@ -150,4 +150,30 @@ export const schemaIndex: SchemaIndex = {
title: "Region reference",
href: "/spec/pointer/expression#region-references"
},
+
+ "schema:ethdebug/format/operation/scope": {
+ href: "/spec/operation/scope"
+ },
+
+ ...(
+ ["begin", "modify", "end"].map(action => ({
+ [`schema:ethdebug/format/operation/scope/${action}`]: {
+ href: "/spec/operation/scope/begin"
+ },
+ })).reduce((a, b) => ({ ...a, ...b }), {})
+ ),
+
+ "schema:ethdebug/format/operation/scope/actions": {
+ href: "/spec/operation/scope/actions",
+ title: "Variable actions"
+ },
+
+ ...(
+ ["Declare", "Undeclare", "Allocate", "Deallocate", "Assign"].map(def => ({
+ [`schema:ethdebug/format/operation/scope/actions#/$defs/${def}`]: {
+ title: `${def} variable schema`,
+ href: `/spec/operation/scope/actions#${def.toLowerCase()}`
+ }
+ })).reduce((a, b) => ({ ...a, ...b }), {})
+ ),
};
diff --git a/schemas/.DS_Store b/schemas/.DS_Store
new file mode 100644
index 00000000..fbcad895
Binary files /dev/null and b/schemas/.DS_Store differ
diff --git a/schemas/operation.schema.yaml b/schemas/operation.schema.yaml
index cbcf9226..d0a3dd5b 100644
--- a/schemas/operation.schema.yaml
+++ b/schemas/operation.schema.yaml
@@ -6,4 +6,71 @@ description:
Represents an operation that corresponds to behavior provided by the
semantics of a high-level language (such as a variable allocation or a
function call)
+
type: object
+properties:
+ domain:
+ type: string
+
+required: [domain]
+
+if:
+ type: object
+ title: Known domain
+ description:
+ If `domain` adheres to the set of known domains defined by this schema
+ properties:
+ domain:
+ $ref: "#/$defs/Domain"
+
+then:
+ type: object
+ title: Known operation
+ description:
+ Then the object must adhere to the corresponding operation schema for that
+ domain.
+
+ allOf:
+ - if:
+ properties:
+ domain:
+ const: scope
+ then:
+ $ref: "schema:ethdebug/format/operation/scope"
+
+ - if:
+ properties:
+ domain:
+ const: nil
+ then:
+ title: Nil operation
+ description:
+ Indicates that no operation happened
+ unevaluatedProperties: false
+
+else: true
+
+examples:
+ - domain: scope
+ begin:
+ id: __contract__Guestbook__
+ variables:
+ visitors:
+ declare:
+ type:
+ kind: mapping
+ contains:
+ key:
+ type:
+ kind: address
+ payable: false
+ value:
+ type:
+ kind: bool
+
+$defs:
+ Domain:
+ type: string
+ enum:
+ - scope
+ - nil
diff --git a/schemas/operation/base.schema.yaml b/schemas/operation/base.schema.yaml
deleted file mode 100644
index c71c80c0..00000000
--- a/schemas/operation/base.schema.yaml
+++ /dev/null
@@ -1,40 +0,0 @@
-$schema: "https://json-schema.org/draft/2020-12/schema"
-$id: "schema:ethdebug/format/operation/base"
-
-title: ethdebug/format/operation/base
-description:
- Defines the minimally necessary schema for a high-level program operation.
-type: object
-
-allOf:
- - oneOf:
- - required:
- - begin
- - required:
- - end
- - required:
- - signal
- - if:
- required:
- - begin
- then:
- $ref: "#/$defs/BeginOperation"
-
-$defs:
- BeginOperation:
- type: object
- properties:
- begin:
- type: string
-
- EndOperation:
- type: object
- properties:
- end:
- type: string
-
- SignalOperation:
- type: object
- properties:
- signal:
- type: string
diff --git a/schemas/operation/scope.schema.yaml b/schemas/operation/scope.schema.yaml
index dee12c34..2f2c88d3 100644
--- a/schemas/operation/scope.schema.yaml
+++ b/schemas/operation/scope.schema.yaml
@@ -3,25 +3,67 @@ $id: "schema:ethdebug/format/operation/scope"
title: ethdebug/format/operation/scope
description: |
- Represents a scope operation
+ An operation that either begins, modifies, or ends a scope.
+
type: object
properties:
- action:
+ domain:
const: scope
+required: [domain]
+
+unevaluatedProperties: false
allOf:
- oneOf:
- required: [begin]
- - required: [end]
- required: [scope]
+ - required: [end]
- if:
required: [begin]
then:
- properties:
- id:
- type: [number, string]
- parent:
- type: [number, string]
+ $ref: "schema:ethdebug/format/operation/scope/begin"
+
+ - if:
+ required: [scope]
+ then:
+ $ref: "schema:ethdebug/format/operation/scope/modify"
+
+ - if:
+ required: [end]
+ then:
+ $ref: "schema:ethdebug/format/operation/scope/end"
+
+examples:
+ - domain: scope
+ begin:
+ id: 1
+ parent:
+ id: 0
+ variables:
+ x:
+ declare:
+ type:
+ kind: uint
+ bits: 256
+ allocate:
+ pointer:
+ location: stack
+ slot: 0
+ - domain: scope
+ scope:
+ id: 1
+ variables:
+ x:
+ assign: true
+ - domain: scope
+ scope:
+ id: 1
+ variables:
+ x:
+ deallocate: true
+ - domain: scope
+ end:
+ id: 1
diff --git a/schemas/operation/scope/actions.schema.yaml b/schemas/operation/scope/actions.schema.yaml
new file mode 100644
index 00000000..cbf4fa63
--- /dev/null
+++ b/schemas/operation/scope/actions.schema.yaml
@@ -0,0 +1,146 @@
+$schema: "https://json-schema.org/draft/2020-12/schema"
+$id: "schema:ethdebug/format/operation/scope/actions"
+
+title: ethdebug/format/operation/scope/actions
+description: |
+ Actions schema for a particular variable
+
+type: object
+
+allOf:
+ - title: Declaration actions
+ description: |
+ This object may specify `{ "declare": ... }` to indicate a type
+ to which this variable belongs following this operation, or
+ `{ "undeclare": true }` to specify that this variable's declaration no
+ longer exists as of this operation.
+ type: object
+ allOf:
+ - $ref: "#/$defs/Declare"
+ - $ref: "#/$defs/Undeclare"
+ - title: Not both declared and undeclared
+ not:
+ required: [declare, undeclare]
+ properties:
+ undeclare:
+ const: true
+
+ - title: Allocation actions
+ description: |
+ This object may specify either `{ "allocate": ... }` to indicate a
+ pointer where this variable has been allocated as part of this operation,
+ or `{ "deallocate": true }` to indicate that this variable's allocation
+ is no longer available following this operation.
+ type: object
+ allOf:
+ - $ref: "#/$defs/Allocate"
+ - $ref: "#/$defs/Deallocate"
+ - title: Not both allocated and deallocated
+ not:
+ required: [allocate, deallocate]
+ properties:
+ deallocate:
+ const: true
+
+ - title: Assignment action
+ description: |
+ This object may specify an `"assign"` field, where a value of `true`
+ indicates that the corresponding variable has been assigned as part of
+ the overall parent operation.
+ type: object
+ $ref: "#/$defs/Assign"
+
+ - title: Non-emptiness constraint
+ description: This object must define at least one positive property.
+ type: object
+ anyOf:
+ - title: required `declare`
+ required: [declare]
+ - title: required `undeclare`
+ required: [undeclare]
+ properties:
+ undeclare:
+ const: true
+ - title: required `allocate`
+ required: [allocate]
+ - title: required `deallocate`
+ required: [deallocate]
+ properties:
+ deallocate:
+ const: true
+ - title: required `assign`
+ required: [assign]
+ properties:
+ assign:
+ const: true
+
+
+examples:
+ - declare:
+ type:
+ kind: bool
+ allocate:
+ pointer:
+ location: storage
+ slot: 0x0
+ offset: 0
+ length: 1
+ assign: true
+ - undeclare: true
+ deallocate: true
+
+
+$defs:
+ Declare:
+ title: '{ "declare": ... }'
+ description: |
+ Indicates this operation results in this variable existing in scope with
+ the specified type.
+ type: object
+ properties:
+ declare:
+ $ref: "schema:ethdebug/format/type/wrapper"
+
+ Undeclare:
+ title: '{ "undeclare": ... }'
+ description: |
+ Indicates that this operation results in this variable is no longer
+ available in this scope.
+ type: object
+ properties:
+ undeclare:
+ type: boolean
+
+ Allocate:
+ title: '{ "allocate": ... }'
+ description: |
+ Indicates that this operation results in space being reserved for this
+ variable at the specified pointer.
+ type: object
+ properties:
+ allocate:
+ type: object
+ properties:
+ pointer:
+ $ref: "schema:ethdebug/format/pointer"
+ required: [pointer]
+
+ Deallocate:
+ title: '{ "deallocate": ... }'
+ description: |
+ Indicates that this operation results in space no longer being reserved
+ for this variable at any known pointer.
+ type: object
+ properties:
+ deallocate:
+ type: boolean
+
+ Assign:
+ title: '{ "assign": ... }'
+ description: |
+ Indicates that this operation includes a new value being saved for this
+ variable.
+ type: object
+ properties:
+ assign:
+ type: boolean
diff --git a/schemas/operation/scope/begin.schema.yaml b/schemas/operation/scope/begin.schema.yaml
index c4b4ce4d..3d960635 100644
--- a/schemas/operation/scope/begin.schema.yaml
+++ b/schemas/operation/scope/begin.schema.yaml
@@ -3,40 +3,75 @@ $id: "schema:ethdebug/format/operation/scope/begin"
title: ethdebug/format/operation/scope/begin
description: |
- Describes the start of a new variables scope.
+ Describes the start of a new variables scope. May also specify variable
+ declarations, allocations, and assignments.
+
type: object
properties:
- begin:
- type: string
+ domain:
const: scope
- id:
+ begin:
+ type: object
+ title: Details about new scope
description:
- The scope ID (defined by compiler)
- $ref: "schema:ethdebug/format/source/id"
+ An operation that begins a new scope **may** specify a parent scope
+ from which to inherit identifiers. This object **must** be a valid
+ "scope reference", i.e., it must define an `"id"`.
+
+ $ref: "schema:ethdebug/format/operation/scope/reference"
+
+ properties:
+ parent:
+ type: object
+ description:
+ Optional reference to the parent scope, from which to inherit variables.
+ $ref: "schema:ethdebug/format/operation/scope/reference"
variables:
- title: Variables by identifier
+ title: Variable declarations/allocations/etc.
+ description: |
+ Optional mapping of variable actions by identifier. Indicates that this
+ operation includes declarations/allocations/etc. for particular variables
+ starting from the beginning of this new scope.
type: object
additionalProperties:
- $ref: "schema:ethdebug/format/operation/scope/variable"
+ $ref: "schema:ethdebug/format/operation/scope/actions"
+ minProperties: 1
required:
- - id
- - variables
-
-$ref: "schema:ethdebug/format/operation/base"
+ - domain
+ - begin
examples:
- - begin: scope
- id: s__function__call__ragequit__uint256
+ - domain: scope
+ begin:
+ id: __contract_C__
+ variables:
+ counter:
+ declare:
+ type:
+ kind: uint
+ bits: 256
+ allocate:
+ pointer:
+ location: storage
+ slot: "0x0"
+ - domain: scope
+ begin:
+ id: __contract_C__function_external_incrementBy__
+ parent:
+ id: __contract_C__
variables:
- "amount":
- type:
- kind: uint
- bits: 256
- pointer:
- location: stack
- slot: 0
+ amount:
+ declare:
+ type:
+ kind: uint
+ bits: 256
+ allocate:
+ pointer:
+ location: calldata
+ offset: 4
+ length: $wordsize
diff --git a/schemas/operation/scope/end.schema.yaml b/schemas/operation/scope/end.schema.yaml
new file mode 100644
index 00000000..47d123bf
--- /dev/null
+++ b/schemas/operation/scope/end.schema.yaml
@@ -0,0 +1,24 @@
+$schema: "https://json-schema.org/draft/2020-12/schema"
+$id: "schema:ethdebug/format/operation/scope/end"
+
+title: ethdebug/format/operation/scope/end
+description: |
+ Describes the end of a variables scope.
+
+type: object
+
+properties:
+ domain:
+ const: scope
+
+ end:
+ $ref: "schema:ethdebug/format/operation/scope/reference"
+
+required:
+ - domain
+ - end
+
+examples:
+ - domain: scope
+ end:
+ id: 5
diff --git a/schemas/operation/scope/modify.schema.yaml b/schemas/operation/scope/modify.schema.yaml
new file mode 100644
index 00000000..968e60b7
--- /dev/null
+++ b/schemas/operation/scope/modify.schema.yaml
@@ -0,0 +1,38 @@
+$schema: "https://json-schema.org/draft/2020-12/schema"
+$id: "schema:ethdebug/format/operation/scope/modify"
+
+title: ethdebug/format/operation/scope/modify
+description: |
+ Describes a change to the variables in a particular scope
+
+type: object
+
+properties:
+ domain:
+ const: scope
+
+ scope:
+ $ref: "schema:ethdebug/format/operation/scope/reference"
+
+ variables:
+ title: Variable declarations/allocations/etc.
+ description: |
+ Mapping of variable actions by identifier. Indicates that this operation
+ includes specified changes to particular variables.
+ type: object
+ additionalProperties:
+ $ref: "schema:ethdebug/format/operation/scope/actions"
+ minProperties: 1
+
+required:
+ - domain
+ - scope
+ - variables
+
+examples:
+ - domain: scope
+ scope:
+ id: 5
+ variables:
+ x:
+ assign: true
diff --git a/schemas/operation/scope/reference.schema.yaml b/schemas/operation/scope/reference.schema.yaml
new file mode 100644
index 00000000..865247f6
--- /dev/null
+++ b/schemas/operation/scope/reference.schema.yaml
@@ -0,0 +1,24 @@
+$schema: "https://json-schema.org/draft/2020-12/schema"
+$id: "schema:ethdebug/format/operation/scope/reference"
+
+title: ethdebug/format/operation/scope/reference
+description: |
+ An object with an ID property used to reference a particular scope
+
+type: object
+
+properties:
+ id:
+ title: Scope identifier
+ description:
+ The scope ID (defined by compiler)
+ type:
+ - number
+ - string
+
+required:
+ - id
+
+examples:
+ - id: 5
+ - id: __C_transferFrom__internal__2
diff --git a/schemas/operation/scope/variable.schema.yaml b/schemas/operation/scope/variable.schema.yaml
deleted file mode 100644
index 407fa4b0..00000000
--- a/schemas/operation/scope/variable.schema.yaml
+++ /dev/null
@@ -1,80 +0,0 @@
-$schema: "https://json-schema.org/draft/2020-12/schema"
-$id: "schema:ethdebug/format/operation/scope/variable"
-
-title: ethdebug/format/operation/scope/variable
-description: |
- Describes a variable as it appears in scope.
-
-type: object
-
-properties:
- type:
- $ref: "schema:ethdebug/format/type"
- pointer:
- title: Optional ethdebug/format/pointer
- declaration:
- $ref: "schema:ethdebug/format/source"
- required: [range]
-
-if:
- required: [pointer]
-then:
- properties:
- uninitialized:
- type: boolean
- default: false
-
-required:
- - type
-
-examples:
- - type:
- kind: uint
- bits: 256
- declaration:
- source:
- id: 3
- range:
- # uint256 x = ...
- # ^^^^^^^^^
- offset: 555
- length: 9
- ast:
- node:
- id: 1
-
- - type:
- kind: array
- contains:
- type:
- kind: uint
- bits: 256
- pointer:
- # example borrowed from ethdebug/format/pointer; see comments there
- group:
- - name: "array-start"
- location: stack
- slot: 0
-
- - name: "array-count"
- location: memory
- offset:
- $read: "array-start"
- length: $wordsize
-
- - list:
- count:
- $read: "array-count"
- each: "item-index"
- is:
- name: "array-item"
- location: "memory"
- offset:
- $sum:
- - .offset: "array-count"
- - .length: "array-count"
- - $product:
- - "item-index"
- - .length: "array-item"
- length: $wordsize
- uninitialized: true
diff --git a/schemas/pointer/.DS_Store b/schemas/pointer/.DS_Store
new file mode 100644
index 00000000..a82c346c
Binary files /dev/null and b/schemas/pointer/.DS_Store differ
diff --git a/sketches b/sketches
new file mode 100644
index 00000000..8febf054
--- /dev/null
+++ b/sketches
@@ -0,0 +1,46 @@
+
+
+# instruction annotation
+operations:
+ - path: "uint"
+ operation:
+ scope: begin
+ id: 5
+ variables:
+ x:
+ declare:
+ kind: uint
+ bits: 256
+ - path: "bytes"
+ operation:
+ scope: begin
+ id: 4
+ variables:
+ x:
+ declare:
+ kind: bytes
+ bytes: 256
+
+
+action: scope
+begin:
+ id: 5
+ parent:
+ id: 4
+declare:
+ x:
+ type:
+ kind: uint
+ bits: 256
+allocate:
+ x:
+ location: stack
+ slot: 0
+assign:
+ - x
+
+action: scope
+scope:
+ id: 5
+assign:
+ - x