diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,797 +1,798 @@ ABY3_Protocols ADS_Functor AI_Planning_Languages_Semantics AODV AOT AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Balog_Szemeredi_Gowers Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binary_Code_Imprimitive Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Birkhoff_Finite_Distributive_Lattices Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Boolos_Curious_Inference_Automated Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CHERI-C_Memory_Model CISC-Kernel Concentration_Inequalities CRDT CRYSTALS-Kyber CRYSTALS-Kyber_Security CSP_RefTK CVP_Hardness CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cardinality_Continuum Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Catoids Cauchy Cayley_Hamilton Certification_Monads Ceva Chandy_Lamport Chebyshev_Polynomials Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorial_Enumeration_Algorithms Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon CommCSL Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers Cook_Levin CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots Coupledsim_Contrasim CryptHOL CryptoBasedCompositionalProperties Crypto_Standards Cubic_Quartic_Equations DCR-ExecutionEquivalence DFS_Framework DOM_Components DPRM_Theorem DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic DigitsInBase Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Directed_Sets Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation Disintegration DiskPaxos Distributed_Distinct_Elements Dominance_CHK DynamicArchitectures Dynamic_Tables E_Transcendental Earley_Parser Echelon_Form EdmondsKarp_Maxflow Edwards_Elliptic_Curves_Group Efficient-Mergesort Efficient_Weighted_Path_Order Elimination_Of_Repeated_Factors Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Euler_Polyhedron_Formula Eudoxus_Reals Eval_FO Example-Submission Executable_Randomized_Algorithms Expander_Graphs Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FO_Theory_Rewriting FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Fixed_Length_Vector Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic Given_Clause_Loops GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Gray_Codes Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOL-CSPM HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms HoareForDivergence Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL HyperHoareLogic Hyperdual Hypergraph_Basics Hypergraph_Colourings IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse Interval_Analysis IO_Language_Conformance IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq IsaNet Isabelle_C Isabelle_hoops Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Kneser_Cauchy_Davenport Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt KnuthMorrisPratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LP_Duality LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_Series Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lovasz_Local Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Martingales Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Maximum_Segment_Sum Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MHComputation MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines MLSS_Decision_Proc ML_Unification Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Multirelations_Heterogeneous Multiset_Ordering_NPC Multitape_To_Singletape_TM Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers No_FTL_observers_Gen_Rel Nominal2 Nominal_Myhill_Nerode Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OmegaCatoidsQuantales OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PAL PAPP_Impossibility PCF PLM POPLmark-deBruijn PSemigroupsConvolution Package_logic Padic_Field Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect_Fields Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polygonal_Number_Theorem Polylog Polynomial_Crit_Geometry Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Probability_Inequality_Completeness Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Logic_Class Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic Q0_Metatheory Q0_Soundness QHLProver QR_Decomposition Quantales Quantales_Converse Quantifier_Elimination_Hybrid Quasi_Borel_Spaces Quaternions Query_Optimization Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Region_Quadtrees Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Cardinality Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rensets Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SCC_Bloemen_Sequential SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 S_Finite_Measure_Monad Safe_Distance Safe_OCL Safe_Range_RC Saturation_Framework Saturation_Framework_Extensions Sauer_Shelah_Lemma Schutz_Spacetime Schwartz_Zippel Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Clause_Learning Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Solidity Sophomores_Dream Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Stalnaker_Logic Standard_Borel_Spaces Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code StrictOmegaCategories Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras +Sumcheck_Protocol SumSquares Sunflowers SuperCalc Suppes_Theorem Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Synthetic_Completeness Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Three_Squares Timed_Automata Topological_Semantics Topology TortoiseHare TsirelsonBound Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Transport Treaps Tree-Automata Tree_Decomposition Tree_Enumeration Triangle Trie Turans_Graph_Theorem Twelvefold_Way Two_Generated_Word_Monoids_Intersection Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Undirected_Graph_Theory Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme VYDRA_MDL Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeckendorf Zeta_3_Irrational Zeta_Function pGCL Labeled_Transition_Systems Pushdown_Systems diff --git a/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Abstract_Multivariate_Polynomials.thy b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Abstract_Multivariate_Polynomials.thy new file mode 100644 --- /dev/null +++ b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Abstract_Multivariate_Polynomials.thy @@ -0,0 +1,189 @@ +(******************************************************************************* + + Project: Sumcheck Protocol + + Authors: Azucena Garvia Bosshard + Christoph Sprenger, ETH Zurich + Jonathan Bootle, IBM Research Europe + +*******************************************************************************) + +section \Abstract Multivariate Polynomials\ + +theory Abstract_Multivariate_Polynomials + imports + Substitutions + "HOL-Analysis.Finite_Cartesian_Product" +begin + +text \Multivariate polynomials, abstractly\ + +locale multi_variate_polynomial = + fixes vars :: \'p :: comm_monoid_add \ 'v set\ + and deg :: \'p \ nat\ + and eval :: \'p \ ('v, 'a::finite) subst \ 'b :: comm_monoid_add\ + and inst :: \'p \ ('v, 'a) subst \ 'p\ +assumes + \ \vars\ + vars_finite: \finite (vars p)\ and + vars_zero: \vars 0 = {}\ and + vars_add: \vars (p + q) \ vars p \ vars q\ and + vars_inst: \vars (inst p \) \ vars p - dom \\ and + + \ \degree\ + deg_zero: \deg 0 = 0\ and + deg_add: \deg (p + q) \ max (deg p) (deg q)\ and + deg_inst: \deg (inst p \) \ deg p\ and + + \ \eval\ + eval_zero: \eval 0 \ = 0\ and + eval_add: \vars p \ vars q \ dom \ \ eval (p + q) \ = eval p \ + eval q \\ and + eval_inst: \vars p \ dom \ \ dom \ \ eval (inst p \) \ = eval p (\ ++ \)\ and + + \ \small number of roots (variant for two polynomials)\ + roots: \card {r. deg p \ d \ vars p \ {x} \ deg q \ d \ vars q \ {x} \ + p \ q \ eval p [x \ r] = eval q [x \ r]} \ d\ +begin + +lemmas vars_addD = vars_add[THEN subsetD] + + +subsection \Arity: definition and some lemmas\ + +definition arity :: \'p \ nat\ where + \arity p = card (vars p)\ + +lemma arity_zero: \arity 0 = 0\ + by (simp add: arity_def vars_zero) + +lemma arity_add: \arity (p + q) \ arity p + arity q\ +proof - + have \card (vars (p + q)) \ card (vars p \ vars q)\ + by (intro card_mono) (auto simp add: vars_add vars_finite) + also have \... \ card (vars p) + card (vars q)\ by (simp add: card_Un_le) + finally show ?thesis by (simp add: arity_def) +qed + +lemma arity_inst: + assumes \dom \ \ vars p\ + shows \arity (inst p \) \ arity p - card (dom \)\ +proof - + have \card (vars (inst p \)) \ card (vars p - dom \)\ + by (auto simp add: vars_finite vars_inst card_mono) + also have \\ = card (vars p) - card (dom \)\ using assms + by (simp add: card_Diff_subset finite_subset vars_finite) + finally show ?thesis by (simp add: arity_def) +qed + +subsection \Lemmas about evaluation, degree, and variables of finite sums\ + +lemma eval_sum: + assumes \finite I\ \\i. i \ I \ vars (pp i) \ dom \\ + shows \eval (\i\I. pp i) \ = (\i\I. eval (pp i) \)\ +proof - + have \eval (\i\I. pp i) \ = (\i\I. eval (pp i) \) \ vars (\i\I. pp i) \ dom \\ using assms + proof (induction rule: finite.induct) + case emptyI + then show ?case by (simp add: eval_zero vars_zero) + next + case (insertI A a) + then show ?case + by (auto simp add: eval_add vars_add sum.insert_if dest!: vars_addD) + qed + then show ?thesis .. +qed + +lemma vars_sum: + assumes \finite I\ + shows \vars (\i\I. pp i) \ (\i\I. vars (pp i))\ + using assms +proof (induction rule: finite.induct) + case emptyI + then show ?case by(auto simp add: vars_zero) +next + case (insertI A a) + then show ?case using insertI by(auto simp add: sum.insert_if dest: vars_addD) +qed + +lemma deg_sum: + assumes \finite I\ and "I \ {}" + shows \deg (\i\I. pp i) \ Max {deg (pp i) | i. i \ I}\ + using assms +proof (induction rule: finite.induct) + case emptyI + then show ?case by(auto simp add: deg_zero) +next + case (insertI A a) + show ?case + proof(cases "A = {}") + assume \A = {}\ + then show ?thesis by(simp) + next + assume \A \ {}\ + then have *: \Max {deg (pp i) |i. i \ A} \ Max {deg (pp i) |i. i = a \ i \ A}\ using \finite A\ + by (intro Max_mono) auto + show ?thesis using insertI \A \ {}\ + by (auto 4 4 simp add: sum.insert_if intro: Max_ge *[THEN [2] le_trans] deg_add[THEN le_trans]) + qed +qed + +subsection \Lemmas combining eval, sum, and inst\ + +lemma eval_sum_inst: + assumes \vars p \ V \ dom \\ \finite V\ + shows \eval (\\ \ substs V H. inst p \) \ = (\\ \ substs V H. eval p (\ ++ \))\ +proof - + have A1: \\\. \ \ substs V H \ vars (inst p \) \ dom \\ using assms(1) vars_inst by blast + have A2: \\\. \ \ substs V H \ vars p \ dom \ \ dom \\ using assms(1) by (auto) + + have \eval (\\ \ substs V H. inst p \) \ = (\\\substs V H. eval (inst p \) \)\ using A1 assms(2) + by (simp add: eval_sum substs_finite) \ \requires @{term "finite H"}\ + also have \... = (\\ \ substs V H. eval p (\ ++ \))\ using A2 + by (simp add: eval_inst) + finally show ?thesis . +qed + +lemma eval_sum_inst_commute: + assumes \vars p \ insert x V\ \x \ V\ \finite V\ + shows \eval (\\\substs V H. inst p \) [x \ r] + = (\\\substs V H. eval (inst p [x \ r]) \)\ +proof - + have \eval (sum (inst p) (substs V H)) [x \ r] = + (\\\substs V H. eval p ([x \ r] ++ \))\ using \vars p \ insert x V\ \finite V\ + by (simp add: eval_sum_inst) + also have \... = (\\\substs V H. eval p (\(x \ r)))\ using \x \ V\ + by (intro Finite_Cartesian_Product.sum_cong_aux) + (auto simp add: map_add_comm subst_dom) + also have \... = (\\\substs V H. eval (inst p [x \ r]) \)\ using \vars p \ insert x V\ + by (intro Finite_Cartesian_Product.sum_cong_aux) + (auto simp add: eval_inst) + finally show ?thesis . +qed + +subsection \Merging sums over substitutions\ + +lemma sum_merge: + assumes \x \ V\ + shows "(\h\H. (\\ \ substs V H. eval p ([x \ h] ++ \))) + = (\\\substs (insert x V) H. eval p \)" +proof - + have "\h \. (h,\) \ H \ substs V H \ dom [x \ h] \ dom \ = {}" using \x \ V\ + by(auto simp add: substs_def) + then have *: "\h \. (h,\) \ H \ substs V H \ [x \ h] ++ \ = \(x \ h)" + by(auto simp add: map_add_comm) + + have "(\h\H. (\\ \ substs V H. eval p ([x \ h] ++ \))) = + (\(h,\) \ H \ substs V H. eval p ([x \ h] ++ \))" + by(auto simp add: sum.cartesian_product) + also have "\ = (\(h,\) \ H \ substs V H. eval p (\(x \ h)))" using * + by (intro Finite_Cartesian_Product.sum_cong_aux) (auto) + also have "\ = (\\\substs (insert x V) H. eval p \)" using \x \ V\ + by(auto simp add: sum.reindex_bij_betw[OF bij_betw_set_substs, + where V1 = "insert x V" and x1 = "x" and H1 = "H" and g = "\\. eval p \", symmetric] + intro: Finite_Cartesian_Product.sum_cong_aux) + finally show ?thesis . +qed + +end + +end diff --git a/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Completeness_Proof.thy b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Completeness_Proof.thy new file mode 100644 --- /dev/null +++ b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Completeness_Proof.thy @@ -0,0 +1,89 @@ +(******************************************************************************* + + Project: Sumcheck Protocol + + Authors: Azucena Garvia Bosshard + Christoph Sprenger, ETH Zurich + Jonathan Bootle, IBM Research Europe + +*******************************************************************************) + +section \Completeness Proof for the Sumcheck Protocol\ + +theory Completeness_Proof + imports + Sumcheck_Protocol +begin + +context multi_variate_polynomial begin + +text \Completeness proof\ + +theorem completeness_inductive: + assumes + \v = (\\ \ substs (set (map fst rm)) H. eval p \)\ + \vars p \ set (map fst rm)\ + \distinct (map fst rm)\ + \H \ {}\ + shows + "sumcheck honest_prover u (H, p, v) r_prev rm" + using assms +proof(induction honest_prover u "(H, p, v)" r_prev rm arbitrary: H p v rule: sumcheck.induct) + case (1 s H p v r_prev) + then show ?case by(simp) +next + case (2 s H p v r_prev x r rm) + + note IH = 2(1) \ \induction hypothesis\ + + let ?V = "set (map fst rm)" + let ?q = "(\\ \ substs ?V H. inst p \)" + + have \vars p \ insert x ?V\ \x \ ?V\ \distinct (map fst rm)\ + using 2(3-4) by(auto) + + \ \evaluation check\ + have \(\\ \ substs (insert x ?V) H. eval p \) = (\h\H. eval ?q [x \ h])\ + proof - + have "(\\\substs (insert x ?V) H. eval p \) = + (\h\H. (\\ \ substs ?V H. eval p ([x \ h] ++ \)))" + using \x \ ?V\ + by(auto simp add: sum_merge) + also have "\ = (\h\H. eval ?q [x \ h])" + using \vars p \ insert x ?V\ + by(auto simp add: eval_sum_inst) + finally show ?thesis . + qed + moreover + \ \recursive check\ + have \sumcheck honest_prover () (H, inst p [x \ r], eval ?q [x \ r]) r rm\ + proof - + have \vars (inst p [x \ r]) \ ?V\ + using \vars p \ insert x ?V\ vars_inst by fastforce + moreover + have "eval ?q [x \ r] = (\\ \ substs ?V H. eval (inst p [x \ r]) \)" + using \vars p \ insert x ?V\ \x \ set (map fst rm)\ + by (auto simp add: eval_sum_inst_commute) + ultimately + show ?thesis using IH \distinct (map fst rm)\ \H \ {}\ + by (simp add: honest_prover_def) + qed + ultimately show ?case using 2(2-3,5) + by (simp add: honest_prover_def honest_prover_vars honest_prover_deg) +qed + + +corollary completeness: + assumes + \(H, p, v) \ Sumcheck\ + \vars p = set (map fst rm)\ + \distinct (map fst rm)\ + \H \ {}\ + shows + "sumcheck honest_prover u (H, p, v) r rm" + using assms + by (auto simp add: Sumcheck_def intro: completeness_inductive) + +end + +end \ No newline at end of file diff --git a/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Probability_Tools.thy b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Probability_Tools.thy new file mode 100644 --- /dev/null +++ b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Probability_Tools.thy @@ -0,0 +1,183 @@ +(******************************************************************************* + + Project: Sumcheck Protocol + + Authors: Azucena Garvia Bosshard + Christoph Sprenger, ETH Zurich + Jonathan Bootle, IBM Research Europe + +*******************************************************************************) + +section \Auxiliary Lemmas Related to Probability Theory\ + +theory Probability_Tools + imports "HOL-Probability.Probability" +begin + +subsection \Tuples\ + +definition tuples :: \'a set \ nat \ 'a list set\ where + \tuples S n = {xs. set xs \ S \ length xs = n}\ + +lemma tuplesI: \\ set xs \ S; length xs = n \ \ xs \ tuples S n\ + by (simp add: tuples_def) + +lemma tuplesE [elim]: \\ xs \ tuples S n; \ set xs \ S; length xs = n \ \ P \ \ P\ + by (simp add: tuples_def) + +lemma tuples_Zero: \tuples S 0 = {[]}\ + by (auto simp add: tuples_def) + +lemma tuples_Suc: \tuples S (Suc n) = (\(x, xs). x # xs) ` (S \ tuples S n)\ + by (fastforce simp add: tuples_def image_def Suc_length_conv dest: sym) + +lemma tuples_non_empty [simp]: \S \ {} \ tuples S n \ {}\ + by (induction n) (auto simp add: tuples_Zero tuples_Suc) + +lemma tuples_finite [simp]: \\ finite (S::'a set); S \ {} \ \ finite (tuples S n :: 'a list set)\ + by (auto simp add: tuples_def dest: finite_lists_length_eq) + + +subsection \Congruence and monotonicity\ + +lemma prob_cong: \ \adapted from Joshua\ + assumes \\x. x \ set_pmf M \ x \ A \ x \ B\ + shows \measure_pmf.prob M A = measure_pmf.prob M B\ + using assms + by (simp add: measure_pmf.finite_measure_eq_AE AE_measure_pmf_iff) + +lemma prob_mono: + assumes \\x. x \ set_pmf M \ x \ A \ x \ B\ + shows \measure_pmf.prob M A \ measure_pmf.prob M B\ + using assms + by (simp add: measure_pmf.finite_measure_mono_AE AE_measure_pmf_iff) + + +subsection \Some simple derived lemmas\ + +lemma prob_empty: + assumes \A = {}\ + shows \measure_pmf.prob M A = 0\ + using assms + by (simp) \ \uses @{thm [source] "measure_empty"}: @{thm "measure_empty"}\ + +lemma prob_pmf_of_set_geq_1: + assumes "finite S" and "S \ {}" + shows "measure_pmf.prob (pmf_of_set S) A \ 1 \ S \ A" using assms + by (auto simp add: measure_pmf.measure_ge_1_iff measure_pmf.prob_eq_1 AE_measure_pmf_iff) + + +subsection \Intersection and union lemmas\ + +lemma prob_disjoint_union: + assumes \A \ B = {}\ + shows \measure_pmf.prob M (A \ B) = measure_pmf.prob M A + measure_pmf.prob M B\ + using assms + by (fact measure_pmf.finite_measure_Union[simplified]) + +lemma prob_finite_Union: + assumes \disjoint_family_on A I\ \finite I\ + shows \measure_pmf.prob M (\i\I. A i) = (\i\I. measure_pmf.prob M (A i))\ + using assms + by (intro measure_pmf.finite_measure_finite_Union) (simp_all) + +lemma prob_disjoint_cases: + assumes \B \ C = A\ \B \ C = {}\ + shows \measure_pmf.prob M A = measure_pmf.prob M B + measure_pmf.prob M C\ +proof - + have \measure_pmf.prob M A = measure_pmf.prob M (B \ C)\ using \B \ C = A\ + by (auto intro: prob_cong) + also have \... = measure_pmf.prob M B + measure_pmf.prob M C\ using \B \ C = {}\ + by (simp add: prob_disjoint_union) + finally show ?thesis . +qed + +lemma prob_finite_disjoint_cases: + assumes \(\i\I. B i) = A\ \disjoint_family_on B I\ \finite I\ + shows \measure_pmf.prob M A = (\i\I. measure_pmf.prob M (B i))\ +proof - + have \measure_pmf.prob M A = measure_pmf.prob M (\i\I. B i)\ using assms(1) + by (auto intro: prob_cong) + also have \... = (\i\I. measure_pmf.prob M (B i))\ using assms(2,3) + by (intro prob_finite_Union) + finally show ?thesis . +qed + + +subsection \Independent probabilities for head and tail of a tuple\ + +lemma pmf_of_set_Times: \ \by Andreas Lochbihler\ + "pmf_of_set (A \ B) = pair_pmf (pmf_of_set A) (pmf_of_set B)" + if "finite A" "finite B" "A \ {}" "B \ {}" + by(rule pmf_eqI)(auto simp add: that pmf_pair indicator_def) + + +lemma prob_tuples_hd_tl_indep: + assumes \S \ {}\ + shows + \measure_pmf.prob (pmf_of_set (tuples S (Suc n))) {(r::'a::finite) # rs | r rs. P r \ Q rs} + = measure_pmf.prob (pmf_of_set (S::'a set)) {r. P r} * + measure_pmf.prob (pmf_of_set (tuples S n)) {rs. Q rs}\ + (is "?lhs = ?rhs") +proof - \ \mostly by Andreas Lochbihler\ + text \ + Step 1: Split the random variable @{term "pmf_of_set (tuples S (Suc n))"} into + two independent (@{term "pair_pmf"}) random variables, one producing the head and one + producing the tail of the list, and then @{term Cons} the two random variables using + @{term "map_pmf"}. + \ + have *: "pmf_of_set (tuples S (Suc n)) + = map_pmf (\(x :: 'a, xs). x # xs) (pair_pmf (pmf_of_set S) (pmf_of_set (tuples S n)))" + unfolding tuples_Suc using \S \ {}\ + by (auto simp add: map_pmf_of_set_inj[symmetric] inj_on_def pmf_of_set_Times) + text \ + Step 2: Transform the event by move the @{term Cons} from the random variable into the event. + This corresponds to using @{term distr} on measures. + \ + have "?lhs = measure_pmf.prob (pair_pmf (pmf_of_set S) (pmf_of_set (tuples S n))) + ((\(x :: 'a, xs). x # xs) -` {r # rs | r rs. P r \ Q rs})" + unfolding * measure_map_pmf by (rule refl) + + text \ + Step 3: Rewrite the event as a pair of events. Then we apply independence of the head + from the tail. + \ + also have "((\(x, xs). x # xs) -` {r # rs | r rs. P r \ Q rs}) = {r. P r} \ {rs. Q rs}" by auto + also have "measure_pmf.prob (pair_pmf (pmf_of_set S) (pmf_of_set (tuples S n))) \ = + measure_pmf.prob (pmf_of_set S) {r. P r} + * measure_pmf.prob (pmf_of_set (tuples S n)) {rs. Q rs}" + by(rule measure_pmf_prob_product) simp_all + + finally show ?thesis . +qed + +lemma prob_tuples_fixed_hd: + \measure_pmf.prob (pmf_of_set (tuples UNIV (Suc n))) {rs::'a list. P rs} + = (\a \ UNIV. measure_pmf.prob (pmf_of_set (tuples UNIV n)) {rs. P (a # rs)}) / real(CARD('a::finite))\ + (is "?lhs = ?rhs") +proof - + { + fix a + have \measure_pmf.prob (pmf_of_set (tuples UNIV (Suc n))) ({rs. P rs} \ {rs. hd rs = a}) + = measure_pmf.prob (pmf_of_set (tuples UNIV (Suc n))) ({r#rs | r rs. r = a \ P (a#rs)})\ + by (intro prob_cong) (auto simp add: tuples_Suc) + also have \... = measure_pmf.prob (pmf_of_set (UNIV::'a set)) {r. r = a} * + measure_pmf.prob (pmf_of_set (tuples UNIV n)) {rs. P (a#rs)}\ + by (intro prob_tuples_hd_tl_indep) simp + also have \... = measure_pmf.prob (pmf_of_set (tuples UNIV n)) {rs. P (a#rs)} / real (CARD ('a))\ + by (simp add: measure_pmf_single) + finally + have \measure_pmf.prob (pmf_of_set (tuples UNIV (Suc n))) ({rs. P rs} \ {rs. hd rs = a}) + = measure_pmf.prob (pmf_of_set (tuples UNIV n)) {rs. P (a#rs)} / real (CARD ('a))\ . + } + note A1 = this + + have \?lhs = (\a \ UNIV. measure_pmf.prob (pmf_of_set (tuples UNIV (Suc n))) ({rs. P rs} \ {rs. hd rs = a}))\ + by (intro prob_finite_disjoint_cases) (auto simp add: disjoint_family_on_def) + also have \... = ?rhs\ using A1 + by (simp add: sum_divide_distrib) + finally show ?thesis . +qed + + +end diff --git a/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Public_Coin_Proofs.thy b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Public_Coin_Proofs.thy new file mode 100644 --- /dev/null +++ b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Public_Coin_Proofs.thy @@ -0,0 +1,107 @@ +(******************************************************************************* + + Project: Sumcheck Protocol + + Authors: Azucena Garvia Bosshard + Christoph Sprenger, ETH Zurich + Jonathan Bootle, IBM Research Europe + +*******************************************************************************) + +section \Generic Public-coin Interactive Proofs\ + +theory Public_Coin_Proofs + imports Probability_Tools +begin + +subsection \Generic definition\ + +type_synonym ('i, 'r, 'a, 'resp, 'ps) prv = "'i \ 'a \ 'a list \ 'r \ 'ps \ 'resp \ 'ps" + +locale public_coin_proof = + fixes ver0 :: "'i \ 'vs \ bool" + and ver1 :: "'i \ 'resp \ 'r \ 'a \ 'a list \ 'vs \ bool \ 'i \ 'vs" +begin + +fun prove :: "'vs \ ('i, 'r, 'a, 'resp, 'ps) prv \ 'ps \ 'i \ 'r \ ('a \ 'r) list \ bool" where + "prove vs prv ps I r [] \ ver0 I vs" | + "prove vs prv ps I r ((x, r')#rm) \ + (let (resp, ps') = prv I x (map fst rm) r ps in + let (ok, I', vs') = ver1 I resp r' x (map fst rm) vs in + ok \ prove vs' prv ps' I' r' rm)" + +text \ +The parameters are +\begin{itemize} +\item @{term "(ver0, ver1)"} and @{term "vs"} are the verifier and its current state, +\item @{term "prv"} and @{term "ps"} are the prover and its current state, +\item @{term "I \ S"} is the problem instance, +\item @{term "r"} is the verifier's randomness for the current round. +\item @{term "rs"} is the (list of) randomness for the remaining rounds, and +\item @{term "xs"} is a list of public per-round information/ +\end{itemize} +We assume that @{term "rs"} and @{term "xs"} have the same length. +\ + +end + + +subsection \Generic soundness and completeness\ + +locale public_coin_proof_security = + public_coin_proof ver0 ver1 + for ver0 :: "'i \ 'vs \ bool" + and ver1 :: "'i \ 'resp \ 'r \ 'a \ 'a list \ 'vs \ bool \ 'i \ 'vs" + + fixes S :: "'i set" \ \problem specification\ + and honest_pr :: "('i, 'r, 'a, 'resp, 'ps) prv" + and compl_err :: "'i \ real" + and sound_err :: "'i \ real" + and compl_assm :: "'vs \ 'ps \ 'i \ 'a list \ bool" + and sound_assm :: "'vs \ 'ps \ 'i \ 'a list \ bool" + assumes + completeness: + "\ I \ S; compl_assm vs ps I xs \ \ + measure_pmf.prob + (pmf_of_set (tuples UNIV (length xs))) + {rs. prove vs honest_pr ps I r (zip xs rs)} \ 1 - compl_err I" and + + soundness: + "\ I \ S; sound_assm vs ps I xs \ \ + measure_pmf.prob + (pmf_of_set (tuples UNIV (length xs))) + {rs. prove vs pr ps I r (zip xs rs)} \ sound_err I" + + +locale public_coin_proof_strong_props = + public_coin_proof ver0 ver1 + for ver0 :: "'i \ 'vs \ bool" + and ver1 :: "'i \ 'resp \ 'r::finite \ 'a \ 'a list \ 'vs \ bool \ 'i \ 'vs" + + fixes S :: "'i set" \ \problem specification\ + and honest_pr :: "('i, 'r, 'a, 'resp, 'ps) prv" + and sound_err :: "'i \ real" + and compl_assm :: "'vs \ 'ps \ 'i \ 'a list \ bool" + and sound_assm :: "'vs \ 'ps \ 'i \ 'a list \ bool" + assumes + completeness: + "\ I \ S; compl_assm vs ps I (map fst rm) \ \ prove vs honest_pr ps I r rm" and + + soundness: + "\ I \ S; sound_assm vs ps I xs \ \ + measure_pmf.prob + (pmf_of_set (tuples UNIV (length xs))) + {rs. prove vs pr ps I r (zip xs rs)} \ sound_err I" +begin + + +text \Show that this locale satisfies the weaker assumptions of @{locale public_coin_proof_security}.\ + +sublocale pc_props: + public_coin_proof_security ver0 ver1 S honest_pr "\_. 0" sound_err compl_assm sound_assm + by (unfold_locales) + (fastforce simp add: prob_pmf_of_set_geq_1 tuples_Suc completeness, + clarsimp simp add: soundness) + +end + + +end \ No newline at end of file diff --git a/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Soundness_Proof.thy b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Soundness_Proof.thy new file mode 100644 --- /dev/null +++ b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Soundness_Proof.thy @@ -0,0 +1,290 @@ +(******************************************************************************* + + Project: Sumcheck Protocol + + Authors: Azucena Garvia Bosshard + Christoph Sprenger, ETH Zurich + Jonathan Bootle, IBM Research Europe + +*******************************************************************************) + +section \Soundness Proof for the Sumcheck Protocol\ + +theory Soundness_Proof + imports + Probability_Tools + Sumcheck_Protocol +begin + +context multi_variate_polynomial begin + +\ \Helper lemma: + Proves that the probability of two different polynomials evaluating to the same value is small.\ +lemma prob_roots: + assumes "deg q2 \ deg p" and "vars q2 \ {x}" + shows "measure_pmf.prob (pmf_of_set UNIV) + {r. deg q1 \ deg p \ vars q1 \ {x} \ q1 \ q2 \ eval q1 [x \ r] = eval q2 [x \ r]} + \ real (deg p) / real CARD('a)" +proof - + have "card {r. deg q1 \ deg p \ vars q1 \ {x} \ + q1 \ q2 \ eval q1 [x \ r] = eval q2 [x \ r]} = + card {r. deg q1 \ deg p \ vars q1 \ {x} \ + deg q2 \ deg p \ vars q2 \ {x} \ + q1 \ q2 \ eval q1 [x \ r] = eval q2 [x \ r]}" using assms by(auto) + also have "\ \ deg p" by(auto simp add: roots) + finally show ?thesis by(auto simp add: measure_pmf_of_set divide_right_mono) +qed + + +text \Soundness proof\ + +theorem soundness_inductive: + assumes + "vars p \ set vs" and + "deg p \ d" and + "distinct vs" and + "H \ {}" + shows + "measure_pmf.prob + (pmf_of_set (tuples UNIV (length vs))) + {rs. + sumcheck pr s (H, p, v) r (zip vs rs) \ + v \ (\\ \ substs (set vs) H. eval p \)} + \ real (length vs) * real d / real (CARD('a))" + using assms +proof(induction vs arbitrary: s p v r) + case Nil + show ?case + by(simp) +next + case (Cons x vs) + + \ \abbreviations\ + let ?prob = "measure_pmf.prob (pmf_of_set (tuples UNIV (Suc (length vs))))" + let ?reduced_prob = "measure_pmf.prob (pmf_of_set (tuples UNIV (length vs)))" + + let ?q = "\\ \ substs (set vs) H. inst p \" \ \honest polynomial q\ + + let ?pr_q = "fst (pr (H, p, v) x vs r s)" \ \polynomial q from prover\ + let ?pr_s' = "snd (pr (H, p, v) x vs r s)" \ \prover's next state\ + + \ \some useful derived facts\ + have \vars (p) \ insert x (set vs)\ \x \ set vs\ \distinct vs\ + using \vars (p) \ set (x # vs)\ \distinct (x # vs)\ by auto + + have P0: + \?prob {r1#rs | r1 rs. + deg (?pr_q) \ deg (p) \ vars (?pr_q) \ {x} \ + v = (\a\H. eval (?pr_q) [x \ a]) \ + sumcheck pr (?pr_s') (H, inst (p) [x \ r1], eval (?pr_q) [x \ r1]) r1 (zip vs rs) \ + v \ (\\ \ substs (insert x (set vs)) H. eval (p) \) \ ?pr_q = ?q} = 0\ + proof - + have "(\a\H. eval (?q) [x \ a]) = + (\a\H. \\ \ substs (set vs) H. eval (p) ([x \ a] ++ \))" + using \vars (p) \ insert x (set vs)\ \x \ set vs\ + by(auto simp add: eval_sum_inst) + moreover + have "(\a\H. \\ \ substs (set vs) H. eval (p) ([x \ a] ++ \)) = + (\\ \ substs (insert x (set vs)) H. eval (p) \)" using \x \ set vs\ + by(auto simp add: sum_merge) + ultimately + have "{r1#rs | r1 rs. + v = (\a\H. eval (?pr_q) [x \ a]) \ + v \ (\\ \ substs (insert x (set vs)) H. eval (p) \) \ ?pr_q = ?q} = {}" + by(auto) + then show "?thesis" + by (intro prob_empty) (auto 4 4) + qed + + { \ \left-hand-side case where we use the roots assumption\ + have \?prob {r1#rs | r1 rs. + deg (?pr_q) \ deg (p) \ vars (?pr_q) \ {x} \ + v = (\a\H. eval (?pr_q) [x \ a]) \ + sumcheck pr (?pr_s') (H, inst (p) [x \ r1], eval (?pr_q) [x \ r1]) r1 (zip vs rs) \ + ?pr_q \ ?q \ eval (?pr_q) [x \ r1] = eval (?q) [x \ r1]} \ + ?prob {r1#rs | r1 rs. + deg (?pr_q) \ deg (p) \ vars (?pr_q) \ {x} \ + ?pr_q \ ?q \ eval (?pr_q) [x \ r1] = eval (?q) [x \ r1]}\ + by (intro prob_mono) (auto 4 4) + + also have \... = + measure_pmf.prob (pmf_of_set UNIV) {r1. + deg (?pr_q) \ deg (p) \ vars (?pr_q) \ {x} \ + ?pr_q \ ?q \ eval (?pr_q) [x \ r1] = eval (?q) [x \ r1]}\ + by (auto simp add: prob_tuples_hd_tl_indep[where Q = "\rs. True", simplified]) + + also have \... \ real (deg (p)) / real CARD('a)\ + using \vars (p) \ insert x (set vs)\ \H \ {}\ + by(auto simp add: prob_roots honest_prover_deg honest_prover_vars) + + also have \... \ real d / real CARD('a)\ using \deg (p) \ d\ + by (simp add: divide_right_mono) + + finally + have \?prob {r1#rs | r1 rs. + deg (?pr_q) \ deg (p) \ vars (?pr_q) \ {x} \ + v = (\a\H. eval (?pr_q) [x \ a]) \ + sumcheck pr (?pr_s') (H, inst (p) [x \ r1], eval (?pr_q) [x \ r1]) r1 (zip vs rs) \ + ?pr_q \ ?q \ eval (?pr_q) [x \ r1] = eval (?q) [x \ r1]} + \ real d / real CARD('a)\ . + } + note RP_left = this + + { + have *: \\\. eval (?q) [x \ \] = (\\ \ substs (set vs) H. eval (inst (p) [x \ \]) \)\ + using \vars (p) \ insert x (set vs)\ \x \ set vs\ + by(auto simp add: eval_sum_inst_commute) + + have \\\. vars (inst (p) [x \ \]) \ set vs\ using vars_inst \vars (p) \ insert x (set vs)\ + by fastforce + have \\\. deg (inst (p) [x \ \]) \ d\ using deg_inst \deg (p) \ d\ + using le_trans by blast + + \ \right-hand-side case where we apply the induction hypothesis\ + have \?prob {r1#rs | r1 rs. + deg (?pr_q) \ deg (p) \ vars (?pr_q) \ {x} \ + v = (\a\H. eval (?pr_q) [x \ a]) \ + sumcheck pr (?pr_s') (H, inst (p) [x \ r1], eval (?pr_q) [x \ r1]) r1 (zip vs rs) \ + ?pr_q \ ?q \ eval (?pr_q) [x \ r1] \ eval (?q) [x \ r1]} + \ ?prob {r1#rs | r1 rs. + sumcheck pr (?pr_s') (H, inst (p) [x \ r1], eval (?pr_q) [x \ r1]) r1 (zip vs rs) \ + eval (?pr_q) [x \ r1] \ (\\ \ substs (set vs) H. eval (inst (p) [x \ r1]) \)}\ + by(intro prob_mono) (auto simp add: *) + + \ \fix @{text "r1"}\ + also have \\ = (\\ \ UNIV. + ?reduced_prob {rs. + sumcheck pr (?pr_s') (H, inst (p) [x \ \], eval (?pr_q) [x \ \]) \ (zip vs rs) \ + eval (?pr_q) [x \ \] \ (\\ \ substs (set vs) H. eval (inst (p) [x \ \]) \)}) + / real(CARD('a))\ + by(auto simp add: prob_tuples_fixed_hd) + + \ \apply the induction hypothesis\ + also have \\ \ (\\ \ (UNIV::'a set). real (length vs) * real d / real CARD('a)) + / real(CARD('a))\ + using \\\. vars (inst (p) [x \ \]) \ set vs\ + \\\. deg (inst (p) [x \ \]) \ d\ + \distinct vs\ \H \ {}\ + by (intro divide_right_mono sum_mono Cons.IH) (auto) + + also have \\ = real (length vs) * real d / real CARD('a)\ + by fastforce + + finally + have \?prob {r1#rs | r1 rs. + deg (?pr_q) \ deg (p) \ vars (?pr_q) \ {x} \ + v = (\a\H. eval (?pr_q) [x \ a]) \ + sumcheck pr (?pr_s') (H, inst (p) [x \ r1], eval (?pr_q) [x \ r1]) r1 (zip vs rs) \ + ?pr_q \ ?q \ eval (?pr_q) [x \ r1] \ eval (?q) [x \ r1]} + \ real (length vs) * real d / real CARD('a)\ . + } + note RP_right = this + + \ \main equational reasoning proof\ + have \?prob {rs. + sumcheck pr s (H, p, v) r (zip (x # vs) rs) \ + v \ (\\ \ substs (insert x (set vs)) H. eval p \)} + = ?prob {r1#rs | r1 rs. sumcheck pr s (H, p, v) r (zip (x # vs) (r1#rs)) + \ v \ (\\ \ substs (insert x (set vs)) H. eval p \)}\ + by(intro prob_cong) (auto simp add: tuples_Suc) + + \ \unfold sumcheck\ + also have \\ = ?prob {r1#rs | r1 rs. + (let (q, s') = pr (H, p, v) x vs r s in + deg q \ deg p \ vars q \ {x} \ + v = (\a \ H. eval q [x \ a]) \ + sumcheck pr s' (H, inst p [x \ r1], eval q [x \ r1]) r1 (zip vs rs)) \ + v \ (\\ \ substs (insert x (set vs)) H. eval p \)}\ + by(intro prob_cong) (auto del: subsetI) + + also have \\ = ?prob {r1#rs | r1 rs . + deg ?pr_q \ deg p \ vars ?pr_q \ {x} \ + v = (\a\H. eval ?pr_q [x \ a]) \ + sumcheck pr ?pr_s' (H, inst p [x \ r1], eval ?pr_q [x \ r1]) r1 (zip vs rs) \ + v \ (\\ \ substs (insert x (set vs)) H. eval p \)}\ + by (intro prob_cong) (auto del: subsetI) + + \ \case split on whether prover's polynomial q equals honest one\ + also have \\ = ?prob {r1#rs | r1 rs. + deg (?pr_q) \ deg (p) \ vars (?pr_q) \ {x} \ + v = (\a\H. eval (?pr_q) [x \ a]) \ + sumcheck pr (?pr_s') (H, inst (p) [x \ r1], eval (?pr_q) [x \ r1]) r1 (zip vs rs) \ + v \ (\\ \ substs (insert x (set vs)) H. eval (p) \) \ ?pr_q = ?q} + + ?prob {r1#rs | r1 rs. + deg (?pr_q) \ deg (p) \ vars (?pr_q) \ {x} \ + v = (\a\H. eval (?pr_q) [x \ a]) \ + sumcheck pr (?pr_s') (H, inst (p) [x \ r1], eval (?pr_q) [x \ r1]) r1 (zip vs rs) \ + v \ (\\ \ substs (insert x (set vs)) H. eval (p) \) \ ?pr_q \ ?q}\ + by(intro prob_disjoint_cases) auto + + \ \first probability is 0\ + also have \\ = ?prob {r1#rs | r1 rs. + deg (?pr_q) \ deg (p) \ vars (?pr_q) \ {x} \ + v = (\a\H. eval (?pr_q) [x \ a]) \ + sumcheck pr (?pr_s') (H, inst (p) [x \ r1], eval (?pr_q) [x \ r1]) r1 (zip vs rs) \ + v \ (\\ \ substs (insert x (set vs)) H. eval (p) \) \ ?pr_q \ ?q}\ + by (simp add: P0) + + \ \dropped condition\ + also have \\ \ ?prob {r1#rs | r1 rs. + deg (?pr_q) \ deg (p) \ vars (?pr_q) \ {x} \ + v = (\a\H. eval (?pr_q) [x \ a]) \ + sumcheck pr (?pr_s') (H, inst (p) [x \ r1], eval (?pr_q) [x \ r1]) r1 (zip vs rs) \ + ?pr_q \ ?q}\ + by(intro prob_mono) (auto) + + also have \\ = + ?prob {r1#rs | r1 rs. + deg (?pr_q) \ deg (p) \ vars (?pr_q) \ {x} \ + v = (\a\H. eval (?pr_q) [x \ a]) \ + sumcheck pr (?pr_s') (H, inst (p) [x \ r1], eval (?pr_q) [x \ r1]) r1 (zip vs rs) \ + ?pr_q \ ?q \ eval (?pr_q) [x \ r1] = eval (?q) [x \ r1]} + + ?prob {r1#rs | r1 rs. + deg (?pr_q) \ deg (p) \ vars (?pr_q) \ {x} \ + v = (\a\H. eval (?pr_q) [x \ a]) \ + sumcheck pr (?pr_s') (H, inst (p) [x \ r1], eval (?pr_q) [x \ r1]) r1 (zip vs rs) \ + ?pr_q \ ?q \ eval (?pr_q) [x \ r1] \ eval (?q) [x \ r1]}\ + by(intro prob_disjoint_cases) (auto) + + also have \\ \ real d / real CARD('a) + + (real (length vs) * real d) / real CARD('a)\ + by (intro add_mono RP_left RP_right) + + also have \\ = (1 + real (length vs)) * real d / real CARD('a)\ + by (metis add_divide_distrib mult_Suc of_nat_Suc of_nat_add of_nat_mult) + + finally show ?case by simp +qed + + +corollary soundness: + assumes + "(H, p, v) \ Sumcheck" + "vars p = set vs" and + "distinct vs" and + "H \ {}" + shows + "measure_pmf.prob + (pmf_of_set (tuples UNIV (arity p))) + {rs. sumcheck pr s (H, p, v) r (zip vs rs)} + \ real (arity p) * real (deg p) / real (CARD('a))" + using assms +proof - + have *: \arity p = length vs\ using \vars p = set vs\ \distinct vs\ + by (simp add: arity_def distinct_card) + + have "measure_pmf.prob (pmf_of_set (tuples UNIV (arity p))) + {rs. sumcheck pr s (H, p, v) r (zip vs rs)} = + measure_pmf.prob (pmf_of_set (tuples UNIV (arity p))) + {rs. sumcheck pr s (H, p, v) r (zip vs rs) \ (H, p, v) \ Sumcheck}" + using \(H, p, v) \ Sumcheck\ + by (intro prob_cong) (auto) + also have "\ \ real (arity p) * real (deg p) / real (CARD('a))" using assms(2-) * + by (auto simp add: Sumcheck_def intro!: soundness_inductive) + finally show ?thesis by simp +qed + + +end + +end \ No newline at end of file diff --git a/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Substitutions.thy b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Substitutions.thy new file mode 100644 --- /dev/null +++ b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Substitutions.thy @@ -0,0 +1,104 @@ +(******************************************************************************* + + Project: Sumcheck Protocol + + Authors: Azucena Garvia Bosshard + Christoph Sprenger, ETH Zurich + Jonathan Bootle, IBM Research Europe + +*******************************************************************************) + +section \Substitutions\ + +theory Substitutions + imports + Main + "HOL-Library.FuncSet" +begin + +type_synonym ('v, 'a) subst = "'v \ 'a" + +definition substs :: "'v set \ 'a set \ ('v, 'a) subst set" where + "substs V H = {\. dom \ = V \ ran \ \ H}" + +text \Small lemmas about the set of substitutions\ + +lemma substE [elim]: "\ \ \ substs V H; \ dom \ = V; ran \ \ H \ \ P \ \ P" + by (simp add: substs_def) + +lemma substs_empty_dom [simp]: "substs {} H = {Map.empty}" + by (auto simp add: substs_def) + +lemma substs_finite: "\ finite V; finite H \ \ finite (substs V H)" + by (simp add: finite_set_of_finite_maps substs_def) + +lemma substs_nonempty: + assumes "H \ {}" + shows "substs V H \ {}" +proof - + obtain h where A1: "h \ H" using assms by(auto) + obtain \ where A2: "\ = (\v. if v \ V then Some h else None)" by(simp) + have "\ \ substs V H" using A1 A2 by(auto simp add: substs_def ran_def dom_def) + then show ?thesis by(auto) +qed + +lemma subst_dom: \\ \ \ substs V H; x \ V \ \ x \ dom \\ + by(auto simp add: substs_def) + +lemma subst_add: + assumes "x \ V" and "\ \ substs (V - {x}) H" and "a \ H" + shows "\(x \ a) \ substs V H" + using assms + by(simp add: substs_def) + (auto simp add: dom_def ran_def) + +lemma subst_im: + assumes "x \ V" and "\ \ substs V H" + shows "the (\ x) \ H" + using assms + by(auto simp add: substs_def dom_def ran_def) + +lemma subst_restr: + assumes "x \ V" and "\ \ substs V H" + shows "\ |` (dom \ - {x}) \ substs (V - {x}) H" + using assms + by(auto simp add: substs_def ran_def dom_def restrict_map_def) + + +text \Bijection between sets of substitutions\ + +lemma restrict_map_dom: "\ |` dom \ = \" + by (metis (no_types, lifting) domIff map_le_antisym map_le_def restrict_in restrict_out) + + +lemma bij_betw_set_substs: + assumes "x \ V" + defines "f \ \(a, \::'v \ 'a). \(x \ a)" + and "g \ \\::'v \ 'a. (the (\ x), \|`(dom \ - {x}))" + shows "bij_betw f + (H \ substs (V - {x}) H) + (substs V H)" +proof (intro bij_betwI) + show "f \ H \ substs (V - {x}) H \ substs V H" + using assms + by(auto simp add: f_def subst_add) +next + show "g \ substs V H \ H \ substs (V - {x}) H" + using assms + by(auto simp add: g_def subst_im subst_restr) +next + fix xa + assume "xa \ H \ substs (V - {x}) H" + then show "g (f xa) = xa" using assms + by (smt (z3) Diff_empty Diff_insert0 Diff_insert_absorb SigmaE case_prod_conv + fun_upd_None_restrict fun_upd_same fun_upd_upd mk_disjoint_insert option.sel + restrict_map_dom subst_dom) +next + fix y + assume "y \ substs V H" + then show "f (g y) = y" using assms + by(auto simp add: g_def f_def) + (metis domIff fun_upd_restrict map_upd_triv option.exhaust_sel restrict_map_dom substE) +qed + +end \ No newline at end of file diff --git a/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Sumcheck_Protocol.thy b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Sumcheck_Protocol.thy new file mode 100644 --- /dev/null +++ b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Sumcheck_Protocol.thy @@ -0,0 +1,120 @@ +(******************************************************************************* + + Project: Sumcheck Protocol + + Authors: Azucena Garvia Bosshard + Christoph Sprenger, ETH Zurich + Jonathan Bootle, IBM Research Europe + +*******************************************************************************) + +section \Sumcheck Protocol\ + +theory Sumcheck_Protocol + imports + Public_Coin_Proofs + Abstract_Multivariate_Polynomials +begin + +subsection \The sumcheck problem\ + +text \Type of sumcheck instances\ +type_synonym ('p, 'a, 'b) sc_inst = "'a set \ 'p \ 'b" + +definition (in multi_variate_polynomial) + Sumcheck :: "('p, 'a, 'b) sc_inst set" where + "Sumcheck = {(H, p, v) | H p v. v = (\\\substs (vars p) H. eval p \)}" + + +subsection \The sumcheck protocol\ + +text \Type of the prover\ +type_synonym ('p, 'a, 'b, 'v, 's) prover = "(('p, 'a, 'b) sc_inst, 'a, 'v, 'p, 's) prv" + +text \Here is how the expanded type lools like @{typ [display] "('p, 'a, 'b, 'v, 's) prover"}.\ + + +context multi_variate_polynomial begin + +text \Sumcheck function\ +fun sumcheck :: "('p, 'a, 'b, 'v, 's) prover \ 's \ ('p, 'a, 'b) sc_inst \ 'a \ ('v \ 'a) list \ bool" where + "sumcheck pr s (H, p, v) r_prev [] \ v = eval p Map.empty" +| "sumcheck pr s (H, p, v) r_prev ((x, r) # rm) \ + (let (q, s') = pr (H, p, v) x (map fst rm) r_prev s in + vars q \ {x} \ deg q \ deg p \ + v = (\y \ H. eval q [x \ y]) \ + sumcheck pr s' (H, inst p [x \ r], eval q [x \ r]) r rm)" + +text \Honest prover definition\ +fun honest_prover :: "('p, 'a, 'b, 'v, unit) prover" where + "honest_prover (H, p, _) x xs _ _ = (\\ \ substs (set xs) H. inst p \, ())" + +declare honest_prover.simps [simp del] +lemmas honest_prover_def = honest_prover.simps + +text \Lemmas on variables and degree of the honest prover.\ + +lemma honest_prover_vars: + assumes "vars p \ insert x V" "finite V" "H \ {}" "finite H" + shows "vars (\\\substs V H. inst p \) \ {x}" +proof - + have *: "\\. \ \ substs V H \ vars (inst p \) \ {x}" using assms + by (metis (no_types, lifting) Diff_eq_empty_iff Diff_insert subset_iff substE vars_inst) + + have "vars (sum (inst p) (substs V H)) \ (\\\substs V H. vars (inst p \))" + using \finite V\ \finite H\ + by (auto simp add: vars_sum substs_finite) + also have "\ \ {x}" using \H \ {}\ * + by (auto simp add: substs_nonempty vars_finite substs_finite) + finally show ?thesis . +qed + +lemma honest_prover_deg: + assumes "H \ {}" "finite V" + shows "deg (\\\substs V H. inst p \) \ deg p" +proof - + have "deg (\\\substs V H. inst p \) \ Max {deg (inst p \) |\. \ \ substs V H}" + by(auto simp add: substs_finite substs_nonempty deg_sum assms) + also have "\ \ deg p" + by(auto simp add: substs_finite substs_nonempty deg_inst assms) + finally show ?thesis . +qed + + +subsection \The sumcheck protocol as a public-coin proof instance\ + +text \Define verifier functions\ + +fun sc_ver0 :: "('p, 'a, 'b) sc_inst \ unit \ bool" where + "sc_ver0 (H, p, v) () \ v = eval p Map.empty" + +fun sc_ver1 :: + "('p, 'a, 'b) sc_inst \ 'p \ 'a \ 'v \ 'v list \ unit \ bool \ ('p, 'a, 'b) sc_inst \ unit" +where + "sc_ver1 (H, p, v) q r x _ () = ( + vars q \ {x} \ deg q \ deg p \ v = (\y \ H. eval q [x \ y]), + (H, inst p [x \ r], eval q [x \ r]), + () + )" + +sublocale sc: public_coin_proof sc_ver0 sc_ver1 . + + +text \Equivalence of @{term sumcheck} with public-coin proofs instance\ + +lemma prove_sc_eq_sumcheck: + \sc.prove () pr ps (H, p, v) r rm = sumcheck pr ps (H, p, v) r rm\ +proof (induction "()" pr ps "(H, p, v)" r rm arbitrary: p v rule: sc.prove.induct) + case (1 vs prv ps r) + then show ?case by (simp) +next + case (2 vs prv ps r r' rs x xs) + then show ?case by (simp split:prod.split) +qed + + +end +end + + + diff --git a/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Sumcheck_as_Public_Coin_Proof.thy b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Sumcheck_as_Public_Coin_Proof.thy new file mode 100644 --- /dev/null +++ b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Sumcheck_as_Public_Coin_Proof.thy @@ -0,0 +1,71 @@ +(******************************************************************************* + + Project: Sumcheck Protocol + + Authors: Azucena Garvia Bosshard + Christoph Sprenger, ETH Zurich + Jonathan Bootle, IBM Research Europe + +*******************************************************************************) + +section \Sumcheck Protocol as Public-coin Proof\ + +theory Sumcheck_as_Public_Coin_Proof + imports + Completeness_Proof + Soundness_Proof +begin + + +context multi_variate_polynomial begin + +subsection \Property-related definitions\ + +fun sc_sound_err :: "('p, 'a, 'b) sc_inst \ real" where + "sc_sound_err (H, p, v) = real (arity p) * real (deg p) / real (CARD('a))" + +fun sc_compl_assm where + "sc_compl_assm vs ps (H, p, v) xs \ + set xs = vars p \ distinct xs \ H \ {}" + +fun sc_sound_assm where + "sc_sound_assm vs ps (H, p, v) xs \ + set xs = vars p \ distinct xs \ H \ {}" + + +subsection \Public coin proof locale interpretation\ + +sublocale + scp: public_coin_proof_strong_props + sc_ver0 sc_ver1 Sumcheck honest_prover sc_sound_err sc_compl_assm sc_sound_assm +proof + fix I :: "('p, 'a, 'b) sc_inst" and + vs :: unit and ps :: unit and + rm :: "('v \ 'a) list" and r :: 'a + assume "I \ Sumcheck" and "sc_compl_assm vs ps I (map fst rm)" + then show "sc.prove vs honest_prover ps I r rm" + by (cases I) (simp add: prove_sc_eq_sumcheck completeness) +next + fix I :: "('p, 'a, 'b) sc_inst" and + vs :: unit and ps :: 'ps and + r :: 'a and rs :: "'a list" and xs :: "'v list" and pr + assume "I \ Sumcheck" and "sc_sound_assm vs ps I xs" + then show + "measure_pmf.prob + (pmf_of_set (tuples UNIV (length xs))) + {rs. sc.prove vs pr ps I r (zip xs rs)} + \ sc_sound_err I" + proof (cases I) + case (fields H p v) + have "length xs = arity p" using \sc_sound_assm vs ps I xs\ fields + by (auto simp add: arity_def distinct_card dest: sym) + then show ?thesis using \I \ Sumcheck\ \sc_sound_assm vs ps I xs\ fields + by (auto simp add: prove_sc_eq_sumcheck intro: soundness) + qed +qed + + +end \ \context @{locale "multi_variate_polynomial"}\ + + +end diff --git a/thys/Sumcheck_Protocol/Instantiation_with_Polynomials/Concrete_Multivariate_Polynomials.thy b/thys/Sumcheck_Protocol/Instantiation_with_Polynomials/Concrete_Multivariate_Polynomials.thy new file mode 100644 --- /dev/null +++ b/thys/Sumcheck_Protocol/Instantiation_with_Polynomials/Concrete_Multivariate_Polynomials.thy @@ -0,0 +1,321 @@ +(******************************************************************************* + + Project: Sumcheck Protocol + + Authors: Azucena Garvia Bosshard + Christoph Sprenger, ETH Zurich + Jonathan Bootle, IBM Research Europe + +*******************************************************************************) + +section \Multivariate Polynomials: Instance\ + +theory Concrete_Multivariate_Polynomials + imports + "../Generalized_Sumcheck_Protocol/Sumcheck_as_Public_Coin_Proof" + Polynomial_Instantiation + Roots_Bounds +begin + +declare total_degree_zero [simp del] + +subsection \Auxiliary lemmas\ + +lemma card_indep_bound: + assumes "P \ card {x. Q x} \ d" + shows "card {x. P \ Q x} \ d" + using assms + by (cases P) auto + +lemma sum_point_neq_zero [simp]: "(\x' | x' = x \ f x' \ 0. f x') = f x" +proof - + have \(\x' | x' = x \ f x' \ 0. f x') = (\x' | x' = x \ f x \ 0. f x')\ + by (intro sum.cong) auto + also have \\ = f x\ + by (cases "f x = 0") (simp_all) + finally show ?thesis . +qed + + +subsection \Proving the assumptions of the locale\ + +subsubsection \Variables\ + +\ \The term @{term vars} is already defined in @{theory "Polynomials.More_MPoly_Type"}.\ + +\ \We show the assumptions @{thm [source] "multi_variate_polynomial.vars_finite"}, +@{thm [source] "multi_variate_polynomial.vars_add"}, +@{thm [source] "multi_variate_polynomial.vars_zero"} and +@{thm [source] "multi_variate_polynomial.vars_inst"} from the locale +@{locale "multi_variate_polynomial"}.\ + +lemma vars_zero: \vars 0 = {}\ + by (simp add: vars_def zero_mpoly.rep_eq) + +lemma vars_inst: \vars (inst p \) \ vars p - dom \\ + by (auto simp add: vars_def inst_defs keys_def MPoly_inverse + finite_inst_fun_keys lookup_inst_monom_resid + elim!: sum.not_neutral_contains_not_neutral split: if_splits) + + +\ \Lemmas for to translate the roots bound to the format of the locale assumption.\ + +lemma vars_minus: \vars p = vars (-p)\ + by(simp add: vars_def uminus_mpoly.rep_eq) + +lemma vars_subtr: + fixes p q :: \'a::comm_ring mpoly\ + shows \vars (p - q) \ vars p \ vars q\ + by(simp add: vars_add[where ?p1.0 = "p" and ?p2.0 = "-q", simplified] vars_minus[where p = "q"]) + + +subsubsection \Degree\ + +\ \We define the degree of a multivariate polynomial as its total degree\ + +abbreviation deg :: \('a::zero) mpoly \ nat\ where + \deg p \ total_degree p\ + + +\ \We show the assumptions @{thm [source] "multi_variate_polynomial.deg_zero"}, +@{thm [source] "multi_variate_polynomial.deg_add"} and @{thm [source] "multi_variate_polynomial.deg_inst"}.\ + +lemma deg_zero: \deg 0 = 0\ by (fact total_degree_zero) + +lemma deg_add: \deg (p + q) \ max (deg p) (deg q)\ +proof - + have \deg (p + q) = Max (insert 0 ((\x. sum (lookup x) (keys x)) ` keys (mapping_of p + mapping_of q)))\ + by (simp add: total_degree.rep_eq plus_mpoly.rep_eq) + also have \... \ Max (insert 0 ((\x. sum (lookup x) (keys x)) ` (keys (mapping_of p) \ keys (mapping_of q))))\ + by (intro Max_mono Set.insert_mono image_mono Poly_Mapping.keys_add) (auto) + also have \... = Max ((insert 0 ((\x. sum (lookup x) (keys x)) ` keys (mapping_of p))) + \ (insert 0 ((\x. sum (lookup x) (keys x)) ` keys (mapping_of q))))\ + by (simp add: image_Un) + also have \... = max (Max (insert 0 ((\x. sum (lookup x) (keys x)) ` keys (mapping_of p)))) + (Max (insert 0 ((\x. sum (lookup x) (keys x)) ` keys (mapping_of q))))\ + by (intro Max_Un) (auto) + also have \... = max (deg p) (deg q)\ + by (simp add: total_degree.rep_eq) + finally show ?thesis . +qed + +lemma deg_inst: \deg (inst p \) \ deg p\ +proof (transfer) + fix p :: \(nat \\<^sub>0 nat) \\<^sub>0 'a\ and \ :: "(nat, 'a) subst" + show \Max (insert 0 ((\m. sum (lookup m) (keys m)) ` keys (inst_aux p \))) + \ Max (insert 0 ((\m. sum (lookup m) (keys m)) ` keys p))\ + by (auto simp add: keys_def inst_defs finite_inst_fun_keys lookup_inst_monom_resid + elim!: sum.not_neutral_contains_not_neutral) + (fastforce simp add: Max_ge_iff intro!: disjI2 intro: sum_mono2) +qed + + +\ \Lemmas for translating the roots bound to the format of the locale assumption.\ + +lemma deg_minus: \deg p = deg (-p)\ + by(auto simp add: total_degree_def uminus_mpoly.rep_eq) + +lemma deg_subtr: + fixes p q :: \'a::comm_ring mpoly\ + shows \deg (p - q) \ max (deg p) (deg (q))\ + by(auto simp add: deg_add[where p = "p" and q = "-q", simplified] deg_minus[where p = "q"]) + + +subsubsection \Evaluation\ + +\ \Our evaluation is defined as insertion in MPoly_Type\ + +abbreviation eval :: \'a mpoly \ (nat, 'a) subst \ ('a::comm_semiring_1)\ where + \eval p \ \ insertion (the o \) p\ + +\ \We show the assumptions @{thm [source] "multi_variate_polynomial.eval_zero"}, +@{thm [source] "multi_variate_polynomial.eval_add"} and @{thm [source] "multi_variate_polynomial.eval_inst"}.\ + +lemma eval_zero: \eval 0 \ = 0\ + by (fact insertion_zero) + +lemma eval_add: \vars p \ vars q \ dom \ \ eval (p + q) \ = eval p \ + eval q \\ + by (intro insertion_add) + +\ \evaluation and instantiation\ + +lemma eval_inst: \eval (inst p \) \ = eval p (\ ++ \)\ +proof (transfer, transfer) + fix p :: \(nat \\<^sub>0 nat) \ 'a\ and \ \ :: \(nat, 'a) subst\ + assume fin: \finite {m. p m \ 0}\ + show \insertion_fun (the \ \) (inst_fun p \) = insertion_fun (the \ \ ++ \) p\ + proof - + let ?mon = \\\ m v. the (\ v) ^ lookup m v\ + + have \x ^ lookup m v \ 1 \ v \ keys m\ for x :: "'a" and v and m :: "nat \\<^sub>0 nat" + using zero_less_iff_neq_zero by (fastforce simp add: in_keys_iff) + then have exp_fin: \finite {v. P v \ f v ^ lookup m v \ 1}\ + for f :: "nat \ 'a" and m :: "nat \\<^sub>0 nat" and P :: "nat \ bool" + by (auto intro: finite_subset[where B="keys m"]) + + note fin_simps [simp] = fin this this[where P1="\_. True", simplified] + note map_add_simps [simp] = map_add_dom_app_simps(1,3) + + have \insertion_fun (the \ \) (inst_fun p \) = + (\m. (\m' | inst_monom_resid m' \ = m \ p m' \ 0 \ inst_monom_coeff m' \ \ 0. + p m' * inst_monom_coeff m' \) * (\v. ?mon \ m v))\ + by (simp add: insertion_fun_def inst_fun_def) + + also have \\ = + (\m. (\m' | inst_monom_resid m' \ = m \ p m' \ 0 \ inst_monom_coeff m' \ \ 0. + p m' * inst_monom_coeff m' \ * (\v. ?mon \ m v)))\ + by (intro Sum_any.cong) (simp add: sum_distrib_right) + + also have \\ = + (\m. (\m' | inst_monom_resid m' \ = m \ p m' \ 0 \ inst_monom_coeff m' \ \ 0. + p m' * inst_monom_coeff m' \ * (\v | v \ dom \ \ ?mon \ m' v \ 1. ?mon \ m' v)))\ + by (intro Sum_any.cong sum.cong) + (auto simp add: lookup_inst_monom_resid Prod_any.expand_set intro: arg_cong) + + also have \\ = + (\m. (\m' | inst_monom_resid m' \ = m \ p m' \ 0 \ + (\v | v \ dom \ \ ?mon \ m' v \ 1. ?mon \ m' v) \ 0. + p m' * + ((\v | v \ dom \ \ ?mon \ m' v \ 1. ?mon (\ ++ \) m' v) * + (\v | v \ dom \ \ ?mon \ m' v \ 1. ?mon (\ ++ \) m' v))))\ + by (simp add: inst_monom_coeff_def mult.assoc) + + also have \\ = + (\m. (\m' | inst_monom_resid m' \ = m \ p m' \ 0 \ + (\v | v \ dom \ \ ?mon \ m' v \ 1. ?mon \ m' v) \ 0 \ + (\v | v \ dom \ \ ?mon \ m' v \ 1. ?mon \ m' v) \ 0. + p m' * + ((\v | v \ dom \ \ ?mon \ m' v \ 1. ?mon (\ ++ \) m' v) * + (\v | v \ dom \ \ ?mon \ m' v \ 1. ?mon (\ ++ \) m' v))))\ + by (intro Sum_any.cong sum.mono_neutral_right) (auto) + + also have \\ = + (\m. (\m' | inst_monom_resid m' \ = m \ p m' \ 0 \ + (\v | v \ dom \ \ ?mon \ m' v \ 1. ?mon \ m' v) \ 0 \ + (\v | v \ dom \ \ ?mon \ m' v \ 1. ?mon \ m' v) \ 0. + p m' * + (\v | v \ dom \ \ ?mon \ m' v \ 1 \ v \ dom \ \ ?mon \ m' v \ 1. ?mon (\ ++ \) m' v)))\ + by (subst prod.union_disjoint[symmetric]) + (auto intro!: Sum_any.cong sum.cong prod.cong intro: arg_cong) + + also have \\ = + (\m. (\m' | inst_monom_resid m' \ = m \ p m' \ 0 \ + (\v | v \ dom \ \ ?mon \ m' v \ 1. ?mon \ m' v) \ 0 \ + (\v | v \ dom \ \ ?mon \ m' v \ 1. ?mon \ m' v) \ 0. + p m' * (\v. ?mon (\ ++ \) m' v)))\ + apply (intro Sum_any.cong sum.cong arg_cong[where f="(*) x" for x], simp) + apply (simp add: Prod_any.expand_set) + apply (intro prod.cong, simp_all) + by (metis (no_types, opaque_lifting) map_add_dom_app_simps(1,3)) + + also have \\ = + (\m. (\m' | inst_monom_resid m' \ = m \ p m' \ 0 \ (\v. ?mon (\ ++ \) m' v) \ 0. + p m' * (\v. ?mon (\ ++ \) m' v)))\ + apply (intro Sum_any.cong sum.mono_neutral_right, simp_all) + apply (safe, simp_all) + \ \fixme: cannot get auto/fastforce to do instantiations below\ + subgoal for m v z + by (auto dest: Prod_any_not_zero[rotated, where a=v]) + subgoal for m' v + by (auto simp add: domIff dest: Prod_any_not_zero[rotated, where a=v]) + done + + also have \\ = + (\m. (sum + (\m'. p m' * (\v. ?mon (\ ++ \) m' v)) + {m' \ {m'. p m' \ 0 \ (\v. ?mon (\ ++ \) m' v) \ 0}. + inst_monom_resid m' \ = m}))\ + by (intro Sum_any.cong sum.cong) (auto) + + also have \\ = + (\m \ (\m'. inst_monom_resid m' \) ` {m'. p m' \ 0 \ (\v. the ((\ ++ \) v) ^ lookup m' v) \ 0}. + (sum + (\m'. p m' * (\v. ?mon (\ ++ \) m' v)) + {m' \ {m'. p m' \ 0 \ (\v. ?mon (\ ++ \) m' v) \ 0}. + inst_monom_resid m' \ = m}))\ + by (intro Sum_any.expand_superset) (auto elim: sum.not_neutral_contains_not_neutral) + + also have \\ = (\m. p m * (\v. ?mon (\ ++ \) m v))\ + by (subst Sum_any.expand_set, subst sum.group) (auto) + + also have \\ = insertion_fun (the \ \ ++ \) p\ + by (simp add: insertion_fun_def) + finally show ?thesis . + qed +qed + +\ \Lemmas for translating the roots bound to the format of the locale assumption.\ + +lemma eval_minus: + fixes p :: \'a::comm_ring_1 mpoly\ + shows \eval (-p) \ = - eval p \\ + using sum_negf[where f = "\a . (lookup (mapping_of p) a * (\aa. the (\ aa) ^ lookup a aa))"] + by(auto simp add: uminus_mpoly.rep_eq insertion_def insertion_aux_def insertion_fun_def) + (smt (verit) Collect_cong Sum_any.expand_set add.inverse_neutral neg_equal_iff_equal) + +lemma eval_subtr: + fixes p q :: \'a::comm_ring_1 mpoly\ + assumes \vars p \ dom \\ \vars q \ dom \\ + shows \eval (p - q) \ = eval p \ - eval q \\ + using assms + by(auto simp add: vars_minus[where p = "q"] eval_minus[where p = "q"] + eval_add[where p = "p" and q = "-q", simplified]) + + +subsubsection \Roots assumption\ + +lemma univariate_eval_as_insertion: + fixes p::\'a::comm_ring_1 mpoly\ and r + assumes "vars p \ {x}" + shows "eval p [x \ r] = insertion (\x. r) p" + using assms + by (intro insertion_irrelevant_vars) auto + +lemma univariate_mpoly_roots_bound_eval: \ \variant using @{term eval}\ + fixes p::"'a::idom mpoly" + assumes \vars p \ {x}\ \p \ 0\ + shows \card {r. eval p [x \ r] = 0} \ deg p\ + using assms + by (simp add: univariate_eval_as_insertion univariate_mpoly_roots_bound) + +lemma mpoly_roots: + fixes p q :: \'a::idom mpoly\ and d x + shows \card {r. deg p \ d \ vars p \ {x} \ deg q \ d \ vars q \ {x} \ + p \ q \ eval p [x \ r] = eval q [x \ r]} \ d\ +proof (intro card_indep_bound) + assume \deg p \ d\ \vars p \ {x}\ \deg q \ d\ \vars q \ {x}\ \p \ q\ + show \card {r. eval p [x \ r] = eval q [x \ r]} \ d\ + proof - + have \card {r. eval p [x \ r] = eval q [x \ r]} = card {r. eval (p - q) [x \ r] = 0}\ + using \vars p \ {x}\ \vars q \ {x}\ by (simp add: eval_subtr) + also have \\ \ deg (p - q)\ + using \vars p \ {x}\ \vars q \ {x}\ \p \ q\ + by (intro univariate_mpoly_roots_bound_eval subset_trans[OF vars_subtr]) (auto) + also have \\ \ d\ using \deg p \ d\ \deg q \ d\ + by (intro le_trans[OF deg_subtr]) (simp) + finally show ?thesis . + qed +qed + + +subsection \Locale interpretation\ + +text \Finally, collect all relevant lemmas and instantiate the abstract polynomials locale.\ + +lemmas multi_variate_polynomial_lemmas = + vars_finite vars_zero vars_add vars_inst + deg_zero deg_add deg_inst + eval_zero eval_add eval_inst + mpoly_roots + +interpretation mpoly: + multi_variate_polynomial vars "deg :: 'a::{finite, idom} mpoly \ nat" eval inst + by (unfold_locales) (auto simp add: multi_variate_polynomial_lemmas) + + +text \Here are the main results, spezialized for type @{typ \'a mpoly\}. +The completeness theorem for this type is @{thm [display] "mpoly.completeness"} +and the soundness theorem reads @{thm [display] "mpoly.soundness"}. +\ + +end diff --git a/thys/Sumcheck_Protocol/Instantiation_with_Polynomials/Polynomial_Instantiation.thy b/thys/Sumcheck_Protocol/Instantiation_with_Polynomials/Polynomial_Instantiation.thy new file mode 100644 --- /dev/null +++ b/thys/Sumcheck_Protocol/Instantiation_with_Polynomials/Polynomial_Instantiation.thy @@ -0,0 +1,120 @@ +(******************************************************************************* + + Project: Sumcheck Protocol + + Authors: Azucena Garvia Bosshard + Christoph Sprenger, ETH Zurich + Jonathan Bootle, IBM Research Europe + +*******************************************************************************) + +section \Instantiation for Multivariate Polynomials\ + +theory Polynomial_Instantiation + imports + "Polynomials.More_MPoly_Type" +begin + +text \ +\textbf{NOTE:} if considered to be useful enough, the definitions and lemmas in this theory could +be moved to the theory @{theory "Polynomials.More_MPoly_Type"}. +\ + +text \Define instantiation of mpoly's. The conditions @{term "(\) 1"} and @{term "(\) 0"} in +the sets being multiplied or added over are needed to prove the correspondence with evaluation: +a full instance corresponds to an evaluation (see lemma below).\ + +subsection \Instantiation of monomials\ + +type_synonym ('a, 'b) subst = "'a \ 'b" + +lift_definition + inst_monom_coeff :: \(nat \\<^sub>0 nat) \ (nat, 'a) subst \ 'a::comm_semiring_1\ + is \\m \. (\v | v \ dom \ \ the (\ v) ^ m v \ 1. the (\ v) ^ m v)\ . + +lift_definition + inst_monom_resid :: \(nat \\<^sub>0 nat) \ (nat, 'a) subst \ (nat \\<^sub>0 nat)\ + is \(\m \ v. m v when v \ dom \)\ + by (metis (mono_tags, lifting) finite_subset mem_Collect_eq subsetI zero_when) + +lemmas inst_monom_defs = inst_monom_coeff_def inst_monom_resid_def + +lemma lookup_inst_monom_resid: + shows \lookup (inst_monom_resid m \) v = (if v \ dom \ then 0 else lookup m v)\ + by transfer simp + + +subsection \Instantiation of polynomials\ + +definition + inst_fun :: \((nat \\<^sub>0 nat) \ 'a) \ (nat, 'a) subst \ (nat \\<^sub>0 nat) \ 'a::comm_semiring_1\ where + \inst_fun p \ = (\m. (\m' | inst_monom_resid m' \ = m \ p m' * inst_monom_coeff m' \ \ 0. + p m' * inst_monom_coeff m' \))\ + +lemma finite_inst_fun_keys: + assumes \finite {m. p m \ 0}\ + shows \finite {m. (\m' | inst_monom_resid m' \ = m \ p m' \ 0 \ inst_monom_coeff m' \ \ 0. + p m' * inst_monom_coeff m' \) \ 0}\ +proof - + from \finite {m. p m \ 0}\ + have \finite ((\m'. inst_monom_resid m' \)`{x. p x \ 0})\ by auto + moreover + have \{m. (\m' | inst_monom_resid m' \ = m \ p m' \ 0 \ inst_monom_coeff m' \ \ 0. + p m' * inst_monom_coeff m' \) \ 0} + \ (\m'. inst_monom_resid m' \)`{m. p m \ 0}\ + by (auto elim: sum.not_neutral_contains_not_neutral) + ultimately show ?thesis + by (auto elim: finite_subset) +qed + +lemma finite_inst_fun_keys_ext: + assumes \finite {m. p m \ 0}\ + shows "finite {a. (\m' | inst_monom_resid m' \ = a \ p m' \ 0 \ inst_monom_coeff m' \ \ 0. + p m' * inst_monom_coeff m' \ * (\aa. the (\ aa) ^ lookup (inst_monom_resid m' \) aa)) \ 0}" +proof - + from \finite {m. p m \ 0}\ + have \finite ((\m'. inst_monom_resid m' \)`{x. p x \ 0})\ by auto + moreover + have \{m. (\m' | inst_monom_resid m' \ = m \ p m' \ 0 \ inst_monom_coeff m' \ \ 0. + p m' * inst_monom_coeff m' \ * + (\aa. the (\ aa) ^ lookup (inst_monom_resid m' \) aa)) \ 0} + \ (\m'. inst_monom_resid m' \)`{m. p m \ 0}\ + by (auto elim: sum.not_neutral_contains_not_neutral) + ultimately show ?thesis + by (auto elim: finite_subset) +qed + +lift_definition + inst_aux :: \((nat \\<^sub>0 nat) \\<^sub>0 'a) \ (nat, 'a) subst \ (nat \\<^sub>0 nat) \\<^sub>0 'a::semidom\ + is inst_fun + by (auto simp add: inst_fun_def intro: finite_inst_fun_keys) + +lift_definition inst :: \'a mpoly \ (nat, 'a::semidom) subst \ 'a mpoly\ + is inst_aux . + +lemmas inst_defs = inst_def inst_aux_def inst_fun_def + + +subsection \Full instantiation corresponds to evaluation\ + +lemma dom_Some: \dom (Some o f) = UNIV\ + by (simp add: dom_def) + +lemma inst_full_eq_insertion: + fixes p :: \('a::semidom) mpoly\ and \ :: \nat \ 'a\ + shows \inst p (Some o \) = Const (insertion \ p)\ +proof transfer + fix p :: \(nat \\<^sub>0 nat) \\<^sub>0 'a\ and \ :: \nat \ 'a\ + show \inst_aux p (Some o \) = Const\<^sub>0 (insertion_aux \ p)\ + unfolding poly_mapping_eq_iff + apply (simp add: Const\<^sub>0_def inst_aux.rep_eq inst_fun_def inst_monom_defs + Poly_Mapping.single.rep_eq insertion_aux.rep_eq insertion_fun_def) + apply (rule ext) + subgoal for m + by (cases "m = 0") + (simp_all add: Sum_any.expand_set Prod_any.expand_set dom_Some) + done +qed + + +end \ No newline at end of file diff --git a/thys/Sumcheck_Protocol/Instantiation_with_Polynomials/Roots_Bounds.thy b/thys/Sumcheck_Protocol/Instantiation_with_Polynomials/Roots_Bounds.thy new file mode 100644 --- /dev/null +++ b/thys/Sumcheck_Protocol/Instantiation_with_Polynomials/Roots_Bounds.thy @@ -0,0 +1,95 @@ +(******************************************************************************* + + Project: Sumcheck Protocol + + Authors: Azucena Garvia Bosshard + Christoph Sprenger, ETH Zurich + Jonathan Bootle, IBM Research Europe + +*******************************************************************************) + +section \Roots Bound for Multivariate Polynomials of Arity at Most One\ + +theory Roots_Bounds + imports + "Polynomials.MPoly_Type_Univariate" + Univariate_Roots_Bound +begin + +text \ +\textbf{NOTE:} if considered to be useful enough, the lemmas in this theory could be moved to +the theory @{theory "Polynomials.MPoly_Type_Univariate"}. +\ + +subsection \Lemmas connecting univariate and multivariate polynomials\ + +subsubsection \Basic lemmas\ + +lemma mpoly_to_poly_zero_iff: + fixes p::"'a::comm_monoid_add mpoly" + assumes \vars p \ {v}\ + shows "mpoly_to_poly v p = 0 \ p = 0" + by (metis assms mpoly_to_poly_inverse poly_to_mpoly0 poly_to_mpoly_inverse) + +lemma keys_monom_subset_vars: + fixes p::"'a::zero mpoly" + assumes \m \ keys (mapping_of p)\ + shows "keys m \ vars p" + using assms + by (auto simp add: vars_def) + +lemma sum_lookup_keys_eq_lookup: + fixes p::"'a::zero mpoly" + assumes \m \ keys (mapping_of p)\ and \vars p \ {v}\ + shows "sum (lookup m) (keys m) = lookup m v" + using assms + by (auto simp add: subset_singleton_iff dest!: keys_monom_subset_vars) + + +subsubsection \Total degree corresponds to degree for polynomials of arity at most one\ + +lemma poly_degree_eq_mpoly_degree: + fixes p::"'a::comm_monoid_add mpoly" + assumes \vars p \ {v}\ + shows "degree (mpoly_to_poly v p) = MPoly_Type.degree p v" + using assms +proof - + have *: "\n. MPoly_Type.coeff p (Poly_Mapping.single v n) \ 0 + \ (\m\keys (mapping_of p). n = lookup m v)" + by (metis (no_types, opaque_lifting) Diff_eq_empty_iff Diff_insert add_0 keys_eq_empty + keys_monom_subset_vars lookup_single_eq remove_key_keys remove_key_sum + singleton_insert_inj_eq' coeff_keys[symmetric] assms) + + have "degree (mpoly_to_poly v p) + = Max (insert 0 {n. MPoly_Type.coeff p (Poly_Mapping.single v n) \ 0})" + by (simp add: poly_degree_eq_Max_non_zero_coeffs) + also have "\ = MPoly_Type.degree p v" + by (simp add: degree.rep_eq image_def *) + finally show ?thesis . +qed + +lemma mpoly_degree_eq_total_degree: + fixes p::"'a::zero mpoly" + assumes \vars p \ {v}\ + shows "MPoly_Type.degree p v = total_degree p" + using assms + by (auto simp add: MPoly_Type.degree_def total_degree_def sum_lookup_keys_eq_lookup) + +corollary poly_degree_eq_total_degree: + fixes p::"'a::comm_monoid_add mpoly" + assumes \vars p \ {v}\ + shows "degree (mpoly_to_poly v p) = total_degree p" + using assms + by (simp add: poly_degree_eq_mpoly_degree mpoly_degree_eq_total_degree) + + +subsection \Roots bound for univariate polynomials of type @{typ "'a mpoly"}\ + +lemma univariate_mpoly_roots_bound: + fixes p::"'a::idom mpoly" + assumes \vars p \ {v}\ \p \ 0\ + shows \card {x. insertion (\v. x) p = 0} \ total_degree p\ + using assms univariate_roots_bound[of "mpoly_to_poly v p", unfolded poly_eq_insertion[OF \vars p \ {v}\]] + by (auto simp add: poly_degree_eq_total_degree mpoly_to_poly_zero_iff) + +end diff --git a/thys/Sumcheck_Protocol/Instantiation_with_Polynomials/Univariate_Roots_Bound.thy b/thys/Sumcheck_Protocol/Instantiation_with_Polynomials/Univariate_Roots_Bound.thy new file mode 100644 --- /dev/null +++ b/thys/Sumcheck_Protocol/Instantiation_with_Polynomials/Univariate_Roots_Bound.thy @@ -0,0 +1,101 @@ +(******************************************************************************* + + Project: Sumcheck Protocol + + Authors: Azucena Garvia Bosshard + Christoph Sprenger, ETH Zurich + Jonathan Bootle, IBM Research Europe + +*******************************************************************************) + +section \Roots Bound for Univariate Polynomials\ + +theory Univariate_Roots_Bound + imports + "HOL-Computational_Algebra.Polynomial" +begin + +text \ +\textbf{NOTE:} if considered to be useful enough, the lemmas in this theory could be moved to +the theory @{theory "HOL-Computational_Algebra.Polynomial"}. +\ + +subsection \Basic lemmas\ + +lemma finite_non_zero_coeffs: \finite {n. poly.coeff p n \ 0}\ + using MOST_coeff_eq_0 eventually_cofinite + by fastforce + +text \Univariate degree in terms of @{term Max}\ + +lemma poly_degree_eq_Max_non_zero_coeffs: + "degree p = Max (insert 0 {n. poly.coeff p n \ 0})" + by (intro le_antisym degree_le) (auto simp add: finite_non_zero_coeffs le_degree) + + +subsection \Univariate roots bound\ + +text \The number of roots of a product of polynomials is bounded by +the sum of the number of roots of each.\ + +lemma card_poly_mult_roots: + fixes p :: "'a::{comm_ring_1,ring_no_zero_divisors} poly" + and q :: "'a::{comm_ring_1,ring_no_zero_divisors} poly" + assumes "p \ 0" and "q \ 0" + shows "card {x. poly p x * poly q x = 0} \ card {x. poly p x = 0} + card {x. poly q x = 0}" +proof - + have "card {x . poly p x * poly q x = 0} \ card ({x . poly p x = 0} \ {x . poly q x = 0})" + by (auto simp add: poly_roots_finite assms intro!: card_mono) + also have "\ \ card {x . poly p x = 0} + card {x . poly q x = 0}" + by(auto simp add: Finite_Set.card_Un_le) + finally show ?thesis . +qed + +text \A univariate polynomial p has at most deg p roots.\ + +lemma univariate_roots_bound: + fixes p :: \'a::idom poly\ + assumes \p \ 0\ + shows \card {x. poly p x = 0} \ degree p\ + using assms +proof (induction "degree p" arbitrary: p rule: nat_less_induct) + case 1 + then show ?case + proof(cases "\r. poly p r = 0") + case True \ \A root exists\ + + \ \Get root r of polynomial and write @{text "p = [:- r, 1:] ^ order r p * q"} for some @{text q}.\ + then obtain r where "poly p r = 0" by(auto) + let ?xr = "[:- r, 1:] ^ order r p" + obtain q where "p = ?xr * q" using order_decomp \p \ 0\ by(auto) + + \ \Useful facts about q and @{term "[:- r, 1:] ^ order r p"}\ + have "q \ 0" using \p = ?xr * q\ \p \ 0\ by(auto) + have "?xr \ 0" by(simp) + have "degree ?xr > 0" using \?xr \ 0\ \p \ 0\ \poly p r = 0\ + by (simp add: degree_power_eq order_root) + have "degree q < degree p" + using \?xr \ 0\ \q \ 0\ \p = ?xr * q\ \degree ?xr > 0\ + degree_mult_eq[where p = "?xr" and q = "q"] + by (simp) + have x_roots: "card {r. poly ?xr r = 0} = 1" using \p \ 0\ \poly p r = 0\ + by(simp add: order_root) + have q_roots: "card {r. poly q r = 0} \ degree q" using \q \ 0\ \degree q < degree p\ 1 + by (simp) + + \ \Final bound\ + have "card {r . poly p r = 0} \ degree p" + using \p = ?xr * q\ \q \ 0\ \?xr \ 0\ \degree q < degree p\ + poly_mult[where p = "?xr" and q = "q"] + card_poly_mult_roots[where p = "?xr" and q = "q"] + x_roots q_roots + by (simp) + then show ?thesis . + next + case False \ \No root exists\ + then show ?thesis by simp + qed +qed + + +end \ No newline at end of file diff --git a/thys/Sumcheck_Protocol/ROOT b/thys/Sumcheck_Protocol/ROOT new file mode 100644 --- /dev/null +++ b/thys/Sumcheck_Protocol/ROOT @@ -0,0 +1,51 @@ +(******************************************************************************* + + Project: Sumcheck Protocol + + Authors: Azucena Garvia Bosshard + Christoph Sprenger, ETH Zurich + Jonathan Bootle, IBM Research Europe + +*******************************************************************************) + +chapter AFP + +(* + Test the entry build using the command: + build -v -o browser_info -o "document=pdf" -o "document_variants=document:outline=/proof,/ML" -D +*) + +session Sumcheck_Protocol (AFP) = "HOL-Probability" + + +description \Formalization of the Sumcheck Protocol\ + +options [timeout = 600] + +sessions + "HOL-Library" + "HOL-Computational_Algebra" + "Polynomials" + +directories + "Generalized_Sumcheck_Protocol" + "Instantiation_with_Polynomials" + +theories + "Generalized_Sumcheck_Protocol/Probability_Tools" + "Generalized_Sumcheck_Protocol/Public_Coin_Proofs" + "Generalized_Sumcheck_Protocol/Substitutions" + "Generalized_Sumcheck_Protocol/Abstract_Multivariate_Polynomials" + "Generalized_Sumcheck_Protocol/Sumcheck_Protocol" + "Generalized_Sumcheck_Protocol/Completeness_Proof" + "Generalized_Sumcheck_Protocol/Soundness_Proof" + "Generalized_Sumcheck_Protocol/Sumcheck_as_Public_Coin_Proof" + "Instantiation_with_Polynomials/Polynomial_Instantiation" + "Instantiation_with_Polynomials/Univariate_Roots_Bound" + "Instantiation_with_Polynomials/Roots_Bounds" + "Instantiation_with_Polynomials/Concrete_Multivariate_Polynomials" + +document_files + "root.tex" "session_graph.tex" + (* "root.bib" *) + + diff --git a/thys/Sumcheck_Protocol/document/root.tex b/thys/Sumcheck_Protocol/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Sumcheck_Protocol/document/root.tex @@ -0,0 +1,70 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Project: Sumcheck Protocol +% +% Authors: Azucena Garvia +% Christoph Sprenger +% Jonathan Bootle +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} + +% additional packages +\usepackage{graphicx} % to display session graph +\usepackage{a4wide} +\usepackage{verbatim} +% have each section start on a fresh page +\renewcommand{\isamarkupsection}[1]{\newpage\section{#1}} + +% this should be the last package used +\usepackage{pdfsetup} + +% for special symbols +\usepackage{amssymb} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + + +\begin{document} + +\title{The Sumcheck Protocol} +\author{Azucena Garvia, Christoph Sprenger and Jonathan Bootle} + +\maketitle + +\begin{abstract} +The sumcheck protocol, first introduced in 1992, is an interactive proof which is a key component of many probabilistic proof systems in computational complexity theory and cryptography, some of which have been deployed. We provide a formally verified security analysis of the sumcheck protocol, following a general and modular approach. + +First, we give a general formalization of public-coin interactive proofs. We then define a \emph{generalized sumcheck protocol} for which we axiomatize the underlying mathematical structure and we establish its soundness and completeness. Finally, we prove that these axioms hold for multivariate polynomials, the original setting of the sumcheck protocol. +% +Our modular analysis will facilitate formal verification of sumcheck instances based on different mathematical structures with little effort, by simply proving that these structures satisfy the axioms. +% +Moreover, the analysis will encourage the development and formal verification of future probabilistic proof systems using the sumcheck protocol as a building block. + +The paper presenting this formalization is to appear at CSF 2024 under the title ``Formal Verification of the Sumcheck Protocol''. +\end{abstract} + + +\tableofcontents + +\newpage + + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +% display the theory dependency graph +\include{session_graph} + +% generated text of all theories +\input{session} + +% optional bibliography +%\bibliographystyle{abbrv} +%\bibliography{root} + +\end{document} diff --git a/thys/Sumcheck_Protocol/document/session_graph.tex b/thys/Sumcheck_Protocol/document/session_graph.tex new file mode 100644 --- /dev/null +++ b/thys/Sumcheck_Protocol/document/session_graph.tex @@ -0,0 +1,18 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Project: Sumcheck Protocol +% +% Authors: Azucena Garvia +% Christoph Sprenger +% Jonathan Bootle +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{figure}[p] + \begin{center} + \includegraphics[scale=.7]{session_graph.pdf} + \caption{Theory dependencies} + \end{center} + \label{fig:theory-dependencies} +\end{figure} +