Support access to type instance

[melodyoncode]

depends-on florianschanda/PyVCG#6

[florianschanda]

I will help out here because this is a very tricky topic

[florianschanda]

@melodyoncode my personal laptop broke - it will take me a bit of time to get to this. But I promise to do so.

[melodyoncode]

Hi @florianschanda ,
Thanks for letting me know! Totally understand—take your time to get your laptop sorted. I really appreciate your help on this whenever you’re able to.
I noticed that the pyvcg release has already been updated. Should I go ahead and update the pyvcg version for testing here?
And if there’s anything in TRLC that I can adjust or improve meanwhile, just let me know!

[florianschanda]

A few thoughts so far.

• PyVCG can be updated, but it's not required for this change
• I think the comment on performance degradation is unwarrented
• I think a new feature on checks would be interesting, something to categorise checks into two buckets:
  • Checks that run immediately when record object is declared (before references are resolved, meaning you cannot use field access inside these checks
  • Checks that run after references, assuming all immediate checks on all objects have passed

That would allow you to rely on some properties when referring to linked objects; instead of having to check everything to avoid errors.

[florianschanda]

Hi @melodyoncode I have a working laptop again, and I just wanted to assure you I have not forgotten about this feature.

[melodyoncode]

Hi @florianschanda,
Awesome! I’m glad to hear your laptop’s back in action 😊.
No worries, we can continue whenever it’s convenient for you.
And Merry Christmas! 🎄

(Just quietly saying, maybe we can stick to minimal changes.)

[florianschanda]

It's not. It's a new laptop :D

I have been thinking about this problem more, and I think I have now figure out all the issues.

We need to tighten up the semantics of when checks are evaluated. I think the correct form will be:

1. after references are resolved
2. in unspecified order, we pick an arbitrary record object and
   1. checks are first evaluated on nested tuple fields (in unspecified order, this part is missing)
   2. checks are then evaluated on the container record

I believe the UF way to access record fields will work. It'll give us, for free:

• if ref A = ref B then we know that all fields in A will be equal to all fields in B
• if all fields in A are equal to all fields in B, then we do not know that A = B (this is what we want)

We do need to emit quantifiers to enforce some type constraints, there is no way around this. Specifically for arrays we need to enforce min/max bounds, and we also need to take care of frozen record fields. (Although that one we can probably do without a quantifier.)

[florianschanda]

There are some complications when tuples interact with records. For example this test is kinda fun:

package Test_5

type R {
  value Integer
}

tuple T {
  first  R
  second R
}

checks T {
  first.value < second.value, fatal "potato"
}

type Q {
  pair T
  goal optional Boolean
}

checks Q {
  pair.first.value >= 0, fatal "kitten"
  goal, "goal"
}

This actually uncovered a pre-existing in evaluation bug that I'll fix.

[florianschanda]

I found some additional issues:

• There are pre-existing problems with tuples that need to be fixed (later)
• Evaluating field access inside quantifiers will not work initially

[florianschanda]

I have commit where things work now, but some additional work is needed to display counter-examples, because we now need to show more than one record in the example.

[florianschanda]

I have had a deep look now and there are large systematic issues with the way VCG works.

I would propose the following approach:

• I have a patch that I will clean up that implements LRM changes and tool changes to make field access work
• VCG support works but is limited

And I then follow this up with a bigger patch that makes VCG work properly.

[florianschanda]

One thing I know for sure is that we want to have two kinds of checks:

• checks that are run at declaration that cannot reference other records (but can reference tuples)
• checks that are run afterwards

type T {
   ref optional Foo
}

checks T {
   ref /= null, error "potato"  // allowed, but you can't do ref.field
}

invariant T {
   ref.field >= 10, error "potato"
}

Existing checks would be checks, and invariants are the new kind of check permitted.

Some changes would need to be done for evaluation, to make null / non-null checks work correctly.

The name invariant we can argue about. We can also consider

checks T after references {
...

[florianschanda]

I've created #156 to track this work

[florianschanda]

@melodyoncode I have created PR #158 that partially implements field access and also fixes CI.

I am sorry I could not get this PR to work directly, and I truly appreciate you trying; you managed to pick a extremely nasty issue and it will require basically a re-write of VCG to make it work properly.

[melodyoncode]

Hi @florianschanda
Apologies for the delayed response — I was on sick leave.
I just caught up with the discussion here: #153 (comment).
I initially assumed that evaluating field access inside quantifiers was not supported by design, but based on your latest comment, I might have misunderstood this.
I’ll take a closer look and get back to you.

[melodyoncode]

@florianschanda
From my understanding, there are two condition that we cannot support.

1. Quantified expressions

forall x in arr => x.ref.field > 0   // not support

2. functional + field access （like tuple）, cannot dereference record_type

type R {
  value Integer
}

tuple T {
  first  R
  second R
}

checks T {
  first.value < second.value, fatal "first should be smaller than second"
}

And I found a funny thing that

type R {
    value Integer
}

tuple T {
    first  R
    value  Integer
}

checks T {
   first.value < value, fatal "first should be smaller than second"      // it works
}

I have doubt here, why this condition can work?

[florianschanda]

@florianschanda From my understanding, there are two condition that we cannot support.

1. Quantified expressions

Yes, this is due to an existing limitation regarding quantifiers. In my rewrite of VCG I expect to lift this restriction.

2. functional + field access （like tuple）, cannot dereference record_type

type R {
  value Integer
}

tuple T {
  first  R
  second R
}

checks T {
  first.value < second.value, fatal "first should be smaller than second"
}

This should work. Does it not?

And I found a funny thing that

type R {
    value Integer
}

tuple T {
    first  R
    value  Integer
}

checks T {
   first.value < value, fatal "first should be smaller than second"      // it works
}

I have doubt here, why this condition can work?

Because first is not optional here. There are only three run-time errors possible in TRLC:

• null dereference
• division by zero
• array out of bounds

None of these are possible here, ans so while the check itself can pass or fail; there are no errors possible here.

If value in either T or R are optional; or first in T is optional, then you could have possible null dereferences.

[florianschanda]

If you're interested here is the branch: https://github.com/florianschanda/trlc/blob/vcg_rewrite/trlc/vcg.py

Nothing works yet, but if you want to contribute something (e.g. unary operators) I can give you direct push access to that repo.

Right now I am trying to sort out all the truly horribly bits first, and then fill in the easy parts. Specifically:

• optional (that works already)
• short-cut semantics (that works, i hope)
• field access (working on that now)
• quantifiers

None of the glue is there, specifically there is no actual solving of VCs / error reporting / counter-examples. I am just trying to get the algorithm sorted out and am manually inspecting the SMTLIB.

Other than the limitations you already mentioned in your previous post, I also found a bug when it comes to order-of-evaluation of multiple check blocks that I am now doing correctly. Here is a fun quiz:

type T {
  x Integer
}

checks T {
  x > 1, fatal "c1"
}

checks T {
  x < 10, "c2"
}

type Q extends T {
}

checks Q {
  10 / x > 0, "baz"
}

• Can check "baz" divide by zero?
• And if Q didn't exist and instead "baz" would be in T, would your answer be any different?

checks T {
  10 / x > 0, "baz"
}

[melodyoncode]

I think fatal checks of the parent type are treated as preconditions for all checks in the derived type.
Therefore, in Q, the check baz cannot divide by zero, because x > 1 is guaranteed by the parent’s fatal check.
However, if baz were in T, it could divide by zero, since all check blocks in the same type are evaluated in parallel, and no block may rely on assumptions established in another block—so x may still be zero.

[melodyoncode]

type R {
  value Integer
}

tuple T {
  first  R
  second R
}

checks T {
  first.value < second.value, fatal "first should be smaller than second"
}

It does work. I just misunderstood it as a warning.

[florianschanda]

Correct answer ;)

Also I had a second thought on the example above. The check works and is error free. However it would actually always evaluate to false... eventually. Since there is no valid set of TRLC files for which this check would not fail somewhere.

However this is totally out of scope for now, for now lint/vcg checks if there are run-time checks, not if its actually possible to build a set of files that pass :)