mrLSD-dev

5 ms·

1.
F# RISC-V v0.6.0 released(github.com)
4 points by mrLSD-dev 4mo ago|0 comments
2.
Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny(arxiv.org)
1 points by mrLSD-dev 11mo ago|0 comments
3.
by mrLSD-dev 1y ago
Swift EVM supports any build target, including Windows.
4.
Swift EVM (Ethereum Virtual Machine) new release v0.5.13(github.com)
2 points by mrLSD-dev 1y ago|3 comments
5.
Aurora EVM rust library: Cancun hard fork release(github.com)
1 points by mrLSD-dev 2y ago|0 comments
6.
Custom Semantic Analyzer library written Rust lang(github.com)
19 points by mrLSD-dev 3y ago|0 comments
7.
Rust library semantic-analyzer-rs for creating subset of compilers(github.com)
2 points by mrLSD-dev 3y ago|1 comments
8.
by mrLSD-dev 3y ago
Research project, rust library for creating subset of compilers and programming languages
9.
by mrLSD-dev 3y ago
Just out of curiosity, what about that: https://people.csail.mit.edu/bthom/riscv-spec.pdf
10.
by mrLSD-dev 3y ago
I completely agree. And I specifically draw your attention to the fact that this is not a formal verification, which it would be reasonable to do: Coq, Isabellll, Agda, F* etc. However, Formal Specification. Those. representation of the spe
11.
by mrLSD-dev 3y ago
You can easily import and use specific functions for the decoder, or executor for specific ISA. Or even use the whole state machine. And this is represented by tests. Those. any single RISC-V architecture instruction, or an entire program.
12.
by mrLSD-dev 3y ago
It's possible to emulate. But not only. The main goal is to formalize the representations of the RISC-V instruction set (ISA), decoder, executor, and state machine. So it's more formal point of view for RISC-V ISA.
13.
by mrLSD-dev 3y ago
unfortunately not, because it does not apply directly to ISA. However, the idea is interesting.
14.
by mrLSD-dev 3y ago
The main competitor of Haskell, and also not the most popular language. However, the only way to popularize a language is to write in it. This project is trying to reveal the possibility of F#, and show the worthy side of F#,
15.
by mrLSD-dev 3y ago
Due to the properties of F# as a functional language, using a pure representation of functions and a strong type system - in this case, this is a formalization of RISC-V ISA (instruction set). Since we don't have side effects for pure
16.
by mrLSD-dev 3y ago
Since F# is a functional language, it allows, using a purely functional approach and a system of strong types, pure functions, to formally verify the correctness of a particular ISA. The emulator is nothing more than a side effect.
17.
F# RISC-V Instruction Set formal specification(github.com)
134 points by mrLSD-dev 3y ago|42 comments
18.
by mrLSD-dev 3y ago
RISC-V CPU formal specification written on F#. Formalazation of RISC-V ISA architecture.