skaslev

open eq

inductive I (F : Type₁ → Prop) : Type₁ :=
mk : I F

axiom InjI : ∀ {x y}, I x = I y → x = y

definition P (x : Type₁) : Prop := ∃ a, I a = x ∧ (a x → false).

definition p := I P

skaslev

/**
 * Sobol Noise Generation
 *	GNU LGPL license
 *	By Dr. John Burkardt (Virginia Tech)
 * https://gist.github.com/alaingalvan/af92ddbaf3bb01f5ef29bc431bd37891
 */

//returns the position of the high 1 bit base 2 in an integer n
int getHighBit1(int n)
{

skaslev

// Ray Tracing Gems Chapter 25
// Code provided by Electronic Arts
// Colin Barré-Brisebois, Henrik Halén, Graham Wihlidal, Andrew Lauritzen,
// Jasper Bekkers, Tomasz Stachowiak, and Johan Andersson
// Errata corrected by Alain Galvan

struct HaltonState
{
    unsigned dimension;
    unsigned sequenceIndex;

skaslev

Effective Modern CMake

Getting Started

For a brief user-level introduction to CMake, watch C++ Weekly, Episode 78, Intro to CMake by Jason Turner. LLVM’s CMake Primer provides a good high-level introduction to the CMake syntax. Go read it now.

After that, watch Mathieu Ropert’s CppCon 2017 talk Using Modern CMake Patterns to Enforce a Good Modular Design (slides). It provides a thorough explanation of what modern CMake is and why it is so much better than “old school” CMake. The modular design ideas in this talk are based on the book [Large-Scale C++ Software Design](https://www.amazon.de/Large-Scale-Soft

skaslev

namespace cat
universes u v

@[class] structure category :=
  (obj : Type u)
  (hom : obj → obj → Type v)
  (cid : ∀ {x : obj}, hom x x)
  (comp : ∀ {x y z : obj}, hom y z → hom x y → hom x z)
  (assoc : ∀ {x y z w} {f : hom x y} {g : hom y z} {h : hom z w},
    comp h (comp g f) = comp (comp h g) f)

skaslev

Use cases

• Bluenoise in the game INSIDE (dithering, raymarching, reflections)
• Dithering, Ray marching, shadows etc

Textures/Matrices for direct use

• Moments In Graphics (void-and-cluster)
• 2D
• 3D and 4D
• Bart Wronski Implementation of Solid Angle
• Forced Random Dithering matrices

skaslev

universe variables u v u1 u2 v1 v2

set_option pp.universes true

open smt_tactic
meta def blast : tactic unit := using_smt $ intros >> add_lemmas_from_facts >> repeat_at_most 3 ematch
notation `♮` := by blast

structure semigroup_morphism { α β : Type u } ( s : semigroup α ) ( t: semigroup β ) :=
  (map: α → β)

skaslev

meta def blast : tactic unit := using_smt $ return ()

structure Category :=
  (Obj : Type)
  (Hom : Obj → Obj → Type)

structure Functor (C : Category) (D : Category) :=
  (onObjects   : C^.Obj → D^.Obj)
  (onMorphisms : Π { X Y : C^.Obj },
                C^.Hom X Y → D^.Hom (onObjects X) (onObjects Y))

skaslev

-- Return the maximum unsigned number of a given width.
def max_unsigned : ℕ → ℕ
| 0 := 0
| (nat.succ x) := 2 * max_unsigned x + 1

open tactic nat

/- Function for convertiong a nat into a Lean expression using nat.zero and nat.succ.
   Remark: the standard library already contains a tactic for converting nat into a binary encoding. -/
meta def nat.to_unary_expr : nat → tactic expr

skaslev

This gist shows how formal conditions of Solidity smart contracts can be automatically verified even in the presence of potential re-entrant calls from other contracts.

Solidity already supports formal verification of some contracts that do not make calls to other contracts. This of course excludes any contract that transfers Ether or tokens.

The Solidity contract below models a crude crowdfunding contract that can hold Ether and some person can withdraw Ether according to their shares. It is missing the actual access control, but the point that wants to be made