rdivyanshu

;; Challenge: find all the bugs in this small functional compiler
#lang racket

(provide (all-defined-out))

(define verbose-mode (make-parameter #t))
(define i-am-a-mac (make-parameter #f))

;; 
;; Our compiler will have several layers

rdivyanshu

function power(x: int, y: int) : int
    requires y >= 0
    decreases y
{
    if y == 0 then 1
    else if y % 2 == 0 then power(x * x, y / 2)
    else x * power(x * x, (y - 1) / 2)
}

lemma PowerOddLemma(x: int, y: int)

rdivyanshu

codatatype Stream = Cons(head: nat, tail: Stream)

function Upwards(n: nat): Stream {
   Cons(n, Upwards (n + 1))
}

function Nats() : Stream {
    Upwards(0)
}

rdivyanshu

import Mathlib.Algebra.Ring.Defs
import Mathlib.Data.Finite.Defs
import Mathlib.Data.Set.Finite
import Mathlib.Data.Nat.Lattice
import Mathlib.Tactic

theorem crux_oc588 {R: Type*} [Ring R] [Finite R]
    (a b : R) (h : (a * b - 1) * b = 0) : b * (a * b - 1) = 0 := by

  let s := { b ^ k | k : ℕ }

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