Lvc.Infra.Option

Lvc.Infra.OptionMap

Lvc.Infra.Get

• Positional membership in a list
• Properties of get

Lvc.Infra.Position

Lvc.Infra.MoreList

• Lemmas and tactics for lists

Lvc.Infra.Terminating

Lvc.Infra.Util

• Reflecting boolean statements to Prop
• Omega Rewrite
• Misc. Tactics
  • List Length automation

Lvc.Infra.TakeSet

Lvc.Infra.AllInRel

• AllInRel: Inductive characterization of lists which are element-wise in relation

Lvc.Infra.AutoIndTac

Lvc.Infra.FiniteFixpointIteration

Lvc.Infra.ListUpdateAt

Lvc.Infra.OUnion

Lvc.Infra.Indexwise

Lvc.Infra.Lattice

Lvc.Infra.Take

Lvc.Infra.OptionR

Lvc.Infra.Computable

• Classical reasoning on decidable propositions.

Lvc.Infra.Drop

Lvc.Infra.Keep

Lvc.Infra.Sublist

Lvc.Infra.EqDec

• Wrapper for decidable equalities in coq.

Lvc.Infra.Filter

Lvc.Infra.Fresh

Lvc.Infra.Status

• Reasoning over monadic computations

Lvc.Infra.SigR

Lvc.Infra.SizeInduction

Lvc.Infra.DecSolve

Lvc.Infra.PartialOrder

Lvc.Infra.LengthEq

Lvc.DVE

• Dead Variable Elimination
  • Correctness with respect to the imperative semantics IL/I
  • Correctness with respect to the functional semantics IL
  • Reconstruction of Liveness Information after DVE
  • DVE and Unreachable Code

Lvc.IL.InRel4

Lvc.IL.Var

• Definitions related to variables
  • A class for counted types
  • Variables
  • Locations
  • Labels
    • equality of labels is decidable
    • labels are counted
  • lab

Lvc.IL.SmallStepRelations

• • plus2 - transitive closure for event-labeled relations
  • plus2 - reflexive, transitive closure for event-labeled relations

Lvc.IL.Env

• Environments for Types and Values
  • Type Environments
  • Value Environments

Lvc.IL.LabelsDefined

Lvc.IL.Patterns

Lvc.IL.Subterm

Lvc.IL.ILDB

• • • Functional Semantics

Lvc.IL.Rename

Lvc.IL.Annotation

Lvc.IL.Sawtooth

Lvc.IL.BlockType

Lvc.IL.IL

• Intermediate Language IL
  • Syntax
    • Free, Defined and Occuring Variables
  • Semantics
    • Functional Semantics
    • Imperative Semantics

Lvc.IL.Events

• • filter_tau

Lvc.IL.ILN

• • • Functional Semantics
    • Imperative Semantics

Lvc.IL.AppExpFree

Lvc.IL.ILN_IL

Lvc.IL.ILStateType

Lvc.IL.Exp

• Extended Expressions
  • Renaming
  • Liveness
  • Alpha Equivalence

Lvc.IL.StateType

Lvc.IL.InRel

Lvc.Liveness.Liveness

• Liveness
  • Inductive Definition of Liveness
  • Relation between different overapproximations
  • live_sound ensures that the annotation matches the program
  • Some monotonicity properties
  • Live variables always contain the free variables
  • Liveness is stable under renaming

Lvc.Liveness.TrueLiveness

• Specification of True Liveness
  • The inductive predicate
    • Some properties of the predicate

Lvc.Liveness.LivenessAnalysisCorrect

Lvc.Liveness.LivenessCorrect

• • For functional programs, only free variables are significant
  • Live variables contain all variables significant to an IL/I program

Lvc.Liveness.LivenessAnalysis

Lvc.Liveness.LivenessValidators

Lvc.Equiv.NonParametricBiSim

• Non-parametric Definitions of Simulation and Bisimulation
  • Bisimulation
    • Bisimulation is an reflexive and symmetric
  • Relationship of bisimulation to the parametric definition
    • Transitivity
  • Simulation
    • Simulation is an reflexive
  • Relationship of simulation to the parametric definition
    • Transitivity

Lvc.Equiv.TraceEquiv

• Divergence
  • Bisimilarity preserves silent divergence
  • Silently diverging programs are bisimlar
• Prefix Trace Equivalence (partial traces)
  • Bisimilarity is sound for prefix inclusion
  • The only prefix is empty if and only if the state diverges
  • Prefix Equivalence is sound for divergence
  • Several closedness properties
• Trace Equivalence (maximal traces)
  • Several closedness properties
  • Bisimilarity is sound for maximal traces
  • Prefix trace equivalence coincides with maximal trace equivalence.
  • Bisimilarity is complete for prefix trace equivalence.

Lvc.Equiv.SimI

• A Framework for Simulation Proofs by Induction: Imperative Version
  • Proof Relation
  • Parameter Relation and Separation
  • Application Relation
  • Label Environment Relation
  • Key Lemmata
    • Fix Compatibility
    • Extension Lemma
    • Fun Compatibility
    • Specialized Version if function bindings are not changed
    • A small study on IL fixed-points in general

Lvc.Equiv.Sim

• Parametric Definition of Simulation and Bisimulation
  • Generating Function
  • Reflexivity, Symmetry
  • Admissible Rules
  • Closedness under Expansion and Reduction
  • Transitivity

Lvc.Equiv.CtxEq

• Program Equivalence
  • Reflexivity
• Contextual Equivalence
  • Program Equivalence is contextual

Lvc.Equiv.SimF

• A Framework for Simulation Proofs by Induction: Functional Version
  • Proof Relation
  • Parameter Relation and Separation
  • Application Relation
  • Label Environment Relation
  • Key Lemmata
    • Fix Compatibility
    • Extension Lemma
    • Fun Compatibility
    • Specialized Version if function bindings are not changed
    • A small study on IL fixed-points in general

Lvc.Equiv.SimTactics

• Admissible Rules and Tactics
  • Tactics
  • Admissible Rules
    • Conditional Elimination

Lvc.Alpha.ShadowingFree

Lvc.Alpha.RenameApart

Lvc.Alpha.Alpha_RenamedApart

• Properties of Alpha Equivalence and Renamed Apart Programs
  • Given an renamedApart program, every alpha-equivalent program
  • Alpha Equivalent programs map to identical De-Bruijn terms

Lvc.Alpha.RenamedApart

• Renamed-apart (formally)
  • Morphisms
  • Relation to freeVars and occurVars
  • The two annotating sets are disjoint.

Lvc.Alpha.Alpha

• Alpha Equivalence
  • Morphisims
  • Properties
    • ϱ and ϱ' are inverses of each other on the free variables of s
    • Reflexivity
    • Symmetry
    • Transitivity
  • Soundness wrt. equivalence

Lvc.Alpha.RenamedApart_Liveness

Lvc.Constr.CSetDisjoint

Lvc.Constr.MapBasics

Lvc.Constr.MapDefined

Lvc.Constr.CSetBasic

Lvc.Constr.PairwiseDisjoint

Lvc.Constr.MapInjectivity

Lvc.Constr.CMap

Lvc.Constr.MapComposition

Lvc.Constr.MapLookupList

Lvc.Constr.CSetComputable

Lvc.Constr.CSetGet

Lvc.Constr.Map

Lvc.Constr.CSetCases

Lvc.Constr.SetOperations

Lvc.Constr.MapAgreement

Lvc.Constr.MapInverse

Lvc.Constr.MapLookup

Lvc.Constr.CSet

Lvc.Constr.MapUpdate

Lvc.Constr.CSetNotation

Lvc.Constr.MapAgreeSet

Lvc.Constr.CSetTac

Lvc.Constr.CSetPartialOrder

Lvc.Isa.Val

• More or less abstract values

Lvc.Isa.BitVector

Lvc.Isa.OrderedBitVector

Lvc.Isa.Op

• Operations

Lvc.CompCert.Integers

• Comparisons
• Parameterization by the word size, in bits.
• Representation of machine integers
• Arithmetic and logical operations over machine integers
• Properties of integers and integer arithmetic
  • Properties of modulus, max_unsigned, etc.
  • Modulo arithmetic
  • Properties of the coercions between Z and int
  • Properties of zero, one, minus one
  • Properties of equality
  • Properties of addition
  • Properties of negation
  • Properties of subtraction
  • Properties of multiplication
  • Properties of division and modulus
  • Bit-level properties
  • Properties of bit-level operations over Z
  • Bit-level reasoning over type int
  • Properties of bitwise and, or, xor
  • Properties of shifts
  • Properties of rotations
  • Properties of Z_one_bits and is_power2.
  • Relation between bitwise operations and multiplications / divisions by powers of 2
  • Properties of shrx (signed division by a power of 2)
  • Properties of integer zero extension and sign extension.
  • Properties of one_bits (decomposition in sum of powers of two)
  • Properties of comparisons
• Specialization to integers of size 8, 32, and 64 bits

Lvc.CompCert.Coqlib

• Useful tactics
• Definitions and theorems over the type positive
• Definitions and theorems over the type Z
• Definitions and theorems on the data types option, sum and list
• Definitions and theorems over boolean types
• Well-founded orderings
• Nonempty lists

Lvc.Coherence.Allocation

• Local Injectivity
  • Inductive definition of local injectivity of a renaming rho
  • Some Properties
  • Renaming with a locally injective renaming yields a coherent program
  • Theorem 6 from the paper.
  • Renaming with a locally injective renaming yields an α-equivalent program
  • Theorem 7 from the paper
  • local injectivity only looks at variables occuring in the program

Lvc.Coherence.Restrict

Lvc.Coherence.Invariance

• • Definition of invariance
  • Agreement Invariant
  • Context coherence for IL/F contexts: approxF
  • Main Theorem about Coherence
  • Coherence implies invariance

Lvc.Coherence.AllocationAlgoBound

• • Bound on the number of registers used
  • Theorem 8 from the paper.

Lvc.Coherence.DelocationAlgo

Lvc.Coherence.AllocationAlgoCorrect

• • the algorithm produces a locally injective renaming
  • Theorem 8 from the paper.

Lvc.Coherence.Coherence

• Definition of Coherence: srd
  • Some monotonicity properties
    • Every renamed apart program is coherent

Lvc.Coherence.AllocationValidator

• • Coherence is decidable
  • local injectivity is decidable

Lvc.Coherence.AllocationAlgo

• SSA-based register assignment formulated for IL

Lvc.Coherence.Delocation

Lvc.Coherence.DelocationCorrect

Lvc.Coherence.DelocationValidator

Lvc.Reachability.ReachabilityAnalysisCorrect

Lvc.Reachability.Reachability

• Rechability Specification
  • The inductive predicate
  • Some Properties of the Predicate

Lvc.Reachability.ReachabilityAnalysis

Lvc.UCE

• Unreachable Code Elimination
  • The transformer
    • Properties of the transformer
  • Correctness with respect to the imperative semantics IL/I
  • Correctness with respect to the functional semantics IL
  • UCE respects parameter/argument matching
  • Reconstruction of Liveness Information after UCE
  • Completeness of Reachability

Lvc.Analysis.AnalysisForward

Lvc.Analysis.Analysis

Lvc.Analysis.AnalysisBackward

Lvc.Lowering.ParallelMove

• Parallel Moves

Lvc.Lowering.EAE

Lvc.Lowering.Renest

Lvc.Compiler