Real programs,
really proved.

//  Pipelines over arrays: reductions, filters, quantifiers and collections, each one
//  fused loop with generated invariants; reductions in contracts mean ghost folds.
package Stats {
    pub subtype Score = Integer range 0..=100;
    pub type Scores = [Positive..]Score;

    //  the sum, and the sum of those that pass
    pub fn Total(A: Scores) -> Integer
        requires A::Length <= 1000
    = A::Reduce("+", 0);

    pub fn Passing_Total(A: Scores, Mark: Score) -> Integer
        requires A::Length <= 1000
    = A.filter(X => X >= Mark).sum();

    //  how many pass: each counts one
    pub fn Passing(A: Scores, Mark: Score) -> Natural
        requires A::Length <= 1000
    = A.filter(X => X >= Mark).count();

    //  a range's values, mapped (the range's bounds bound its values)
    pub subtype Count = Natural range 0..=100;

    pub fn Sum_Of_Squares(N: Count) -> Natural = [for I in 1..=N => I * I]::Reduce("+", 0);

    //  the largest, by a function reducer
    pub fn Best(A: Scores) -> Score = A::Reduce(Score::Max, 0);

    //  quantifiers, with and without a filter
    pub fn All_Valid(A: Scores) -> Boolean = A.all(X => X <= 100);

    pub fn Any_Perfect(A: Scores) -> Boolean = A.any(X => X == 100);

    //  the scores that pass, collected into an array as long as their number
    pub fn Above(A: Scores, Mark: Score) -> Scores
        requires A::Length <= 1000
    = A.filter(X => X > Mark).collect();

    //  each score curved, collected; nothing filtered, so as long as the source
    pub fn Curved(A: Scores) -> Scores
        requires (A::First == 1) & (A::Length <= 1000)
        ensures result::Length == A::Length
    = A.map(X => (X + 100) / 2).collect();

    //  a loop the programmer writes, proved against the reduction it computes
    pub fn Running_Total(A: Scores) -> Integer
        requires A::Length <= 1000
        ensures result == A::Reduce("+", 0)
    {
        var S: Integer = 0;
        for I in A::Range {
            invariant (S == [for J in A::First..=I - 1 => A[J]]::Reduce("+", 0)) & (S <= 100 * (I - A::First));
            S = S + A[I];
        }
        return S;
    }
}

import Ada.Text_IO;
use Ada.Text_IO;
import Stats;
use Stats;
fn Main() {
    let Class: Scores = (72, 45, 100, 88, 61, 39, 95);
    let High: Scores = Above(Class, 80);
    let Fair: Scores = Curved(Class);
    Put_Line("total" ++ Integer::Image(Total(Class)) ++ Integer::Image(Running_Total(Class)));
    Put_Line("passing" ++ Integer::Image(Passing(Class, 60)) ++ Integer::Image(Passing_Total(Class, 60)));
    Put_Line("squares" ++ Integer::Image(Sum_Of_Squares(10)));
    Put_Line("best" ++ Integer::Image(Best(Class)));
    Put_Line("valid " ++ Boolean::Image(All_Valid(Class)) ++ ", perfect " ++ Boolean::Image(Any_Perfect(Class)));
    Put("above 80:");
    for S in High {
        Put(Integer::Image(S));
    }
    New_Line();
    Put("curved:");
    for S in Fair {
        Put(Integer::Image(S));
    }
    New_Line();
}

--  Pipelines over arrays: reductions, filters, quantifiers and collections, each one
--  fused loop with generated invariants; reductions in contracts mean ghost folds.
package Stats is
   subtype Score is Integer range 0 .. 100;
   type Scores is array (Positive range <>) of Score;

   --  the sum, and the sum of those that pass
   function Total (A : Scores) return Integer is (A'Reduce ("+", 0))
   with Pre => A'Length <= 1000;

   function Passing_Total (A : Scores; Mark : Score) return Integer is
     ([for X of A when X >= Mark => X]'Reduce ("+", 0))
   with Pre => A'Length <= 1000;

   --  how many pass: each counts one
   function Passing (A : Scores; Mark : Score) return Natural is
     ([for X of A when X >= Mark => 1]'Reduce ("+", 0))
   with Pre => A'Length <= 1000;

   --  a range's values, mapped (the range's bounds bound its values)
   subtype Count is Natural range 0 .. 100;
   function Sum_Of_Squares (N : Count) return Natural is
     ([for I in 1 .. N => I * I]'Reduce ("+", 0));

   --  the largest, by a function reducer
   function Best (A : Scores) return Score is (A'Reduce (Score'Max, 0));

   --  quantifiers, with and without a filter
   function All_Valid (A : Scores) return Boolean is (for all X of A => X <= 100);
   function Any_Perfect (A : Scores) return Boolean is (for some X of A => X = 100);

   --  the scores that pass, collected into an array as long as their number
   function Above (A : Scores; Mark : Score) return Scores is
     ([for X of A when X > Mark => X])
   with Pre => A'Length <= 1000;

   --  each score curved, collected; nothing filtered, so as long as the source
   function Curved (A : Scores) return Scores is ([for X of A => (X + 100) / 2])
   with Pre => A'First = 1 and A'Length <= 1000,
        Post => Curved'Result'Length = A'Length;

   --  a loop the programmer writes, proved against the reduction it computes
   function Running_Total (A : Scores) return Integer
   with Pre => A'Length <= 1000,
        Post => Running_Total'Result = A'Reduce ("+", 0);
end Stats;

package body Stats is
   function Running_Total (A : Scores) return Integer is
      S : Integer := 0;
   begin
      for I in A'Range loop
         pragma Loop_Invariant
           (S = [for J in A'First .. I - 1 => A (J)]'Reduce ("+", 0)
            and S <= 100 * (I - A'First));
         S := S + A (I);
      end loop;
      return S;
   end Running_Total;
end Stats;

"""A bounded buffer between tasks."""

from byron import Array, Modular, Natural, Protected, entry, when


class Slot(Modular, modulus=4):
    pass


class Ring(Array[int], index=Slot):
    pass


class Buffer(Protected):
    items: Ring = Ring([0, 0, 0, 0])
    first: Slot = 0
    count: Natural = 0

    @entry
    def put(self, x: int) -> None:
        when(self.count < 4)
        self.items[self.first + Slot(self.count)] = x
        self.count = self.count + 1

    @entry
    def get(self) -> int:
        when(self.count > 0)
        x = self.items[self.first]
        self.first = self.first + 1
        self.count = self.count - 1
        return x


shared = Buffer()

"""Two tasks: a producer of squares and a consumer that prints them, then ends the program."""

from byron import sleep, stop, task

from buffers import shared


@task
def producer() -> None:
    for i in range(1, 6):
        shared.put(i * i)
    while True:
        sleep(1.0)


@task
def consumer() -> None:
    for _ in range(5):
        x: int = shared.get()
        print("got", x)
    stop()
    while True:
        sleep(1.0)

import workers


# the program is its tasks: the main function has nothing to do
def main() -> None:
    pass