gaxiiiiiiiiiiii

  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

gaxiiiiiiiiiiii

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

gaxiiiiiiiiiiii

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"

gaxiiiiiiiiiiii

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)

gaxiiiiiiiiiiii

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.

gaxiiiiiiiiiiii

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.

gaxiiiiiiiiiiii

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 ================== *)

gaxiiiiiiiiiiii

From mathcomp Require Export fintype.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module NonEmptyFintype.

  Section Def.

gaxiiiiiiiiiiii

From mathcomp Require Import ssreflect.
Require Import List Nat Ensembles Image.
Import  ListNotations.


Notation empty := (Empty_set _).
Notation single := (Singleton _).
Notation union := (Union _).

Definition bigcup {T} (X : Ensemble (Ensemble T)) : Ensemble T :=

gaxiiiiiiiiiiii

From mathcomp Require Import all_ssreflect.
Require Import Bool Nat.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Class lattice := Lattice {
  base : finType;
  meet : base -> base -> base;