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) |
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_) |
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 |
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 |
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" | |
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) |
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. |
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. |
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 ================== *) |
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. |
NewerOlder