type state = {
  w : int; (* current wind speed *)
  y : int; (* y-position of the vehicle *)
  v : int; (* accumulated velocity *)
}

let controller sgn_y sgn_old_y =
  (-3 * sgn_y) + (2 * sgn_old_y)

let sgn x =
  if x < 0 then -1
  else if x = 0 then 0
  else 1

let next_state dw s =
  { w = s.w + dw;
    y = s.y + s.v + s.w + dw;
    v = s.v +
        controller
          (sgn (s.y + s.v + s.w + dw))
          (sgn s.y)
  }

let arbitrary_delta_ws = List.for_all (fun x -> x = -1 || x = 0 || x = 1)

let rec final_state s dws =
  match dws with
  | [] -> s
  | dw :: dws' ->
    let s' = next_state dw s in
    final_state s' dws'
[@@adm dws]

let good_state s =
  match s.y, s.w + s.v with
  | -3, 1 -> true
  | -2, 1 -> true
  | -2, 2 -> true
  | -1, 2 -> true
  | -1, 3 -> true
  | 0, -1 -> true
  | 0, 0  -> true
  | 0, 1  -> true
  | 1, -2 -> true
  | 1, -3 -> true
  | 2, -1 -> true
  | 2, -2 -> true
  | 3, -1 -> true
  | _ -> false

theorem safety_1 s dw =
  good_state s
  && (dw = -1 || dw = 0 || dw = 1)
 ==>
  good_state (next_state dw s)
[@@rw]


lemma all_good s dws =
  good_state s && arbitrary_delta_ws dws
  ==>
  good_state ((final_state s dws))
[@@by induct ~on_fun:[%id final_state] ()]
[@@disable next_state, good_state]

type t = bool list

(* little-endian encoding, e.g., 2 is [false; true] *)
let rec of_nat n =
  if n <= 0 then []
  else (n mod 2 <> 0) :: of_nat (n / 2)

eval of_nat 2
eval of_nat 8
eval of_nat 255

let rec pow_2 n =
  if n <= 0 then 1
  else 2 * (pow_2 (n-1))

eval pow_2 3

let rec to_nat_aux bs p =
  match bs with
  | b::bs ->
    (if b then pow_2 p else 0)
    + to_nat_aux bs (p+1)
  | [] -> 0

let to_nat bs = to_nat_aux bs 0

eval (to_nat (of_nat 8))

let rec bv_op f (xs:bool list) (ys:bool list) =
    match xs, ys with
    | [], y::ys -> (f false y) :: bv_op f [] ys
    | x::xs, [] -> (f x false) :: bv_op f xs []
    | x::xs, y::ys -> (f x y) :: bv_op f xs ys
    | _ -> []
[@@adm xs,ys]

eval (bv_op (fun x y -> x) [] [false;false])

let bv_and xs ys = bv_op (fun x y -> x && y) xs ys
let bv_xor xs ys = bv_op (fun a b -> a <> b) xs ys

(* little-endian shl just prepends 0 on the left! *)

let bv_shl bs =
    false :: bs

eval to_nat (bv_shl (of_nat 2))

lemma _ a b c =
  bv_and [a;b;c] [a;b;c] = [a;b;c]
[@@by auto]

verify (fun a b c ->
  bv_xor [a;b;c] [a;b;c] = [false; false; false]
)

let rec add_two_numbers_without_using_arithmetic_operators x y =
    if to_nat y = 0 then x else (
      let carry = bv_and x y in
      let x = bv_xor x y in
      let y = bv_shl carry in
      add_two_numbers_without_using_arithmetic_operators x y)
[@@no_validate]

(* evaluates to 51 *)
eval (to_nat (add_two_numbers_without_using_arithmetic_operators (of_nat 20) (of_nat 31)))

let add_fun_correct n m =
    (to_nat (add_two_numbers_without_using_arithmetic_operators (of_nat n) (of_nat m)) = n + m)

verify (add_fun_correct 0 0)
verify (add_fun_correct 0 1)
verify (add_fun_correct 1 0)

(* correctness for unsigned ints expressible in 4 bits! *)
lemma foo n m a b c d e f g h =
  of_nat n = [a;b;c;d]
  && of_nat m = [e;f;g;h]
  ==>
  add_fun_correct n m
[@@by unroll 200]