ECMAScript® 2021 Language Specification

Draft ECMA-262 / February 25, 2021

6.2 ECMAScript Specification Types

A specification type corresponds to meta-values that are used within algorithms to describe the semantics of ECMAScript language constructs and ECMAScript language types. The specification types include Reference, List, Completion, Property Descriptor, Environment Record, Abstract Closure, and Data Block. Specification type values are specification artefacts that do not necessarily correspond to any specific entity within an ECMAScript implementation. Specification type values may be used to describe intermediate results of ECMAScript expression evaluation but such values cannot be stored as properties of objects or values of ECMAScript language variables.

6.2.1 The List and Record Specification Types

The List type is used to explain the evaluation of argument lists (see 13.3.8) in new expressions, in function calls, and in other algorithms where a simple ordered list of values is needed. Values of the List type are simply ordered sequences of list elements containing the individual values. These sequences may be of any length. The elements of a list may be randomly accessed using 0-origin indices. For notational convenience an array-like syntax can be used to access List elements. For example, arguments[2] is shorthand for saying the 3rd element of the List arguments.

When an algorithm iterates over the elements of a List without specifying an order, the order used is the order of the elements in the List.

For notational convenience within this specification, a literal syntax can be used to express a new List value. For example, « 1, 2 » defines a List value that has two elements each of which is initialized to a specific value. A new empty List can be expressed as « ».

The Record type is used to describe data aggregations within the algorithms of this specification. A Record type value consists of one or more named fields. The value of each field is either an ECMAScript value or an abstract value represented by a name associated with the Record type. Field names are always enclosed in double brackets, for example [[Value]].

For notational convenience within this specification, an object literal-like syntax can be used to express a Record value. For example, { [[Field1]]: 42, [[Field2]]: false, [[Field3]]: empty } defines a Record value that has three fields, each of which is initialized to a specific value. Field name order is not significant. Any fields that are not explicitly listed are considered to be absent.

In specification text and algorithms, dot notation may be used to refer to a specific field of a Record value. For example, if R is the record shown in the previous paragraph then R.[[Field2]] is shorthand for “the field of R named [[Field2]]”.

Schema for commonly used Record field combinations may be named, and that name may be used as a prefix to a literal Record value to identify the specific kind of aggregations that is being described. For example: PropertyDescriptor { [[Value]]: 42, [[Writable]]: false, [[Configurable]]: true }.

6.2.2 The Set and Relation Specification Types

The Set type is used to explain a collection of unordered elements for use in the memory model. Values of the Set type are simple collections of elements, where no element appears more than once. Elements may be added to and removed from Sets. Sets may be unioned, intersected, or subtracted from each other.

The Relation type is used to explain constraints on Sets. Values of the Relation type are Sets of ordered pairs of values from its value domain. For example, a Relation on events is a set of ordered pairs of events. For a Relation R and two values a and b in the value domain of R, a R b is shorthand for saying the ordered pair (a, b) is a member of R. A Relation is least with respect to some conditions when it is the smallest Relation that satisfies those conditions.

A strict partial order is a Relation value R that satisfies the following.

  • For all a, b, and c in R's domain:

    • It is not the case that a R a, and
    • If a R b and b R c, then a R c.
Note 1

The two properties above are called irreflexivity and transitivity, respectively.

A strict total order is a Relation value R that satisfies the following.

  • For all a, b, and c in R's domain:

    • a is identical to b or a R b or b R a, and
    • It is not the case that a R a, and
    • If a R b and b R c, then a R c.
Note 2

The three properties above are called totality, irreflexivity, and transitivity, respectively.

6.2.3 The Completion Record Specification Type

The Completion type is a Record used to explain the runtime propagation of values and control flow such as the behaviour of statements (break, continue, return and throw) that perform nonlocal transfers of control.

Values of the Completion type are Record values whose fields are defined by Table 9. Such values are referred to as Completion Records.

Table 9: Completion Record Fields
Field Name Value Meaning
[[Type]] One of normal, break, continue, return, or throw The type of completion that occurred.
[[Value]] any ECMAScript language value or empty The value that was produced.
[[Target]] any ECMAScript string or empty The target label for directed control transfers.

The term “abrupt completion” refers to any completion with a [[Type]] value other than normal.

6.2.3.1 Await

Algorithm steps that say

  1. Let completion be Await(value).

mean the same thing as:

  1. Let asyncContext be the running execution context.
  2. Let promise be ? PromiseResolve(%Promise%, value).
  3. Let stepsFulfilled be the algorithm steps defined in Await Fulfilled Functions.
  4. Let lengthFulfilled be the number of non-optional parameters of the function definition in Await Fulfilled Functions.
  5. Let onFulfilled be ! CreateBuiltinFunction(stepsFulfilled, lengthFulfilled, "", « [[AsyncContext]] »).
  6. Set onFulfilled.[[AsyncContext]] to asyncContext.
  7. Let stepsRejected be the algorithm steps defined in Await Rejected Functions.
  8. Let lengthRejected be the number of non-optional parameters of the function definition in Await Rejected Functions.
  9. Let onRejected be ! CreateBuiltinFunction(stepsRejected, lengthRejected, "", « [[AsyncContext]] »).
  10. Set onRejected.[[AsyncContext]] to asyncContext.
  11. Perform ! PerformPromiseThen(promise, onFulfilled, onRejected).
  12. Remove asyncContext from the execution context stack and restore the execution context that is at the top of the execution context stack as the running execution context.
  13. Set the code evaluation state of asyncContext such that when evaluation is resumed with a Completion completion, the following steps of the algorithm that invoked Await will be performed, with completion available.
  14. Return.
  15. NOTE: This returns to the evaluation of the operation that had most previously resumed evaluation of asyncContext.

where all aliases in the above steps, with the exception of completion, are ephemeral and visible only in the steps pertaining to Await.

Note

Await can be combined with the ? and ! prefixes, so that for example

  1. Let result be ? Await(value).

means the same thing as:

  1. Let result be Await(value).
  2. ReturnIfAbrupt(result).

6.2.3.1.1 Await Fulfilled Functions

An Await fulfilled function is an anonymous built-in function that is used as part of the Await specification device to deliver the promise fulfillment value to the caller as a normal completion. Each Await fulfilled function has an [[AsyncContext]] internal slot.

When an Await fulfilled function is called with argument value, the following steps are taken:

  1. Let F be the active function object.
  2. Let asyncContext be F.[[AsyncContext]].
  3. Let prevContext be the running execution context.
  4. Suspend prevContext.
  5. Push asyncContext onto the execution context stack; asyncContext is now the running execution context.
  6. Resume the suspended evaluation of asyncContext using NormalCompletion(value) as the result of the operation that suspended it.
  7. Assert: When we reach this step, asyncContext has already been removed from the execution context stack and prevContext is the currently running execution context.
  8. Return undefined.

The "length" property of an Await fulfilled function is 1𝔽.

6.2.3.1.2 Await Rejected Functions

An Await rejected function is an anonymous built-in function that is used as part of the Await specification device to deliver the promise rejection reason to the caller as an abrupt throw completion. Each Await rejected function has an [[AsyncContext]] internal slot.

When an Await rejected function is called with argument reason, the following steps are taken:

  1. Let F be the active function object.
  2. Let asyncContext be F.[[AsyncContext]].
  3. Let prevContext be the running execution context.
  4. Suspend prevContext.
  5. Push asyncContext onto the execution context stack; asyncContext is now the running execution context.
  6. Resume the suspended evaluation of asyncContext using ThrowCompletion(reason) as the result of the operation that suspended it.
  7. Assert: When we reach this step, asyncContext has already been removed from the execution context stack and prevContext is the currently running execution context.
  8. Return undefined.

The "length" property of an Await rejected function is 1𝔽.

6.2.3.2 NormalCompletion

The abstract operation NormalCompletion with a single argument, such as:

  1. Return NormalCompletion(argument).

Is a shorthand that is defined as follows:

  1. Return Completion { [[Type]]: normal, [[Value]]: argument, [[Target]]: empty }.

6.2.3.3 ThrowCompletion

The abstract operation ThrowCompletion with a single argument, such as:

  1. Return ThrowCompletion(argument).

Is a shorthand that is defined as follows:

  1. Return Completion { [[Type]]: throw, [[Value]]: argument, [[Target]]: empty }.

6.2.3.4 UpdateEmpty ( completionRecord, value )

The abstract operation UpdateEmpty takes arguments completionRecord and value. It performs the following steps when called:

  1. Assert: If completionRecord.[[Type]] is either return or throw, then completionRecord.[[Value]] is not empty.
  2. If completionRecord.[[Value]] is not empty, return Completion(completionRecord).
  3. Return Completion { [[Type]]: completionRecord.[[Type]], [[Value]]: value, [[Target]]: completionRecord.[[Target]] }.

6.2.4 The Reference Record Specification Type

The Reference Record type is used to explain the behaviour of such operators as delete, typeof, the assignment operators, the super keyword and other language features. For example, the left-hand operand of an assignment is expected to produce a Reference Record.

A Reference Record is a resolved name or property binding; its fields are defined by Table 10.

Table 10: Reference Record Fields
Field Name Value Meaning
[[Base]] One of: The value or Environment Record which holds the binding. A [[Base]] of unresolvable indicates that the binding could not be resolved.
[[ReferencedName]] String or Symbol The name of the binding. Always a String if [[Base]] value is an Environment Record.
[[Strict]] Boolean true if the Reference Record originated in strict mode code, false otherwise.
[[ThisValue]] any ECMAScript language value or empty If not empty, the Reference Record represents a property binding that was expressed using the super keyword; it is called a Super Reference Record and its [[Base]] value will never be an Environment Record. In that case, the [[ThisValue]] field holds the this value at the time the Reference Record was created.

The following abstract operations are used in this specification to operate upon References:

6.2.4.1 IsPropertyReference ( V )

The abstract operation IsPropertyReference takes argument V. It performs the following steps when called:

  1. Assert: V is a Reference Record.
  2. If V.[[Base]] is unresolvable, return false.
  3. If Type(V.[[Base]]) is Boolean, String, Symbol, BigInt, Number, or Object, return true; otherwise return false.

6.2.4.2 IsUnresolvableReference ( V )

The abstract operation IsUnresolvableReference takes argument V. It performs the following steps when called:

  1. Assert: V is a Reference Record.
  2. If V.[[Base]] is unresolvable, return true; otherwise return false.

6.2.4.3 IsSuperReference ( V )

The abstract operation IsSuperReference takes argument V. It performs the following steps when called:

  1. Assert: V is a Reference Record.
  2. If V.[[ThisValue]] is not empty, return true; otherwise return false.

6.2.4.4 GetValue ( V )

The abstract operation GetValue takes argument V. It performs the following steps when called:

  1. ReturnIfAbrupt(V).
  2. If V is not a Reference Record, return V.
  3. If IsUnresolvableReference(V) is true, throw a ReferenceError exception.
  4. If IsPropertyReference(V) is true, then
    1. Let baseObj be ! ToObject(V.[[Base]]).
    2. Return ? baseObj.[[Get]](V.[[ReferencedName]], GetThisValue(V)).
  5. Else,
    1. Let base be V.[[Base]].
    2. Assert: base is an Environment Record.
    3. Return ? base.GetBindingValue(V.[[ReferencedName]], V.[[Strict]]) (see 9.1).
 Note

The object that may be created in step 4.a is not accessible outside of the above abstract operation and the ordinary object [[Get]] internal method. An implementation might choose to avoid the actual creation of the object.

6.2.4.5 PutValue ( V, W )

The abstract operation PutValue takes arguments V and W. It performs the following steps when called:

  1. ReturnIfAbrupt(V).
  2. ReturnIfAbrupt(W).
  3. If V is not a Reference Record, throw a ReferenceError exception.
  4. If IsUnresolvableReference(V) is true, then
    1. If V.[[Strict]] is true, throw a ReferenceError exception.
    2. Let globalObj be GetGlobalObject().
    3. Return ? Set(globalObj, V.[[ReferencedName]], W, false).
  5. If IsPropertyReference(V) is true, then
    1. Let baseObj be ! ToObject(V.[[Base]]).
    2. Let succeeded be ? baseObj.[[Set]](V.[[ReferencedName]], W, GetThisValue(V)).
    3. If succeeded is false and V.[[Strict]] is true, throw a TypeError exception.
    4. Return.
  6. Else,
    1. Let base be V.[[Base]].
    2. Assert: base is an Environment Record.
    3. Return ? base.SetMutableBinding(V.[[ReferencedName]], W, V.[[Strict]]) (see 9.1).
 Note

The object that may be created in step 5.a is not accessible outside of the above abstract operation and the ordinary object [[Set]] internal method. An implementation might choose to avoid the actual creation of that object.

6.2.4.6 GetThisValue ( V )

The abstract operation GetThisValue takes argument V. It performs the following steps when called:

  1. Assert: IsPropertyReference(V) is true.
  2. If IsSuperReference(V) is true, return V.[[ThisValue]]; otherwise return V.[[Base]].

6.2.4.7 InitializeReferencedBinding ( V, W )

The abstract operation InitializeReferencedBinding takes arguments V and W. It performs the following steps when called:

  1. ReturnIfAbrupt(V).
  2. ReturnIfAbrupt(W).
  3. Assert: V is a Reference Record.
  4. Assert: IsUnresolvableReference(V) is false.
  5. Let base be V.[[Base]].
  6. Assert: base is an Environment Record.
  7. Return base.InitializeBinding(V.[[ReferencedName]], W).

6.2.5 The Property Descriptor Specification Type

The Property Descriptor type is used to explain the manipulation and reification of Object property attributes. Values of the Property Descriptor type are Records. Each field's name is an attribute name and its value is a corresponding attribute value as specified in 6.1.7.1. In addition, any field may be present or absent. The schema name used within this specification to tag literal descriptions of Property Descriptor records is “PropertyDescriptor”.

Property Descriptor values may be further classified as data Property Descriptors and accessor Property Descriptors based upon the existence or use of certain fields. A data Property Descriptor is one that includes any fields named either [[Value]] or [[Writable]]. An accessor Property Descriptor is one that includes any fields named either [[Get]] or [[Set]]. Any Property Descriptor may have fields named [[Enumerable]] and [[Configurable]]. A Property Descriptor value may not be both a data Property Descriptor and an accessor Property Descriptor; however, it may be neither. A generic Property Descriptor is a Property Descriptor value that is neither a data Property Descriptor nor an accessor Property Descriptor. A fully populated Property Descriptor is one that is either an accessor Property Descriptor or a data Property Descriptor and that has all of the fields that correspond to the property attributes defined in either Table 3 or Table 4.

The following abstract operations are used in this specification to operate upon Property Descriptor values:

6.2.5.1 IsAccessorDescriptor ( Desc )

The abstract operation IsAccessorDescriptor takes argument Desc (a Property Descriptor or undefined). It performs the following steps when called:

  1. If Desc is undefined, return false.
  2. If both Desc.[[Get]] and Desc.[[Set]] are absent, return false.
  3. Return true.

6.2.5.2 IsDataDescriptor ( Desc )

The abstract operation IsDataDescriptor takes argument Desc (a Property Descriptor or undefined). It performs the following steps when called:

  1. If Desc is undefined, return false.
  2. If both Desc.[[Value]] and Desc.[[Writable]] are absent, return false.
  3. Return true.

6.2.5.3 IsGenericDescriptor ( Desc )

The abstract operation IsGenericDescriptor takes argument Desc (a Property Descriptor or undefined). It performs the following steps when called:

  1. If Desc is undefined, return false.
  2. If IsAccessorDescriptor(Desc) and IsDataDescriptor(Desc) are both false, return true.
  3. Return false.

6.2.5.4 FromPropertyDescriptor ( Desc )

The abstract operation FromPropertyDescriptor takes argument Desc (a Property Descriptor or undefined). It performs the following steps when called:

  1. If Desc is undefined, return undefined.
  2. Let obj be ! OrdinaryObjectCreate(%Object.prototype%).
  3. Assert: obj is an extensible ordinary object with no own properties.
  4. If Desc has a [[Value]] field, then
    1. Perform ! CreateDataPropertyOrThrow(obj, "value", Desc.[[Value]]).
  5. If Desc has a [[Writable]] field, then
    1. Perform ! CreateDataPropertyOrThrow(obj, "writable", Desc.[[Writable]]).
  6. If Desc has a [[Get]] field, then
    1. Perform ! CreateDataPropertyOrThrow(obj, "get", Desc.[[Get]]).
  7. If Desc has a [[Set]] field, then
    1. Perform ! CreateDataPropertyOrThrow(obj, "set", Desc.[[Set]]).
  8. If Desc has an [[Enumerable]] field, then
    1. Perform ! CreateDataPropertyOrThrow(obj, "enumerable", Desc.[[Enumerable]]).
  9. If Desc has a [[Configurable]] field, then
    1. Perform ! CreateDataPropertyOrThrow(obj, "configurable", Desc.[[Configurable]]).
  10. Return obj.

6.2.5.5 ToPropertyDescriptor ( Obj )

The abstract operation ToPropertyDescriptor takes argument Obj. It performs the following steps when called:

  1. If Type(Obj) is not Object, throw a TypeError exception.
  2. Let desc be a new Property Descriptor that initially has no fields.
  3. Let hasEnumerable be ? HasProperty(Obj, "enumerable").
  4. If hasEnumerable is true, then
    1. Let enumerable be ! ToBoolean(? Get(Obj, "enumerable")).
    2. Set desc.[[Enumerable]] to enumerable.
  5. Let hasConfigurable be ? HasProperty(Obj, "configurable").
  6. If hasConfigurable is true, then
    1. Let configurable be ! ToBoolean(? Get(Obj, "configurable")).
    2. Set desc.[[Configurable]] to configurable.
  7. Let hasValue be ? HasProperty(Obj, "value").
  8. If hasValue is true, then
    1. Let value be ? Get(Obj, "value").
    2. Set desc.[[Value]] to value.
  9. Let hasWritable be ? HasProperty(Obj, "writable").
  10. If hasWritable is true, then
    1. Let writable be ! ToBoolean(? Get(Obj, "writable")).
    2. Set desc.[[Writable]] to writable.
  11. Let hasGet be ? HasProperty(Obj, "get").
  12. If hasGet is true, then
    1. Let getter be ? Get(Obj, "get").
    2. If IsCallable(getter) is false and getter is not undefined, throw a TypeError exception.
    3. Set desc.[[Get]] to getter.
  13. Let hasSet be ? HasProperty(Obj, "set").
  14. If hasSet is true, then
    1. Let setter be ? Get(Obj, "set").
    2. If IsCallable(setter) is false and setter is not undefined, throw a TypeError exception.
    3. Set desc.[[Set]] to setter.
  15. If desc.[[Get]] is present or desc.[[Set]] is present, then
    1. If desc.[[Value]] is present or desc.[[Writable]] is present, throw a TypeError exception.
  16. Return desc.

6.2.5.6 CompletePropertyDescriptor ( Desc )

The abstract operation CompletePropertyDescriptor takes argument Desc (a Property Descriptor). It performs the following steps when called:

  1. Assert: Desc is a Property Descriptor.
  2. Let like be the Record { [[Value]]: undefined, [[Writable]]: false, [[Get]]: undefined, [[Set]]: undefined, [[Enumerable]]: false, [[Configurable]]: false }.
  3. If IsGenericDescriptor(Desc) is true or IsDataDescriptor(Desc) is true, then
    1. If Desc does not have a [[Value]] field, set Desc.[[Value]] to like.[[Value]].
    2. If Desc does not have a [[Writable]] field, set Desc.[[Writable]] to like.[[Writable]].
  4. Else,
    1. If Desc does not have a [[Get]] field, set Desc.[[Get]] to like.[[Get]].
    2. If Desc does not have a [[Set]] field, set Desc.[[Set]] to like.[[Set]].
  5. If Desc does not have an [[Enumerable]] field, set Desc.[[Enumerable]] to like.[[Enumerable]].
  6. If Desc does not have a [[Configurable]] field, set Desc.[[Configurable]] to like.[[Configurable]].
  7. Return Desc.

6.2.6 The Environment Record Specification Type

The Environment Record type is used to explain the behaviour of name resolution in nested functions and blocks. This type and the operations upon it are defined in 9.1.

6.2.7 The Abstract Closure Specification Type

The Abstract Closure specification type is used to refer to algorithm steps together with a collection of values. Abstract Closures are meta-values and are invoked using function application style such as closure(arg1, arg2). Like abstract operations, invocations perform the algorithm steps described by the Abstract Closure.

In algorithm steps that create an Abstract Closure, values are captured with the verb "capture" followed by a list of aliases. When an Abstract Closure is created, it captures the value that is associated with each alias at that time. In steps that specify the algorithm to be performed when an Abstract Closure is called, each captured value is referred to by the alias that was used to capture the value.

If an Abstract Closure returns a Completion Record, that Completion Record's [[Type]] must be either normal or throw.

Abstract Closures are created inline as part of other algorithms, shown in the following example.

  1. Let addend be 41.
  2. Let closure be a new Abstract Closure with parameters (x) that captures addend and performs the following steps when called:
    1. Return x + addend.
  3. Let val be closure(1).
  4. Assert: val is 42.

6.2.8 Data Blocks

The Data Block specification type is used to describe a distinct and mutable sequence of byte-sized (8 bit) numeric values. A byte value is an integer value in the range 0 through 255, inclusive. A Data Block value is created with a fixed number of bytes that each have the initial value 0.

For notational convenience within this specification, an array-like syntax can be used to access the individual bytes of a Data Block value. This notation presents a Data Block value as a 0-origined integer-indexed sequence of bytes. For example, if db is a 5 byte Data Block value then db[2] can be used to access its 3rd byte.

A data block that resides in memory that can be referenced from multiple agents concurrently is designated a Shared Data Block. A Shared Data Block has an identity (for the purposes of equality testing Shared Data Block values) that is address-free: it is tied not to the virtual addresses the block is mapped to in any process, but to the set of locations in memory that the block represents. Two data blocks are equal only if the sets of the locations they contain are equal; otherwise, they are not equal and the intersection of the sets of locations they contain is empty. Finally, Shared Data Blocks can be distinguished from Data Blocks.

The semantics of Shared Data Blocks is defined using Shared Data Block events by the memory model. Abstract operations below introduce Shared Data Block events and act as the interface between evaluation semantics and the event semantics of the memory model. The events form a candidate execution, on which the memory model acts as a filter. Please consult the memory model for full semantics.

Shared Data Block events are modeled by Records, defined in the memory model.

The following abstract operations are used in this specification to operate upon Data Block values:

6.2.8.1 CreateByteDataBlock ( size )

The abstract operation CreateByteDataBlock takes argument size (an integer). It performs the following steps when called:

  1. Assert: size ≥ 0.
  2. Let db be a new Data Block value consisting of size bytes. If it is impossible to create such a Data Block, throw a RangeError exception.
  3. Set all of the bytes of db to 0.
  4. Return db.

6.2.8.2 CreateSharedByteDataBlock ( size )

The abstract operation CreateSharedByteDataBlock takes argument size (a non-negative integer). It performs the following steps when called:

  1. Assert: size ≥ 0.
  2. Let db be a new Shared Data Block value consisting of size bytes. If it is impossible to create such a Shared Data Block, throw a RangeError exception.
  3. Let execution be the [[CandidateExecution]] field of the surrounding agent's Agent Record.
  4. Let eventList be the [[EventList]] field of the element in execution.[[EventsRecords]] whose [[AgentSignifier]] is AgentSignifier().
  5. Let zero be « 0 ».
  6. For each index i of db, do
    1. Append WriteSharedMemory { [[Order]]: Init, [[NoTear]]: true, [[Block]]: db, [[ByteIndex]]: i, [[ElementSize]]: 1, [[Payload]]: zero } to eventList.
  7. Return db.

6.2.8.3 CopyDataBlockBytes ( toBlock, toIndex, fromBlock, fromIndex, count )

The abstract operation CopyDataBlockBytes takes arguments toBlock, toIndex (a non-negative integer), fromBlock, fromIndex (a non-negative integer), and count (a non-negative integer). It performs the following steps when called:

  1. Assert: fromBlock and toBlock are distinct Data Block or Shared Data Block values.
  2. Let fromSize be the number of bytes in fromBlock.
  3. Assert: fromIndex + count ≤ fromSize.
  4. Let toSize be the number of bytes in toBlock.
  5. Assert: toIndex + count ≤ toSize.
  6. Repeat, while count > 0,
    1. If fromBlock is a Shared Data Block, then
      1. Let execution be the [[CandidateExecution]] field of the surrounding agent's Agent Record.
      2. Let eventList be the [[EventList]] field of the element in execution.[[EventsRecords]] whose [[AgentSignifier]] is AgentSignifier().
      3. Let bytes be a List whose sole element is a nondeterministically chosen byte value.
      4. NOTE: In implementations, bytes is the result of a non-atomic read instruction on the underlying hardware. The nondeterminism is a semantic prescription of the memory model to describe observable behaviour of hardware with weak consistency.
      5. Let readEvent be ReadSharedMemory { [[Order]]: Unordered, [[NoTear]]: true, [[Block]]: fromBlock, [[ByteIndex]]: fromIndex, [[ElementSize]]: 1 }.
      6. Append readEvent to eventList.
      7. Append Chosen Value Record { [[Event]]: readEvent, [[ChosenValue]]: bytes } to execution.[[ChosenValues]].
      8. If toBlock is a Shared Data Block, then
        1. Append WriteSharedMemory { [[Order]]: Unordered, [[NoTear]]: true, [[Block]]: toBlock, [[ByteIndex]]: toIndex, [[ElementSize]]: 1, [[Payload]]: bytes } to eventList.
      9. Else,
        1. Set toBlock[toIndex] to bytes[0].
    2. Else,
      1. Assert: toBlock is not a Shared Data Block.
      2. Set toBlock[toIndex] to fromBlock[fromIndex].
    3. Set toIndex to toIndex + 1.
    4. Set fromIndex to fromIndex + 1.
    5. Set count to count - 1.
  7. Return NormalCompletion(empty).