search

au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

CorresProof theory file fails for a swapping function (master branch) #377

Open amblafont opened 4 years ago

amblafont commented 4 years ago 
type Example = {ptr : U8}
type Example2 = { ptr2 : U8}

main : (Example, Example2) -> (Example, Example2)
main (r {ptr}, r2 {ptr2}) =
  (r { ptr = ptr2}, r2 { ptr2 = ptr})

The last lines of CorresSetup shows that some take/put lemmas fail to be proven by the automatic tactics.

amblafont commented 3 years ago

Actually, the put lemmas also fails with the following simplest example:

idA : { a : U8 } -> { a : U8 }
idA r { a } = r { a }

idB : { b : U8 } -> { b : U8 }
idB b = b

I believe the problem is that the putboxed tactic doesn't work when two essentially identical cogent types are compiled to different (although isomorphic) C types.

amblafont commented 3 years ago

I think the problem happens whenever two cogent types having the same representation are compiled to different C types.

The problem is in the relation between C heaps h and the update semantics environment σ (assigning pointers to values): this relation basically states that given any C type τ corresponding to a cogent type t, and any pointer p, if σ(p) has the "representational" type t, then h_τ(p) should relate to σ(p). But, if two cogent types have the same representation, then this relation is not preserved when updating a record in place, therefore the hypotheses of lemma all_heap_rel_updE can never be satisfied in the put boxed tactic. The reason is that on the C side, we only update the heap corresponding to the C record, but not the other heaps corresponding to the same "representational" cogent type.

With dargent, the issue is currently even more visible because the representation does not mention the layout, so the issue would occur if the same type is used with different layouts.

Possible fixes that I can think of (by decreasing order of preference / increasing amount of work):

  1. change the monadic-update correspondence statement so that it includes another environment remembering which C type is at such location (could this idea be upstreamed in AutoCorres ?).
  2. lift the heap abstraction in the update semantics
  3. do not rely on the heap abstraction feature of AutoCorres
amblafont commented 3 years ago

This branch seems to solve this issue: https://github.com/amblafont/cogent/tree/heapabsptrsigma

amblafont commented 3 years ago

In this branch above, the type relation is no longer necessary. Christine suggests an alternative fix : put the field names in the type representation. For the dargent case, it should be enough to assign layouts to the record type representation / update value.