Proofs out of thin air

Google Group
1

From time to time, I feel the need to say something
about proof construction involved in ATS programming :slight_smile:

Suppose we have got an array A of the type arrayref(T, N).
In other words, A is a persistent array of size N in which each
store element is of type T. Given an offset I and a natural number
J such that I+J <= N, it is obvious that there is a subarray
of size J located at A+I (where A refers to the starting location
of the array). How can we get out this subarray for use temporarily?

Yes, we could try to do it safely but that is not easy. It may
need years of training for someone to pick up this kind of skill.
Instead, let us do it by creating some proof out of thin air:

staload
UN = “prelude/SATS/unsafe.sats”
//
extern
fun
{a:t@ype}
arrayref_get_subarray
{n:int}
{i,j:nat|i+j <= n}
(
A: arrayref(a, n), size_t(i)
) : [l:addr] (array_v(a, l, j), array_v(a, l, i) -> void | ptr(l))
//
implement
{a}(tmp)
arrayref_get_subarray
(A, i) = $UN.castvwtp0(ptr_add(arrayref2ptr(A), i))
//
(* ****** ****** *)

A typical use of arrayref_get_subarray looks like this:

val (pf, fpf | p) = arrayref_get_subarray (A, i)
…
prval ((returned)) = fpf(pf) // the subarray is returned after this

This gist here is:

  1. you should describe clearly what you want (the type of
    arrayref_get_subarray)
  2. but you may simply use $UN.cast to bypass proof construction
2

I fixed some typos. See a running version here:

https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST20/test24.datsOn Sunday, October 25, 2015 at 1:01:45 PM UTC-4, gmhwxi wrote:

From time to time, I feel the need to say something
about proof construction involved in ATS programming :slight_smile:

Suppose we have got an array A of the type arrayref(T, N).
In other words, A is a persistent array of size N in which each
store element is of type T. Given an offset I and a natural number
J such that I+J <= N, it is obvious that there is a subarray
of size J located at A+I (where A refers to the starting location
of the array). How can we get out this subarray for use temporarily?

Yes, we could try to do it safely but that is not easy. It may
need years of training for someone to pick up this kind of skill.
Instead, let us do it by creating some proof out of thin air:

staload
UN = “prelude/SATS/unsafe.sats”
//
extern
fun
{a:t@ype}
arrayref_get_subarray
{n:int}
{i,j:nat|i+j <= n}
(
A: arrayref(a, n), size_t(i)
) : [l:addr] (array_v(a, l, j), array_v(a, l, i) → void | ptr(l))
//
implement
{a}(tmp)
arrayref_get_subarray
(A, i) = $UN.castvwtp0(ptr_add(arrayref2ptr(A), i))
//
(* ****** ****** *)

A typical use of arrayref_get_subarray looks like this:

val (pf, fpf | p) = arrayref_get_subarray (A, i)
…
prval ((returned)) = fpf(pf) // the subarray is returned after this

This gist here is:

  1. you should describe clearly what you want (the type of
    arrayref_get_subarray)
  2. but you may simply use $UN.cast to bypass proof construction