hacklex

module MinimalApplyLemmaBugReproduction

open FStar.Tactics.V2
open FStar.List
open FStar.List.Tot

noeq type setoid_monoid (a: Type) = {
  eq: a -> a -> Type;
  op: a -> a -> a;  
  id: a;   

hacklex

module SimpleAlgebraTactics

open FStar.Tactics.V2
open FStar.List
open FStar.List.Tot

noeq type setoid_monoid (a: Type) = {
  eq: a -> a -> Type; (* Equivalence relation *)
  op: a -> a -> a;  
  id: a; (* Identity element *)

hacklex

module TacSandbox

open FStar.Tactics.V2
open FStar.List
open FStar.List.Tot

noeq type setoid_monoid (a: Type) (eq: a -> a -> Type) = {
  op: a -> a -> a;
  
  (* Equivalence relation properties *)

hacklex

int size = 24;

(int aWins, int bWins, int draws, int indecisives) SequentialNonRandomTest()
{
    int topBound = 1 << size; 
    int aWins = 0;
    int bWins = 0;
    int draws = 0; 
    int indecisives = 0;
    for (int i = 0; i < topBound; i++)

hacklex

using System.Windows.Media;
using JetBrains.Annotations;

// ReSharper disable once CheckNamespace
namespace ZetaColorEditor.Colors;

[PublicAPI]
public interface IColor<out T> where T:IColor<T>
{
    /// <summary>

hacklex

Order = 1
       # 0 1  2
    hist 1 3  4
       Δ 1 1 -2
    2C₂ᵏ 2 4  2
   NoZ Δ 1 2  0
 NoZHist 1 2  2 2 1
Order = 2
       # 0 1  2  3  4
    hist 1 5 12 12  2

hacklex

Console.OutputEncoding = System.Text.Encoding.UTF8;
const int Order = 6;
int basisSize = Order * 2;

var reachabilities = GetReachabilities(Enumerable.Range(0, basisSize).Select(i => 1ul << (i)).ToArray());
Console.WriteLine("Reachabilities dump: ");
WriteArray(reachabilities);
Console.WriteLine(); 
Console.WriteLine("Histogram:"); 
PrintHistogram(reachabilities);

hacklex

Console.OutputEncoding = System.Text.Encoding.UTF8;

Console.WriteLine("Permutation: (0 1)");

Console.WriteLine("Permutation polynomial:");

Console.WriteLine(BytePolynomial.FromPermutation(new BitSwapPermutation(0, 1))); 

Console.ReadKey();

hacklex

module OpaqueExample

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

type binary_op (a:Type) = a -> a -> a
type unary_op (a:Type) = a -> a
type predicate (a:Type) = a -> bool
type binary_relation (a: Type) = a -> a -> bool
 
[@@"opaque_to_smt"]

hacklex

module Sheera

open FStar.Seq
open FStar.Seq.Base

open FStar.IntegerIntervals

open FStar.Mul

//Name Your Variables Properly!