hwayne / lets-prove-leftpad Goto Github PK

Hi! Thanks very much for this repo & your write-up, I really enjoy them.

Would a Cryptol version be welcome? Here's a first attempt at one:

module leftpad where

leftpad: {pad, in, out}
         (fin pad, fin in, fin out, pad >= in, out == max pad in) =>
         Char -> String in -> String out
leftpad c s = repeat`{pad - in} c # s

leftpadLength: {pad, in, out}
         (fin pad, fin in, fin out, pad >= in, out == max pad in) =>
         Char -> String in -> Bit
property leftpadLength c s = length (leftpad`{pad, in, out}c s) == `out

leftpadPrefix: {pad, in, out}
               (fin pad, fin in, fin out, pad >= in, out == max pad in) =>
               Char -> String in -> Bit
property leftpadPrefix c s = take`{pad - in}(leftpad`{pad, in, out}c s) == repeat`{pad - in}c

leftpadSuffix: {pad, in, out}
               (fin pad, fin in, fin out, pad >= in, out == max pad in) =>
               Char -> String in -> Bit
property leftpadSuffix c s = drop`{pad - in}(leftpad`{pad, in, out}c s) == s

Though the cryptol REPL can prove things via the :prove command, it "cannot directly prove polymorphic properties as they may hold for certain monomorphic instances while not for others." For instance,

┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.13.0
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol> :l leftpad.cry
Loading module Cryptol
Loading module leftpad
leftpad> :prove leftpadLength
Not a monomorphic type:
{pad, in, out}
  (fin pad, fin in, fin out, pad >= in, out == max pad in) =>
  [8] -> [in][8] -> Bit
(Total Elapsed Time: 0.000s)
leftpad> :prove leftpadLength`{10,3,10}
Q.E.D.
(Total Elapsed Time: 0.019s, using "Z3")

This can be nice in some respects; for instance, :prove leftpadLength`{10,3,0} throws an error about the unsolvable constraint 0 == 10. That said, I'm not sure needing explicitly specify pad, in, and out yourself fulfills the spirit of this challenge.

Thanks again!

This issue stems from the discussion at #38; I'm adding this so there's a proper issue tracking this work. Quote from @hwayne in that discussion:

I should really write a full explainer to explain to everybody what we're looking for

ACKN

Slightly related: #41.

An example of using refinement types and dependent types to write a padded string in ATS described below:

http://blog.vmchale.com/article/practical-ats

More about ATS: https://en.wikipedia.org/wiki/ATS_(programming_language)

It's because it uses a lemma from the Lean4 std (nat.sub_add_eq_max) but the online prover is running Lean3

• ATS
• Iris
• AutoProof

I'll add more as I run into them

Hey,

You missed these by @cipher1024, from a while back:

• leftpad in Lean
• unique in Lean

I proved leftpad in rust, using creusot: https://github.com/suhr/leftpad

How to verify:

• cargo creusot --span-mode=absolute -- --features=contracts
• «creusot repo»/ide target/debug/leftpad-rlib.mlcfg

NB: you need to apply “Split VC” on the leftpad VC to avoid CVC5 timeout.

Creusot is a research software, so I'm not sure if I should make a PR yet.

I found this repository incredibly interesting.

I think it would be very informative to extract some kind of naive summary statistics (e.g. LOC) to understand the compromises between different proof systems.

As an old user of Spec#, Dafny's precursor, I was pleasantly surprised to see how well Dafny and other systems (e.g. Lean, Agda, F*, Coq/SSReflect or Idris) compare to Isabelle or Liquid Haskell.