Module StoreVec

Function set_store_default


unchecked eff * -> * -> * ! <@public>

pub extern fn set_store_default
[
N : Nat,
@D
]
(  ref st : store[uint[N], uint[N]] $pre @D,
   def : bool $pre @D
) 
-> () $pre @public

Setting if the given $pre store uses a default value when looking up a missing key or not (if set to false, a failure occurs in such case).

Function store_new


pub  fn store_new
[
N : Nat,
$S,
@D
]
(   writeOnce : bool $pre @public,
   contiguous : bool $pre @public,
   def : bool $pre @public
) 
-> Store[N, $S, @D] $pre @public

where

  Field[N]

A new empty store with given parameters: writeOnce being true means that the value for every key is set at most once; contiguous being true means that the used keys are consecutive; def being true means that a default value is returned if a missing key is looked up. It is up to the programmer that the conditions assumed by writeOnce and contiguous be valid.

Function store_new_def


pub  fn store_new_def
[
N : Nat,
$S,
@D
]
() 
-> Store[N, $S, @D] $pre @public

where

  Field[N]

A new empty store with no writing once or contiguity assumptions and using a default value.

Function store_new_nodef


pub  fn store_new_nodef
[
N : Nat,
$S,
@D
]
() 
-> Store[N, $S, @D] $pre @public

where

  Field[N]

A new empty store with no writing once or contiguity assumptions and not using a default value.

Function store_read


pub  fn store_read
[
N : Nat,
$S,
@D
]
(  ref st : Store[N, $S, @D] $pre @public,
   key : uint[N] $S @D
) 
-> uint[N] $S @D

where

  Field[N]

Getting the value that corresponds to the key given as the second argument in the store given as the first argument.

Function store_read_vec


pub  fn store_read_vec
[
N : Nat,
@D
]
(  ref st : Store[N, $post, @D] $pre @public,
   keys : arr[uint[N] $post @D] $pre @public
) 
-> arr[uint[N] $post @D] $pre @public

where

  Vectorization

The array of values that correspond to the keys in the array given as the second argument in the $post store given as the first argument.

Function store_write


pub  fn store_write
[
N : Nat,
$S,
@D
]
(  ref st : Store[N, $S, @D] $pre @public,
   key : uint[N] $S @D,
   val : uint[N] $S @D
) 
-> () $pre @public

Setting the value given as the third argument to correspond to the key given as the second argument in the store given as the first argument.