clutch.clutch

clutch.approxis.adequacy

clutch.approxis.adequacy_rel

clutch.approxis.app_rel_rules

• Primitive rules
  • Forward reductions on the LHS
  • Forward reductions on the RHS
• Some derived (symbolic execution) rules
  • Stateful reductions on the LHS

clutch.approxis.app_weakestpre

• Coupling modalities
  • spec_coupl
• prog_coupl
• The weakest precondition
• Derived rules
• Proofmode class instances

clutch.approxis.approxis

clutch.approxis.compatibility

clutch.approxis.coupling_rules

• Coupling rules
• rand(N) ~ rand(N) coupling
• fragmented state rand N ~ state rand M, M>=N, under injective function from N to M
• Exact couplings
• rand(unit, N) ~ state_step(α', N) coupling
• rand(α, N) ~ rand(α, N) wrong bound coupling

clutch.approxis.derived_laws

• Rules for allocation
• Rules for accessing array elements

clutch.approxis.ectx_lifting

clutch.approxis.fundamental

clutch.approxis.interp

• Interpretation of types
  • Properties of the type inrpretation w.r.t. the substitutions
• Interpretation of the environments
• The semantic typing judgement

clutch.approxis.lifting

clutch.approxis.model

clutch.approxis.primitive_laws

clutch.approxis.proofmode

clutch.approxis.rel_tactics

• General-purpose tactics
• Symbolic execution

clutch.approxis.reltac2

clutch.approxis.soundness

clutch.approxis.examples.ElGamal_closed_ctx

clutch.approxis.examples.ElGamal_defs

clutch.approxis.examples.ElGamal_semantic

clutch.approxis.examples.ElGamal_syntactic

clutch.approxis.examples.KEM

clutch.approxis.examples.KEMDEM

clutch.approxis.examples.LR_tac

clutch.approxis.examples.advantage_laws

clutch.approxis.examples.avoid_collision_rel

clutch.approxis.examples.b_tree

clutch.approxis.examples.b_tree_adt

clutch.approxis.examples.bounded_oracle

clutch.approxis.examples.diffie_hellman

clutch.approxis.examples.intctxt_ideal_dec

clutch.approxis.examples.intptxt_ideal_dec

clutch.approxis.examples.iterable_expression

clutch.approxis.examples.kem_elgamal

clutch.approxis.examples.kemdem_hybrid_cpa_generic

clutch.approxis.examples.kemdem_hybrid_cpa_instance_otp

clutch.approxis.examples.kemdem_hybrid_cpa_instance_rf

clutch.approxis.examples.linked_list

clutch.approxis.examples.list

clutch.approxis.examples.map

clutch.approxis.examples.one_time_pad

clutch.approxis.examples.option

clutch.approxis.examples.prf

clutch.approxis.examples.prf_cpa

clutch.approxis.examples.prf_cpa_combined

clutch.approxis.examples.prf_cpa_combined_sem_typ

clutch.approxis.examples.prf_cpa_with_dec

clutch.approxis.examples.prf_local_state

clutch.approxis.examples.prg

clutch.approxis.examples.prg_extension

clutch.approxis.examples.prg_prf

clutch.approxis.examples.prp

clutch.approxis.examples.prp_prf_adaptive

clutch.approxis.examples.prp_prf_test

clutch.approxis.examples.prp_prf_weak

clutch.approxis.examples.pubkey

clutch.approxis.examples.pubkey_class

clutch.approxis.examples.rejection_samplers

clutch.approxis.examples.sampling_without_replacement

clutch.approxis.examples.security_aux

clutch.approxis.examples.sum_seq

clutch.approxis.examples.symmetric

clutch.approxis.examples.symmetric_init

clutch.approxis.examples.valgroup

clutch.approxis.examples.valgroup_Zp

clutch.approxis.examples.valgroup_Zpx

clutch.approxis.examples.von_neumann_coin

clutch.approxis.examples.wmf_attack

clutch.approxis.examples.wmf_eav_security

clutch.approxis.examples.wmf_protocol

clutch.approxis.examples.xor

clutch.base_logic.error_credits

• • RA for the reals in the interval 0, 1) with addition as the operation.

clutch.base_logic.error_credits_mult

• • RA for the nonnegative reals with addition as the operation.

clutch.base_logic.spec_auth_markov

clutch.base_logic.spec_update

clutch.bi.weakestpre

clutch.caliper.adequacy

• A step-indexed left-partial coupling
• Soundness

clutch.caliper.derived_laws

• Rules for allocation
• Rules for accessing array elements
• Rules for allocation
• Rules for accessing array elements

clutch.caliper.ectx_lifting

• RSWP

clutch.caliper.lifting

• RWP
• RSWP

clutch.caliper.primitive_laws

• RSWP
• RWP

clutch.caliper.proofmode

clutch.caliper.seq_weakestpre

clutch.caliper.weakestpre

• A coupling fixpoint for rwp
• The refinement weakest preconditions
• RWP
• RSWP
• Derived rules
• Derived rules

clutch.caliper.examples.bounded_random_walk

clutch.caliper.examples.coin_random_walk

clutch.caliper.examples.determinize

• Higher-order spec w/model construction
• Higher-order spec w/o model construction

clutch.caliper.examples.flip

clutch.caliper.examples.galton_watson_tree

• Task loop
• Galton-Watson tree

clutch.caliper.examples.lazy_real

clutch.caliper.examples.listgen

clutch.caliper.examples.nat_random_walk

clutch.caliper.examples.treap

clutch.caliper.examples.lib.list

• Linked list
• Queue implemented using a linked list

clutch.clutch.adequacy

clutch.clutch.adequacy_rel

clutch.clutch.compatibility

clutch.clutch.coupling_rules

• Coupling rules
• state_step(α, N) ~ state_step(α', N) coupling
• state_step(α, N) ~ rand(N) coupling
• rand(N) ~ state_step(α', N) coupling
• rand(α, N) ~ rand(N) coupling
• rand(N) ~ rand(α, N) coupling
• rand(N) ~ rand(N) coupling
• rand(α, N) ~ rand(α, N) coupling
• rand(α, N) ~ rand(α, N) wrong bound coupling
• rand(α, N) ~ rand(N) wrong bound coupling
• rand(N) ~ rand(α, N) wrong bound coupling

clutch.clutch.derived_laws

• Rules for allocation
• Rules for accessing array elements

clutch.clutch.ectx_lifting

clutch.clutch.fundamental

clutch.clutch.interp

• Interpretation of types
  • Properties of the type interpretation w.r.t. the substitutions
• Interpretation of the environments
• The semantic typing judgement

clutch.clutch.lifting

clutch.clutch.model

clutch.clutch.primitive_laws

clutch.clutch.proofmode

clutch.clutch.rel_rules

• Primitive rules
  • Forward reductions on the LHS
  • Forward reductions on the RHS
• Some derived (symbolic execution) rules
  • Stateful reductions on the LHS

clutch.clutch.rel_tactics

• General-purpose tactics
• Symbolic execution

clutch.clutch.reltac2

clutch.clutch.soundness

clutch.clutch.weakestpre

• Coupling modalities
• spec_coupl
• prog_coupl
• The weakest precondition
• Derived rules

clutch.clutch.examples.DH_assumptions

clutch.clutch.examples.awkward_deterministic

clutch.clutch.examples.awkward_lazy_eager_coin

clutch.clutch.examples.awkward_probabilistic

clutch.clutch.examples.counterexample

clutch.clutch.examples.coupon

• implementation refines spec

clutch.clutch.examples.env_bisim

clutch.clutch.examples.erasure

clutch.clutch.examples.flip_once_many_synchronised_coin

clutch.clutch.examples.geometric

clutch.clutch.examples.hash

clutch.clutch.examples.id_rec

clutch.clutch.examples.in_place_quicksort

clutch.clutch.examples.keyed_hash

clutch.clutch.examples.lazy_eager_coin

clutch.clutch.examples.lazy_eager_nat

clutch.clutch.examples.lazy_int

clutch.clutch.examples.one_time_pad

clutch.clutch.examples.rng

clutch.clutch.examples.sample_int

clutch.clutch.examples.split_rng

clutch.clutch.examples.stream

clutch.clutch.examples.von_neumann_coin

clutch.clutch.examples.crypto.ElGamal

clutch.clutch.examples.crypto.ElGamal_bijection

clutch.clutch.examples.crypto.ElGamal_closed_ctx

clutch.clutch.examples.crypto.advantage_laws

clutch.clutch.examples.crypto.valgroup

clutch.clutch.examples.crypto.valgroup_Zp

clutch.clutch.examples.crypto.valgroup_Zpx

clutch.clutch.lib.array

• array_free, to deallocate an entire array in one go.
• array_copy_to, a function which copies to an array in-place.
• Using array_copy_to we also implement array_clone, which allocates a fresh
• array_init, to create and initialize an array with a given

clutch.clutch.lib.conversion

clutch.clutch.lib.flip

• Derived laws for a fair coin flip
• Tape allocation
• Unlabelled flip
• Labelled flip
• Coupling rules

clutch.clutch.lib.list

clutch.clutch.lib.map

clutch.common.con_ectx_language

• Some lemmas about this language

clutch.common.con_ectxi_language

clutch.common.con_inject

clutch.common.con_language

clutch.common.ectx_language

• Some lemmas about this language

clutch.common.ectxi_language

clutch.common.erasable

clutch.common.exec

• strengthen this lemma?
• strengthen this lemma?
• strengthen lemma?

clutch.common.inject

clutch.common.language

clutch.common.locations

clutch.common.sch_erasable

clutch.con_prob_lang.class_instances

• Instances of the Atomic class
• Instances of the PureExec class

clutch.con_prob_lang.ctx_subst

clutch.con_prob_lang.erasure

clutch.con_prob_lang.lang

clutch.con_prob_lang.lub_termination

clutch.con_prob_lang.metatheory

• commenting out couplings atm

clutch.con_prob_lang.notation

clutch.con_prob_lang.tactics

clutch.con_prob_lang.wp_tactics

clutch.con_prob_lang.spec.spec_ra

clutch.con_prob_lang.spec.spec_tactics

• • bind

clutch.con_prob_lang.typing.contextual_refinement

clutch.con_prob_lang.typing.tychk

clutch.con_prob_lang.typing.types

• Types
• Typing judgements

clutch.coneris.adequacy

clutch.coneris.atomic

clutch.coneris.coneris

clutch.coneris.derived_laws

• Rules for allocation
• Rules for accessing array elements

clutch.coneris.ectx_lifting

clutch.coneris.error_rules

• Coneris error bound rules rules
• rand(N) no error
• rand(N) error

clutch.coneris.lifting

clutch.coneris.primitive_laws

clutch.coneris.proofmode

clutch.coneris.weakestpre

• One step prog coupl
• The weakest precondition
• Derived rules

clutch.coneris.wp_update

clutch.coneris.examples.con_two_add

• This is the con_two_add example in the paper of Coneris
• This is the proof sketched for the example con_two_add in the paper of Coneris.

clutch.coneris.examples.concurrent_hash

clutch.coneris.examples.coneris_examples

clutch.coneris.examples.hash

clutch.coneris.examples.message_pass

clutch.coneris.examples.parallel_add

clutch.coneris.examples.race

clutch.coneris.examples.two_die

• This is the con_prog example in the paper of Coneris
• This is the proof presented for the example con_prog in the paper of Coneris

clutch.coneris.examples.bloom_filter.bloom_filter

clutch.coneris.examples.bloom_filter.concurrent_bloom_filter

clutch.coneris.examples.bloom_filter.concurrent_bloom_filter_alt

clutch.coneris.examples.hash.coll_free_hash_view_impl

clutch.coneris.examples.hash.coll_free_hash_view_interface

clutch.coneris.examples.hash.con_hash_impl0

clutch.coneris.examples.hash.con_hash_impl1

• Code

clutch.coneris.examples.hash.con_hash_impl2

• Code

clutch.coneris.examples.hash.con_hash_impl3

• Code

clutch.coneris.examples.hash.con_hash_impl4

• Sequential hash function with per key presampling tapes

clutch.coneris.examples.hash.con_hash_interface0

• Operations
• Ghost state
• Predicates
• General properties of the predicates

clutch.coneris.examples.hash.con_hash_interface1

• Operations
• Ghost state
• Predicates
• General properties of the predicates

clutch.coneris.examples.hash.con_hash_interface2

• Operations
• Ghost state
• Predicates
• General properties of the predicates

clutch.coneris.examples.hash.con_hash_interface3

• Operations
• Ghost state
• Predicates
• General properties of the predicates

clutch.coneris.examples.hash.con_hash_interface4

• Operations
• Predicates
• General properties of the predicates

clutch.coneris.examples.hash.hash_race

clutch.coneris.examples.hash.hash_view_impl

clutch.coneris.examples.hash.hash_view_interface

clutch.coneris.examples.hash.seq_hash_impl

clutch.coneris.examples.hash.seq_hash_interface

• seq hash interface. Not completed. To be deleted
• Operations
• Ghost state
• Predicates
• General properties of the predicates

clutch.coneris.examples.lazy_rand.lazy_rand_impl

clutch.coneris.examples.lazy_rand.lazy_rand_interface

• Operations
• Ghost state
• Predicates
• General properties of the predicates

clutch.coneris.examples.lazy_rand.lazy_rand_race

clutch.coneris.examples.random_counter.client

clutch.coneris.examples.random_counter.client2

clutch.coneris.examples.random_counter.impl1

clutch.coneris.examples.random_counter.impl2

clutch.coneris.examples.random_counter.impl3

clutch.coneris.examples.random_counter.random_counter

• Operations
• Ghost state
• Predicates
• General properties of the predicates
• Program specs

clutch.coneris.examples.random_counter2.client

clutch.coneris.examples.random_counter2.impl1

clutch.coneris.examples.random_counter2.impl2

clutch.coneris.examples.random_counter2.impl3

clutch.coneris.examples.random_counter2.random_counter

• Operations
• Ghost state
• Predicates
• General properties of the predicates
• Program specs

clutch.coneris.examples.random_counter3.client

clutch.coneris.examples.random_counter3.impl1

clutch.coneris.examples.random_counter3.impl2

clutch.coneris.examples.random_counter3.impl3

clutch.coneris.examples.random_counter3.random_counter

• Operations
• Ghost state
• Predicates
• General properties of the predicates
• Program specs

clutch.coneris.lib.abstract_tape

• Abstract tapes
• TODO add

clutch.coneris.lib.array

• array_free, to deallocate an entire array in one go.
• array_copy_to, a function which copies to an array in-place.
• Using array_copy_to we also implement array_clone, which allocates a fresh
• array_init, to create and initialize an array with a given

clutch.coneris.lib.conversion

clutch.coneris.lib.flip

• Derived laws for a fair coin flip

clutch.coneris.lib.hocap_flip

• Operations
• Ghost state
• Predicates
• General properties of the predicates
• Program specs

clutch.coneris.lib.hocap_rand

• Hocap rand specs
• Operations
• Ghost state
• Predicates
• General properties of the predicates
• Program specs

clutch.coneris.lib.hocap_rand_alt

• This file is an experimental attempt in deriving a different spec for the abstract rand module
• Operations
• Ghost state
• Predicates
• General properties of the predicates
• Program specs

clutch.coneris.lib.hocap_rand_atomic

• Hocap atomic rand specs
• Operations
• Ghost state
• Predicates
• General properties of the predicates
• Program specs

clutch.coneris.lib.lazy

• Library for lazy sampling

clutch.coneris.lib.list

clutch.coneris.lib.lock

• Operations
• Ghost state
• Predicates
• General properties of the predicates
• Program specs

clutch.coneris.lib.map

clutch.coneris.lib.par

clutch.coneris.lib.spawn

clutch.coneris.lib.spin_lock

clutch.delay_prob_lang.class_instances

• Instances of the Atomic class
• Instances of the PureExec class

clutch.delay_prob_lang.commute

clutch.delay_prob_lang.lang

• Syntax
• typing for well formness
• semantics

clutch.delay_prob_lang.metatheory

• Lemmas about updating urns
• remove drand
  • * Note that this function also checks whether everything is simple

clutch.delay_prob_lang.notation

clutch.delay_prob_lang.preserve_atomicity

clutch.delay_prob_lang.tactics

clutch.delay_prob_lang.urn_erasable

clutch.delay_prob_lang.urn_subst

• Well constructed expressions and values

clutch.delay_prob_lang.wp_tactics

clutch.delay_prob_lang.typing.types

• Types
• Typing judgements

clutch.diffpriv.adequacy

clutch.diffpriv.adequacy_rel

clutch.diffpriv.app_rel_rules

• Primitive rules
  • Forward reductions on the LHS
  • Forward reductions on the RHS
• Some derived (symbolic execution) rules
  • Stateful reductions on the LHS

clutch.diffpriv.compatibility

clutch.diffpriv.coupling_rules

• Coupling rules
• rand(N) ~ rand(N) coupling
• fragmented state rand N ~ state rand M, M>=N, under injective function from N to M
• Exact couplings
• rand(unit, N) ~ state_step(α', N) coupling
• rand(α, N) ~ rand(α, N) wrong bound coupling

clutch.diffpriv.derived_laws

• Rules for allocation
• Rules for accessing array elements

clutch.diffpriv.diffpriv

clutch.diffpriv.diffpriv_rules

clutch.diffpriv.distance

clutch.diffpriv.ectx_lifting

clutch.diffpriv.fundamental

clutch.diffpriv.interp

• Interpretation of types
  • Properties of the type inrpretation w.r.t. the substitutions
• Interpretation of the environments
• The semantic typing judgement

clutch.diffpriv.lifting

clutch.diffpriv.model

clutch.diffpriv.primitive_laws

clutch.diffpriv.proofmode

clutch.diffpriv.rel_tactics

• General-purpose tactics
• Symbolic execution

clutch.diffpriv.soundness

clutch.diffpriv.weakestpre

• Coupling modalities
  • spec_coupl
• prog_coupl
• The weakest precondition
• Derived rules
• Proofmode class instances

clutch.diffpriv.examples.SVT_experiments

clutch.diffpriv.examples.adaptive_count

clutch.diffpriv.examples.diffpriv_basic_examples

clutch.diffpriv.examples.exact_cache

clutch.diffpriv.examples.laplace_tapes

clutch.diffpriv.examples.list

clutch.diffpriv.examples.map

clutch.diffpriv.examples.pointwise_eq_exact_cache

clutch.diffpriv.examples.pointwise_eq_list

clutch.diffpriv.examples.pointwise_eq_sparse_vector_technique

clutch.diffpriv.examples.privacy_filter

clutch.diffpriv.examples.report_noisy_max

clutch.diffpriv.examples.report_noisy_max_lemmas

clutch.diffpriv.examples.report_noisy_max_pointwise

clutch.diffpriv.examples.rnm_inspired_problems

clutch.diffpriv.examples.sparse_vector_technique

clutch.diffpriv.examples.sum_queries

clutch.diffpriv.examples.from_approxis.LR_tac

clutch.diffpriv.examples.from_approxis.avoid_collision_rel

clutch.diffpriv.examples.from_approxis.b_tree

clutch.diffpriv.examples.from_approxis.b_tree_adt

clutch.diffpriv.examples.from_approxis.bounded_oracle

clutch.diffpriv.examples.from_approxis.option

clutch.diffpriv.examples.from_approxis.prf

clutch.diffpriv.examples.from_approxis.prf_cpa

clutch.diffpriv.examples.from_approxis.prp

clutch.diffpriv.examples.from_approxis.prp_prf_adaptive

clutch.diffpriv.examples.from_approxis.prp_prf_test

clutch.diffpriv.examples.from_approxis.prp_prf_weak

clutch.diffpriv.examples.from_approxis.rejection_samplers

clutch.diffpriv.examples.from_approxis.security_aux

clutch.diffpriv.examples.from_approxis.sum_seq

clutch.diffpriv.examples.from_approxis.symmetric

clutch.diffpriv.examples.from_approxis.von_neumann_coin

clutch.diffpriv.examples.from_approxis.xor

clutch.elton.adequacy

clutch.elton.derived_laws

• Rules for allocation
• Rules for accessing array elements

clutch.elton.ectx_lifting

clutch.elton.elton

clutch.elton.error_rules

• Elton error bound rules rules
• rand(N) no error

clutch.elton.lifting

clutch.elton.primitive_laws

clutch.elton.proofmode

clutch.elton.pupd

clutch.elton.rupd

clutch.elton.weakestpre

• One step prog coupl
• The weakest precondition
• Value promotion makes this rule hard to prove
• Derived rules

clutch.elton.examples.basic_hash

• Start of first case of disjunction
• End of first case of disjunction
• Start of second case of disjunction
• End of second case of disjunction

clutch.elton.examples.generic_group

clutch.elton.examples.guess

clutch.elton.examples.hash

• This specification of the hash is modified to support delayed values as dom

clutch.elton.examples.hash_guess

• Final bit

clutch.elton.examples.multiple_guess

clutch.elton.examples.prophecy

• Counter example of prophecy variables

clutch.elton.examples.repeat_flip

clutch.elton.examples.repeat_flip_neg

clutch.elton.examples.repeat_neg

clutch.elton.lib.flip

clutch.elton.lib.map

• Map that supports delayed values

clutch.elton.unary_rel.unary_app_rel_rules

• Primitive rules
  • Forward reductions on the LHS

clutch.elton.unary_rel.unary_compatibility

clutch.elton.unary_rel.unary_fundamental

clutch.elton.unary_rel.unary_interp

• Interpretation of types
  • Properties of the type inrpretation w.r.t. the substitutions
• Interpretation of the environments
• The semantic typing judgement

clutch.elton.unary_rel.unary_model

clutch.elton.unary_rel.unary_rel_tactics

• General-purpose tactics
• Symbolic execution

clutch.eris.adequacy

clutch.eris.array_laws

• Rules for allocation

clutch.eris.derived_laws

• Rules for accessing array elements

clutch.eris.ectx_lifting

clutch.eris.eris

clutch.eris.error_rules

• Union bound rules
• rand(N) no error
• rand(N) error

clutch.eris.lifting

clutch.eris.presample_rules

• Rules for presampling to tapes
• Approximate Lifting

clutch.eris.primitive_laws

clutch.eris.proofmode

clutch.eris.seq_amplification

• Calculation for the Sequential Amplification Rile

clutch.eris.total_adequacy

clutch.eris.total_derived_laws

• Rules for accessing array elements

clutch.eris.total_ectx_lifting

clutch.eris.total_lifting

clutch.eris.total_primitive_laws

clutch.eris.total_weakestpre

• The total weakest precondition
• Derived rules

clutch.eris.weakestpre

• The graded lifting modality glm
• The weakest precondition
• Derived rules

clutch.eris.examples.cf_hash

clutch.eris.examples.cf_hashmap

clutch.eris.examples.dynamic_vec

clutch.eris.examples.eris_examples

clutch.eris.examples.fisher_yates

clutch.eris.examples.golden_toss

clutch.eris.examples.hash

clutch.eris.examples.miller_rabin

clutch.eris.examples.noproph

clutch.eris.examples.random_walk

• 1D Random walk with equal probability of stepping left or right

clutch.eris.examples.rec_toss

clutch.eris.examples.spline

• Examples related to rejection samplers with a bounded number of attempts
• Example 5.4 from "A New Proof Rule for Almost-Sure Termination" by McIver et al.

clutch.eris.examples.approximate_samplers.approx_higherorder_incremental

• Higher order specification for incremental sampling algorithms

clutch.eris.examples.approximate_samplers.approx_higherorder_rejection_sampler

• Examples related to rejection samplers with a bounded number of attempts

clutch.eris.examples.approximate_samplers.approx_rejection_sampler

• Examples related to rejection samplers with a bounded number of attempts
• Correctness of bounded and unbounded rejection samplers using error credits instead of Löb induction

clutch.eris.examples.approximate_samplers.approx_rejection_sampler_presampled

• Examples related to rejection samplers with a bounded number of attempts

clutch.eris.examples.approximate_samplers.approx_sampler_lib

• Higher order specification for incremental sampling algorithms

clutch.eris.examples.approximate_samplers.approx_walkSAT

• Termination with probability 1 of the WalkSAT algorithm

clutch.eris.examples.merkle.merkle_tree

clutch.eris.examples.merkle.unreliable

clutch.eris.lib.array

• array_free, to deallocate an entire array in one go.
• array_copy_to, a function which copies to an array in-place.
• Using array_copy_to we also implement array_clone, which allocates a fresh
• array_init, to create and initialize an array with a given

clutch.eris.lib.list

clutch.eris.lib.map

clutch.eris.tutorial.basic

• Separation logic in Rocq
  • Separation Logic Connectives

clutch.eris.tutorial.basic_eris

• Eris

clutch.eris.tutorial.bloom_filter_multi

• Bloom filter with multiple hash functions

clutch.eris.tutorial.bloom_filter_single

• Bloom filters
  • Representation predicate for Bloom filters
  • Proving the specifications for the Bloom filter
  • A client of the Bloom filter

clutch.eris.tutorial.eris_rules

clutch.eris.tutorial.eris_tutorial

clutch.eris.tutorial.geometric

• Geometric distribution

clutch.eris.tutorial.geometric_total

• Geometric distribution
  • Correctness of the geometric sampler

clutch.eris.tutorial.hash_interface

• Hash Functions
  • Hash interface
  • Derived lemmas about hash functions
  • An example program

clutch.eris.tutorial.quicksort

clutch.eris.tutorial.tutorial

clutch.foxtrot.adequacy

clutch.foxtrot.coneris_relate

clutch.foxtrot.coupling_rules

• Coupling rules
• rand(N) ~ rand(N) coupling
• Coupling a rand on LHS with two rands on the RHS
• Lemmas for von neumann coin example
• Lemmas for associativity of probabilitic choice
• Exact couplings
• rand(α, N) ~ rand(α, N) wrong bound coupling

clutch.foxtrot.derived_laws

• Rules for allocation
• Rules for accessing array elements

clutch.foxtrot.ectx_lifting

clutch.foxtrot.error_rules

• Coupling rules

clutch.foxtrot.foxtrot

clutch.foxtrot.full_info

clutch.foxtrot.lifting

clutch.foxtrot.oscheduler

• Full evaluation (limit of stratification)
• Full evaluation (limit of stratification)

clutch.foxtrot.primitive_laws

clutch.foxtrot.proofmode

clutch.foxtrot.pupd

clutch.foxtrot.weakestpre

• One step prog coupl
• The weakest precondition
• Derived rules
• Proofmode class instances

clutch.foxtrot.binary_rel.binary_adequacy_rel

clutch.foxtrot.binary_rel.binary_app_rel_rules

• Primitive rules
  • Forward reductions on the LHS

clutch.foxtrot.binary_rel.binary_compatibility

clutch.foxtrot.binary_rel.binary_fundamental

clutch.foxtrot.binary_rel.binary_interp

• Interpretation of types
  • Properties of the type inrpretation w.r.t. the substitutions
• Interpretation of the environments
• The semantic typing judgement

clutch.foxtrot.binary_rel.binary_model

clutch.foxtrot.binary_rel.binary_rel_tactics

• General-purpose tactics
• Symbolic execution

clutch.foxtrot.binary_rel.binary_soundness

clutch.foxtrot.examples.algebraic

• Algebraic theory

clutch.foxtrot.examples.batch_sampling

clutch.foxtrot.examples.batch_sampling_seq

• Sequential version of the batch sampler

clutch.foxtrot.examples.encryption

clutch.foxtrot.examples.encryption_unknown

clutch.foxtrot.examples.entropy_mixer

clutch.foxtrot.examples.libsodium

clutch.foxtrot.examples.nodet_example

clutch.foxtrot.examples.presample_rhs

• Counter example of presampling on the RHS

clutch.foxtrot.examples.rejection_samplers

clutch.foxtrot.examples.von_neumann

clutch.foxtrot.lib.conversion

clutch.foxtrot.lib.diverge

clutch.foxtrot.lib.min

clutch.foxtrot.lib.nodet

clutch.foxtrot.lib.or

clutch.foxtrot.lib.par

clutch.foxtrot.lib.sampler

• Operations
• Predicates
• General properties of the predicates
• Program specs

clutch.foxtrot.lib.spawn

clutch.foxtrot.lib.toss

clutch.foxtrot.unary_rel.unary_app_rel_rules

• Primitive rules
  • Forward reductions on the LHS

clutch.foxtrot.unary_rel.unary_compatibility

clutch.foxtrot.unary_rel.unary_fundamental

clutch.foxtrot.unary_rel.unary_interp

• Interpretation of types
  • Properties of the type inrpretation w.r.t. the substitutions
• Interpretation of the environments
• The semantic typing judgement

clutch.foxtrot.unary_rel.unary_model

clutch.foxtrot.unary_rel.unary_rel_tactics

• General-purpose tactics
• Symbolic execution

clutch.meas_lang.class_instances

clutch.meas_lang.ctx_subst

clutch.meas_lang.ectx_language

clutch.meas_lang.ectxi_language

clutch.meas_lang.erasable

clutch.meas_lang.erasure

clutch.meas_lang.exec

• strengthen this lemma?
• strengthen this lemma?
• strengthen lemma?

clutch.meas_lang.exec_lang

clutch.meas_lang.lang

clutch.meas_lang.language

clutch.meas_lang.metatheory

• state_step(α, N) ~ state_step(α', N) coupling
• Generalized state_step(α) ~ state_step(α') coupling
• rand(unit, N) ~ state_step(α', N) coupling
• state_step(α, N) ~ rand(unit, N) coupling
• e1 ~ rand(α', N) coupling for α' ↪ₛ (N, ☐)
• Approximate rand(N) ~ rand(M) coupling, N <= M
• Approximate rand(N) ~ rand(M) coupling, N <= M, along an injection
• Approximate rand(N) ~ rand(M) coupling, M <= N
• Approximate rand(N) ~ rand(M) coupling, M <= N, along an injection
• Approximate state_step(α, N) ~ state_step(α', N) coupling
• a coupling between rand n and rand n avoiding results from a list
• state_step ~ fair_coin
• state_step ≫= state_step ~ dprod fair_coin fair_coin

clutch.meas_lang.notation

clutch.meas_lang.tactics

clutch.meas_lang.wp_tactics

clutch.prelude.Coquelicot_ext

clutch.prelude.NNRbar

• Definitions
  • Order
  • Operations
• Compatibility with real numbers
• Properties of order
  • Relations between inequalities
  • Decidability
  • Transitivity
• Properties of operations
  • Additive operators
  • Multiplicative
• NNRbar_min

clutch.prelude.Reals_ext

clutch.prelude.Series_ext

clutch.prelude.asubst

clutch.prelude.base

clutch.prelude.classical

clutch.prelude.fiber_bounds

clutch.prelude.fin

clutch.prelude.iris_ext

clutch.prelude.mc_stdlib

clutch.prelude.properness

clutch.prelude.stdpp_ext

• • nat_to_bool
  • Z_to_bool
• list
  • Properties of the filter function that need permutation
• sum_list

clutch.prelude.tactics

• Tactics from Dimsum
  • iDestruct!
  • iSplit!

clutch.prelude.uniform_list

clutch.prelude.zmodp_fin

clutch.prob.countable_sum

clutch.prob.couplings

clutch.prob.couplings_app

clutch.prob.couplings_dp

clutch.prob.couplings_dp_complete

• Completeness of DP couplings
  • Indicator series monotonicity
  • Staircase approximation
  • Threshold counting and its closed form
  • Bounds on the staircase approximation
  • Main staircase bound for the relational case
  • Upper and lower bounds for the SeriesC of staircase approximations
  • Completeness theorems

clutch.prob.couplings_exp

clutch.prob.couplings_kanto

clutch.prob.differential_privacy

clutch.prob.diffpriv_facts

clutch.prob.distribution

• Sum-swapping equalities for distributions
• Monadic return
• Monadic bind
• Lemmas about the interplay of monadic bind and return
• Monadic map
• Monadic strength
• Monadic fold left
• Monadic itereration
• Coins
• The zero distribution
• Diagonal
• Products
• swap
• Marginals
• Pointwise order
• Scaled distribution
• Limit distribution
• Uniform sampling

clutch.prob.generic_lifting

clutch.prob.graded_predicate_lifting

clutch.prob.markov

• Markov Chains
• Strict partial evaluation
• Non-strict partial evaluation
• Stratified evaluation to a final state
• Full evaluation (limit of stratification)
• Iterated Markov chain
• Ranking Supermartingales

clutch.prob.mdp

• Markov decision process
• Full evaluation (limit of stratification)

clutch.prob.monad.bind

clutch.prob.monad.compose

clutch.prob.monad.const

clutch.prob.monad.discrete_mapout

clutch.prob.monad.eval

clutch.prob.monad.examples

clutch.prob.monad.extras

clutch.prob.monad.identity

clutch.prob.monad.integrate

clutch.prob.monad.join

clutch.prob.monad.laws

clutch.prob.monad.map

clutch.prob.monad.ret

clutch.prob.monad.types

clutch.prob.monad.uniform

clutch.prob.monad.zero

clutch.prob_lang.advantage

clutch.prob_lang.class_instances

• Instances of the Atomic class
• Instances of the PureExec class

clutch.prob_lang.ctx_subst

clutch.prob_lang.erasure

clutch.prob_lang.exec_lang

clutch.prob_lang.lang

clutch.prob_lang.metatheory

• rand(N) ~ rand(N) coupling
• rand(N, α1) ~ rand(N, α2) coupling, "wrong" N
• rand(N,α) ~ rand(N) coupling, "wrong" N
• rand(N) ~ rand(N, α) coupling, "wrong" N
• state_step(α, N) ~ state_step(α', N) coupling
• Generalized state_step(α) ~ state_step(α') coupling
• rand(unit, N) ~ state_step(α', N) coupling
• state_step(α, N) ~ rand(unit, N) coupling
• e1 ~ rand(α', N) coupling for α' ↪ₛ (N, ☐)
• Approximate rand(N) ~ rand(M) coupling, N <= M
• Approximate rand(N) ~ rand(M) coupling, N <= M, along an injection
• Approximate rand(N) ~ rand(M) coupling, M <= N
• Approximate rand(N) ~ rand(M) coupling, M <= N, along an injection
• Approximate state_step(α, N) ~ state_step(α', N) coupling
• a coupling between rand n and rand n avoiding results from a list
• state_step ~ fair_coin
• state_step ≫= state_step ~ dprod fair_coin fair_coin

clutch.prob_lang.notation

clutch.prob_lang.tactics

clutch.prob_lang.wp_tactics

clutch.prob_lang.gwp.arith

clutch.prob_lang.gwp.gen_weakestpre

clutch.prob_lang.gwp.linked_list

clutch.prob_lang.gwp.list

clutch.prob_lang.gwp.map

clutch.prob_lang.gwp.set

clutch.prob_lang.gwp.table

clutch.prob_lang.spec.spec_ra

clutch.prob_lang.spec.spec_rules

clutch.prob_lang.spec.spec_tactics

• • bind

clutch.prob_lang.typing.contextual_refinement

clutch.prob_lang.typing.contextual_refinement_alt

clutch.prob_lang.typing.tychk

clutch.prob_lang.typing.types

• Types
• Typing judgements

clutch.pure_complete.coupl

clutch.pure_complete.eris_ast

clutch.pure_complete.prob_additional

clutch.pure_complete.pure

clutch.pure_complete.samples_one

clutch.pure_complete.tachis_ert

clutch.pure_complete.term

clutch.tachis.adequacy

clutch.tachis.cost_models

• Cost models
  • Cost 1 for all steps
  • Cost 1 model for rand
  • Entropy cost model for rand
  • Cost n for tick n

clutch.tachis.derived_laws

• Rules for allocation
• Rules for accessing array elements

clutch.tachis.ectx_lifting

clutch.tachis.ert_rules

• ERT rules

clutch.tachis.ert_weakestpre

• The expected runtime modality ERM
• The weakest precondition
• Derived rules

clutch.tachis.expected_time_credits

• • Non-negative real numbers with addition as the operation.

clutch.tachis.lifting

clutch.tachis.primitive_laws

clutch.tachis.problang_wp

clutch.tachis.proofmode

clutch.tachis.examples.amortized_op

• Batz. et al 2023 (POPL 2023), Example 5.7

clutch.tachis.examples.batchsampling

• Batch Sampling

clutch.tachis.examples.couponcollector

• Exact time credit accounting for Coupon collecting

clutch.tachis.examples.expected_val_reference

• Lohse & Garg 2024, Section 7

clutch.tachis.examples.fisher_yates

clutch.tachis.examples.geometric

• Simple Geometric Example

clutch.tachis.examples.kway_merge

• A ≤ head comparator for lists of intergers

clutch.tachis.examples.meldable_heap

• Meldable Heaps

clutch.tachis.examples.min_heap_spec

clutch.tachis.examples.quicksort

• Exact time credit accounting for Quicksort

clutch.tachis.examples.race

clutch.tachis.examples.simple_loops

clutch.tachis.examples.hashmap.hash

• Hash

clutch.tachis.examples.hashmap.hashmap

• Hashmap

clutch.tachis.examples.hashmap.linkedlist

• library for linkedlist specific for hashmap

clutch.tachis.examples.hashmap.map

clutch.tachis.examples.hashmap.rabinkarp

• Rabin Karp string detection

clutch.tachis.examples.lib.list

• Functional list in the CostTick cost model