rdivyanshu

From RecordUpdate Require Import RecordUpdate.
From stdpp Require Import gmap.

From TLA Require Import logic.

Module OneBit.

  Inductive pc := ncs | wait | w2 | w3 | w4 | cs | exit.
  Inductive threads := t0 | t1.

rdivyanshu

datatype State = State(min: int)

predicate Init(s: State){
  s.min == 5
}

predicate EnabledDecreaseMin(s: State){
  s.min > 0
}

rdivyanshu

#const n = 4.

% count(X, Y, N) - Number of ghoulish fiends (N) visible from X, Y.
% Grid is extended to include 0th and (n + 1)th row as well as 0th and (n + 1)th column
count(0, 1, 0). count(0, 2, 2). count(0, 3, 2). count(0, 4, 3).
count(1, 0, 2). count(2, 0, 1). count(3, 0, 2). count(4, 0, 0).
count(5, 1, 1). count(5, 2, 1). count(5, 3, 1). count(5, 4, 2).
count(1, 5, 1). count(2, 5, 1). count(3, 5, 2). count(4, 5, 1).

% mirror(X, Y, T) - There is mirror of type T on X, Y.

rdivyanshu

#lang rosette/safe

(output-smt "/tmp/rosette")

(define-symbolic x (bitvector 4))

(define (range x)
  (if (zero? x)
      (list)
      (append (range (sub1 x)) (list x))))

rdivyanshu

#lang racket

(require metapict)
(require metapict/pict)

(struct M-edge (turn) #:transparent)

(struct X+ M-edge () #:transparent)
(struct X- M-edge () #:transparent)
(struct A+ M-edge () #:transparent)

rdivyanshu

rdivyanshu

% square size
#const n = 5.
% number of partition
#const m = 5.
% sum of each partition
#const sm = (n * (n + 1) * (2 * n + 1)) / (6 * m).

% given(N, X, Y) - there is N at (X, Y).
given(4, 1, 2). given(3, 1, 5).
given(5, 5, 1). given(5, 5, 4).

rdivyanshu

% number of rows and columns
#const r = 7.
#const c = 10.

% numbers(X, Y, N) is a relation when there is number N
% at coordinate (X, Y)
numbers(1, 3, 2; 1, 10, 4).
numbers(2, 4, 4; 2, 6, 2; 2, 8, 3).
numbers(3, 5, 3; 3, 7, 4).
numbers(4, 9, 5).

rdivyanshu

predicate decreasing(s: seq<nat>)
{
  forall i :: 0 <= i < |s| - 1 ==> s[i] >= s[i+1]
}

predicate increasing(s: seq<nat>)
{
  forall i :: 0 <= i < |s| - 1 ==> s[i] <= s[i+1]
}

rdivyanshu

abstract module Group {
  type T(==)
  const elems : set<T>
  function identity(): (r: T)
    ensures r in elems
    ensures forall a :: a in elems ==> compose(a, r) == a && compose(r, a) == a
  function compose(a: T, b: T): (r: T)
    requires a in elems && b in elems
    ensures r in elems
  function inverse(a: T) : (r: T)