Conflicting requirements in proof functions

[Mark Thom]

I'm trying to use dataviewtypes to implement a growable, malloc allocated vector type.

I defined the vector type like so:

dataview vector_v (a:vt@ype+, addr, int) =
  | {l:addr} vector_v_nil (a, l, 0)
  | {l:addr} {n:nat} vector_v_cons (a, l, n+1) of (a? @ l, vector_v (a, l+sizeof(a), n))

datavtype vector_vt (a:vt@ype+, addr, int) =
  | {l:addr} {n:nat} vector_vt(a, l, n) of (vector_v (a, l, n) | ptr(l))

I want to write a proof function to convert the view bytes_v(l, n * sizeof(a)) (= @[byte?][n] @ l) to vector_v (a, l, n),

but I'm confused by some conflicting requirements given by patscc. I've written these functions:

praxi bytes_v_to_at_view :
  {a:vt0p}{l:addr}
  ( bytes_v(l, sizeof(a)) ) -> a? @ l

prfun bytes_v_to_vector_v{a:vt0p}{l:agz}{n:pos} (
  pf: bytes_v (l, n * sizeof(a))
):<> vector_v (a, l, n)

primplement bytes_v_to_vector_v{a}{l}{n} (pf) = let
  prfun loop{n:nat} .<n>. ( pf: bytes_v(l, n * sizeof(a)) ): vector_v(a, l, n) =
    sif n > 0 then let
        prval (pf1, pf2bytes) = bytes_v_split{l}{n*sizeof(a)}{sizeof(a)}(pf) // should return (pf1: bytes_v (l, sizeof(a)), pf2bytes: bytes_v (l+sizeof(a), (n-1)*sizeof(a)))
        prval pfa = bytes_v_to_at_view(pf1)
      in
        vector_v_cons (pfa, loop(pf2bytes))
      end
    else
      vector_v_nil ()
 in
  loop(pf)
 end

First, I'm not sure how else to write bytes_v_to_at_view. Is a praxi appropriate here? Wouldn't a

castfn make more sense since what I'm after is a pointer cast? I thought praxi was intended for

stating axioms.

Second, patscc reports two error messages regarding bytes_v_to_vector_v. The first is that the dynamic variable

pf is consumed but needs to be retained by bytes_v_to_vector_v, and the second is that pf is retained but needs to

be consumed by loop. pf is described as a "dynamic variable" of bytes_v_to_vector_v, but a "linear dynamic variable"

of loop.

This is all very confusing. Is pf a linear variable in one context, but not the other? Shouldn't it be a static variable?

[Hongwei Xi]

I went ahead to fix several issues.

1)

The built-in constraint-solver of ATS cannot handle integer inequality involving

multiplication. You may want to use Z3 for constriant-solving. It should give you a much

better experience.

2)

The typechecker does not know that a zero-length bytes_v contains no resources.

It is the programmers obligation to eliminate it.

3. The original loop did not work (as it was not polymorphic on 'l'); it has been fixed.

In practice, I would just skip proving bytes_v_to_vector and treat it as a praxi instead:
Theorems are "always" correctly stated but implementations "always" contain bugs :)

############

staload UN = "prelude/SATS/unsafe.sats"

extern

praxi
bytes_v_to_at_view :
  {a:vt0p}{l:addr}
  ( bytes_v(l, sizeof(a)) ) -> a? @ l

extern

prfun
bytes_v_to_vector_v
{a:vt0p}{l:agz}{n:pos}

(pf: bytes_v (l, n * sizeof(a))):<> vector_v (a, l, n)

primplement
bytes_v_to_vector_v{a}{l}{n}(pf) = let

stadef asz = sizeof(a)
prval () = $UN.prop_assert{asz >= 0}()

prfun
loop{l:addr}{n:nat} .<n>.
(pf: bytes_v(l, n * sizeof(a)) ): vector_v(a, l, n) =

sif n > 0 then
let

  prval () = $UN.prop_assert{n*asz >= asz}()
  prval (pf1, pf2bytes) =
  bytes_v_split{l}{n*asz}{asz}(pf) // should return (pf1: bytes_v (l, sizeof(a)), pf2bytes: bytes_v (l+sizeof(a), (n-1)*sizeof(a)))

  prval pfa = bytes_v_to_at_view(pf1)
in

  vector_v_cons (pfa, loop{l+asz}{n-1}(pf2bytes))
end
else
let
prval () =
$UN.prop_assert{n*asz==0}()
prval () = array_v_unnil(pf)
in
  vector_v_nil ()
end

in
  loop(pf)
end

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/4820775f-70d0-4578-b42b-1643908b29c8%40googlegroups.com.

[gmhwxi]

Strictly speaking, the following lemma needs

to assume that 'l' is "well-aligned":

prfun
bytes_v_to_vector_v
{a:vt0p}{l:agz}{n:pos}
(pf: bytes_v (l, n * sizeof(a))):<> vector_v (a, l, n)

Also, vector_v(a, l, n) should be changed to vector_v(a?, l, n).

Program verification is really just a form conditional verification

of some sort. Implicit assumptions are made all the time in practice.

[Mark Thom]

I see your point about the alignment, I think, but why is the vector_v(a?, l, n) necessary? The at-view (a? @ l) is already part of the vector_v definition.

[gmhwxi]

I see. I missed it.

Then differentiating an uninitialized vector from an initialized one is now a problem.

[Mark Thom]

Yes, I see your point.

[Mark Thom]

OK, I'm making gradual progress on this. This is the next bit of code:

extern praxi vector_v_to_b0ytes_v{a:vt0p}{l:agz}{n:nat}
  ( vector_v(a, l, n) ): b0ytes_v(l, n * sizeof(a))

fun imul{n,m:int}(n: int(n), m: int(m)): (MUL(n, m, n*m) | int(n*m)) =
  (mul_make{n,m}() | n*m)

fun{a:vt0p}
make_vector_vt{n:nat}(
  n: int(n)
): [l:addr] option_vt(vector_vt(a?, l, n), l > null) = let
  val (pf | sz) = imul(n, sz2i(sizeof<a>))
  prval () = mul_nat_nat_nat(pf) // $UN.prop_assert{n * sizeof(a) >= 0}()
  val [l:addr] (pfopt | p) = malloc_libc{n * sizeof(a)}(i2sz(sz))
in
  case+ pfopt of
  | malloc_libc_v_succ(pfbytes, pfmfree) =>
    option_vt_some(vector_vt(pfmfree, b0ytes_v_to_vector_v{a}{l}{n}(pfbytes) | p))
  | malloc_libc_v_fail() =>
    option_vt_none()
end   

fun{a:vt0p}
free_vector_vt {l:agz}{n:int}
(
  v: vector_vt(a, l, n)
): void = let
    val ~vector_vt (pmfree, pfv_v | p) = v // notice the errors that are produced if we omit ~!
    prval pfBytes = vector_v_to_b0ytes_v(pfv_v)
  in
    mfree_libc(pfBytes, pmfree | p)
  end

free_vector_vt seems to pass the typechecker, but make_vector_vt does not. I don't know how to prove

that l > null is false in the malloc_libc_v_fail case.

[Hongwei Xi]

The following code would not work  (even if it could pass typechecking):

case+ pfopt of
  | malloc_libc_v_succ(pfbytes, pfmfree) =>
    option_vt_some(vector_vt(pfmfree, b0ytes_v_to_vector_v{a}{l}{n}(pfbytes) | p))
  | malloc_libc_v_fail() => option_vt_none()

Note that pfopt is a proof value, which is erased after typechecking. The proper way

to do this is doing something like:

if

p > the_null_ptr

then let

   prval malloc_libc_v_succ(pf) = pfopt

in

   ...

end

else let

  prval malloc_libc_v_fail() = pfopt

in

  ...

end

I would like to point out that it is very difficult to code like what you are doing (which I did

in the past). These days I mostly try to use the type system of ATS to do what I call 'static debugging':

http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x4387.html

--

You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/dca64a29-e014-4901-9173-25763452c7e8%40googlegroups.com.