Assembly state propagation reasoning

colltoaction / widip

A system for programming with diagrams

Creative Commons Zero v1.0 Universal

18 stars 2 forks source link

Assembly state propagation reasoning #5

Open colltoaction opened 3 months ago

colltoaction commented 3 months ago

Diagrams naturally model instruction sets with multi-input to multi-output boxes for each instruction.

Each instruction such as mul or jump can be decorated as seen here:

https://github.com/colltoaction/widip/tree/main/examples/rosetta#factorial-x86-assembly

The goal is to aid the user reasoning about state propagation between instructions. There should be wires for registers, labels, constants, flags. Connections should be inferred from the definition in the chosen ISA.

colltoaction commented 3 months ago

WebAssembly seems like a good target being a Lisp- (or at least S-expression-) based language.

https://developer.mozilla.org/en-US/docs/WebAssembly/Understanding_the_text_format

Unachieved goals become simple in this system:

https://github.com/WebAssembly/spec/blob/master/proposals/multi-value/Overview.md