Deliberately "unfixed" a carry bug in the code, CBMC was able to catch it in 5 minutes using the Z3 solver.

Added a tricky optimization, saves 2 cycles, but I'm afraid it's sometimes wrong. But CBMC proved its correctness, magic.

Managed to save yet another cycle with the help from the formal verifier.

Someone should make a video tutorial on formal verification and name it "Bugs DESTROYED by FACTS and LOGIC!11!" Of all things that use this stupid meme, this will be the only legit one...

> size of program expression: 50300 steps
> Generated 8194 VCC(s)
> Running SMT2 QF_AUFBV using Z3

I don't think the solver is able to answer this huge problem. Anyway, I'll know when I wake up tomorrow...

#Why3 looks like an interesting platform. Unfortunately, little documentation exists for WhyML as a standalone programming language. Unless you're already have ML/OCaml/F# experience, all can you do is asking "why" 3 times. It comes with a handy IDE that lists all the goals and options you need to prove a program, but something is missing: for newcomers the first goal should always be "close the IDE, go and learn Standard ML for 2 months before you come back..."

Cryptoline looks like the most complete solution for verifying crypto code for now. But the toolchain couldn't fully understand bitwise operations. A simple add routine requires 83 TODO items.

Still can't understand the purpose of adding precondition and postcondition to bitshift instructions... Time to start nagging the researchers with my clueless emails.

Found the answer without nagging the researchers. It's in the 5th research paper, previously I only checked 4 papers...

Lesson learned: spending 2 days to hack the code can easily save an hour of paper reading.

GCC optimizes an 1-bit leftshift on a 17-bit integer to...

addl %eax, %eax
andl $0x1FFFE, %eax

The unused top 15 bits are cleared, which makes sense. But why does it clear the 0th bit too? It's guaranteed to be 0 unless my understanding of a computer is horribly wrong. Spent 20 minutes on this question... I was overthinking it, it's probably just a meaningless compiler artifact.

Verifying the complied Cryptoline assembly code from C, which itself is a model of the PDP-11 assembly code, is a futile attempt. After C optimization, logic is different and useful invariants disappear. New idea: write an assembler to convert PDP-11 assembly directly to the Cryptoline verification language - both are at the assembly level and should be easier to work with.

Wrote the quickest and ugliest Python script for that.

My PDP-11 to Cryptoline assembler is working, just got my first successful verification attempt in Cryptoline.

I still have difficulties on verifying the full PDP-11 multiplication routine. Arguing with #Singular on the correctness of the math is not fun at all - the actual equation it's verifying looks like this... Good luck if the output is not zero. This is how humanity ends.

Ha! Problem solved. The formal verification was failing because my code has a typo!

#Singular: I told ya so but you didn't believe me...

Just verified 800 lines of unrolled PDP-11 assembly code for 120 x 120 = 240 bit bignum multiplication using the #Cryptoline verification tool and my script. This routine uses 16-bit words to represent radix-15 integers, correctness is not obvious. It's amazing that #Singular can solve these crazy equations in 0.1 seconds.

Finished formal verification for PDP-11 column-wise (Comba) bignum multiplication, should be 20% faster than row-wise multiplication. The messy macro assembly macros are difficult for humans to audit, but not a problem for #Cryptoline, #Boolector and #Singular. Next step: implementing and verifying Karastuba multiplication.

@niconiconi I'd have guessed, it's because of possible interference with ADC (add with carry) instruction, but IDK, ADD unlike ADC.

@amiloradovsky I thought about it too, the 17-bit integer is simulated using 32-bit word, it should never carry out, and ADD ignores the carry flag. Perhaps it's useful on other architectures. Still, I can't think of a computer that doesn't allow you to ignore the carry flag, other than the 6502.

@amiloradovsky @niconiconi It's probably because the compiler has a function to generate a bitmask, and it takes a starting bit and a length. The length is going to be 16, but the starting bit is also 16 (the 17th bit), so the mask will have a total of 16 1s in it, leaving bit 0 ... 0.

@niconiconi this looks immensely useful to me. i know enough crypto to know how easy it is to fake but i keep getting tasked with evaluating draft implementations.