Snap encoding of array assignments #877

Pointerbender · 2022-02-20T13:08:11Z

This issue is a spin-off from #819, which revealed that currently Prusti is unable to verify programs like:

#[ensures(result <= 3)]
fn foo() -> usize {
    let mut a = [1, 2, 3];
    let mut i = 0;
    while i < 3 {
        body_invariant!(i < 3);
        body_invariant!(forall(|j: usize| (0 <= j && j < i) ==> (a[j] <= j + 2),triggers=[(a[j],)]));
        body_invariant!(forall(|j: usize| (i <= j && j < 3) ==> (a[j] <= j + 1),triggers=[(a[j],)]));
        body_invariant!(a[i] <= i + 1);
        let tmp = a[i] + 1;
        a[i] = tmp;
        i += 1;
    }
    a[1]
}

but Prusti can verify this program okay:

#[ensures(result <= 3)]
fn bar() -> usize {
    let mut a = [1, 2, 3];
    let mut i= 0;
    while i < 3 {
        body_invariant!(i < 3);
        body_invariant!(forall(|j: usize| (0 <= j && j < i) ==> (a[j] <= j + 2),triggers=[(a[j],)]));
        body_invariant!(forall(|j: usize| (i <= j && j < 3) ==> (a[j] <= j + 1),triggers=[(a[j],)]));
        body_invariant!(a[i] <= i + 1);
        let tmp = a[i] + 1;
        set(&mut a, i, tmp);
        i += 1;
    }
    a[1]
}

#[requires(0 <= i && i < 3)]
#[ensures(forall(|j: usize| (0 <= j && j < 3 && j != old(i)) ==> (a[j] == old(a[j])), triggers=[(a[j],)]))]
#[ensures(a[old(i)] == old(v))]
fn set(a: &mut [usize; 3], i: usize, v: usize) {
    a[i] = v;
}

The underlying issue seems to be related to the snapshot encoding of a.

Some ideas that were suggested in #819 are:

Wait for Use snapshot encoding for Rust assertions #796 which addresses snap encoding of Rust assertions. Then we can add (debug_)assert! statements at the end of the loop which will invoke snap$__$TY$__Snap$Array$10$i32$. This one is currently blocked by the refactoring.

We could update the quantifier triggers for array/slice assignment to also trigger on { read$Snap$Array$10$i32$__$TY$__(X, i) }, currently those only trigger on { lookup_pure__$TY$__Array$10$i32$i32$(X, i). This would be nice for the end-user experience, because less Rust assertions would be needed. However, this may decrease overall performance because of the extra trigger and larger Viper programs when snap encoding is not needed for the verification.

Find another way to preserve information about the array assignment between loop iterations. Johannes also suggested this option in his master thesis in section "6.1 Future Work".

I started looking into option 2 and discovered that adding just the trigger is not sufficient to make the program verify. The Viper program for foo generates the following Viper statements for the array assignment:

inhale (let _LET_4 == (old[l8](_33)) in (
    forall i: Int ::
    { lookup_pure__$TY$__Array$3$usize$usize$(_1, i) }
    0 <= i && (i < 3 && !(i == _LET_4))
      ==> lookup_pure__$TY$__Array$3$usize$usize$(_1, i)
      == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i))
  ))
inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

With a bit of manual hacking in the Viper program, I can make the Viper program for foo verify if I replace the above 2 statements with:

inhale (let _LET_4 == (old[l8](_1)) in (
    let _LET_5 == (old[l8](_33)) in (
      forall i: Int ::
      { lookup_pure__$TY$__Array$3$usize$usize$(_LET_4, i) }
      { read$Snap$Array$3$usize$__$TY$__(snap$__$TY$__Snap$Array$3$usize$(_LET_4), i) }
      0 <= i && i < 3 && !(i == _LET_5)
        ==> read$Snap$Array$3$usize$__$TY$__(snap$__$TY$__Snap$Array$3$usize$(_LET_4), i)
        == old[l8](read$Snap$Array$3$usize$__$TY$__(snap$__$TY$__Snap$Array$3$usize$(_1), i))
    )
))
inhale read$Snap$Array$3$usize$__$TY$__(snap$__$TY$__Snap$Array$3$usize$(_1), old[l8](_33)) == __t27.val_int

Would it be desirable to implement array assignments in this snap encoded form everywhere? I believe that these are fully backwards-compatible with the non-snapshot version, due to:

The trigger { lookup_pure__$TY$__Array$3$usize$usize$(_LET_4, i) } makes sure that the quantifier is triggered in all the places were it is triggered now.
The Viper functions snap$__$TY$__Snap$Array$3$usize$ and lookup_pure__$TY$__Array$3$usize$usize$ both require the same access predicates, namely requires acc(Array$3$usize(self), read$()).
The second inhale statement and the post-condition of snap$__$TY$__Snap$Array$3$usize$ ensures that the knowledge about the array values is propagated to both the Snap and non-Snap domains:

function snap$__$TY$__Snap$Array$10$i32$(self: Ref): Snap$Array$10$i32
  requires acc(Array$10$i32(self), read$())
  ensures (forall i: Int ::
         { read$Snap$Array$10$i32$__$TY$__(result, i) }
         { lookup_pure__$TY$__Array$10$i32$i32$(self, i) }
         0 <= i && i < 10 ==>
                  read$Snap$Array$10$i32$__$TY$__(result, i)
                  == lookup_pure__$TY$__Array$10$i32$i32$(self, i))
{
  cons$Snap$Array$10$i32$__$TY$__(seq_collect$Array$10$i32$__$TY$__(self, 0))
}

However, I'm not sure about what performance implications this would bring with it, so I wanted to bounce this idea off everyone here before implementing it and creating a PR :)

Thanks!

The text was updated successfully, but these errors were encountered:

Pointerbender · 2022-02-20T16:02:58Z

Actually, it turns out that the snap encoding is not needed after all! Instead of these 2 statements:

inhale (let _LET_4 == (old[l8](_33)) in (
    forall i: Int ::
    { lookup_pure__$TY$__Array$3$usize$usize$(_1, i) }
    0 <= i && (i < 3 && !(i == _LET_4))
      ==> lookup_pure__$TY$__Array$3$usize$usize$(_1, i)
      == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i))
  ))
inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

this also does the trick of making foo verify:

inhale (let _LET_4 == (old[l8](_1)) in (
    let _LET_5 == (old[l8](_33)) in (
      forall i: Int ::
      { lookup_pure__$TY$__Array$3$usize$usize$(_LET_4, i) }
      0 <= i && (i < 3 && !(i == _LET_5))
        ==> lookup_pure__$TY$__Array$3$usize$usize$(_LET_4, i)
        == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i))
  )))
inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

(this works for foo, but not for the selection_sort.rs test case, unfortunately)

vakaras · 2022-02-20T19:49:30Z

Actually, it turns out that the snap encoding is not needed after all! Instead of these 2 statements:

inhale (let _LET_4 == (old[l8](_33)) in (
    forall i: Int ::
    { lookup_pure__$TY$__Array$3$usize$usize$(_1, i) }
    0 <= i && (i < 3 && !(i == _LET_4))
      ==> lookup_pure__$TY$__Array$3$usize$usize$(_1, i)
      == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i))
  ))
inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

this also does the trick of making foo verify:

inhale (let _LET_4 == (old[l8](_1)) in (
    let _LET_5 == (old[l8](_33)) in (
      forall i: Int ::
      { lookup_pure__$TY$__Array$3$usize$usize$(_LET_4, i) }
      0 <= i && (i < 3 && !(i == _LET_5))
        ==> lookup_pure__$TY$__Array$3$usize$usize$(_LET_4, i)
        == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i))
  )))
inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

(this works for foo, but not for the selection_sort.rs test case, unfortunately)

Wait… Is the only difference between the examples _1 being replaced with old[l8](_1) via _LET_4? Since _1 is a local Viper variable, putting it inside old has no effect on it (or at least, it should). I am confused…

Pointerbender · 2022-02-20T20:28:28Z

Wait… Is the only difference between the examples _1 being replaced with old[l8](_1) via _LET_4?

Yup, that's the only change. I suspect that the exhale/inhale acc(Array$3$usize(_1), write) statements in between the label l8 and the array assignment have something to do with it. Maybe it prevents Viper from triggering the quantifier if _1 is "havoc'ed", but it somehow remembers old[l8](_1) from before the havoc'ing?

Pointerbender · 2022-02-20T20:30:09Z

Full relevant code section without LET:

  // [mir] _1[_33] = move _32
  label l8
  exhale acc(Array$3$usize(_1), write)
  inhale acc(Array$3$usize(_1), write)
  inhale (forall i: Int :: { lookup_pure__$TY$__Array$3$usize$usize$(old[l8](_1), i) } 0 <= i && (i < 3 && !(i == old[l8](_33))) ==> lookup_pure__$TY$__Array$3$usize$usize$(old[l8](_1), i) == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i)))
  __t27 := _32
  label l9
  inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

vakaras · 2022-02-20T20:47:40Z

Wait… Is the only difference between the examples _1 being replaced with old[l8](_1) via _LET_4?

Yup, that's the only change. I suspect that the exhale/inhale acc(Array$3$usize(_1), write) statements in between the label l8 and the array assignment have something to do with it. Maybe it prevents Viper from triggering the quantifier if _1 is "havoc'ed", but it somehow remembers old[l8](_1) from before the havoc'ing?

_1 is not havocked because there is no assignment to it and that is why I am confused. _1 is just the address, the statements

  exhale acc(Array$3$usize(_1), write)
  inhale acc(Array$3$usize(_1), write)

havoc the memory stored at address _1, but the address itself stays the same. You should be able to assert that:

assert old[l8](_1) == _1

My only guess is that syntactically changing the program somehow enables Z3 to trigger the quantifier.

vakaras · 2022-02-20T20:50:49Z

Full relevant code section without LET:

  // [mir] _1[_33] = move _32
  label l8
  exhale acc(Array$3$usize(_1), write)
  inhale acc(Array$3$usize(_1), write)
  inhale (forall i: Int :: { lookup_pure__$TY$__Array$3$usize$usize$(old[l8](_1), i) } 0 <= i && (i < 3 && !(i == old[l8](_33))) ==> lookup_pure__$TY$__Array$3$usize$usize$(old[l8](_1), i) == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i)))
  __t27 := _32
  label l9
  inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

Is this the original code? old[l8](_1) inside the trigger looks very suspicious to me: triggers are syntactic rules, so it is possible that the quantifier is not triggered because of that unnecessary old. What happens if you replace old[l8](_1) with _1?

Pointerbender · 2022-02-20T21:06:47Z

Is this the original code?

No, I have some local changes to Prusti that generates that version (and verifies). The original statements (as currently generated from the master branch from Prusti) that don't verify for foo are:

  // [mir] _1[_33] = move _32
  label l8
  exhale acc(Array$3$usize(_1), write)
  inhale acc(Array$3$usize(_1), write)
  inhale (let _LET_4 == (old[l8](_33)) in (forall i: Int :: { lookup_pure__$TY$__Array$3$usize$usize$(_1, i) } 0 <= i && (i < 3 && !(i == _LET_4)) ==> lookup_pure__$TY$__Array$3$usize$usize$(_1, i) == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i))))
  __t27 := _32
  label l9
  inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == __t27.val_int

My only guess is that syntactically changing the program somehow enables Z3 to trigger the quantifier.

What you describe regarding the syntactic rules sounds like what could be happening for the Viper program for foo.

old[l8](_1) inside the trigger looks very suspicious to me: triggers are syntactic rules, so it is possible that the quantifier is not triggered because of that unnecessary old.

Only in this case foo only verifies with the old[l8](_1) :)

What happens if you replace old[l8](_1) with _1?

In the case of the Viper program for foo, verification fails (can be replicated on current master branch). I was trying to make a smaller Viper-only example to replicate this, but I was not able to make a smaller version by hand that fails.

Pointerbender · 2022-02-20T21:11:03Z

_1 is not havocked because there is no assignment to it and that is why I am confused.

Apologies :) For better context about what I mean by "havoc", I was going off of this comment in the code:

prusti-dev/prusti-viper/src/encoder/procedure_encoder.rs

Lines 5215 to 5224 in 00fa0d0

    
           // We can't just inhale lookup_pure(base, index) == new_val, because that would 
        
           // add conflicting info with the previous state of the array at that index. 
        
           // So the idea is 
        
           //   label lbl; 
        
           //   exhale array; 
        
           //   inhale array; 
        
           //   // now all info about the array is `havoc`ed 
        
           //   inhale forall i:: i != index ==> lookup_pure(array, i) == old[lbl](lookup_pure(array, i)) 
        
           //   inhale lookup_pure(array, index) == encoded_rhs 
        
           //   // now we have all the contents as before, just one item updated

Pointerbender · 2022-02-20T21:36:28Z

In case it helps, this small hand-crafted example which does not use old[l8](_1) in the trigger verifies okay:

method example()
{
  var _1: Ref
  var _33: Int
  _1 := builtin$havoc_ref()
  _33 := builtin$havoc_int()
  inhale acc(Array$3$usize(_1), write)
  inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, 0) == 1
  inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, 1) == 2
  inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, 2) == 3
  _33 := 0
  label l8
  exhale acc(Array$3$usize(_1), write)
  inhale acc(Array$3$usize(_1), write)
  inhale (forall i: Int ::
    { lookup_pure__$TY$__Array$3$usize$usize$(_1, i) }
    0 <= i && (i < 3 && !(i == old[l8](_33)))
        ==> lookup_pure__$TY$__Array$3$usize$usize$(_1, i)
        == old[l8](lookup_pure__$TY$__Array$3$usize$usize$(_1, i))
  )
  inhale lookup_pure__$TY$__Array$3$usize$usize$(_1, old[l8](_33)) == 3
  assert read$Snap$Array$3$usize$__$TY$__(snap$__$TY$__Snap$Array$3$usize$(_1), 1) == 2
}

I guess that this is in-line with what would be expected. I'm not sure why a similar approach fails for foo, though.

vakaras · 2022-02-20T22:01:23Z

old[l8](_1) inside the trigger looks very suspicious to me: triggers are syntactic rules, so it is possible that the quantifier is not triggered because of that unnecessary old.

Only in this case foo only verifies with the old[l8](_1) :)

This is very confusing…

vakaras · 2022-02-20T22:02:20Z

_1 is not havocked because there is no assignment to it and that is why I am confused.

Apologies :) For better context about what I mean by "havoc", I was going off of this comment in the code:

prusti-dev/prusti-viper/src/encoder/procedure_encoder.rs

Lines 5215 to 5224 in 00fa0d0

// We can't just inhale lookup_pure(base, index) == new_val, because that would

// add conflicting info with the previous state of the array at that index.

// So the idea is

// label lbl;

// exhale array;

// inhale array;

// // now all info about the array is `havoc`ed

// inhale forall i:: i != index ==> lookup_pure(array, i) == old[lbl](lookup_pure(array, i))

// inhale lookup_pure(array, index) == encoded_rhs

// // now we have all the contents as before, just one item updated

I see ☺. That comment should say that the contents of the array are havocked.

vakaras · 2022-02-20T22:07:17Z

I looked into the Viper encoding for a bit, but I, unfortunately, do not see what is going wrong here. Coming back to:

Would it be desirable to implement array assignments in this snap encoded form everywhere?

I think it would make our life easier if we everywhere used the same lookup function. @Aurel300 Do you see any reason not to do that?

fpoli · 2022-02-21T07:34:17Z

My only guess is that syntactically changing the program somehow enables Z3 to trigger the quantifier.

I'd also compare the change randomizing the Z3 seeds:

// Prusti.toml
extra_verifier_args = [ "--z3RandomizeSeeds" ]

Pointerbender · 2022-02-21T19:52:12Z

My only guess is that syntactically changing the program somehow enables Z3 to trigger the quantifier.

I'd also compare the change randomizing the Z3 seeds:
// Prusti.toml
extra_verifier_args = [ "--z3RandomizeSeeds" ]

The extra_verifier_args = [ "--z3RandomizeSeeds" ] seems to have no effect on the verification result of foo. Increasing the assert_timeout flag or adding extra_verifier_args = [ "--z3RandomizeSeeds", "--checkTimeout=100", "--z3SaturationTimeout=1000", "--qpSplitTimeout=1000" ] also does not result in longer verification times, indicating Z3 manages to exhaust the search space.The version { lookup_pure__$TY$__Array$3$usize$usize$(_1, i) } consistently fails verification even with a different seed every time. The version with { lookup_pure__$TY$__Array$3$usize$usize$(old[l8](_1), i) } consistently passes verification for foo.

It's starting to look more and more like this is an obscure corner case which confuses Viper/Z3 (and in a deterministic fashion despite random seeds, too 😅 ). There is more to it than just the choice for triggers. So far I've not been able to trigger the same circumstances without a loop. Maybe the mix of goto, the trigger syntax using old and "havoc'ing the contents of the array" would cause it to trip up? I'm not quite sure how to go about crafting a manual Viper example for this one, though.

Pointerbender · 2022-02-23T20:45:02Z

I looked into the Viper encoding for a bit, but I, unfortunately, do not see what is going wrong here. Coming back to:

Would it be desirable to implement array assignments in this snap encoded form everywhere?

I think it would make our life easier if we everywhere used the same lookup function. @Aurel300 Do you see any reason not to do that?

I was playing around with this a bit more today and it gets more confusing :) The version where array assignments are snapshot encoded suffer from the same quirk where the Viper program for foo only verifies if it uses the trigger { read$Snap$Array$3$usize$__$TY$__(snap$__$TY$__Snap$Array$3$usize$(old[l8](_1)), i) }, but it fails verification when using a trigger without old i.e. { read$Snap$Array$3$usize$__$TY$__(snap$__$TY$__Snap$Array$3$usize$(_1), i) }.

The original version that Prusti gives me that doesn't verify is: lib.rs_prusti_example::foo 20220223 unmodified.vpr.txt.
Here is an annotated version of the same program that does verify: lib.rs_prusti_example::foo 20220223 modified.vpr.txt. All changes and comments are within lines 409-426.

vakaras · 2022-02-24T12:33:34Z

This sounds more and more like a bug in the Viper backend. However, the examples are way too large to ask the backend developers to look into. Would be nice to get a repro on a 20 or so lines example.

An alternative would be to wait until the refactoring is complete and see whether it addresses the problem.

Pointerbender · 2022-02-25T08:46:10Z

Would be nice to get a repro on a 20 or so lines example.

I'll see if I can whip up something during the weekend :)

An alternative would be to wait until the refactoring is complete and see whether it addresses the problem.

In case we don't manage to reproduce a small example, would it be acceptable to use the old triggers until the refactoring lands?

vakaras · 2022-02-25T16:38:54Z

Would be nice to get a repro on a 20 or so lines example.

I'll see if I can whip up something during the weekend :)

Thanks!

An alternative would be to wait until the refactoring is complete and see whether it addresses the problem.

In case we don't manage to reproduce a small example, would it be acceptable to use the old triggers until the refactoring lands?

If it has no regressions, I think we could.

Pointerbender · 2022-02-28T08:06:29Z

I'll see if I can whip up something during the weekend :)

This is the smallest version I could come up with: lib.rs_prusti_example::foo 20220228 small.vpr.txt

Surprisingly, the confusing behavior can be triggered without loops or goto statements!

…iperproject#877. remove auxiliary helper function for `selection_sort.rs` viperproject#819. added regression test for viperproject#877.

vakaras · 2022-03-03T10:54:07Z

I'll see if I can whip up something during the weekend :)

This is the smallest version I could come up with: lib.rs_prusti_example::foo 20220228 small.vpr.txt

Surprisingly, the confusing behavior can be triggered without loops or goto statements!

Thank you very much for reducing the example. I have filed a Silicon issue: viperproject/silicon#603

888: use `old` in trigger for direct array assignments r=vakaras a=Pointerbender This PR experiments with addressing 2 things: 1. It implements the suggested work-around for #877 together with a regression test (the test suite indicated no regressions locally). 2. The `selection_sort.rs` test case was updated to use this fix in order to remove the auxiliary `set` function (#819). Some notes apply to the approach chosen to make `selection_sort.rs` verify: * A "dummy" `body_invariant!(a[0] <= a[i]);` was added to the outer and inner loops in order to correctly trigger the quantifiers. * A change was made in `prusti-viper/src/encoder/foldunfold/mod.rs` to prevent Prusti from running into an encoder error when the `old` expresion was only present in the trigger, but not in the quantifier body. Without this change, `selection_sort.rs` will complain about a fold-unfold error. Since access predicates are not needed when the `old` expression is only present in the trigger, this should be sound (but please do double check this during the peer review). * Without the auxiliary `set` function, the verification time roughly doubled, but it is still well within the `-Pverification_deadline=180` compiler parameter. Execution time now hovers around ~2 minutes on my PC. If the chosen approach sounds good, then this PR can be merged. I'm still a bit suspicious about why the `set` function yields better performance, I could look into this deeper with some guidance (possibly in a separate PR if that makes more sense). For now I came up empty-handed for what could be causing this performance regression (if this happens to be related to how Viper gives hints to Z3 based on the Viper/Silver syntax, then my current experience may not be of much help, but am willing to learn more!). Thanks! p.s. Issue #877 can be left open for now in case we want to file a bug report with the Viper back-end developers to investigate the `old` trigger issue. I posted a ~30 lines example there that hopefully is small enough to investigate. Co-authored-by: Pointerbender <pointerbender@gmail.com>

Pointerbender mentioned this issue Feb 28, 2022

use old in trigger for direct array assignments #888

Merged

vakaras mentioned this issue Mar 3, 2022

Old on a local variable affects triggering viperproject/silicon#603

Closed

Pointerbender mentioned this issue Apr 17, 2022

Failing (trivial) assertion in presence of a quantifier over a slice #962

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Snap encoding of array assignments #877

Snap encoding of array assignments #877

Pointerbender commented Feb 20, 2022

Pointerbender commented Feb 20, 2022 •

edited

Loading

vakaras commented Feb 20, 2022

Pointerbender commented Feb 20, 2022

Pointerbender commented Feb 20, 2022

vakaras commented Feb 20, 2022

vakaras commented Feb 20, 2022

Pointerbender commented Feb 20, 2022

Pointerbender commented Feb 20, 2022

Pointerbender commented Feb 20, 2022

vakaras commented Feb 20, 2022

vakaras commented Feb 20, 2022

vakaras commented Feb 20, 2022

fpoli commented Feb 21, 2022 •

edited

Loading

Pointerbender commented Feb 21, 2022

Pointerbender commented Feb 23, 2022

vakaras commented Feb 24, 2022 •

edited

Loading

Pointerbender commented Feb 25, 2022

vakaras commented Feb 25, 2022

Pointerbender commented Feb 28, 2022

vakaras commented Mar 3, 2022

Snap encoding of array assignments #877

Snap encoding of array assignments #877

Comments

Pointerbender commented Feb 20, 2022

Pointerbender commented Feb 20, 2022 • edited Loading

vakaras commented Feb 20, 2022

Pointerbender commented Feb 20, 2022

Pointerbender commented Feb 20, 2022

vakaras commented Feb 20, 2022

vakaras commented Feb 20, 2022

Pointerbender commented Feb 20, 2022

Pointerbender commented Feb 20, 2022

Pointerbender commented Feb 20, 2022

vakaras commented Feb 20, 2022

vakaras commented Feb 20, 2022

vakaras commented Feb 20, 2022

fpoli commented Feb 21, 2022 • edited Loading

Pointerbender commented Feb 21, 2022

Pointerbender commented Feb 23, 2022

vakaras commented Feb 24, 2022 • edited Loading

Pointerbender commented Feb 25, 2022

vakaras commented Feb 25, 2022

Pointerbender commented Feb 28, 2022

vakaras commented Mar 3, 2022

Pointerbender commented Feb 20, 2022 •

edited

Loading

fpoli commented Feb 21, 2022 •

edited

Loading

vakaras commented Feb 24, 2022 •

edited

Loading