add.c

## add.c
#include <stdint.h>

uint8_t add(uint8_t a, uint8_t b) {
  uint8_t sum = a + b;
  return sum < a ? UINT8_MAX : sum;
}

## add.saw
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;

## cadd.c
#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);
}