hacklex

module Sandbox


open FStar.Seq
open FStar.IntegerIntervals

let rec subseq_from_indices (#n: nat) (s: seq nat {length s == n})
                                    (h: seq (under n))
  : Tot (seq nat) (decreases length h) = 
  if length h = 0 then empty

hacklex

module FStar.Algebra.Setoid

module TC = FStar.Tactics.Typeclasses
module F = FStar.FunctionalExtensionality


open FStar.Tactics

class equivalence_relation a = {
  eq : a -> a -> bool;

hacklex

module FStar.Algebra.ProofSandbox

open FStar.Algebra.Classes.Equatable
open FStar.Algebra.Classes.Grouplikes
open FStar.Algebra.Classes.Ringlikes

module LB = FStar.List.Tot.Base
module TC = FStar.Tactics.Typeclasses

#set-options "--z3rlimit 1 --ifuel 1 --fuel 1"

hacklex

module FStar.Seq.Partitions
 
open FStar.Seq
open FStar.IntegerIntervals

(**
  This module contains theory for no-duplicates seqence partitions.
  We only work with eqtypes here.

  Here we call 

hacklex

module NodeTestSandbox

open FStar.Seq
open FStar.Seq.Base

open FStar.IntegerIntervals

type address = UInt32.t

type address_list = seq address

hacklex

module SequenceFilterProperty

open FStar.Seq 

let uint = UInt32.t

let pair = uint & uint
 
let rec snds_having_fst (i: uint) (e: seq pair)
  : Tot (seq uint)

hacklex

module Sandbox
 
#set-options "--ifuel 0 --fuel 0 --z3rlimit 1"


open FStar.Seq
open FStar.Seq.Base


//type vertex_id = UInt32.t

hacklex

module Sandbox
 
#set-options "--ifuel 0 --fuel 0 --z3rlimit 1"


open FStar.Seq
open FStar.Seq.Base
open FStar.IntegerIntervals
open FStar.UInt32
module U32 = FStar.UInt32

hacklex

module ArrayTest

open FStar.Mul 
open FStar.Bytes
open FStar.Endianness
open FStar.Seq
open FStar.IntegerIntervals

let block_size = 1024

hacklex

module MemorySandbox
open FStar.Mul 
open FStar.Bytes
open FStar.Endianness
open FStar.Seq
open FStar.IntegerIntervals


type qword = UInt64.t