module Func_multiply_by_repeated_addition
open Pulse
open Pulse.Lib.C
#lang-pulse

divergent fn func_multiply_by_repeated_addition
    (var_x: Typedef_uint32_t.ty_uint32_t)
    (var_y: Typedef_uint32_t.ty_uint32_t)
  requires ((Typedef_uint32_t.ty_uint32_t__pred var_x 1.0R))
  requires ((Typedef_uint32_t.ty_uint32_t__pred var_y 1.0R))
  requires
    (with_pure
      (((id #int (UInt32.v var_x)) * (id #int (UInt32.v var_y))) <=
        (id #int (UInt32.v 4294967295ul))))
  returns return_1 : Typedef_uint32_t.ty_uint32_t
  ensures ((Typedef_uint32_t.ty_uint32_t__pred var_x 1.0R))
  ensures ((Typedef_uint32_t.ty_uint32_t__pred var_y 1.0R))
  ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
  ensures
    (with_pure
      ((id #int (UInt32.v return_1)) = ((id #int (UInt32.v var_x)) * (id #int (UInt32.v var_y)))))
{
  let mut var_x = var_x;
  let mut var_y = var_y;
  let mut var_ctr : Typedef_uint32_t.ty_uint32_t;
  var_ctr := 0ul;
  let mut var_acc : Typedef_uint32_t.ty_uint32_t;
  var_acc := 0ul;
  while (((!var_ctr) `UInt32.lt` (!var_y)))
    invariant ((live var_ctr) ** (live var_acc))
    invariant (with_pure
        (((!var_ctr) `UInt32.lte` (!var_y)) &&
          ((id #int (UInt32.v (!var_acc))) =
            ((id #int (UInt32.v (!var_x))) * (id #int (UInt32.v (!var_ctr)))))))
  {
    var_acc := ((!var_acc) `Pulse.Lib.C.UInt32.add_wrap` (!var_x));
    var_ctr := ((!var_ctr) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
  };
  return (!var_acc);
}