module Website.VectorAdd

#lang-pulse

open Kuiper
open Kuiper.Tensor
open Kuiper.Tensor.Layout.Alg
module Map = Kuiper.Kernel.Map

#push-options "--z3rlimit 10"

fn vector_add
  (n : szp { n <= max_blocks * max_threads })
  (a : array1 f32 (l1_forward n) { is_global a })
  (b : array1 f32 (l1_forward n) { is_global b })
  (out : array1 f32 (l1_forward n) { is_global out })
  preserves cpu **
    on gpu_loc (a |-> 'a) ** on gpu_loc (b |-> 'b)
  requires on gpu_loc (out |-> 'old)
  ensures on gpu_loc
    (out |-> mk1 (fun i -> add (acc1 'a i) (acc1 'b i)))
{
  Map.map_gpu2_to add n a b out;
}

#pop-options