Skip to content

Instantly share code, notes, and snippets.

@ttaubert
Last active February 7, 2017 00:06
Show Gist options
  • Save ttaubert/ecf5b710e849ddfefa81c14a70631eec to your computer and use it in GitHub Desktop.
Save ttaubert/ecf5b710e849ddfefa81c14a70631eec to your computer and use it in GitHub Desktop.
#include <stdint.h>
uint8_t add(uint8_t a, uint8_t b) {
uint8_t sum = a + b;
return sum < a ? UINT8_MAX : sum;
}
m1 <- llvm_load_module "add.bc";
m2 <- llvm_load_module "cadd.bc";
add <- llvm_extract m1 "add" llvm_pure;
cadd <- llvm_extract m2 "add" llvm_pure;
let thm = {{ \x y -> add x y == cadd x y }};
prove_print abc thm;
#include <stdint.h>
// 0xff if MSB(x) = 1 else 0x00
uint8_t msb(uint8_t x) {
return 0 - (x >> (8 * sizeof(x) - 1));
}
// 0xff if a < b else 0x00
uint8_t lt(uint8_t a, uint8_t b) {
return msb(a ^ ((a ^ b) | ((a - b) ^ b)));
}
uint8_t add(uint8_t a, uint8_t b) {
return (a + b) | lt(a + b, a);
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment