Skip to content

Commit

Permalink
fix more links
Browse files Browse the repository at this point in the history
  • Loading branch information
RalfJung committed Oct 5, 2023
1 parent 26387d9 commit 056bdd3
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 2 deletions.
4 changes: 3 additions & 1 deletion spec/lang/machine.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,9 @@
This defines the state that makes up the MiniRust Abstract Machine:
which components together make up the state of a MiniRust program during its execution?
This key data structure says a lot about how the Abstract Machine is structured.
(The "reduction relation" aka operational semantics aka `step` function is defined in [the next file](step.md).)

The "reduction relation" aka operational semantics is defined by the `step` function below,
which is defined in terms of many [evaluation functions for our various syntactic categories](step/).

```rust
/// This type contains everything that needs to be tracked during the execution
Expand Down
2 changes: 1 addition & 1 deletion spec/lang/representation.md
Original file line number Diff line number Diff line change
Expand Up @@ -377,7 +377,7 @@ The last property might sound surprising, but consider what happens for padding:
so a bytes-value-bytes roundtrip of some data with padding will reset some bytes to `Uninit`.

Together, these properties ensure that it is okay to optimize away a self-assignment like `tmp = x; x = tmp`.
The effect of this assignment (as defined [later](step.md)) is to decode the `bytes1` stored at `x`, and then encode the resulting value again into `bytes2` and store that back.
The effect of this assignment (as defined [later](step/statements.md)) is to decode the `bytes1` stored at `x`, and then encode the resulting value again into `bytes2` and store that back.
(We ignore the intermediate storage in `tmp`.)
The second round-trip property ensures that `bytes2 <= bytes1`.
If we remove the assignment, `x` ends up with `bytes1` rather than `bytes2`; we thus "increase memory" (as in, the memory in the transformed program is "more defined" than the one in the source program).
Expand Down

0 comments on commit 056bdd3

Please sign in to comment.