index
:
yellowsquid/helium.git
abstract
axiomatic
dev/bitvec-arith
last-attempt
master
[no description]
Chloe Brown
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
Age
Commit message (
Collapse
)
Author
2022-01-07
Introduce semantics for sequences of instructions.
Greg Brown
2022-01-07
Rename ⟦_⟧ to float.
Greg Brown
2021-12-28
Make the denotational semantics total.
Greg Brown
2021-12-27
Introduce Everything.agda to aid in overall compilation.
Greg Brown
2021-12-21
Define execBeats, a wrapper to execute beat-wise instructions.
Greg Brown
2021-12-21
Define semantics of vqdmulh.
Greg Brown
2021-12-21
Define semantics for vmulh.
Greg Brown
2021-12-20
Define vsub.
Greg Brown
2021-12-20
Remove bitstring addition.
Greg Brown
2021-12-20
Extract structures shared by most binary vector operations.
Greg Brown
This is the extraction promised a couple of commits ago.
2021-12-20
Define vmul.
Greg Brown
2021-12-20
Inline and rearrange to make vadd and vhsub look more similar.
Greg Brown
If there are other functions with a similar structure, I may extract larger patterns. copy-masked is one example of a structure that was easy to extract.
2021-12-20
Define semantics of vhsub.
Greg Brown
2021-12-20
Improve type-checking efficiency.
Greg Brown
2021-12-20
Define semantics for vadd.
Greg Brown
2021-12-20
Add references to the core denotational semantics.
last-attempt
Greg Brown
2021-12-20
Add some convenience functions.
Greg Brown
2021-12-19
Define core of denotational semantics.
Greg Brown
2021-12-19
Define a minimal interface for working with Arm pseudocode.
Greg Brown
