ATSLIB/prelude/array_prf

This package contains some commonly used proof functions for manipulating array-views.

array_v_split

array_v_unsplit

array_v_extend

array_v_split

Synopsis

prfun
array_v_split
  {a:vt0p}
  {l:addr}
  {n:int}{i:nat | i <= n}
(
  pfarr: array_v (INV(a), l, n)
) :<prf> @(
  array_v (a, l, i), array_v (a, l+i*sizeof(a), n-i)
) // end of [array_v_split]

Description

This proof function splits a given proof of array-view into two proofs of adjacently located array-views.

array_v_unsplit

Synopsis

prfun
array_v_unsplit
  {a:vt0p}
  {l:addr}
  {n1,n2:int}
(
  pf1arr: array_v (INV(a), l, n1)
, pf2arr: array_v (a, l+n1*sizeof(a), n2)
) :<prf> array_v (a, l, n1+n2) // end of [array_v_unsplit]

Description

This proof function is the inverse of array_v_split: It combines two proofs of adjacently located array-views into one proof of array-view.

array_v_extend

Synopsis

prfun
array_v_extend :
  {a:vt0p}
  {l:addr}{n:int}
  (array_v (INV(a), l, n), a @ l+n*sizeof(a)) -<prf> array_v (a, l, n+1)

Description

This proof function extends a proof of array-view by a proof of at-view located at the end of the array-view.

array_v_unextend

Synopsis

prfun
array_v_unextend :
  {a:vt0p}
  {l:addr}
  {n:int | n > 0}
  (array_v (INV(a), l, n)) -<prf> (array_v (a, l, n-1), a @ l+(n-1)*sizeof(a))

Description

This proof function is the inverse of array_v_extend: It decomposes a given proof of array-view of size n into a proof of array-view of size n-1 and a proof of at-view, where n is positive.

array_v_takeout

Synopsis

prfun
array_v_takeout
  {a:vt0p}
  {l:addr}
  {n:int }
  {i:nat | i < n}
(
  pfarr: array_v (INV(a), l, n)
) :<prf> vtakeout (
  array_v (a, l, n), a @ (l+i*sizeof(a))
) (* end of [array_v_takeout] *)

Description

This proof function takes out a proof of at-view from a given proof of array-view, repsenting the rest as a linear proof function that returns a proof of the original array-view when applied to a proof of the taken-out at-view.

Example

A proper implementation of array-subscripting is given as follows:

fun{a:t@ype}
array_get_at
  {n:int}{i:nat | i < n} (
  A: &(@[a][n]), i: size_t (i)
) : a = x where {
  prval (pfat, fpf) =
    array_v_takeout{..}{..}{n}{i} (view@(A))
  val x = ptr_get<a> (pfat | ptr1_add_guint<a> (addr@(A), i))
  prval () = view@(A) := fpf (pfat)
} // end of [array_get_at]

where array_v_takeout is called to generate a proof of the at-view needed for reading from cell i in the given array A.

array_v_group

Synopsis

praxi
array_v_group
  {a:vt0p}{l:addr}{m,n:int}
  (pf: array_v (INV(a), l, m*n)): array_v (@[a][n], l, m)

array_v_ungroup

Synopsis

praxi
array_v_ungroup
  {a:vt0p}{l:addr}{m,n:int}
  (pf: array_v (@[INV(a)][n], l, m)): array_v (INV(a), l, m*n)

This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi.