LAProof.accuracy_proofs.preamble

LAProof.accuracy_proofs.real_lemmas

• • Real Arithmetic Auxiliary Lemmas

LAProof.accuracy_proofs.common

• Common Definitions and Lemmas for Floating-Point Accuracy Proofs
  • Global Definitions and Setup
  • Parameterization by Nans and type
  • Zero Predicates
    • Number of Nonzeros
  • Error Bound Constants
  • Upper bounds on default_abs and default_rel
  • Error Accumulation Factors
    • Relative Error Factor g
    • Mixed Error Factor g1
  • Floating-Point Operation Lemmas
  • Automation

LAProof.accuracy_proofs.float_acc_lems

• Floating-Point Operation Accuracy
  • Structure
  • Signed Zero Lemmas
  • Signed Zero Values
  • No-Overflow Predicates
  • Generic Rounding Error Decomposition
  • Fused Multiply-Add
  • Floating-Point Multiplication
  • Floating-Point Addition
  • Floating-Point Subtraction

LAProof.accuracy_proofs.dotprod_model

• Dot Product Definitions and Properties
  • Overview of contents
  • Generic dot product
  • Floating-point dot product
  • Floating-point dot product with FMA
  • Real-number dot product
  • Non-zero detection for dot products

LAProof.accuracy_proofs.sum_model

• Floating-Point Summation: Functional Models and Equivalences
  • General Summation Relation
  • Any-Order Floating-Point Summation
  • Equivalence Between sum_rel and sum_any
  • Bounds via Absolute Value Summation
  • Singleton Summation Lemmas
  • Permutation Invariance
  • Uniform Bound on Sum Magnitude
  • sumR: Functional Real Summation
  • Uniform Bounds on Floating-Point Sums via Real Arithmetic
  • Floating-Point Summation Instances and Properties
  • Subtraction Loop

LAProof.accuracy_proofs.sum_acc

• Floating-Point Summation Accuracy Theorems
  • Error Factors
  • Main Results
  • Dependencies
  • Backward Error: List Version
  • Backward Error: Indexed Version
  • Forward Error: List Version
  • Forward Error: Indexed Version
  • Forward Error Under Permutation

LAProof.accuracy_proofs.dot_acc_lemmas

• Forward and Mixed Error Bounds for Floating-Point Dot Products
  • Summary of Main Results
    • Forward Error Bounds
    • Sparse Forward Error Bounds
    • Mixed Error Bounds
• Section 1: Forward Error Bound — Non-FMA Dot Product
• Section 2: Forward Error Bound — FMA Dot Product
• Section 3: Mixed Error Bound — Non-FMA Dot Product
• Section 4: Mixed Error Bound — FMA Dot Product
• Section 5: Sparse Forward Error Bound — Non-FMA Dot Product
• Section 6: Sparse Forward Error Bound — FMA Dot Product

LAProof.accuracy_proofs.dot_acc

• Dot Product Accuracy Proofs (Non-FMA)
  • Error Factors
  • Main Results
  • Dependencies
  • Structure

LAProof.accuracy_proofs.vecnorm_acc

• Floating-Point Vector Norm Accuracy Bounds
  • Error Factors
  • Main Results
  • Dependencies
• Two-Norm
• One-Norm

LAProof.accuracy_proofs.fma_dot_acc

• FMA Dot Product Accuracy Theorems
  • Error Factors
  • Main Results
  • Dependencies
• Mixed Error
• Forward Error

LAProof.accuracy_proofs.sum_is_finite

• Finite Sum Boundedness
  • Overflow-free addition preserves finiteness
  • Per-element bound for finite summation
  • Monotonicity of fun_bnd
  • Main theorem: element-wise bound implies finite sum

LAProof.accuracy_proofs.fma_is_finite

• Finite Sum from Bounded Inputs
  • Key Definitions
  • Key Lemmas
  • Bound Function
  • Positivity of fun_bnd Components
  • Monotonicity of fun_bnd
  • List Splitting Lemmas
  • Main Result: Finiteness from Bounded Inputs

LAProof.accuracy_proofs.mv_mathcomp

• Matrix and Vector Operations: MathComp–List Correspondence
  • Main Results
  • Structure
  • Dependencies
  • Norm and sequence definitions
  • Tactics
    • Example uses of case_splitP
  • Enumeration and list lemmas
  • Lemmas about the maxr operator
  • Norm lemmas
  • Auxiliary definitions
  • Module F: Floating-point MathComp matrix/vector operations
  • Conversions between MathComp matrices and list-of-lists
  • List-based floating-point operations
  • Main theorem: floating-point matrix–vector multiplication

LAProof.accuracy_proofs.gemv_acc

• Matrix-Vector Multiplication Error Bounds
  • Error Factors
  • Main Results
  • Dependencies
  • Row-Vector Times Column-Vector: Mixed Error Bound
  • General Matrix-Vector Product: Mixed Error Bound
  • Matrix-Vector Product: Forward Error Bound

LAProof.accuracy_proofs.vec_op_acc

• Mixed Error Bounds for Floating-Point Matrix-Vector Operations
  • Main Results
  • Dependencies
  • Scalar-Matrix Multiplication: Mixed Error Bound
  • Entry-wise Matrix Addition: Mixed Error Bound
  • Scaled Matrix Sum: Mixed Error Bound
  • Scaled Matrix-Vector Product: Mixed Error Bound
  • General Matrix-Vector Multiply-Accumulate (GEMV): Mixed Error Bound

LAProof.accuracy_proofs.gemm_acc

• Matrix Multiplication Forward and Mixed Error Analysis
  • Error Factors
  • Error Bound Taxonomy
  • Key Results
  • Matrix Multiplication Error
  • Scalar-Matrix Multiplication Error
  • Scaled Matrix Product Error
  • Matrix Addition Error
  • Scaled Matrix Sum Error
  • General GEMM Error

LAProof.accuracy_proofs.export

LAProof.accuracy_proofs.libvalidsdp

• Importing a proof from libValidSDP into LAProof
  • Demonstrations and applications
  • Main Cholesky equivalence theorem

LAProof.accuracy_proofs.solve_model: models of Cholesky decomposition and triangular solve

• MathComp matrices over a nonring
• Functional model of Cholesky decomposition (jik algorithm)

LAProof.C.floatlib

LAProof.C.sparse_model

LAProof.C.sparse

LAProof.C.spec_sparse

LAProof.C.verif_sparse

LAProof.C.verif_sparse_byrows

LAProof.C.VSU_sparse

LAProof.C.cholesky

LAProof.C.verif_cholesky

LAProof.C.alloc

LAProof.C.spec_alloc

LAProof.C.verif_alloc

LAProof.C.densemat

LAProof.C.spec_densemat: VST specifications of functions on dense matrices.

• • Corresponds to C program densemat.h and densemat.c
  • Abstracting the floating-point precision
  • Conversions between floats, float-options, and val
  • Representation predicates for dense matrices
• Function specifications (funspecs)
• Not-yet-specified functions
• Building the "Abstract Specification Interface", the list of funspecs for this module

LAProof.C.densemat_lemmas: Supporting lemmas for VST proofs of functions on dense matrices.

• VSU definitions
• Many useful supporting lemmas about column_major, ordinal, ord_enum, etc.
• Tactics for calling matrix subscripting functions

LAProof.C.verif_densemat: VST proofs of functions on dense matrices.

• • Corresponds to C program densemat.c
• Prologue.
• densemat_malloc verification
• densemat_free verification
• Unpacking dependently typed WITH components
• densemat_clear verification
• densemat_get verification
• densemat_set verification
• densemat_addto verification
• data_norm and densemat_norm verification

LAProof.C.verif_densemat_mult: VST proofs dense matrix multiply functions

• • Corresponds to C program densemat.c
• Prologue.

LAProof.C.verif_densemat_cholesky: VST proofs of Cholesky functions on dense matrices.

• • Corresponds to C program densemat.c
• Prologue.
• densemat_cfactor verification: Cholesky factorization
• densemat_csolve verification: Cholesky solve by forward substitution and back substitution

LAProof.C.VSU_densemat: Packaging the [densematVSU], the Verified Software Unit

• • Corresponds to C program densemat.c
• Prologue.

LAProof.C.matrix_model: Functional models of matrix operations

• Prologue: typical imports for MathComp floating-point matrix functional models
• Definitions for manipulating triangular matrices

LAProof.C.bandmat

LAProof.C.build_csr

LAProof.C.verif_build_csr

LAProof.C.distinct

LAProof.C.partial_csr