This message was deleted.

This message was deleted.

This message was deleted.

I'm about 90% done with that refinement spec. Should I add a 'proofs' directory to Venice and submit a PR?

Definitely!

This message was deleted.

Should I also check in leap frog (the spec, not the code)? It's in the data validation closed source right now.

I admit, that spec currently has one case it doesn't cover. It's a case we're not super concerned about, but it nags at me that it reduces the specs 'thoroughness'

I don’t think we should open source the proof for leap frog until we also open source leap frog… otherwise it doesn’t make much sense, IMHO

And I do hope we open source LF/LP soon 😄 …

Makes sense. We need to do some tech debt on that front. Put it through it's rounds across more prod stores

Also. Gives me an inDay or two to fix it up a bit

This message was deleted.

This message was deleted.

This message was deleted.

This message was deleted.

For folks in this channel who are interested in this sort of thing, I published VIP-2, which contains a TLA+ spec for LeapFrog. LeapFrog was actually the original motivator for looking into TLA+ for me, and was the first Venice thing we spec'd internally. This is the first time we've talked about it in detail in open source, so please take a look. I'm expecting to add one more spec to this PR when I get time, as the VIP discusses how we'd need to change some of the implementation of LeapFrog, so I need to add a refinement spec to show that the heartbeat approach doesn't break the original invariants of the first spec.

The proofs channel archive is here: https://www.linen.dev/s/venicedb/c/proofs