Checking LeftPad with Apalache

[bugarela]

Hi! Asking here since https://apalache.discourse.group/ is read-only (not sure if it's on purpose - if so, maybe update the link on README to point to here (discussions))

@crodriguezvega has tried using Quint [1] for this fun exercise from @hwayne [2], where people try to use multiple tools to prove some properties for the leftpad function.

Notably, @will62794 managed to prove those with SMT and Z3 [3].

I managed to get a version [4] working with limited string sizes (10 for the input string, 2^8 - 1 for the others). Apalache can check¹ this in under 1 minute while TLC doesn't give me any hope.

My question is: do you think there can be way to get Apalache to check this "more symbolically" so I don't have to constraint the input size? Kinda like to produce an equivalent input as the one in the SMT solution by Will (which iiuc is just (declare-const s String)). One thing is that we are using arrays of 1-length strings here to represent a string, since there is no concat for the string type. If we could using actual strings, maybe STRING [5] would solve this issue.

I'd also understand if this is not possible at all since we are working with a fragment of SMT here.

I did try to just have one big init action with all the possible inputs/outputs, but this was too big of a set for Apalache to expand.

Footnotes

1. I ran it with no invariants for now, still need to fix the properties. ↩

[konnov]

In my opinion, the Leftpad example does not demonstrate any strong features of TLA+/Quint and Apalache. It needs a purely functional specification that does plenty of iterative computations. No wonder that all proof systems shine there. As for SMT, the Dafny spec is nice and simple. Will's encoding is using the theory of strings, which is working here well, too. F* proof also looks nice and simple.

Is there any realistic use case that would motivate us to further think about that? Leftpad is a typical example of verifying simple sequential code using Hoare logic.

[bugarela]

I don't think so, I was just curious regarding this exercise, but I'm now convinced that Quint/TLA+ really aren't the tools for that. Thank you for providing your view