Coq: The World's Best Macro Assembler? (2013) [pdf]

https://nickbenton.name/coqasm.pdf

by addaon • 8 months ago

167 74 8 months ago

nickbenton.name

throwaway198846• 8 months ago

They are going by Rocq today

AdieuToLogic• 8 months ago

The linked PDF was created on 8/5/13.

volemo2• 8 months ago

Then the title needs (2013), no?

volemo2• 8 months ago

I understand and respect the renaming, Coq was a much cooler name though.

graemep• 8 months ago

It was.

Renaming languages to suit American taste really grates.

Nimrod to Nim was even worse. Apparently Americans cannot get Biblical references.

addaon6• 8 months ago

Poster here. I re-read this paper about once a year. I continue to think that it may be one of the most important papers I've read. As someone who works on high-reliability safety-critical real-time systems (automotive, avionics), being able to work in an environment where I could prove semantic properties of assembly code is pretty close to my dream -- the cost of demonstrating code correct is already so much higher than the cost of writing the code that the incremental cost of going to assembly seems minor, if there's even a small payback in time to demonstrate correctness. In practice, I think my dream language would be a relatively rich macro assembler plus a (guided, greedy) register allocator, designed entirely to simplify and allow semantic proofs. I don't really have a sense as to whether Coq (Rocq) is the right answer today, vs other options; or if there's a newer literature advancing this approach; but I'd truly love to see a deeper focus of making low level languages more useful in this space, rather than moving towards more constrained, higher level languages.

kragen15• 8 months ago

Have you found Coq or other formal-methods tooling useful?

addaon6• 8 months ago

No, I haven't, but I want to. I haven't had the opportunity to go deep into formal methods for a work project yet, and on personal projects I've mostly played with Ada SPARK, not Coq. I've played with Coq a little (to the extent of re-implementing the linked paper for a subset of a different ISA), but there's definitely a learning curve. One of my personal benchmark projects is to implement a (fixed-maximum-size) MMM heap in a language, and convince myself it's both correct and of high performance; and I've yet to achieve that in any language, even SPARK, without leaning heavily on testing and hand-waving along with some amount of formal proof. I've written the code and comprehensive testing in various assembly languages (again, this is sort of my benchmark bring-up-a-new-platform-in-the-brain example), and I /think/ that for the way I think proving properties as invariants maintained across individual instructions maps pretty well to how I convince myself it's correct, but I haven't had the time, depth, or toolchain to really bottom any of this out.

throw-qqqqq3• 8 months ago

I have found huge value in CBMC and KLEE for statically verifying C code for real time safety critical embedded applications.

ACL2 is also VERY powerful and capable.

nextos2• 8 months ago

I have found Isabelle very useful, and Dafny even more so.

Amazon AWS uses Dafny to prove the correctness of some complex components.

Then, they extract verified Java code. There are other target languages.

Being based on Hoare logic, Dafny is really simple. The barrier of entry is low.

quanto3• 8 months ago

During the days I was studying/working with Coq, one visiting professor gave a presentation on defense software design. An example presented was control logic for F-16, which the professor presumably worked on. A student asked how do you prove "correctness", i.e. operability, of a jet fighter and its control logic? I don't think the professor had a satisfying answer.

My question is the same, albeit more technically refined. How do you prove the correctness of a numerical algorithm (operating on a quantized continuum) using type-theoretic/category-theoretic tools like theorem provers like Coq? There are documented tragedies where numerical rounding error of the control logic of a missile costed lives. I have proved mathematical theorems before (Curry-Howard!) but they were mathematical object driven (e.g. sets, groups) not continuous numbers.

dwohnitmok5• 8 months ago

You use floating point numbers instead of real numbers in your theorems and function definitions.

This sounds flippant, but I'm being entirely earnest. It's a significantly larger pain because floating point numbers have some messy behavior, but the essential steps remain the same. I've proved theorems about floating point numbers, not reals. Although, again, it's a huge pain, and when I can get away with it I'd prefer to prove things with real numbers and assume magically they transfer to floating point. But if the situation demands it and you have the time and energy, it's perfectly fine to use Coq/Rocq or any other theorem prover to prove things directly about floating point arithmetic.

The article itself is talking about an approach sufficiently low level that you would be proving things about floating point numbers because you would have to be since it's all assembly!

But even at a higher level you can have theorems about floating point numbers. E.g. https://flocq.gitlabpages.inria.fr/

There's nothing category theoretic or even type theoretic about the entities you are trying to prove with the theorem prover. Type theory is merely the "implementation language" of the prover. (And even if there was there's nothing tying type theory or category theory to the real numbers and not to floats)

tensegrist• 8 months ago

There are documented tragedies where numerical rounding error of the control logic of a missile costed lives.

curious about this

OneDeuxTriSeiGo• 8 months ago

So the answer is that you are proving two things:

1. That the model/specification makes sense. i.e. that certain properties in the model hold and that it does what you expect.

2. That the SUV/SUT (system under verification/test) corresponds to the model. This encompasses a lot but really what you are doing here is establishing how your system interacts with the world, with what accuracy it does so, etc. And from there you are walking along the internal logic of your system and mapping your representations of the data and the algorithms you are using into some projection from the model with a specified error bound.

So you are inherently dealing with the discrete nature of the system the entire time but you can reason about that discrete value as some distribution of possible values that you carry through the system with each step either

- introducing some additional amount of error/variability or

- tightening the bound of error/variability but trapping outside values into predictable edge cases.

Then it's a matter of reasoning about those edge cases and whether they break the usefulness of the system compared against the idealised model.

auggierose• 8 months ago

Curry-Howard is not needed for theorem proving, it's just that type theorists like it.

See https://www.cl.cam.ac.uk/~jrh13/papers/thesis.html for your question, John Harrison got a job with Intel based on this after their floating point disaster.

But in short: theorem proving is not about equalities, it is about inequalities. And theorems about numerical algorithms are a great example of this.

sylware• 8 months ago

The second your macro-assembler has a significantly complex syntax, you are done: feature creep for 2042 features then 2043 then 2044... and it mechanically reduces the number the alternative implementations and make the effort required to develop a new more and more unreasonable.

In this end, it is all about the complexity and stability in time for this matter.

quanto3• 8 months ago

This paper reminds me of a class assignment in grad school where the prof asked the students to write a compiler in Coq for some toy Turning-complete language in a week. Having no background in compiler design or functional programming, I found it daunting at first, but eventually managed it. The Coq language's rigor really helps with something like this.

I wonder if AI's compute graph would benefit from a language-level rigor as of Coq.

kragen15• 8 months ago

The canonical URL, dating back to at least 02015, may be http://research.microsoft.com/en-us/um/people/nick/coqasm.pd..., which now redirects to https://www.microsoft.com/en-us/research/publication/coq-wor.... This site presumably belongs to the Nick Benton who is one of its authors.

asdefghyk• 8 months ago

The x86 architecture and instruction set is complex - so it absolutely needs a powerful assembler to help prevent mistakes.

kragen15• 8 months ago

That doesn't seem right to me. If the problem is that it has too many instructions and addressing modes, you can decide to only use a small subset of those instructions and addressing modes, which really isn't much of a handicap for implementing functionality. (It doesn't help with analyzing existing code, but neither does a powerful assembler.)

I'm no expert on assembly-language programming, but probably 90% of the assembly I write on i386, amd64, RISC-V, and ARM is about 40 instructions: ldr, mov, bl, cmp, movs, push, pop, add, b/jmp, bl/blx/call, ret, str, beq/jz, bne/jnz, bhi/ja, bge/jge, cbz, stmia, ldmia, ldmdb, add/adds, addi, sub/subs, bx, xor/eor, and, or/orr, lsls/shl, lsrs/sar/shr, test/tst, inc, dec, lea, and slt, I think. Every once in a while you need a mul or a div or something. But the other 99% of the instruction set is either for optimized vectorized inner loops or for writing operating system kernels.

I think that the reason that i386 assembly (or amd64 assembly) is error-prone is something else, something it has in common with very simple architectures and instruction sets like that of the PDP-8.

yjftsjthsd-h• 8 months ago

I think that the reason that i386 assembly (or amd64 assembly) is error-prone is something else, something it has in common with very simple architectures and instruction sets like that of the PDP-8.

What reason is that? (And, if it's not obvious, what are ARM/RISC-V doing that make them less bad?)

mmastrac• 8 months ago

It's a bit of an awkward syntax to get a reliable assembler. Does it at least allow you to prove the behaviour of a larger block of assembly? For example, could I use it to prove that a block of assembly is equivalent to a given set of operations?

kragen15• 8 months ago

Yes.

anthk3• 8 months ago

A Lisp can mimic Prolog and the rigour of Coq with ease.

attila-lendvai• 8 months ago

i'm a long time lisper, but i don't think this is justified.

implementing prolog/backtracking on top of lisp is certainly possible and not even too hard (see e.g. https://github.com/nikodemus/screamer)

and implementing Coq on top of lisp is also possible.

but IMO the "with ease" phrase is not justified in this context.

if you only mean that lisp will not be in the way if you set out to implement these, then i agree. lisp -- the language and the typical opensource implementation -- will be much less of an obstacle than other languages when chosen as foundations.

addaon6• 8 months ago

Can you give an example? With something like Figure 1 of the paper converted to a convenient form for Lisp (s-expressions, presumedly), and assuming a function to convert it to binary, what would it look like to prove correctness of that assembly in Lisp? What's the ecosystem of proof assistants that would get you there?

kragen15• 8 months ago

You can write a prover like Coq in a Lisp, but, though it's easier than doing it in C, I think it's somewhat harder than doing it in something like OCaml. ACL2 is an example of such a thing.

dang• 8 months ago

Discussed at the time:

Coq: The world’s best macro assembler? (2013) [pdf] - https://news.ycombinator.com/item?id=8752385 - Dec 2014 (61 comments)

Svoka• 8 months ago

This is great. I honestly never thought of computer as a register state and instructions/asm commands as functions applied to it. But that makes so much sense.

peter_d_sherman• 8 months ago

"3. Assembling x86

A particular emphasis of our work on machine code verification is on using Coq as a place to do everything: modelling the machine, writing programs, assembling or compiling programs, and proving properties of programs.

Coq’s powerful notation feature makes it possible to write assembly programs, and higher-level language programs, inside Coq itself with no need for external tools."

Looks very promising! There is definitely something here!

Coq: The World's Best Macro Assembler? (2013) [pdf]

Related Stories