dafny-lang / libraries Goto Github PK

src/Unicode has a fairly pure implementation of UTF-16 and UTF-8, but it uses bit vector types and doesn't use char or string at all. We definitely need a standard library that does (and the incoming JSON PR does itself, since it needs to encode a string in UTF-8), although this means we'll need at least some Dafny code that is duplicated to account for the difference in behavior from --unicode-char.

Here is sample code that could be integrated, need to test if it's fast enough and relevant.

datatype Option<W> = None | Some(value: W)

function MapWithFailure<U, V, W>(oldmap: map<U, V>, f: V -> Option<W>): (result: Option<map<U, W>>) {
  if forall k <- oldmap :: f(oldmap[k]).Some? then
    Some(map k <- oldmap :: k := f(oldmap[k]).value)
  else
    None
} by method {
  var keySet := oldmap.Keys;
  ghost var keySetcomplement := {};
  var tmp := map[];
  while |keySet| > 0
    invariant keySet !! keySetcomplement
    invariant keySet + keySetcomplement == oldmap.Keys
    invariant forall k <- keySetcomplement :: f(oldmap[k]).Some?
    invariant Some(tmp) == MapWithFailure(map k <- oldmap | k in keySetcomplement :: k := oldmap[k], f)
  {
    var x :| x in keySet;
    keySet := keySet - {x};
    var t := f(oldmap[x]);
    if t.None? {
      return None;
    }
    ghost var oldTmp := tmp;
    tmp := tmp[x := t.value];
    calc {
      tmp;
      oldTmp[x := t.value];
      MapWithFailure(map k <- oldmap | k in keySetcomplement :: k := oldmap[k], f).value[x := t.value];
      MapWithFailure(map k <- oldmap | k in keySetcomplement + {x} :: k := oldmap[k], f).value;
    }
    keySetcomplement := keySetcomplement + {x};
  }
  result := Some(tmp);
  assert keySetcomplement == oldmap.Keys;
  assert oldmap == map k <- oldmap | k in keySetcomplement :: k := oldmap[k];
}

Spun off from #49. Once that is merged we'll have the definition of [strict] total orderings, and can sensibly define this ordering for seq<T> values based on an element ordering on T values.

This is particularly valuable because Dafny defines < on string values to be "proper prefix of" to make termination proofs easier, but many many users will also want the more common definition as well.

We also need to be careful about implying that using this ordering on Dafny string values will align with the actual intentions, since char values are currently UTF-16 code units and therefore a naive lexicographic comparison will likely not be correct for most uses. This will still be true even after dafny-lang/rfcs#13 is implemented, since individual Unicode scalar values don't always correspond to human-perceived characters either. We will likely want separate stdlib utilities for Unicode-compliant collation. See https://unicode.org/reports/tr10/ for the gory details.

Very common ask from projects that want efficient executable code as well.

It would be very expensive to have enough static analysis/verification to detect when it is safe to rewrite myMap := myMap[k := v] as an update to a mutable value, so in the short term the better option is to offer Dafny bindings for target language implementations of mutable values with the appropriate specifications. These SHOULD be the concurrency-safe versions by default to ensure the specifications actually hold, but we could offer alternative faster versions that are only safe for sequential code.

Another spinoff from #49, which was de-scoped to use plain (T, T) -> bool predicates instead. A tri-valued comparison function tends to be more general and saves on the number of comparisons necessary in many algorithms.

We have a bunch of code from the compiler-bootstrap project that we can borrow from on this: https://github.com/dafny-lang/compiler-bootstrap/blob/28299a21101342e5384664c71103c562ad707a80/src/Utils/Library.dfy#L670

Follow-up from #49, which will close #39 but uses my quick-and-dirty-but-correct MergeSort from https://github.com/dafny-lang/dafny-reportgenerator/blob/main/src/StandardLibrary.dfy#L38. That code is actually very inefficient at runtime because it relies on s[..1] slices which currently impose a full copy.

I'd personally be happy with anything based on arrays instead of sequences, but as per #39 https://en.wikipedia.org/wiki/Timsort may be an even better option.

I suggest we move the relevant code in https://github.com/dafny-lang/libraries/blob/master/src/Wrappers.dfy to a separate module that contains a superset of the code below. I am following https://github.com/ocaml/ocaml/blob/trunk/stdlib/option.ml.

// RUN: %dafny /compile:0 "%s"

/*******************************************************************************
*  Copyright by the contributors to the Dafny Project
*  SPDX-License-Identifier: MIT 
*******************************************************************************/

module {:options "-functionSyntax:4"} Option {

  datatype Option<+T> = None | Some(value: T)

  function Some<T>(v: T): Option<T> {
    Option.Some(v)
  }

  function Bind<S,T>(o: Option<S>, f: S -> Option<T>): Option<T> {
    match o 
    case None => None
    case Some(v) => f(v)
  }

  predicate IsNone<T>(o: Option<T>) {
    o.None?
  }

  predicate IsSome<T>(o: Option<T>) {
    o.Some?
  }

  function Get<T>(o: Option<T>): (v: T) 
    requires o.Some?
    ensures o.value == v
  {
    o.value
  }
 
  function Join<T>(oo: Option<Option<T>>): Option<T> {
    match oo
    case None => None
    case Some(o) => o
  }

  function Map<S,T>(f: S -> T, o: Option<S>): (o2: Option<T>)
  {
    match o 
    case None => None
    case Some(v) => Some(f(v))
  }

  function Equal<T>(eq: (T, T) -> bool): (Option<T>, Option<T>) -> bool {
    (o1: Option<T>, o2: Option<T>) =>
      match (o1, o2)
      case (Some(v1), Some(v2)) => eq(v1, v2)
      case (None, None) => true
      case _ => false
  }
  
  function Compare<T>(cmp: (T, T) -> int): (Option<T>, Option<T>) -> int {
    (o1: Option<T>, o2: Option<T>) =>
      match (o1, o2)
      case (Some(v1), Some(v2)) => cmp(v1, v2)
      case (None, None) => 0
      case (None, Some(_)) => -1
      case (Some(_), None) => 1
  }

  function ToSeq<T>(o: Option<T>): seq<T> {
    match o 
    case None => []
    case Some(v) => [v]
  }

  function ToSet<T>(o: Option<T>): set<T> {
    match o
    case None => {}
    case Some(v) => {v}
  }

}

It would be nice to have LemmaUniqueMaximum, which should be analagous to LemmaUniqueMinimum in Sets.dfy.

This lemma proves this implication:

  lemma LemmaCardinalityOfSetNoDuplicates<T>(s: seq<T>)
    requires HasNoDuplicates(s)
    ensures |ToSet(s)| == |s|

But the opposite implication would also be very useful:

  lemma LemmaNoDuplicatesCardinalityOfSet<T>(s: seq<T>)
    requires |ToSet(s)| == |s|
    ensures HasNoDuplicates(s)

Especially because |ToSet(s)| == |s| is much cheaper to evaluate at runtime than HasNoDuplicates(s) would be (if it was a compiled function method)

(pulling a discussion from the original first big PR out: #7 (comment))

Besides what @samuelgruetter is saying about testing that pre- and post-conditions make sense, I want the CI to ensure the code can be compiled and run and produce the right results. Given that there are lots of function methods in this library and not just functions, it should be a requirement to ensure that the code is actually compilable and works correctly.

Here's a really simple example:

module SeqTest {
  import Seq
  method {:test} TestApply() {
    var input := [1, 2, 3, 4, 5];
    var output := Seq.apply(i => i * 2, input);
    expect output == [2, 4, 6, 8, 10];
  }
}

Building and testing would be a two step process:

dafny /compile:0 /spillTargetCode:2 <all Dafny source files>

That will still run verification on all the source files and potentially fail. If verification succeeds, you would then execute the resulting C# tests:

dotnet test

This would require a .csproj file similar to the one used in the Dafny test suite: https://github.com/dafny-lang/dafny/blob/master/Test/DafnyTests/DafnyTests.csproj.

The {:test} attribute is only handled by the C# compiler for now but we're adding support for the other target languages. Plus, as I mentioned in dafny-lang/dafny#1322 (comment), we should make the process a single simple step by adding something like a dafny test command.

Note that this implies dropping the lit tool for verifying and testing this library. lit is a great tool for testing compilers or CLI tools themselves, but it's a poor match for end-user programs using such tools. We shouldn't expect any of this code to fail to verify or compile, so we don't need the ability to assert the exact expected error/warning behavior. This project can instead serve as an example for best practices in maintaining Dafny code, which should only involve verifying, compiling, and running Dafny code.

Dropping lit will mean that we need to change the solution we set up for testing this package in the CI of the dafny-lang/dafny repo, but that is definitely doable, and can be handled at the same time that we update the submodule pointer to pick up the new version without lit header commands in all the Dafny files.

There is a decent mix of ->, -->, and ~> arrow types in this repo, owing mostly to personal taste and/or willingness to spend the time generalizing. Ideally all code would be maximally general and use ~>, but that does lead to more complicated specifications and verification so it is not free.

Should we add this to the style guide? Or even a CI mechanism to insist on ~>?

The upper bound of int16 should be 0x8000 (it is 0x80000)

https://github.com/dafny-lang/libraries/blob/master/src/Std.dfy#L9

I whipped up a quick mergesort implementation for the new dafny-reportgenerator tool, but more for fun than because I thought it was the absolute best default choice of algorithm for any Dafny user: https://github.com/dafny-lang/dafny-reportgenerator/blob/main/src/StandardLibrary.dfy#L38 There are lots of sorting algorithm implementations floating around in Dafny, including at least 4 in the regression suite. :) But there should be a sensible default implementation in the standard library.

I'd suggest implementing these signatures (with the appropriate pre- and post-conditions), for maximum flexibility (Edit: avoid requiring T<0> by using ToArray):

  method SortArray<T>(a: array<T>, compare: (T, T) -> bool) {
    ...
  }

  function Sort<T>(s: seq<T>, compare: (T, T) -> bool): seq<T> {
    ...
  } by method {
    var a := Seq.ToArray(s);  // From https://github.com/dafny-lang/libraries/blob/master/src/Collections/Sequences/Seq.dfy#L128
    SortArray(a, compare);
    return a[..];
  }

I'd recommend implementing Musser's Introspective Sort, which is becoming the standard: https://en.wikipedia.org/wiki/Introsort. I'd be happy with just a heapsort to start with, though, as it has the most predictable runtime and minimal space overhead if you're starting with a mutable array. We can always add the optimization of quicksort-until-it-tends-quadratic later.

Another wrinkle is how to parameterize by the comparison function. Expressing the total ordering requirements using forall expressions is easy IF we assume T is not a reference type, but I expect that will be limiting. Perhaps it's feasible to require the comparison function is a total ordering just over all values being sorted, rather than all possible T values?

Hello! As part of my Bachelor's and Master's thesis, @ClaraSegura, @manuelmontenegro and I have developed a library of mutable abstract data types. They are fully verified and specified in Dafny, with no calls to external code. We have taken into account how the user would use our library, so we have an extensive set of examples using the library. We have submitted a paper that explains our work to a journal. It is currently under review, but in the meantime you can check this conference paper, my Bachelor's Thesis or my Master's Thesis. The ADTs that we have developed are the following:

• Lists: implemented with doubly linked lists and with arrays.
• Stacks, queues and deques: with linked-based and array-based implementations.
• Maps, sets and multisets: their specification and implementation is currently experimental. We are working on their implementation based on red-black trees.

We have specified and verified mutable iterators for lists (although linked list iterators and vector iterators behave slightly differently, which is expressed in their specification). Iterators for maps/sets/multisets are currently very much work in progress, but they are our next target.

We don't know if this code would fit better as part of Dafny Core, as an "official" library in this repository or as a standalone library like it already is in our GitHub repository at https://github.com/jorge-jbs/adt-verification-dafny, so we are open to your comments.

lit.site.cfg looks for pydiff.py in the test_source_root directory on Windows platform. lit will error out when pydiff.py is missing. Potentially borrow the pydiff.py from dafny repo?

Very broad category, probably at least will become one library per target language.

Nearly all compiled Dafny code needs to convert between Dafny string values and native language string values for example. Projects like the Dafny ESDK have utilities for this, but not only is this not something Dafny users should have to implement themselves, but the linked implementation is coupled to Dafny compiler/runtime internals that are not guaranteed to remain stable across releases (and have definitely changed in the past, for good reasons).

In the long term it would be wonderful to not only provide these conversion functions, but also provide meta-utilities to generate the calls to these conversions automatically via something like annotations.

Follow-up from #7 (comment): we agree that while it is reasonable for a Dafny standard library to make limited use of triggers, we want to ensure that Dafny programmers are strongly encouraged to avoid triggers in their own code.

Follow-up from #13 (comment), which raced with the PR getting merged. :)

I propose we remove https://github.com/dafny-lang/libraries/blob/master/src/Wrappers.dfy and create a separate file for each of the existing wrappers, and for any wrapper we add in the future. (Perhaps it would be good to group them in one folder.) In particular, I suggest that we extend the existing code for the result monad such that it contains at least the code below. Please ignore the include of Wrappers.dfy for now. I am particularly impressed that Dafny proves all monad laws by itself.

include "Wrappers.dfy"

module {:options "-functionSyntax:4"} Result {

  import opened Wrappers 

  datatype Result<+S,+E> = | Success(value: S) | Failure(error: E)

  function Success<S,E>(v: S): Result<S,E> {
    Result.Success(v)
  }

  function Failure<S,E>(e: E): Result<S,E> {
    Result.Failure(e)
  }

  predicate IsSuccess<S,E>(r: Result<S,E>) {
    r.Success?
  }  

  predicate IsFailure<S,E>(r: Result<S,E>) {
    r.Failure?
  }  

  function GetValue<S,E>(r: Result<S,E>): S 
    requires r.Success?
  {
    r.value
  }

  function GetValueDefault<S,E>(r: Result<S,E>, default: S): S {
    match r 
    case Success(v) => v
    case Failure(_) => default
  }

  function GetError<S,E>(r: Result<S,E>): E 
    requires r.Failure?
  {
    r.error
  }

  function Bind<S1,S2,E>(r: Result<S1,E>, f: S1 -> Result<S2,E>): Result<S2,E> {
    match r
    case Success(v) => f(v)
    case Failure(e) => Result<S2,E>.Failure(e)
  }

  function Join<S,E>(rr: Result<Result<S,E>,E>): Result<S,E> {
    match rr
    case Success(v) => v
    case Failure(e) => Result<S,E>.Failure(e)
  }

  function Map<S1,S2,E>(f: S1 -> S2): Result<S1,E> -> Result<S2,E> {
    (r: Result<S1,E>) =>
      match r 
      case Success(v) => Result<S2,E>.Success(f(v))
      case Failure(e) => Result<S2,E>.Failure(e)
  }

  function MapError<S,E1,E2>(f: E1 -> E2): Result<S,E1> -> Result<S,E2> {
    (r: Result<S,E1>) =>
      match r 
      case Success(v) => Result<S,E2>.Success(v)
      case Failure(e) => Result<S,E2>.Failure(f(e))
  }  

  function Fold<S,E,T>(f: S -> T, g: E -> T): Result<S,E> -> T {
    (r: Result<S,E>) =>
      match r 
      case Success(v) => f(v)
      case Failure(e) => g(e)
  }

  function Composition<S1,S2,S3,E>(f: S1 -> Result<S2,E>, g: S2 -> Result<S3,E>): S1 -> Result<S3,E> {
    x => Bind(f(x), g)
  }

  function ToSeq<S,E>(r: Result<S,E>): seq<S> {
    match r
    case Success(v) => [v]
    case Failure(_) => []
  }

  function ToSet<S,E>(r: Result<S,E>): set<S> {
    match r
    case Success(v) => {v}
    case Failure(_) => {}   
  }

  function ToOption<S,E>(r: Result<S,E>): Option<S> {
    match r
    case Success(v) => Some(v)
    case Failure(_) => None()
  }

  lemma LemmaUnitalityJoin<S,E>(r: Result<S,E>)
    ensures Join(Map(Success<S,E>)(r)) == r == Join(Success<Result<S,E>,E>(r))
  {
  }

  lemma LemmaAssociativityJoin<S,E>(rrr: Result<Result<Result<S,E>,E>,E>) 
    ensures Join(Map(Join<S,E>)(rrr)) == Join(Join<Result<S,E>,E>(rrr))
  {
  }  

  lemma LemmaLeftUnitalityBind<S1,S2,E>(v: S1, f: S1 -> Result<S2,E>)
    ensures Bind(Success(v), f) == f(v)
  {
  }

  lemma LemmaRightUnitalityBind<S,E>(r: Result<S,E>)
    ensures Bind(r, Success) == r
  {
  }

  lemma LemmaAssociativityBind<S1,S2,S3,E>(r: Result<S1,E>, f: S1 -> Result<S2,E>, g: S2 -> Result<S3,E>)
    ensures Bind(Bind(r, f), g) == Bind(r, Composition(f, g))
  {
  }

}

At the very least the Valid()/Repr idiom is not something Dafny users tend to stumble on by themselves. That idiom is also very general, and a more structured specialization of it would be good enough for a lot of Dafny code and much easier to work with.

#22 is a very basic first step towards this but unfortunately blocked by dafny-lang/dafny#1588. It may be possible to avoid that and @seebees and @jtristan have been working on an alternative.

Very challenging to model well to support verification and interoperability with other programming languages. #37 is a good start but I'm dissatisfied with the explosion of different interfaces it was steering into.

Consider the following

function Work() : Result<int, string> {
  var something := Magic();
  :- Need(|something| == 0, "Woops => " + Join(something, ","));
}

function Join(ss: seq<string>) : string
  requires 0 < |ss|

This will fail to verify.
Because Join requires 0 < |something|.
But we know (because this is how Need works,
that this condition is only important if |something| != 0.

It would be great to both rely on this.
But also to automatically thunk the second argument.
This way Dafny users can write nice clear code,
and get all the efficiency benefits in the compiler :)

This issue duplicates #2430 in the Dafny project.

There is a Dafny style guide in the main Dafny project. There is a modification of that style guide in the libraries project.

Duplicating information leads to maintenance headaches.

I propose consolidating to one style guide (in the main project) that is referenced from the libraries project.

Follow up from: #15 (comment)

Blocked by dafny-lang/dafny#1481

This was cut out of scope from #60 because of the blocking issues dafny-lang/dafny#2989 (which prevents declaring {:extern} methods returning string) and dafny-lang/dafny#2045 (which leaves Golang incompatible with the one-{:extern}-fits-all approach).

Update ModInternals to use assert by

Example:

src/NonlinearArithmetic/Internals/ModInternals.dfy(94,4): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead

I found this repo through a StackOverflow post, which links to some filesystem externs. The repo has a lot more than that, however, and much of which would be helpful in a standard library.

The latter is better organized and documented, but we need to give customers at least some time to migrate off the former before we start only adding code to the latter.

Follow-up from #7, which includes functions like Subset on maps and imaps: https://github.com/dafny-lang/libraries/blob/master/src/Collections/Maps/Maps.dfy#L65

Ideally we can switch the whole repo over to the new syntax and use the CLI option directly, or we could do it more incrementally if necessary via {:options "/functionSyntax:4"}.

I'm seeing many warnings of the form:

o:\Projects\Science\dafny\libraries\src\Collections\Sequences\Seq.dfy(138,32): Warning: deprecated style: a semi-colon is not needed here
    |
139 |     requires xs' == xs[a..b];
    |                             ^

I assume this has to do with different version of Dafny have slightly different syntax.

Hello. I am working on gaining more experience with Dafny and thought it would be good to check if there is any library in particular that would be especially welcome in this repository at the moment. Thanks!

We already kind of have ordered sets because of definitions like https://github.com/dafny-lang/libraries/blob/master/src/Collections/Sequences/Seq.dfy#L182. In both cases it would be very nice to provide subset types for these concepts.

What it says on the tin :)

Currently it looks like there are two versions of the library existing at the same time in the repo, but it's not at all clear why this is the case.

It would be good if the main Readme.md would explain what is going on here, and what someone who's looking at the repo for the first time should be using.

Presumably there's a good rational for this duplication rather than just having two branches, but to a newcomer it's a little hard to understand what's going on.

My impression is I should use the code in the 'dafny' subdirectory. But if I want to add functionality to the library, do I need to modify both versions, or do I only need to worry about the code in the 'dafny' subdirectory?

Follow-up from #7 (comment): we agree that while it is reasonable for a Dafny standard library to make limited use of triggers, we want to ensure that Dafny programmers are strongly encouraged to avoid triggers in their own code.

We made some progress but couldn't get my workaround to verify on Dafny 4.0, and although @RustanLeino made progress on fixing Java backend limitations there are still some remaining.

Only implemented for Java so far

Care of @ajewellamz, some suggestions for useful utilities when working with the JSON library:

  function DecimalToNat(num: Decimal) : Result<nat, string>
  {
    :- Need(num.n >= 0, "Number must be > 0");
    if num.n == 0 then
      Success(0)
    else
      :- Need(num.e10 >= 0, "Number must be a whole number");
      :- Need(num.e10 < 100, "Number must be less than a googol");
      Success(GetPower(num.n, num.e10))
  }

  function DecimalToInt(num: Decimal) : Result<int, string>
  {
    if num.n == 0 then
      Success(0)
    else
      :- Need(num.e10 >= 0, "Number must be a whole number");
      :- Need(num.e10 < 100, "Number must be less than a googol");
      Success(GetPower(num.n, num.e10))
  }

  function DecimalToStr(num: Decimal) : Result<string, string>
  {
    if num.n == 0 then
      Success("0")
    else
      :- Need(-1000 < num.e10 < 1000, "Exponent must be between -1000 and 1000");
      var str := String.Base10Int2String(num.n);
      if num.e10 >= 0 then
        Success(str + Zeros(num.e10))
      else if -num.e10 < |str| then
        var pos := |str| + num.e10;
        Success(str[..pos] + "." + str[pos..])
      else
        Success("0." + Zeros(|str| - num.e10) + str)
  }

  // Return a string of this many zeros
  function Zeros(n : nat) : (ret : string)
  {
    seq(n, i => '0')
  }

  // return n x 10^pow
  function GetPower(n : nat, pow : nat) : nat
  {
    if pow == 0 then
      n
    else
      10 * GetPower(n, pow-1)
  }

The following should probably be in the stdlib:

include "../../libraries/src/Collections/Sequences/MergeSort.dfy"
include "../../libraries/src/Relations.dfy"

module {:options "-functionSyntax:4"} Set.Sort {
  import opened Seq.MergeSort
  import opened Relations

  ghost function GhostSetToSeq<X>(xs: set<X>): (xx: seq<X>)
    ensures multiset(xs) == multiset(xx)
  {
    if xs == {} then [] else var x :| x in xs; [x] + GhostSetToSeq(xs - {x})
  }

  method SetToSeq<X>(xs: set<X>) returns (xx: seq<X>)
    ensures multiset(xs) == multiset(xx)
  {
    xx := [];
    var left: set<X> := xs;
    while left != {}
      invariant multiset(left) + multiset(xx) == multiset(xs)
    {
      var x :| x in left;
      left := left - {x};
      xx := xx + [x];
    }
  }

  lemma SortedUnique<X>(xx: seq<X>, xx': seq<X>, lessThanOrEq: (X, X) -> bool)
    requires SortedBy(xx, lessThanOrEq)
    requires SortedBy(xx', lessThanOrEq)
    requires TotalOrdering(lessThanOrEq)
    requires multiset(xx) == multiset(xx')
    ensures xx == xx'
  {
    assert |xx| == |multiset(xx)| == |multiset(xx')| == |xx'|;
    if xx == [] || xx' == [] {
    } else {
      assert xx == [xx[0]] + xx[1..];
      assert xx' == [xx'[0]] + xx'[1..];
      assert multiset(xx[1..]) == multiset(xx) - multiset{xx[0]};
      assert multiset(xx'[1..]) == multiset(xx') - multiset{xx'[0]};
      assert xx[0] == xx'[0]; // ??
      assert multiset(xx[1..]) == multiset(xx'[1..]); // ??
      SortedUnique(xx[1..], xx'[1..], lessThanOrEq);
    }
  }

  function SortSet<X>(xs: set<X>, lessThanOrEq: (X, X) -> bool): (xx: seq<X>)
    requires TotalOrdering(lessThanOrEq)
    ensures multiset(xs) == multiset(xx)
    ensures SortedBy(xx, lessThanOrEq)
  {
    MergeSortBy(GhostSetToSeq(xs), lessThanOrEq)
  } by method {
    xx := SetToSeq(xs);
    xx := MergeSortBy(xx, lessThanOrEq);
    SortedUnique(xx, SortSet(xs, lessThanOrEq), lessThanOrEq);
  }
}

I was impressed to see the two lines marked // ?? prove automatically. I supposed Dafny is using this:

      assert xx[0] in multiset(xx');
      assert xx'[0] in multiset(xx);
      assert lessThanOrEq(xx[0], xx'[0]);
      assert lessThanOrEq(xx'[0], xx[0]);
      assert xx[0] == xx'[0];

If C is a compile target,
these function are useful.
However, it is hard because they use int | nat et al.
This makes sense,
but blocks using theses function if you want to support a C compile target.

There are many ways that might work to support this.
This might imply some feature in Dafny
such that if I can prove that I'm always using bounded numbers,
then everything will just work.

Fair warning, this is one of my classic thinking out loud issues that may not be immediately actionable. :)

I'm glad that the majority of the function definitions in this repository are function methods, so that it is possible for consumers to use them at runtime if they so desire. As per the discussion in dafny-lang/dafny#1492 this is definitely part of the contract of the definition, and it doesn't make sense for the language to support consumers making this decision instead.

However, runtime efficiency is not currently an explicit goal of these libraries, and yet there should be some very low-hanging fruit in terms of easy, classic functional programming optimizations. For example, Seq.FoldRight is not tail-recursive, so it could very easily lead to a stack overflow in several target languages:

Besides actually improving the implementations here, we need to actually define where the sweet spot should be in terms of runtime efficiency, and add some actual mechanisms in the CI to ensure the expectations are met. This will be tightly coupled to the Dafny compiler and runtime implementations themselves, to ensure the idioms we encourage at least eventually lead to good runtime performance.

For example, repeatedly concatenating small sequences (as most of the functions in Seq.dfy do recursively) should be considered an efficient pattern. That is currently only the case when compiling to C# and Java, since they have lazy evaluation of sequence concatenation, but this should be a property of any runtime and therefore not a reason to make the Dafny code more complex to work around it (such as by defining a List<T> = Nil | Cons(car: T, cdr: List<T>) datatype to use instead).

I've been intentionally cautious about this, since it requires linking to external code in each language no matter how you slice it. But I think the timing is right to experiment with very basic methods for reading and writing files, without streaming and without any model of the file system.

Since this repo contains only "pure" Dafny logic and no externs, I assert the I/O should go into a separate repo. That way we can continue to support consuming this repo as a simple submodule, whereas the I/O library will have to be packaged together with native code in some way.

This was cut out of scope from #60 because of complications with importing the necessary helper code from translated Python code.

Already implemented as a Dafny integration test: https://github.com/dafny-lang/dafny/blob/master/Test/dafny4/BinarySearch.dfy

I notice there are two Math.dfy files. One in src and one in src/dafny

I'm using a new VS code, Dafny add-in install on Windows. When I try to compile
src\Math.dfy (or src\Collections\Sequences\Seq.dfy) I get an error:

Dafny program verifier finished with 1 verified, 0 errors
Errors compiling program into library_example
(3009,40): error CS0234: The type or namespace name 'Abs' does not exist in the namespace 'Math' (are you missing an assembly reference?)

I can work around the error by renaming the module in src/Math.dfy to "Math2" and also changing the import in Seq.dfy.

Follow-up to #7: This repository doesn't have any checks running to verify the source code yet.

Forked off from dafny-lang/dafny#2062 : it would be nice to have a canonical way to fold over a set (including converting it to a sequence) that's reasonably fast.

For conversion to a sequence we want to be deterministic, so we need to sort. For folding, we could iterate in undetermined order, as long as the function that we're folding is symmetric and associative (or more precisely, as long as forall x, y, a | x in s && y in s :: f(x, f(y, a)) == f(y, f(x, a)) for f: T -> TAcc -> TAcc).