Property testing library for guile? for Zoe escrow as goblins

would anyone care to recommend one?

@markm expressed an interest in a correct-by-construction methodology for writing the escrow service in Zoe 2. I made a spike to explore various approaches. (It also has more background and a bibliography of related research).

One of them is ACL2. (Dr. Boyer was one of my favorite profs at U.T. Austin. We’re still in touch from time to time, and he still strongly evangelizes ACL2.)

I made more tangible progress in dafny, but I hit a wall around promises and async stuff.

The other day, I wondered whether there are actor libraries for idris or ACL2. Then it occurred to me: goblins supports state transitions as pure functions. I could do it in goblins, and port the result to ACL2.

So I got started by taking the original 42 line escrow implementation from the 2013 paper and porting it to scheme: escrow2013.scm

I’ve done some property testing for ERTP:
Algebraic properties of amounts · Issue #557 · Agoric/agoric-sdk

I’d like to port that to guile to test stuff related to escrow2013.scm, and to prototype ACL2 proof claims.

1 Like

I’m afraid I can’t offer much help regarding proofs because I still haven’t read The Little Prover. :wink:

A search for “guile property testing” turned up Guile-QuickCheck. Is this along the lines of what you are looking for?

yes; QuickCheck in haskell is the original property testing library, so the guile analog is just what I’m looking for. Thanks!

Hm. how do I use it?

I got as far as guix install guile-quickcheck, but then when I use c-x c-e on (use-modules (quickcheck)), it dies with no code for module (quickcheck).

I don’t see much about modules in the scheme primer.

I eventually found the files:

$ find -L ~/.guix-profile/ -name 'quickcheck.scm'

(Is there a command to files in a guix package? Web searching turns up little.)

More clues, please?

Is Guile installed in your profile? You’ll need that in order to have the right shell config to source to get the necessary load path environment variables.

Alternatively, use guix shell:

dave@ikaruga ~$ guix shell guile guile-quickcheck
dave@ikaruga ~ [env]$ guile
GNU Guile 3.0.9
Copyright (C) 1995-2023 Free Software Foundation, Inc.

Guile comes with ABSOLUTELY NO WARRANTY; for details type `,show w'.
This program is free software, and you are welcome to redistribute it
under certain conditions; type `,show c' for details.

Enter `,help' for help.
scheme@(guile-user)> (use-modules (quickcheck))
scheme@(guile-user)> ,apropos quickcheck
(quickcheck): quickcheck-results	#<procedure quickcheck-results (test)>
(quickcheck): quickcheck	#<procedure quickcheck (test)>
(quickcheck): configure-quickcheck

does that guix shell trick work inside emacs, as an inferior scheme/lisp?

aha! found 10. Appendix: Setting up Guile, Wisp, and Goblins by way of a nearby post where somebody pointed out the link from the scheme primer to the heart of spritely. I’ll chew on that for a bit.

I recommend getting the basics working in a terminal, first, to keep the moving parts to a minimum. Integrating Emacs and guix shell is totally possible (I do it) but it’s a more advanced setup. Installing packages to your user profile is easier for starting with Emacs development.

Speaking of moving parts, I discovered Hall and kicked the tires. I didn’t have complete success, but it felt like it would eventually be cost-effective.

Do you use / recommend it?

No, I don’t use it. Not sure how usable it is. I use Guix because I can manage everything with it, not just Guile stuff.

ok. good to know.

Hall seems to integrate with Guix pretty well, fwiw.

In fact, I got the impression that some of the guix package files around here were generated by hall. (hence asking whether you use it)