Instantly share code, notes, and snippets.

# gaxiiiiiiiiiiii

Created February 9, 2024 09:43
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 From mathcomp Require Import ssreflect. Require Import Nat. Definition name := nat. Inductive proc := | Nil | Tau (P : proc) | Para (P Q : proc) | Sum (P Q : proc)
Created February 3, 2024 08:39
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 From mathcomp Require Import ssreflect. From Autosubst Require Import Autosubst. Require Import Nat. Inductive proc_ := | Var (x : var) | Nil | Para (P Q : proc_) | Repl (P : proc_) | Send (M : proc_) (N : proc_) (P : proc_)
Created January 9, 2024 13:35
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 function Pow(n:nat, k:nat) : (r:nat) ensures n > 0 ==> r > 0 { if k == 0 then 1 else if k == 1 then n else var p := k / 2; var np := Pow(n,p); if p*2 == k then np * np else
Created January 9, 2024 13:34
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 function Pow(n:nat, k:nat) : (r:nat) // Following needed for some proofs ensures n > 0 ==> r > 0 { if k == 0 then 1 else if k == 1 then n else var p := k / 2; var np := Pow(n,p); if p*2 == k then np * np
Last active January 5, 2024 11:18
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 include "evm-dafny/src/dafny/core/memory.dfy" include "evm-dafny/src/dafny/util/int.dfy" include "evm-dafny/src/dafny/util/bytes.dfy" include "evm-dafny/src/dafny/bytecode.dfy" include "evm-dafny/src/dafny/evm.dfy" // include "evm-dafny/libs/DafnyCrypto/src/dafny/util/math.dfy"
Created December 14, 2023 11:10
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 datatype Expr = | Num(nat) | Add(Expr, Expr) | Mul(Expr, Expr) function eval (e : Expr) : nat { match e case Num(n) => n case Add(e1, e2) => eval(e1) + eval(e2)
Last active November 21, 2023 12:56
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 From UniMath Require Export MoreFoundations.All. From UniMath Require Export OrderTheory.Posets. From UniMath Require Export OrderTheory.DCPOs. From DomainTheory Require Export Pataraia. From mathcomp Require Export ssreflect. Open Scope dcpo. Open Scope subtype. Open Scope logic.
Created October 29, 2023 19:38
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 Require Export UniMath.MoreFoundations.All. Require Export UniMath.Algebra.Monoids. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Examples.Products. Require Import UniMath.OrderTheory.DCPOs.Examples.SubDCPO. Require Import UniMath.OrderTheory.DCPOs.FixpointTheorems.Pataraia.
Created May 17, 2023 11:36
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 Require Import Ensembles Classical_sets. Require Import ssreflect. From mathcomp Require Import finset eqtype ssrbool seq. Require Import NonEmptyFintype. Open Scope list_scope. Unset Strict Implicit. Unset Printing Implicit Defensive. (* ================== Notation of finset ================== *)
Created April 30, 2023 12:16
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 From mathcomp Require Export fintype. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Module NonEmptyFintype. Section Def.