Alex Rozanov hacklex

hacklex / ShiftProperties.fst

Created September 30, 2023 09:26

Backward-forward shift is identity on applicable domain

	module ShiftProperties

	open FStar.Seq
	open FStar.Seq.Base

	open FStar.IntegerIntervals

	open FStar.Mul

	//Name Your Variables Properly!

hacklex / MemorySandbox.fst

Created July 7, 2023 17:36

Memory access helper lemmas

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


	type qword = UInt64.t

hacklex / MemorySandbox.fst

Created July 6, 2023 20:37

F* Memory read/write helpers

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


	type qword = UInt64.t

hacklex / ArrayTest.fst

Created May 18, 2023 16:29

Asserted read/write over F* sequences

	module ArrayTest

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

	let block_size = 1024

hacklex / Sandbox.fst

Last active February 13, 2023 09:19

Properties hold for inner slices if they do for outer ones

	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 / Sandbox.fst

Created February 10, 2023 17:42

seq-based set lemmas

	module Sandbox

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


	open FStar.Seq
	open FStar.Seq.Base


	//type vertex_id = UInt32.t

hacklex / SequenceFilterProperty.fst

Last active February 5, 2023 13:38

Sequence filter respects Seq.append

	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 / NodeTestSandbox.fst

Created January 29, 2023 17:03

Node reachability theory

	module NodeTestSandbox

	open FStar.Seq
	open FStar.Seq.Base

	open FStar.IntegerIntervals

	type address = UInt32.t

	type address_list = seq address

hacklex / FStar.Seq.Partitions.fst

Last active January 17, 2023 18:03

FStar Seq Partition Theory

	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 / FStar.Algebra.ProofSandbox.fst

Created January 11, 2023 20:17

Proving fold_right/fold_left equivalence for an arbitrary commutative operation

	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"