theory of pointers is inconsistent

[DestyNova]

I tried to build an example program with the snippet from README.md which uses theory for typestate enumeration / sequencing. However, I ran into syntax errors immediately, indicating that the syntax of theory has changed a bit recently.

So I looked at a working example in the typestate_wrong_order test, which compiles fine. I tried to simplify it to be more like the README example, using a straight int instead of a struct Socket { int fd }. However, I've gotten stuck at either expected int* got int or static_attest leads to conflicting constraints.

Here's what I have right now:

using <stdio.h>::{printf}

export fn main() -> int {
  int mut i = 0;

  open(&i);
  read(&i);
  close(&i);

  printf("Greetings, tree! i = %d\n", i);
  return 0;
}

pub theory is_open(int *a) -> bool;

fn open(int mut *a)
    model is_open(a)
{
    static_attest(is_open(a) == true);
    static_assert(is_open(a) == true);
    *a = 1;
}

fn read(int mut *a) -> int
    where is_open(a)
    model is_open(a)
{
    return *a;
}

fn close(int mut *a)
    where is_open(a)
    model !is_open(a)
{
    *a = 0;
    static_attest(!is_open(a));
}

I was also unable to compile the new+ example of creating a string with a tail object.

To be honest, I only ever learned enough C to be extremely dangerous, and am quite unfamiliar with theorem provers (outside of a little excursion into Idris which was interesting but impractical). It might be a good time to refresh the docs to make it easier for people to get started playing with zz? I'd love to help, but I'm still struggling with the basics :sweat:

[aep]

thanks for the report!

tl;dr: "theory != something" is confusing, dont use it. instead remove state by not putting it into the model

unfortunately type state is difficult to understand because the implementation is not good. specifically the error messages are not helpful.

in your case

[ERROR] callsite effect would break SSA
 --> /private/tmp/k/src/main.zz:8:9
  |
8 |   close(&i);␊

is because the model of close is !is_open(), which conflicts with its previous state of is_open. You could look into the SSA output in target/ssa to understand why, but thats tedious.

type state is lost after each mutable self call, because transferring it implicitly would be messy. so in order to have a "not open" state, you just remove the open state from model.

using <stdio.h>::{printf}

export fn main() -> int {
  int mut i = 0;

  open(&i);
  read(&i);
  close(&i);

  printf("Greetings, tree! i = %d\n", i);
  return 0;
}

pub theory is_open(int *a) -> bool;

fn open(int mut *a)
    model is_open(a)
{
    static_attest(is_open(a) == true);
    static_assert(is_open(a) == true);
    *a = 1;
}

fn read(int mut *a) -> int
    where is_open(a)
    model is_open(a)
{
    return *a;
}

fn close(int mut *a)
    where is_open(a)
{
    *a = 0;
}

[DestyNova]

Ah I understand now, thanks. I assumed that once is_open(a) was attested, then it would continue to hold until explicitly contradicted, but what you said makes sense.

I'll keep plugging away then 😄

[DestyNova]

"so in order to have a "not open" state, you just remove the open state from model."

Hmm, I'm still not sure about this. I removed the model !is_open(a) and static_attest from the close() function, and now the following is legal:

  open(&i);
  close(&i);
  read(&i);

This would indicate that after calling close, the compiler still considers is_open(a) to be true. What's a better way to make it so that calling read after close would be illegal?

[aep]

that sounds like a bug

[aep]

well technically its sort of a bug, but unfortunately not one that i can fix quickly because its an effect of how pointers are treated as values.

the pointer never changes, so its temporal doesnt change, so the state effects never apply.

however you can easily just ignore the whole problem by not using pointers in theories

using <stdio.h>::{printf}

export fn main() -> int {
  int mut i = 0;

  int mut* b = &i;

  open(b);
  read(b);
  close(b);
  read(b);

  printf("Greetings, tree! i = %d\n", i);
  return 0;
}

pub theory is_open(int a) -> bool;

fn open(int mut *a)
    model is_open(*a)
{
    *a = 1;
    static_attest(is_open(*a) == true);
    static_assert(is_open(*a) == true);
}

fn read(int mut *a) -> int
    where is_open(*a)
    model is_open(*a)
{
    return *a;
}

fn close(int mut *a)
    where is_open(*a)
{
    *a = 0;
}

[DestyNova]

I tried something like that (but without the extra int mut* b = &i step) and couldn't get it to work. When I tried your version above though, I get this:

ERROR] unproven callsite assert for interpretation of theory ::helo::main::is_open o
ver i
 --> /home/omf/code/zz/helo/src/main.zz:9:8
  |
9 |   read(b);␊
  |        ^^
  |
  = in this callsite

  --> /home/omf/code/zz/helo/src/main.zz:26:19
   |
26 |     where is_open(*a)␊
   |                   ^-^
   |
   = function call requires these conditions

  --> /home/omf/code/zz/helo/src/main.zz:25:1
   |
25 | fn read(int mut *a) -> int␊
   | ...
30 | }␊
   | ^
   |
   = for this function

  --> /home/omf/code/zz/helo/src/main.zz:26:19
   |
26 |     where is_open(*a)␊
   |                   ^-^
   |
   = for interpretation of theory ::helo::main::is_open over i |0| = false

 --> /home/omf/code/zz/helo/src/main.zz:9:8
  |
9 |   read(b);␊
  |        ^^
  |
  = last callsite

[DestyNova]

So that works (including compiling as expected when the order of read and close) :+1:

[jwerle]

@aep is this issue valid or a bug or?

[aep]

I'd say it's a documentation issue.

Type state can get confusing quickly, so it needs to be more clear what the limits are.