# Flux Storm

## V1

#[flux::opaque]
#[flux::refined_by(inv: R -> bool)]
pub struct Query<R> {
    _marker: std::marker::PhantomData<R>,
}

#[flux::generics(R as base)]
impl<R> Query<R> {
    #[flux::trusted]
    #[flux::sig(fn(Query<R>[@q1], Query<R>[@q2]) -> Query<R>[|r| q1(r) && q2(r)])]
    fn and(self, rhs: Query<R>) -> Query<R> {
        Query { _marker: std::marker::PhantomData }
    }

    #[flux::sig(fn(self: Query<R>[@q]) -> R{v: q(v)})]
    fn run(self) -> R {
        todo!()
    }
}

#[flux::refined_by(price: int)]
struct Wish {
    #[flux::field(i32[price])]
    price: i32,
}

struct WishPrice;

#[flux::generics(R as base, V as base)]
#[flux::assoc(fn proj(row: R) -> V)]
trait Field<R, V> {}

#[flux::assoc(fn proj(row: Wish) -> int { row.price })]
impl Field<Wish, i32> for WishPrice {}

#[flux::trusted]
#[flux::sig(fn<R as base, V as base>(f: F, v: V) -> Query<R>[|r| <F as Field<R, V>>::proj(r) == v])]
fn eq<R, V, F: Field<R, V>>(f: F, v: V) -> Query<R> {
    Query { _marker: std::marker::PhantomData }
}

#[flux::trusted]
#[flux::sig(fn<R as base, V as base>(f: F, v: V) -> Query<R>[|r| <F as Field<R, V>>::proj(r) > v])]
fn gt<R, V, F: Field<R, V>>(f: F, v: V) -> Query<R> {
    Query { _marker: std::marker::PhantomData }
}

#[flux::trusted]
#[flux::sig(fn<R as base, V as base>(f: F, v: V) -> Query<R>[|r| <F as Field<R, V>>::proj(r) < v])]
fn lt<R, V, F: Field<R, V>>(f: F, v: V) -> Query<R> {
    Query { _marker: std::marker::PhantomData }
}

#[flux::sig(fn() -> i32{v: v > 0 && v < 10})]
fn client() -> i32 {
    let query = gt(WishPrice, 0).and(lt(WishPrice, 10));
    let wish = query.run();
    wish.price
}

## V2

#[flux::generics(R as base, Self as base)]
#[flux::assoc(
    fn run(self: Self, row: R) -> bool
)]
trait Query<R>: Sized {
    #[flux::trusted]
    #[flux::sig(fn<Rhs as base>(self: Self, rhs: Rhs) -> And<Self, Rhs>[self, rhs])]
    fn and<Rhs>(self, rhs: Rhs) -> And<Self, Rhs>
    where
        Rhs: Query<R>,
    {
        todo!()
    }

    #[flux::trusted]
    #[flux::sig(fn(self: Self) -> R{row: <Self as Query<R>>::run(self, row)})]
    fn run(self) -> R {
        todo!()
    }
}

#[flux::opaque]
#[flux::refined_by(q1: Q1, q2: Q2)]
struct And<Q1, Q2> {
    _q1: std::marker::PhantomData<Q1>,
    _q2: std::marker::PhantomData<Q2>,
}

#[flux::generics(R as base, Q1 as base, Q2 as base)]
#[flux::assoc(
    fn run(query: And<Q1, Q2>, row: R) -> bool {
        <Q1 as Query<R>>::run(query.q1, row) && <Q2 as Query<R>>::run(query.q2, row)
    }
)]
impl<R, Q1, Q2> Query<R> for And<Q1, Q2>
where
    Q1: Query<R>,
    Q2: Query<R>,
{
}

#[flux::opaque]
#[flux::refined_by(val: V)]
struct Eq<F, V> {
    _field: std::marker::PhantomData<F>,
    _val: std::marker::PhantomData<V>,
}

#[flux::generics(R as base, V as base)]
#[flux::assoc(
    fn run(query: Eq<V>, row: R) -> bool {
        <F as Field<R, V>>::proj(row) == query.val
    }
)]
impl<R, F, V> Query<R> for Eq<F, V> where F: Field<R, V> {}

#[flux::opaque]
#[flux::refined_by(val: V)]
struct Gt<F, V> {
    _field: std::marker::PhantomData<F>,
    _val: std::marker::PhantomData<V>,
}

#[flux::generics(R as base, V as base)]
#[flux::assoc(
    fn run(query: Gt<V>, row: R) -> bool {
        <F as Field<R, V>>::proj(row) > query.val
    }
)]
impl<R, F, V> Query<R> for Gt<F, V> where F: Field<R, V> {}

#[flux::opaque]
#[flux::refined_by(val: V)]
struct Lt<F, V> {
    _field: std::marker::PhantomData<F>,
    _val: std::marker::PhantomData<V>,
}

#[flux::generics(R as base, V as base)]
#[flux::assoc(
    fn run(query: Lt<V>, row: R) -> bool {
        <F as Field<R, V>>::proj(row) < query.val
    }
)]
impl<R, F, V> Query<R> for Lt<F, V> where F: Field<R, V> {}

#[flux::generics(R as base, V as base)]
#[flux::assoc(fn proj(row: R) -> V)]
trait Field<R, V> {}

#[flux::refined_by(price: int)]
struct Wish {
    #[flux::field(i32[price])]
    price: i32,
}

struct WishPrice;

#[flux::assoc(fn proj(w: Wish) -> int { w.price })]
impl Field<Wish, i32> for WishPrice {}

#[flux::trusted]
#[flux::sig(fn<R as base, V as base>(f: F, v: V) -> Eq<F, V>[v])]
fn eq<R, V, F: Field<R, V>>(f: F, v: V) -> Eq<F, V> {
    Eq { _field: std::marker::PhantomData, _val: std::marker::PhantomData }
}

#[flux::trusted]
#[flux::sig(fn<R as base, V as base>(f: F, v: V) -> Gt<F, V>[v])]
fn gt<R, V, F: Field<R, V>>(f: F, v: V) -> Gt<F, V> {
    Gt { _field: std::marker::PhantomData, _val: std::marker::PhantomData }
}

#[flux::trusted]
#[flux::sig(fn<R as base, V as base>(f: F, v: V) -> Lt<F, V>[v])]
fn lt<R, V, F: Field<R, V>>(f: F, v: V) -> Lt<F, V> {
    Lt { _field: std::marker::PhantomData, _val: std::marker::PhantomData }
}

#[flux::sig(fn() -> i32{v: v > 0 && v < 10})]
fn client() -> i32 {
    let query = gt(WishPrice, 0).and(lt(WishPrice, 10));
    let wish = query.run();
    wish.price
}

## V3

#[flux::generics(Self as base, R as base)]
#[flux::assoc(fn eval(expr: Self, row: R) -> <Self as Expr<R>>::Value)]
trait Expr<R>: Sized {
    type Value;
}

#[flux::generics(R as base)]
#[flux::assoc(fn eval(val: int, _: R) -> int { val })]
impl<R> Expr<R> for i32 {
    type Value = i32;
}

#[flux::refined_by(price: int)]
struct Wish {
    #[flux::field(i32[price])]
    price: i32,
}

struct WishPrice;

#[flux::assoc(fn eval(_: WishPrice, wish: Wish) -> int { wish.price })]
impl Expr<Wish> for WishPrice {
    type Value = i32;
}

#[flux::opaque]
#[flux::refined_by(lhs: E1, rhs: E2)]
struct Gt<E1, E2> {
    _lhs: std::marker::PhantomData<E1>,
    _rhs: std::marker::PhantomData<E2>,
}

#[flux::generics(R as base, E1 as base, E2 as base)]
#[flux::assoc(
    fn eval(expr: Gt<E1, E2>, row: R) -> bool {
        <E1 as Expr<R>>::eval(expr.lhs, row) > <E2 as Expr<R>>::eval(expr.rhs, row)
    }
)]
impl<R, E1, E2, V> Expr<R> for Gt<E1, E2>
where
    E1: Expr<R, Value = V>,
    E2: Expr<R, Value = V>,
{
    type Value = bool;
}

#[flux::opaque]
#[flux::refined_by(lhs: E1, rhs: E2)]
struct And<E1, E2> {
    _lhs: std::marker::PhantomData<E1>,
    _rhs: std::marker::PhantomData<E2>,
}

#[flux::generics(R as base, E1 as base, E2 as base)]
#[flux::assoc(
    fn eval(expr: And<E1, E2>, row: R) -> bool {
        <E1 as Expr<R>>::eval(expr.lhs, row) && <E2 as Expr<R>>::eval(expr.rhs, row)
    }
)]
impl<R, E1, E2> Expr<R> for And<E1, E2>
where
    E1: Expr<R, Value = bool>,
    E2: Expr<R, Value = bool>,
{
    type Value = bool;
}

## V4

#[flux::generics(Self as base, R as base)]
#[flux::assoc(fn eval(expr: Self, row: R) -> V)]
trait Expr<R, V>: Sized {}

#[flux::generics(R as base)]
#[flux::assoc(fn eval(val: int, _: R) -> int { val })]
impl<R> Expr<R, i32> for i32 {}

#[flux::refined_by(price: int)]
struct Wish {
    #[flux::field(i32[price])]
    price: i32,
}

struct WishPrice;

#[flux::assoc(fn eval(_: WishPrice, wish: Wish) -> int { wish.price })]
impl Expr<Wish, i32> for WishPrice {}

#[flux::opaque]
#[flux::refined_by(lhs: E1, rhs: E2)]
struct Gt<V, E1, E2> {
    _value: std::marker::PhantomData<V>,
    lhs: E1,
    rhs: E2,
}

#[flux::generics(R as base, E1 as base, E2 as base, V as base)]
#[flux::assoc(
    fn eval(expr: Gt<E1, E2>, row: R) -> bool {
        <E1 as Expr<R, V>>::eval(expr.lhs, row) > <E2 as Expr<R, V>>::eval(expr.rhs, row)
    }
)]
impl<R, E1, E2, V> Expr<R, bool> for Gt<V, E1, E2>
where
    E1: Expr<R, V>,
    E2: Expr<R, V>,
{
}

#[flux::opaque]
#[flux::refined_by(lhs: E1, rhs: E2)]
struct And<E1, E2> {
    lhs: E1,
    rhs: E2,
}

#[flux::generics(R as base, E1 as base, E2 as base)]
#[flux::assoc(
    fn eval(expr: And<E1, E2>, row: R) -> bool {
        <E1 as Expr<R, bool>>::eval(expr.lhs, row) && <E2 as Expr<R, bool>>::eval(expr.rhs, row)
    }
)]
impl<R, E1, E2> Expr<R, bool> for And<E1, E2>
where
    E1: Expr<R, bool>,
    E2: Expr<R, bool>,
{
}

#[flux::trusted]
#[flux::generics(R as base, V as base, E1 as base, E2 as base)]
#[flux::sig(fn(lhs: E1, rhs: E2) -> Gt<V, E1, E2>[lhs, rhs])]
fn gt<R, V, E1, E2>(lhs: E1, rhs: E2) -> Gt<V, E1, E2>
where
    E1: Expr<R, V>,
    E2: Expr<R, V>,
{
    Gt { _value: std::marker::PhantomData, lhs, rhs }
}

#[flux::sig(
    fn<R as base, Q as base>(query: Q) -> R{row: <Q as Expr<R, bool>>::eval(query, row)}
)]
fn run<R, Q>(query: Q) -> R
where
    Q: Expr<R, bool>,
{
    todo!()
}

#[flux::sig(fn() -> i32{v: v > 0 })]
fn client() -> i32 {
    let query = gt(WishPrice, 0);
    let wish = run(query);
    wish.price
}

## Horn/App

a0 (func(0, [int;bool]))

(qualif Asdf ((v int) (a0 (Pred @(0)))) (papp1 a0 v))

(var $k0 ((int) ((Pred int))))

(constant papp1 (func(1, [(Pred  @(0)); @(0); bool])))

(constraint
  (forall ((a0 (Pred int)) (true))
    (and
      (forall ((x int) (papp1 a0 x))
        (($k0 x a0)))
      (forall ((y int) ($k0 y a0))
        (forall ((v int) (true))
         (($k0 v a0))
        )
      )
      (forall ((z int) ($k0 z a0))
        ((papp1 a0 z))
      )
    )
  )
)

(constant a0 (func(0, [int;bool])))
(qualif Asdf ((v int)) (a0 v))

(var $k0 ((int) ((func(0, [int; bool])))))

(constraint
  (and
    (forall ((x int) (a0 x))
      (($k0 x a0)))
    (forall ((y int) ($k0 y a0))
      (forall ((v int) (v = y))
       (($k0 v a0))
      )
    )
    (forall ((z int) ($k0 z a0))
      ((a0 z))
    )
  )
)

(fixpoint "--allowho")

(fixpoint "--allowhoqs")

(qualif MyQual ((v int) (p (func(0, [int;bool])))) (p v))

(var $k0 ((int) ((func(0, [int;bool])))))

(constraint
  (forall ((p0 (func(0, [int;bool]))) (true))
    (and
      (forall ((x int) (p0 x))
        (($k0 x p0)))
      (forall ((y int) ($k0 y p0))
        (forall ((v int) ((v = y)))
         (($k0 v p0))
        )
      )
      (forall ((z int) ($k0 z p0))
        (tag (p0 z) "h")
      )
    )
  )
)

(qualif Asdf ((v @(0)) (a0 (Pred @(0)))) (papp1 a0 v))

(var $k0 ((int) ((Pred int))))

(constant papp1 (func(1, [(Pred  @(0)); @(0); bool])))

(constraint
  (forall ((a0 (Pred int)) (true))
    (and
      (forall ((x int) (papp1 a0 x))
        (($k0 x a0)))
      (forall ((y int) ($k0 y a0))
        (forall ((v int) (v = y))
         (($k0 v a0))
        )
      )
      (forall ((z int) ($k0 z a0))
        ((papp1 a0 z))
      )
    )
  )
)

## Update Stuff / Changeset etc.

fn upd_where1(t: &Table, q:&Query, f1:Field, v1:Val);
fn upd_where2(t: &Table, q:&Query, f1:Field, v1:Val, f2:Field, v2:Val);
fn upd_where3(t: &Table, q:&Query, f1:Field, v1:Val, f2:Field, v2:Val, f3:Field,v3:Val);

## Tracking Contexts and Users

// lib.rs

#[flux::refined_by(user: U)]
struct Ctxt<U> {
    user: std::maker::PhantomData<U>,
    
}


authUser : forall User. () -> User

impl<U> Ctxt<U> {
    fn new(...) -> Ctxt<U>;
    
    fn require_session_user(&self) -> Option<U>;
}

// client.rs

#[flux::refined_by(id: int, level: int)]
struct User {
    id: i32,
    name: String,
    level: usize,
}

type Ctxt = rdiesel::Ctxt<User>;


// policy = |user, old| user.level == admin