finegeometer/Ideas - Change G6QCTDRPPQGIC7CFYDFV62D2IJJGQKGRLKDHDTTSQOESPFLN7KTQC

Mention a useful paper for reasoning about assembly code.

Created by finegeometer on January 13, 2022

G6QCTDRPPQGIC7CFYDFV62D2IJJGQKGRLKDHDTTSQOESPFLN7KTQC

Dependencies

[2] Z22OYEOI4JVBZ7SXSMLGMFBPJ2F36FSOQLQR5LCAPJVW3KF47P7QC

In channels

main

Change contents

Replacement in src/speedrunning_lower_bound.md at line 51 [2.52]
B:BD[2.3010] → [2.3010:3014]
```
---
```
[2.3010]
[2.3014]
```
### My own thoughts
```

Insertion in src/speedrunning_lower_bound.md at line 81 [2.52]

[2.4678]

[2.4678]


### Potentially useful prior work
I found this paper:
[High-Level Separation Logic for Low-Level Code](https://jbj.github.io/research/hlsl.pdf)

Insertion in src/speedrunning_lower_bound.md at line 87 [2.52]

[2.4679]

[2.4679]

This seems useful. But it's not perfect. In particular, their `safe` primitive is not quite what we need,
because we want to prove something stronger than the fact that the program doesn't crash.