format: state the postcondition convention for instruction contexts - #281
Merged
Conversation
The instruction context description carried one sentence framing pointers
as resolving against the pre-execution ("trace step") state, contradicting
the rest of the same description ("following the execution"), the
program-example walkthrough, and compiler emission — all of which treat a
context as a postcondition. This states the intended convention plainly.
- program/instruction: a context holds following the instruction's
execution; both its semantic facts and its pointers resolve against the
post-execution state. Contexts form a chain — the program-level context
is the precondition before the first instruction, each instruction's
context is its postcondition (and the next instruction's precondition),
and a debugger paused about to execute instruction i reads instruction
i-1's context.
- program: the program-level context description now names its role as the
base case of that chain (the precondition to the first instruction).
- program example: under the postcondition reading the Incrementer example
was correct except at the ADD and the following PUSH0, where it still
listed localValue on the stack after ADD had consumed it (leaving only
storedValue + 1). localValue is now dropped from those two contexts.
Also removes a stale 'value = tmp;' line from the pseudo-code.
Contributor
|
Adds the equivalent trace-position framing to the instruction context description: prepending the program-level context to the sequence of instruction contexts gives one sequence indexed by trace position, so the context in effect before executing the instruction at position i is element i — no special case for the first instruction.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Instruction contexts use postcondition semantics, pointers included. The description of
program/instruction'scontextcarried a single sentence framing pointers as resolving against the pre-execution "trace step" state — an outlier that contradicted the rest of that same description ("the context known to exist following the execution"), theprogram-example walkthrough on the spec site, and existing compiler emission. This PR states the convention plainly and fixes the one example that was wrong under it.program/instruction — a context holds following the instruction's execution; both its semantic facts and its pointers resolve against the post-execution state. Contexts form a chain: the program-level
contextis the precondition before the first instruction, each instruction's context is its postcondition (and the next instruction's precondition), and a debugger paused about to execute instruction i reads instruction i − 1's context.program — the program-level
contextdescription now names its role as the base case of that chain (the precondition to the first instruction).program example — under the postcondition convention the
Incrementerexample was already correct except at theADDand thePUSH0after it, which wrongly keptlocalValuelisted on the stack; this PR removes it from those two contexts, and nothing else in the example changes. In this examplelocalValueis the loadedstoredValue(let localValue = storedValue; storedValue += 1;), soADDconsumes it, leavingstoredValue + 1. Post-execution stack per instruction:PUSH0[0x00]SLOAD[localValue]PUSH1 0x01[localValue, 0x01]ADD[storedValue+1]PUSH0[storedValue+1, 0x00]SSTORE[]localValueis now dropped from theADDand followingPUSH0contexts, matching how the spec-site walkthrough omits a local once it is consumed. The offset-1 and offset-2 stack pointers were already correct post-execution and are unchanged. A stalevalue = tmp;line is also removed from the pseudo-code.This supersedes #278, which had reworked the same example toward the pre-execution reading.