Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

nickbenton.name

Post reply on HN
Print view View original

71–75 of 75 posts

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

#71

Post by anthk »

dwohnitmok wrote: post #70
anthk wrote: post #27

Earlier quoted context omitted.

You use reducing rationals everywhere you can, not floast.

This is potentially horrendous for performance, and even worse, unpredictably so. Instead of getting the incorrect answer (or NaN) with floating point if you have an unfortunate series of calculations, you get extreme memory blowup, where your numerator and denominator can explode in size, which in turn leads to runtime slowdown. In the worst case you can actually run out of memory (because certain fairly natural cal…

Most people versed in fixed point (microcontroller programmers, Forth programmers) will use rationals at decent speeds because they know all the tricks for performance, kinda like HAKMEM algos applied to Forth instead of a PDP10 (and OFC the Forth Scientific Library).

https://www.inwap.com/pdp10/hbaker/hakmem/hakmem.html

Edit: link

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

#72

Post by dwohnitmok »

anthk wrote: post #71
dwohnitmok wrote: post #70

Earlier quoted context omitted.

This is potentially horrendous for performance, and even worse, unpredictably so. Instead of getting the incorrect answer (or NaN) with floating point if you have an unfortunate series of calculations, you get extreme memory blowup, where your numerator and denominator can explode in size, which in turn leads to runtime slowdown. In the worst case you can actually run out of memory (because certain fairly natural cal…

Most people versed in fixed point (microcontroller programmers, Forth programmers) will use rationals at decent speeds because they know all the tricks for performance, kinda like HAKMEM algos applied to Forth instead of a PDP10 (and OFC the Forth Scientific Library). https://www.inwap.com/pdp10/hbaker/hakmem/hakmem.html Edit: link

I don't see anywhere in HAKMEM where they advocate for the use of unbounded rational numbers.

Do you have any examples of unbounded rational numbers used in a microcontroller program, in a production Forth program, or really in any production user-facing codebase?

I ask specifically for unbounded rational numbers because again bounded rational numbers are effectively equivalent to floating point and fixed denominator rational numbers are equivalent to fixed point.

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

#73

Post by throw-qqqqq »

kragen wrote: post #62
addaon wrote: post #39

Earlier quoted context omitted.

I'd love some examples here.

So would I!

I can't give a good, covering answer without writing a wall of text, sorry in advance.

CBMC and KLEE try to statically verify assertions in one of three outcomes:

1. Verified: No counter-example was found, that breaks the assertion(s).

2. Rejected: A counter-example was found, that makes an assertion false.

3. Tool runs forever or exhausts system resources.

That means, any test/verification you can do at runtime, can be determined statically. You can use modal logics, automata, everything within practical limits.

The modeling language is also just C, which simplifies things HUGELY.

A very simple example can be found here: https://github.com/kokke/tiny-regex-c/blob/master/formal_ver... (note, this has no specific assertions, only the ones inserted automatically by the tool, to check for run-time errors like zero division, array out of bounds etc.).

For more involved examples, see https://www.cprover.org/cbmc/applications/ or https://klee-se.org/publications/

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

#74

Post by kragen »

throw-qqqqq wrote: post #73
kragen wrote: post #62

Earlier quoted context omitted.

So would I!

I can't give a good, covering answer without writing a wall of text, sorry in advance. CBMC and KLEE try to statically verify assertions in one of three outcomes: 1. Verified: No counter-example was found, that breaks the assertion(s). 2. Rejected: A counter-example was found, that makes an assertion false. 3. Tool runs forever or exhausts system resources. That means, any test/verification you can do at runtime, can…

That's fantastic, thanks! These sound like astounding systems.

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

#75

Post by throw-qqqqq »

kragen wrote: post #74
throw-qqqqq wrote: post #73

Earlier quoted context omitted.

I can't give a good, covering answer without writing a wall of text, sorry in advance. CBMC and KLEE try to statically verify assertions in one of three outcomes: 1. Verified: No counter-example was found, that breaks the assertion(s). 2. Rejected: A counter-example was found, that makes an assertion false. 3. Tool runs forever or exhausts system resources. That means, any test/verification you can do at runtime, can…

That's fantastic, thanks! These sound like astounding systems.

I would say KLEE is coolest, as it works on LLVM bitcode, so anything you can compile to that, you can verify.

CBMC scales worse (best for smaller modules, not complete systems), but is also very capable.

You can use both as general-purpose solvers for any problem you can formulate in C/LLVM. You assert that there is no solution, run the tool and (unless you run out of time/resources), you get a counter-example refuting the assertion -> which will then be a valid solution.

I’ve used this to find e.g. a sequence of N bytes with a specific (non-cryptographic) checksum etc. They are very powerful tools.

Post reply on HN