From f3d10c477e620da69268a964ab23391103a3aeb5 Mon Sep 17 00:00:00 2001 From: Samuel Teuber Date: Mon, 12 Jan 2026 23:19:24 +0100 Subject: [PATCH 1/5] Step 1 for ONNX parser update (unfinished) --- Manifest.toml | 1037 ++++++++++++++++++----- src/Definitions/Definitions.jl | 8 +- src/Definitions/Network.jl | 184 ++-- src/Transformers/Diff_Transformers.jl | 6 - src/Transformers/Single_Transformers.jl | 8 - src/Util.jl | 17 - src/Verifier.jl | 6 +- src/VeryDiff.jl | 1 - 8 files changed, 955 insertions(+), 312 deletions(-) delete mode 100644 src/Util.jl diff --git a/Manifest.toml b/Manifest.toml index 324336c0..1ace84af 100644 --- a/Manifest.toml +++ b/Manifest.toml @@ -1,24 +1,71 @@ # This file is machine-generated - editing it directly is not advised -julia_version = "1.10.1" +julia_version = "1.10.10" manifest_format = "2.0" -project_hash = "6c3e3683d6b3b804f07923e8b2baff8bacba7fd6" +project_hash = "abf3877108b478f6b9583465c99f8b2dffaf0ef6" + +[[deps.AbstractFFTs]] +deps = ["LinearAlgebra"] +git-tree-sha1 = "d92ad398961a3ed262d8bf04a1a2b8340f915fef" +uuid = "621f4979-c628-5d54-868e-fcf4e3e8185c" +version = "1.5.0" +weakdeps = ["ChainRulesCore", "Test"] + + [deps.AbstractFFTs.extensions] + AbstractFFTsChainRulesCoreExt = "ChainRulesCore" + AbstractFFTsTestExt = "Test" [[deps.AbstractTrees]] git-tree-sha1 = "2d9c9a55f9c93e8887ad391fbae72f8ef55e1177" uuid = "1520ce14-60c1-5f80-bbc7-55ef81b5835c" version = "0.4.5" +[[deps.Accessors]] +deps = ["CompositionsBase", "ConstructionBase", "Dates", "InverseFunctions", "MacroTools"] +git-tree-sha1 = "856ecd7cebb68e5fc87abecd2326ad59f0f911f3" +uuid = "7d9f7c33-5ae7-4f3b-8dc6-eff91059b697" +version = "0.1.43" + + [deps.Accessors.extensions] + AxisKeysExt = "AxisKeys" + IntervalSetsExt = "IntervalSets" + LinearAlgebraExt = "LinearAlgebra" + StaticArraysExt = "StaticArrays" + StructArraysExt = "StructArrays" + TestExt = "Test" + UnitfulExt = "Unitful" + + [deps.Accessors.weakdeps] + AxisKeys = "94b1ba4f-4ee9-5380-92f1-94cde586c3c5" + IntervalSets = "8197267c-284f-5f27-9208-e0e47529a953" + LinearAlgebra = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e" + StaticArrays = "90137ffa-7385-5640-81b9-e52037218182" + StructArrays = "09ab397b-f2b6-538f-b94a-2f83cf4a842a" + Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40" + Unitful = "1986cc42-f94f-5a68-af5c-568840ba703d" + [[deps.Adapt]] deps = ["LinearAlgebra", "Requires"] -git-tree-sha1 = "cde29ddf7e5726c9fb511f340244ea3481267608" +git-tree-sha1 = "7e35fca2bdfba44d797c53dfe63a51fabf39bfc0" uuid = "79e6a3ab-5dfb-504d-930d-738a2a938a0e" -version = "3.7.2" -weakdeps = ["StaticArrays"] +version = "4.4.0" +weakdeps = ["SparseArrays", "StaticArrays"] [deps.Adapt.extensions] + AdaptSparseArraysExt = "SparseArrays" AdaptStaticArraysExt = "StaticArrays" +[[deps.AliasTables]] +deps = ["PtrArrays", "Random"] +git-tree-sha1 = "9876e1e164b144ca45e9e3198d0b689cadfed9ff" +uuid = "66dad0bd-aa9a-41b7-9441-69ab47430ed8" +version = "1.1.3" + +[[deps.ArgCheck]] +git-tree-sha1 = "f9e9a66c9b7be1ad7372bbd9b062d9230c30c5ce" +uuid = "dce04be8-c92d-5529-be00-80e4d2c0e197" +version = "2.5.0" + [[deps.ArgParse]] deps = ["Logging", "TextWrap"] git-tree-sha1 = "22cf435ac22956a7b45b0168abbc871176e7eecc" @@ -30,51 +77,100 @@ uuid = "0dad84c5-d112-42e6-8d28-ef12dabb789f" version = "1.1.1" [[deps.ArrayInterface]] -deps = ["ArrayInterfaceCore", "Compat", "IfElse", "LinearAlgebra", "SnoopPrecompile", "Static"] -git-tree-sha1 = "dedc16cbdd1d32bead4617d27572f582216ccf23" +deps = ["Adapt", "LinearAlgebra"] +git-tree-sha1 = "d81ae5489e13bc03567d4fbbb06c546a5e53c857" uuid = "4fba245c-0d91-5ea0-9b3e-6abc04ee57a9" -version = "6.0.25" - -[[deps.ArrayInterfaceCore]] -deps = ["LinearAlgebra", "SnoopPrecompile", "SparseArrays", "SuiteSparse"] -git-tree-sha1 = "e5f08b5689b1aad068e01751889f2f615c7db36d" -uuid = "30b0a656-2188-435a-8636-2ec0e6a096e2" -version = "0.1.29" - -[[deps.ArrayInterfaceOffsetArrays]] -deps = ["ArrayInterface", "OffsetArrays", "Static"] -git-tree-sha1 = "3d1a9a01976971063b3930d1aed1d9c4af0817f8" -uuid = "015c0d05-e682-4f19-8f0a-679ce4c54826" -version = "0.1.7" - -[[deps.ArrayInterfaceStaticArrays]] -deps = ["Adapt", "ArrayInterface", "ArrayInterfaceCore", "ArrayInterfaceStaticArraysCore", "LinearAlgebra", "Static", "StaticArrays"] -git-tree-sha1 = "f12dc65aef03d0a49650b20b2fdaf184928fd886" -uuid = "b0d46f97-bff5-4637-a19a-dd75974142cd" -version = "0.1.5" - -[[deps.ArrayInterfaceStaticArraysCore]] -deps = ["ArrayInterfaceCore", "LinearAlgebra", "StaticArraysCore"] -git-tree-sha1 = "01a9f8e6cfc2bfdd01d333f70b8014a04893103c" -uuid = "dd5226c6-a4d4-4bc7-8575-46859f9c95b9" -version = "0.1.4" +version = "7.22.0" + + [deps.ArrayInterface.extensions] + ArrayInterfaceBandedMatricesExt = "BandedMatrices" + ArrayInterfaceBlockBandedMatricesExt = "BlockBandedMatrices" + ArrayInterfaceCUDAExt = "CUDA" + ArrayInterfaceCUDSSExt = ["CUDSS", "CUDA"] + ArrayInterfaceChainRulesCoreExt = "ChainRulesCore" + ArrayInterfaceChainRulesExt = "ChainRules" + ArrayInterfaceGPUArraysCoreExt = "GPUArraysCore" + ArrayInterfaceMetalExt = "Metal" + ArrayInterfaceReverseDiffExt = "ReverseDiff" + ArrayInterfaceSparseArraysExt = "SparseArrays" + ArrayInterfaceStaticArraysCoreExt = "StaticArraysCore" + ArrayInterfaceTrackerExt = "Tracker" + + [deps.ArrayInterface.weakdeps] + BandedMatrices = "aae01518-5342-5314-be14-df237901396f" + BlockBandedMatrices = "ffab5731-97b5-5995-9138-79e8c1846df0" + CUDA = "052768ef-5323-5732-b1bb-66c8b64840ba" + CUDSS = "45b445bb-4962-46a0-9369-b4df9d0f772e" + ChainRules = "082447d4-558c-5d27-93f4-14fc19e9eca2" + ChainRulesCore = "d360d2e6-b24c-11e9-a2a3-2a2ae2dbcce4" + GPUArraysCore = "46192b85-c4d5-4398-a991-12ede77f4527" + Metal = "dde4c033-4e86-420c-a63e-0dd931031962" + ReverseDiff = "37e2e3b7-166d-5795-8a7a-e32c996b4267" + SparseArrays = "2f01184e-e22b-5df5-ae63-d93ebab69eaf" + StaticArraysCore = "1e83bf80-4336-4d27-bf5d-d5a4f845583c" + Tracker = "9f7883ad-71c0-57eb-9f7f-b5c9e6d3789c" [[deps.Artifacts]] uuid = "56f22d72-fd6d-98f1-02f0-08ddc0907c33" +[[deps.Atomix]] +deps = ["UnsafeAtomics"] +git-tree-sha1 = "29bb0eb6f578a587a49da16564705968667f5fa8" +uuid = "a9b6321e-bd34-4604-b9c9-b65b8de01458" +version = "1.1.2" + + [deps.Atomix.extensions] + AtomixCUDAExt = "CUDA" + AtomixMetalExt = "Metal" + AtomixOpenCLExt = "OpenCL" + AtomixoneAPIExt = "oneAPI" + + [deps.Atomix.weakdeps] + CUDA = "052768ef-5323-5732-b1bb-66c8b64840ba" + Metal = "dde4c033-4e86-420c-a63e-0dd931031962" + OpenCL = "08131aa3-fb12-5dee-8b74-c09406e224a2" + oneAPI = "8f75cd03-7ff8-4ecb-9b8f-daf728133b1b" + +[[deps.BangBang]] +deps = ["Accessors", "ConstructionBase", "InitialValues", "LinearAlgebra"] +git-tree-sha1 = "a49f9342fc60c2a2aaa4e0934f06755464fcf438" +uuid = "198e06fe-97b7-11e9-32a5-e1d131e6ad66" +version = "0.4.6" + + [deps.BangBang.extensions] + BangBangChainRulesCoreExt = "ChainRulesCore" + BangBangDataFramesExt = "DataFrames" + BangBangStaticArraysExt = "StaticArrays" + BangBangStructArraysExt = "StructArrays" + BangBangTablesExt = "Tables" + BangBangTypedTablesExt = "TypedTables" + + [deps.BangBang.weakdeps] + ChainRulesCore = "d360d2e6-b24c-11e9-a2a3-2a2ae2dbcce4" + DataFrames = "a93c6f00-e57d-5684-b7b6-d8193f3e46c0" + StaticArrays = "90137ffa-7385-5640-81b9-e52037218182" + StructArrays = "09ab397b-f2b6-538f-b94a-2f83cf4a842a" + Tables = "bd369af6-aec1-5ad0-b16a-f7cc5008161c" + TypedTables = "9d95f2ec-7b3d-5a63-8d20-e2491e220bb9" + [[deps.Base64]] uuid = "2a0f44e3-6c83-55bd-87e4-b1978d98bd5f" +[[deps.Baselet]] +git-tree-sha1 = "aebf55e6d7795e02ca500a689d326ac979aaf89e" +uuid = "9718e550-a3fa-408a-8086-8db961cd8217" +version = "0.1.1" + [[deps.BenchmarkTools]] -deps = ["JSON", "Logging", "Printf", "Profile", "Statistics", "UUIDs"] -git-tree-sha1 = "f1dff6729bc61f4d49e140da1af55dcd1ac97b2f" +deps = ["Compat", "JSON", "Logging", "Printf", "Profile", "Statistics", "UUIDs"] +git-tree-sha1 = "7fecfb1123b8d0232218e2da0c213004ff15358d" uuid = "6e4b80f9-dd63-53aa-95a3-0cdb28fa8baf" -version = "1.5.0" +version = "1.6.3" [[deps.Bijections]] -git-tree-sha1 = "95f5c7e2d177b7ba1a240b0518038b975d72a8c0" +git-tree-sha1 = "6aaafea90a56dc1fc8cbc15e3cf26d6bc81eb0a3" uuid = "e2ed5e7c-b2de-5872-ae92-c73ca462fb04" -version = "0.1.7" +version = "0.1.10" [[deps.BitTwiddlingConvenienceFunctions]] deps = ["Static"] @@ -83,15 +179,15 @@ uuid = "62783981-4cbd-42fc-bca8-16325de8dc4b" version = "0.1.6" [[deps.BufferedStreams]] -git-tree-sha1 = "4ae47f9a4b1dc19897d3743ff13685925c5202ec" +git-tree-sha1 = "6863c5b7fc997eadcabdbaf6c5f201dc30032643" uuid = "e1450e63-4bb3-523b-b2a4-4ffa8c0fd77d" -version = "1.2.1" +version = "1.2.2" [[deps.Bzip2_jll]] -deps = ["Artifacts", "JLLWrappers", "Libdl", "Pkg"] -git-tree-sha1 = "9e2a6b69137e6969bab0152632dcb3bc108c8bdd" +deps = ["Artifacts", "JLLWrappers", "Libdl"] +git-tree-sha1 = "1b96ea4a01afe0ea4090c5c8039690672dd13f2e" uuid = "6e34b625-4abd-537c-b88f-471c36dfa7a0" -version = "1.0.8+1" +version = "1.0.9+0" [[deps.CEnum]] git-tree-sha1 = "389ad5c84de1ae7cf0e28e381131c98ea87d54fc" @@ -99,55 +195,66 @@ uuid = "fa961155-64e5-5f13-b03f-caf6b980ea82" version = "0.5.0" [[deps.CPUSummary]] -deps = ["CpuId", "IfElse", "PrecompileTools", "Static"] -git-tree-sha1 = "5a97e67919535d6841172016c9530fd69494e5ec" +deps = ["CpuId", "IfElse", "PrecompileTools", "Preferences", "Static"] +git-tree-sha1 = "f3a21d7fc84ba618a779d1ed2fcca2e682865bab" uuid = "2a0fbf3d-bb9c-48f3-b0a9-814d99fd7ab9" -version = "0.2.6" +version = "0.2.7" + +[[deps.ChainRules]] +deps = ["Adapt", "ChainRulesCore", "Compat", "Distributed", "GPUArraysCore", "IrrationalConstants", "LinearAlgebra", "Random", "RealDot", "SparseArrays", "SparseInverseSubset", "Statistics", "StructArrays", "SuiteSparse"] +git-tree-sha1 = "3b704353e517a957323bd3ac70fa7b669b5f48d4" +uuid = "082447d4-558c-5d27-93f4-14fc19e9eca2" +version = "1.72.6" [[deps.ChainRulesCore]] deps = ["Compat", "LinearAlgebra"] -git-tree-sha1 = "71acdbf594aab5bbb2cec89b208c41b4c411e49f" +git-tree-sha1 = "e4c6a16e77171a5f5e25e9646617ab1c276c5607" uuid = "d360d2e6-b24c-11e9-a2a3-2a2ae2dbcce4" -version = "1.24.0" +version = "1.26.0" weakdeps = ["SparseArrays"] [deps.ChainRulesCore.extensions] ChainRulesCoreSparseArraysExt = "SparseArrays" [[deps.CloseOpenIntervals]] -deps = ["ArrayInterface", "Static"] -git-tree-sha1 = "d61300b9895f129f4bd684b2aff97cf319b6c493" +deps = ["Static", "StaticArrayInterface"] +git-tree-sha1 = "05ba0d07cd4fd8b7a39541e31a7b0254704ea581" uuid = "fb6a15b2-703c-40df-9091-08a04967cfa9" -version = "0.1.11" +version = "0.1.13" [[deps.CodecBzip2]] -deps = ["Bzip2_jll", "Libdl", "TranscodingStreams"] -git-tree-sha1 = "9b1ca1aa6ce3f71b3d1840c538a8210a043625eb" +deps = ["Bzip2_jll", "TranscodingStreams"] +git-tree-sha1 = "84990fa864b7f2b4901901ca12736e45ee79068c" uuid = "523fee87-0ab8-5b00-afb7-3ecf72e48cfd" -version = "0.8.2" +version = "0.8.5" [[deps.CodecZlib]] deps = ["TranscodingStreams", "Zlib_jll"] -git-tree-sha1 = "59939d8a997469ee05c4b4944560a820f9ba0d73" +git-tree-sha1 = "962834c22b66e32aa10f7611c08c8ca4e20749a9" uuid = "944b1d66-785c-5afd-91f1-9de20f533193" -version = "0.7.4" +version = "0.7.8" [[deps.Combinatorics]] -git-tree-sha1 = "08c8b6831dc00bfea825826be0bc8336fc369860" +git-tree-sha1 = "c761b00e7755700f9cdf5b02039939d1359330e1" uuid = "861a8166-3701-5b0c-9a16-15d98fcdc6aa" -version = "1.0.2" +version = "1.1.0" [[deps.CommonSubexpressions]] -deps = ["MacroTools", "Test"] -git-tree-sha1 = "7b8a93dba8af7e3b42fecabf646260105ac373f7" +deps = ["MacroTools"] +git-tree-sha1 = "cda2cfaebb4be89c9084adaca7dd7333369715c5" uuid = "bbf7d656-a473-5ed7-a52c-81e309532950" -version = "0.3.0" +version = "0.3.1" + +[[deps.CommonWorldInvalidations]] +git-tree-sha1 = "ae52d1c52048455e85a387fbee9be553ec2b68d0" +uuid = "f70d9fcc-98c5-4d4a-abd7-e4cdeebd8ca8" +version = "1.0.0" [[deps.Compat]] deps = ["TOML", "UUIDs"] -git-tree-sha1 = "b1c55339b7c6c350ee89f2c1604299660525b248" +git-tree-sha1 = "9d8a54ce4b17aa5bdce0ea5c34bc5e7c340d16ad" uuid = "34da2185-b29b-5c13-b0c7-acf172513d20" -version = "4.15.0" +version = "4.18.1" weakdeps = ["Dates", "LinearAlgebra"] [deps.Compat.extensions] @@ -156,13 +263,22 @@ weakdeps = ["Dates", "LinearAlgebra"] [[deps.CompilerSupportLibraries_jll]] deps = ["Artifacts", "Libdl"] uuid = "e66e0078-7015-5450-92f7-15fbd957f2ae" -version = "1.1.0+0" +version = "1.1.1+0" + +[[deps.CompositionsBase]] +git-tree-sha1 = "802bb88cd69dfd1509f6670416bd4434015693ad" +uuid = "a33af91c-f02d-484b-be07-31d278c5ca2b" +version = "0.1.2" +weakdeps = ["InverseFunctions"] + + [deps.CompositionsBase.extensions] + CompositionsBaseInverseFunctionsExt = "InverseFunctions" [[deps.ConstructionBase]] deps = ["LinearAlgebra"] -git-tree-sha1 = "260fd2400ed2dab602a7c15cf10c1933c59930a2" +git-tree-sha1 = "d8a9c0b6ac2d9081bf76324b39c78ca3ce4f0c98" uuid = "187b0558-2788-49d3-abe0-74a17ed4e7c9" -version = "1.5.5" +version = "1.5.6" [deps.ConstructionBase.extensions] ConstructionBaseIntervalSetsExt = "IntervalSets" @@ -172,6 +288,12 @@ version = "1.5.5" IntervalSets = "8197267c-284f-5f27-9208-e0e47529a953" StaticArrays = "90137ffa-7385-5640-81b9-e52037218182" +[[deps.ContextVariablesX]] +deps = ["Compat", "Logging", "UUIDs"] +git-tree-sha1 = "25cc3803f1030ab855e383129dcd3dc294e322cc" +uuid = "6add18c4-b38d-439d-96f6-d6bc489c04c5" +version = "0.1.3" + [[deps.CpuId]] deps = ["Markdown"] git-tree-sha1 = "fcbb72b032692610bfbdb15018ac16a36cf2e406" @@ -185,9 +307,9 @@ version = "1.16.0" [[deps.DataStructures]] deps = ["Compat", "InteractiveUtils", "OrderedCollections"] -git-tree-sha1 = "1d0a14036acb104d9e89698bd408f63ab58cdc82" +git-tree-sha1 = "4e1fe97fdaed23e9dc21d4d664bea76b65fc50a0" uuid = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8" -version = "0.18.20" +version = "0.18.22" [[deps.DataValueInterfaces]] git-tree-sha1 = "bfc1187b79289637fa0ef6d4436ebdfe6905cbd6" @@ -198,6 +320,11 @@ version = "1.0.0" deps = ["Printf"] uuid = "ade2ca70-3891-5945-98fb-dc099432e06a" +[[deps.DefineSingletons]] +git-tree-sha1 = "0fba8b706d0178b4dc7fd44a96a92382c9065c2c" +uuid = "244e2a9f-e319-4986-a169-4d1fe445cd52" +version = "0.1.2" + [[deps.DelimitedFiles]] deps = ["Mmap"] git-tree-sha1 = "9e2f36d3c96a820c678f2f1f1782582fcf685bae" @@ -216,11 +343,14 @@ git-tree-sha1 = "23163d55f885173722d1e4cf0f6110cdbaf7e272" uuid = "b552c78f-8df3-52c6-915a-8e097449b14b" version = "1.15.1" +[[deps.Distributed]] +deps = ["Random", "Serialization", "Sockets"] +uuid = "8ba89e20-285c-5b6f-9357-94700520ee1b" + [[deps.DocStringExtensions]] -deps = ["LibGit2"] -git-tree-sha1 = "2fb1e02f2b635d0845df5d7c167fec4dd739b00d" +git-tree-sha1 = "7442a5dfe1ebb773c29cc2962a8980f47221d76c" uuid = "ffbed154-4ef7-542d-bbb7-c09d3a79fcae" -version = "0.9.3" +version = "0.9.5" [[deps.Downloads]] deps = ["ArgTools", "FileWatching", "LibCURL", "NetworkOptions"] @@ -234,34 +364,94 @@ uuid = "7c1d4256-1411-5781-91ec-d7bc3513ac07" version = "0.4.6" [[deps.EnumX]] -git-tree-sha1 = "bdb1942cd4c45e3c678fd11569d5cccd80976237" +git-tree-sha1 = "bddad79635af6aec424f53ed8aad5d7555dc6f00" uuid = "4e289a0a-7415-4d19-859d-a7e5c4648b56" -version = "1.0.4" +version = "1.0.5" + +[[deps.EnzymeCore]] +git-tree-sha1 = "990991b8aa76d17693a98e3a915ac7aa49f08d1a" +uuid = "f151be2c-9106-41f4-ab19-57ee4f262869" +version = "0.8.18" +weakdeps = ["Adapt", "ChainRulesCore"] + + [deps.EnzymeCore.extensions] + AdaptExt = "Adapt" + EnzymeCoreChainRulesCoreExt = "ChainRulesCore" [[deps.ExprTools]] git-tree-sha1 = "27415f162e6028e81c72b82ef756bf321213b6ec" uuid = "e2ba6199-217a-4e67-a87a-7c52f15ade04" version = "0.1.10" +[[deps.FLoops]] +deps = ["BangBang", "Compat", "FLoopsBase", "InitialValues", "JuliaVariables", "MLStyle", "Serialization", "Setfield", "Transducers"] +git-tree-sha1 = "0a2e5873e9a5f54abb06418d57a8df689336a660" +uuid = "cc61a311-1640-44b5-9fba-1b764f453329" +version = "0.2.2" + +[[deps.FLoopsBase]] +deps = ["ContextVariablesX"] +git-tree-sha1 = "656f7a6859be8673bf1f35da5670246b923964f7" +uuid = "b9860ae5-e623-471e-878b-f6a53c775ea6" +version = "0.1.1" + [[deps.FileWatching]] uuid = "7b1f6079-737a-58dc-b8bc-7a2ca5c1b5ee" [[deps.FillArrays]] -deps = ["LinearAlgebra", "Random", "SparseArrays", "Statistics"] -git-tree-sha1 = "7072f1e3e5a8be51d525d64f63d3ec1287ff2790" +deps = ["LinearAlgebra"] +git-tree-sha1 = "5bfcd42851cf2f1b303f51525a54dc5e98d408a3" uuid = "1a297f60-69ca-5386-bcde-b61e274b549b" -version = "0.13.11" +version = "1.15.0" + + [deps.FillArrays.extensions] + FillArraysPDMatsExt = "PDMats" + FillArraysSparseArraysExt = "SparseArrays" + FillArraysStatisticsExt = "Statistics" + + [deps.FillArrays.weakdeps] + PDMats = "90014a1f-27ba-587c-ab20-58faa44d9150" + SparseArrays = "2f01184e-e22b-5df5-ae63-d93ebab69eaf" + Statistics = "10745b16-79ce-11e8-11f9-7d13ad32a3b2" + +[[deps.Flux]] +deps = ["Adapt", "ChainRulesCore", "Compat", "EnzymeCore", "Functors", "LinearAlgebra", "MLCore", "MLDataDevices", "MLUtils", "MacroTools", "NNlib", "OneHotArrays", "Optimisers", "Preferences", "ProgressLogging", "Random", "Reexport", "Setfield", "SparseArrays", "SpecialFunctions", "Statistics", "Zygote"] +git-tree-sha1 = "efa66783e2ad06bfd4c148cb34648e24c99f7626" +uuid = "587475ba-b771-5e3f-ad9e-33799f191a9c" +version = "0.16.7" + + [deps.Flux.extensions] + FluxAMDGPUExt = "AMDGPU" + FluxCUDAExt = "CUDA" + FluxCUDAcuDNNExt = ["CUDA", "cuDNN"] + FluxEnzymeExt = "Enzyme" + FluxMPIExt = "MPI" + FluxMPINCCLExt = ["CUDA", "MPI", "NCCL"] + + [deps.Flux.weakdeps] + AMDGPU = "21141c5a-9bdb-4563-92ae-f87d6854732e" + CUDA = "052768ef-5323-5732-b1bb-66c8b64840ba" + Enzyme = "7da242da-08ed-463a-9acd-ee780be4f1d9" + MPI = "da04e1cc-30fd-572f-bb4f-1f8673147195" + NCCL = "3fe64909-d7a1-4096-9b7d-7a0f12cf0f6b" + cuDNN = "02a925ec-e4fe-4b08-9a7e-0d78e3d38ccd" [[deps.ForwardDiff]] deps = ["CommonSubexpressions", "DiffResults", "DiffRules", "LinearAlgebra", "LogExpFunctions", "NaNMath", "Preferences", "Printf", "Random", "SpecialFunctions"] -git-tree-sha1 = "cf0fe81336da9fb90944683b8c41984b08793dad" +git-tree-sha1 = "b2977f86ed76484de6f29d5b36f2fa686f085487" uuid = "f6369f11-7733-5829-9624-2563aa707210" -version = "0.10.36" +version = "1.3.1" weakdeps = ["StaticArrays"] [deps.ForwardDiff.extensions] ForwardDiffStaticArraysExt = "StaticArrays" +[[deps.Functors]] +deps = ["Compat", "ConstructionBase", "LinearAlgebra", "Random"] +git-tree-sha1 = "60a0339f28a233601cb74468032b5c302d5067de" +uuid = "d9f16b24-f501-4c13-a1f2-28368ffc5196" +version = "0.5.2" + [[deps.Future]] deps = ["Random"] uuid = "9fa8497b-333b-5362-9e8d-4d0656e87820" @@ -274,37 +464,31 @@ version = "1.2.1" [[deps.GLPK_jll]] deps = ["Artifacts", "GMP_jll", "JLLWrappers", "Libdl", "Pkg"] -git-tree-sha1 = "fe68622f32828aa92275895fdb324a85894a5b1b" +git-tree-sha1 = "6aa6294ba949ccfc380463bf50ff988b46de5bc7" uuid = "e8aa6df9-e6ca-548a-97ff-1f85fc5b8b98" -version = "5.0.1+0" +version = "5.0.1+1" [[deps.GMP_jll]] deps = ["Artifacts", "Libdl"] uuid = "781609d7-10c4-51f6-84f2-b8444358ff6d" version = "6.2.1+6" -[[deps.GPUArrays]] -deps = ["Adapt", "GPUArraysCore", "LLVM", "LinearAlgebra", "Printf", "Random", "Reexport", "Serialization", "Statistics"] -git-tree-sha1 = "2e57b4a4f9cc15e85a24d603256fe08e527f48d1" -uuid = "0c68f7d7-f131-5f86-a1c3-88cf8149b2d7" -version = "8.8.1" - [[deps.GPUArraysCore]] deps = ["Adapt"] -git-tree-sha1 = "2d6ca471a6c7b536127afccfa7564b5b39227fe0" +git-tree-sha1 = "83cf05ab16a73219e5f6bd1bdfa9848fa24ac627" uuid = "46192b85-c4d5-4398-a991-12ede77f4527" -version = "0.1.5" +version = "0.2.0" [[deps.Glob]] -git-tree-sha1 = "97285bbd5230dd766e9ef6749b80fc617126d496" +git-tree-sha1 = "83cb0092e2792b9e3a865b6655e88f5b862607e2" uuid = "c27321d9-0574-5035-807b-f59d2c89b15c" -version = "1.3.1" +version = "1.4.0" [[deps.Gurobi]] deps = ["Gurobi_jll", "Libdl", "MathOptInterface", "PrecompileTools"] -git-tree-sha1 = "ae75fef9ef2f84f03e7bbb288e5fee541a822ec8" +git-tree-sha1 = "7e700e7cec5c72ede0115684c447c1944911be5b" uuid = "2e9cd046-0924-5485-92f1-d5272153d98b" -version = "1.9.0" +version = "1.9.1" [[deps.Gurobi_jll]] deps = ["Artifacts", "JLLWrappers", "Libdl"] @@ -312,25 +496,67 @@ git-tree-sha1 = "ec2817f5a9be1e84ebc0ee8207a4bfd8d22b99a5" uuid = "c018c7e6-a5b0-4aea-8f80-9c1ef9991411" version = "13.0.0" +[[deps.HashArrayMappedTries]] +git-tree-sha1 = "2eaa69a7cab70a52b9687c8bf950a5a93ec895ae" +uuid = "076d061b-32b6-4027-95e0-9a2c6f6d7e74" +version = "0.2.0" + [[deps.HostCPUFeatures]] -deps = ["BitTwiddlingConvenienceFunctions", "IfElse", "Libdl", "Static"] -git-tree-sha1 = "8e070b599339d622e9a081d17230d74a5c473293" +deps = ["BitTwiddlingConvenienceFunctions", "IfElse", "Libdl", "Preferences", "Static"] +git-tree-sha1 = "af9ab7d1f70739a47f03be78771ebda38c3c71bf" uuid = "3e5b6fbb-0976-4d2c-9146-d79de83f2fb0" -version = "0.1.17" +version = "0.1.18" + +[[deps.Hwloc]] +deps = ["CEnum", "Hwloc_jll", "Printf"] +git-tree-sha1 = "6a3d80f31ff87bc94ab22a7b8ec2f263f9a6a583" +uuid = "0e44f5e4-bd66-52a0-8798-143a42290a1d" +version = "3.3.0" +weakdeps = ["AbstractTrees"] + + [deps.Hwloc.extensions] + HwlocTrees = "AbstractTrees" + +[[deps.Hwloc_jll]] +deps = ["Artifacts", "JLLWrappers", "Libdl", "XML2_jll", "Xorg_libpciaccess_jll"] +git-tree-sha1 = "3d468106a05408f9f7b6f161d9e7715159af247b" +uuid = "e33a78d0-f292-5ffc-b300-72abe9b543c8" +version = "2.12.2+0" + +[[deps.IRTools]] +deps = ["InteractiveUtils", "MacroTools"] +git-tree-sha1 = "57e9ce6cf68d0abf5cb6b3b4abf9bedf05c939c0" +uuid = "7869d1d1-7146-5819-86e3-90919afe41df" +version = "0.4.15" [[deps.IfElse]] git-tree-sha1 = "debdd00ffef04665ccbb3e150747a77560e8fad1" uuid = "615f187c-cbe4-4ef1-ba3b-2fcf58d6d173" version = "0.1.1" +[[deps.InitialValues]] +git-tree-sha1 = "4da0f88e9a39111c2fa3add390ab15f3a44f3ca3" +uuid = "22cec73e-a1b8-11e9-2c92-598750a2cf9c" +version = "0.3.1" + [[deps.InteractiveUtils]] deps = ["Markdown"] uuid = "b77e0a4c-d291-57a0-90e8-8db25a27a240" +[[deps.InverseFunctions]] +git-tree-sha1 = "a779299d77cd080bf77b97535acecd73e1c5e5cb" +uuid = "3587e190-3f89-42d0-90ee-14403ec27112" +version = "0.1.17" +weakdeps = ["Dates", "Test"] + + [deps.InverseFunctions.extensions] + InverseFunctionsDatesExt = "Dates" + InverseFunctionsTestExt = "Test" + [[deps.IrrationalConstants]] -git-tree-sha1 = "630b497eafcc20001bba38a4651b327dcfc491d2" +git-tree-sha1 = "b2d91fe939cae05960e760110b328288867b5758" uuid = "92d709cd-6900-40b7-9082-c6be49f344b6" -version = "0.2.2" +version = "0.2.6" [[deps.IteratorInterfaceExtensions]] git-tree-sha1 = "a3f24677c21f5bbe9d2a714f95dcd58337fb2856" @@ -339,21 +565,39 @@ version = "1.0.0" [[deps.JLLWrappers]] deps = ["Artifacts", "Preferences"] -git-tree-sha1 = "7e5d6779a1e09a36db2a7b6cff50942a0a7d0fca" +git-tree-sha1 = "0533e564aae234aff59ab625543145446d8b6ec2" uuid = "692b3bcd-3c85-4b1f-b108-f13ce0eb3210" -version = "1.5.0" +version = "1.7.1" [[deps.JSON]] -deps = ["Dates", "Mmap", "Parsers", "Unicode"] -git-tree-sha1 = "31e996f0a15c7b280ba9f76636b3ff9e2ae58c9a" +deps = ["Dates", "Logging", "Parsers", "PrecompileTools", "StructUtils", "UUIDs", "Unicode"] +git-tree-sha1 = "5b6bb73f555bc753a6153deec3717b8904f5551c" uuid = "682c06a0-de6a-54ab-a142-c8b1cf79cde6" -version = "0.21.4" +version = "1.3.0" + + [deps.JSON.extensions] + JSONArrowExt = ["ArrowTypes"] + + [deps.JSON.weakdeps] + ArrowTypes = "31f734f8-188a-4ce0-8406-c8a06bd891cd" + +[[deps.JSON3]] +deps = ["Dates", "Mmap", "Parsers", "PrecompileTools", "StructTypes", "UUIDs"] +git-tree-sha1 = "411eccfe8aba0814ffa0fdf4860913ed09c34975" +uuid = "0f8b85d8-7281-11e9-16c2-39a750bddbf1" +version = "1.14.3" + + [deps.JSON3.extensions] + JSON3ArrowExt = ["ArrowTypes"] + + [deps.JSON3.weakdeps] + ArrowTypes = "31f734f8-188a-4ce0-8406-c8a06bd891cd" [[deps.JuMP]] deps = ["LinearAlgebra", "MacroTools", "MathOptInterface", "MutableArithmetics", "OrderedCollections", "PrecompileTools", "Printf", "SparseArrays"] -git-tree-sha1 = "7e10a0d8b534f2d8e9f712b33488584254624fb1" +git-tree-sha1 = "b76f23c45d75e27e3e9cbd2ee68d8e39491052d0" uuid = "4076af6c-e467-56ae-b986-b466b2749572" -version = "1.22.2" +version = "1.29.3" [deps.JuMP.extensions] JuMPDimensionalDataExt = "DimensionalData" @@ -361,35 +605,35 @@ version = "1.22.2" [deps.JuMP.weakdeps] DimensionalData = "0703355e-b756-11e9-17c0-8b28908087d0" -[[deps.LLVM]] -deps = ["CEnum", "LLVMExtra_jll", "Libdl", "Preferences", "Printf", "Requires", "Unicode"] -git-tree-sha1 = "839c82932db86740ae729779e610f07a1640be9a" -uuid = "929cbde3-209d-540e-8aea-75f648917ca0" -version = "6.6.3" +[[deps.JuliaVariables]] +deps = ["MLStyle", "NameResolution"] +git-tree-sha1 = "49fb3cb53362ddadb4415e9b73926d6b40709e70" +uuid = "b14d175d-62b4-44ba-8fb7-3064adc8c3ec" +version = "0.2.4" - [deps.LLVM.extensions] - BFloat16sExt = "BFloat16s" +[[deps.KernelAbstractions]] +deps = ["Adapt", "Atomix", "InteractiveUtils", "MacroTools", "PrecompileTools", "Requires", "StaticArrays", "UUIDs"] +git-tree-sha1 = "b5a371fcd1d989d844a4354127365611ae1e305f" +uuid = "63c18a36-062a-441e-b654-da1e3ab1ce7c" +version = "0.9.39" +weakdeps = ["EnzymeCore", "LinearAlgebra", "SparseArrays"] - [deps.LLVM.weakdeps] - BFloat16s = "ab4f0b2a-ad5b-11e8-123f-65d77653426b" - -[[deps.LLVMExtra_jll]] -deps = ["Artifacts", "JLLWrappers", "LazyArtifacts", "Libdl", "TOML"] -git-tree-sha1 = "88b916503aac4fb7f701bb625cd84ca5dd1677bc" -uuid = "dad2f222-ce93-54a1-a47d-0025e8a3acab" -version = "0.0.29+0" + [deps.KernelAbstractions.extensions] + EnzymeExt = "EnzymeCore" + LinearAlgebraExt = "LinearAlgebra" + SparseArraysExt = "SparseArrays" [[deps.LabelledArrays]] -deps = ["ArrayInterfaceCore", "ArrayInterfaceStaticArrays", "ArrayInterfaceStaticArraysCore", "ChainRulesCore", "ForwardDiff", "LinearAlgebra", "MacroTools", "PreallocationTools", "RecursiveArrayTools", "StaticArrays"] -git-tree-sha1 = "0a92979c14dfa71adbf892f0cd073e34b7189197" +deps = ["ArrayInterface", "ChainRulesCore", "ForwardDiff", "LinearAlgebra", "MacroTools", "PreallocationTools", "RecursiveArrayTools", "StaticArrays"] +git-tree-sha1 = "fccbe22c5a5602237870694d08f2040532a04b66" uuid = "2ee39098-c373-598a-b85f-a56591580800" -version = "1.13.0" +version = "1.17.0" [[deps.LayoutPointers]] -deps = ["ArrayInterface", "ArrayInterfaceOffsetArrays", "ArrayInterfaceStaticArrays", "LinearAlgebra", "ManualMemory", "SIMDTypes", "Static"] -git-tree-sha1 = "0ad6f0c51ce004dadc24a28a0dfecfb568e52242" +deps = ["ArrayInterface", "LinearAlgebra", "ManualMemory", "SIMDTypes", "Static", "StaticArrayInterface"] +git-tree-sha1 = "a9eaadb366f5493a5654e843864c13d8b107548c" uuid = "10f19ff3-798f-405d-979b-55457f8fc047" -version = "0.1.13" +version = "0.1.17" [[deps.LazyArtifacts]] deps = ["Artifacts", "Pkg"] @@ -422,15 +666,21 @@ version = "1.11.0+1" [[deps.Libdl]] uuid = "8f399da3-3557-5675-b5ff-fb832c97cbdb" +[[deps.Libiconv_jll]] +deps = ["Artifacts", "JLLWrappers", "Libdl"] +git-tree-sha1 = "be484f5c92fad0bd8acfef35fe017900b0b73809" +uuid = "94ce4f54-9a6c-5748-9c1c-f9c7231a4531" +version = "1.18.0+0" + [[deps.LinearAlgebra]] deps = ["Libdl", "OpenBLAS_jll", "libblastrampoline_jll"] uuid = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e" [[deps.LogExpFunctions]] deps = ["DocStringExtensions", "IrrationalConstants", "LinearAlgebra"] -git-tree-sha1 = "a2d09619db4e765091ee5c6ffe8872849de0feea" +git-tree-sha1 = "13ca9e2586b89836fd20cccf56e57e2b9ae7f38f" uuid = "2ab3a3ac-af41-5b50-aa03-7779005ae688" -version = "0.3.28" +version = "0.3.29" [deps.LogExpFunctions.extensions] LogExpFunctionsChainRulesCoreExt = "ChainRulesCore" @@ -446,26 +696,86 @@ version = "0.3.28" uuid = "56ddb016-857b-54e1-b83d-db4d58db5568" [[deps.LoopVectorization]] -deps = ["ArrayInterface", "ArrayInterfaceCore", "ArrayInterfaceOffsetArrays", "ArrayInterfaceStaticArrays", "CPUSummary", "CloseOpenIntervals", "DocStringExtensions", "HostCPUFeatures", "IfElse", "LayoutPointers", "LinearAlgebra", "OffsetArrays", "PolyesterWeave", "SIMDTypes", "SLEEFPirates", "SnoopPrecompile", "Static", "ThreadingUtilities", "UnPack", "VectorizationBase"] -git-tree-sha1 = "9696a80c21a56b937e3fd89e972f8db5db3186e2" +deps = ["ArrayInterface", "CPUSummary", "CloseOpenIntervals", "DocStringExtensions", "HostCPUFeatures", "IfElse", "LayoutPointers", "LinearAlgebra", "OffsetArrays", "PolyesterWeave", "PrecompileTools", "SIMDTypes", "SLEEFPirates", "Static", "StaticArrayInterface", "ThreadingUtilities", "UnPack", "VectorizationBase"] +git-tree-sha1 = "a9fc7883eb9b5f04f46efb9a540833d1fad974b3" uuid = "bdcacae8-1622-11e9-2a5c-532679323890" -version = "0.12.150" -weakdeps = ["ChainRulesCore", "ForwardDiff", "SpecialFunctions"] +version = "0.12.173" +weakdeps = ["ChainRulesCore", "ForwardDiff", "NNlib", "SpecialFunctions"] [deps.LoopVectorization.extensions] ForwardDiffExt = ["ChainRulesCore", "ForwardDiff"] + ForwardDiffNNlibExt = ["ForwardDiff", "NNlib"] SpecialFunctionsExt = "SpecialFunctions" +[[deps.MLCore]] +deps = ["DataAPI", "SimpleTraits", "Tables"] +git-tree-sha1 = "73907695f35bc7ffd9f11f6c4f2ee8c1302084be" +uuid = "c2834f40-e789-41da-a90e-33b280584a8c" +version = "1.0.0" + +[[deps.MLDataDevices]] +deps = ["Adapt", "Functors", "Preferences", "Random", "SciMLPublic"] +git-tree-sha1 = "8ee5a145845703a46f1ff28ac449bcaef7a0ce14" +uuid = "7e8f7934-dd98-4c1a-8fe8-92b47a384d40" +version = "1.17.1" + + [deps.MLDataDevices.extensions] + AMDGPUExt = "AMDGPU" + CUDAExt = "CUDA" + ChainRulesCoreExt = "ChainRulesCore" + ChainRulesExt = "ChainRules" + ComponentArraysExt = "ComponentArrays" + FillArraysExt = "FillArrays" + GPUArraysSparseArraysExt = ["GPUArrays", "SparseArrays"] + MLUtilsExt = "MLUtils" + MetalExt = ["GPUArrays", "Metal"] + OneHotArraysExt = "OneHotArrays" + OpenCLExt = ["GPUArrays", "OpenCL"] + ReactantExt = "Reactant" + RecursiveArrayToolsExt = "RecursiveArrayTools" + ReverseDiffExt = "ReverseDiff" + SparseArraysExt = "SparseArrays" + TrackerExt = "Tracker" + ZygoteExt = "Zygote" + cuDNNExt = ["CUDA", "cuDNN"] + oneAPIExt = ["GPUArrays", "oneAPI"] + + [deps.MLDataDevices.weakdeps] + AMDGPU = "21141c5a-9bdb-4563-92ae-f87d6854732e" + CUDA = "052768ef-5323-5732-b1bb-66c8b64840ba" + ChainRules = "082447d4-558c-5d27-93f4-14fc19e9eca2" + ChainRulesCore = "d360d2e6-b24c-11e9-a2a3-2a2ae2dbcce4" + ComponentArrays = "b0b7db55-cfe3-40fc-9ded-d10e2dbeff66" + FillArrays = "1a297f60-69ca-5386-bcde-b61e274b549b" + GPUArrays = "0c68f7d7-f131-5f86-a1c3-88cf8149b2d7" + MLUtils = "f1d291b0-491e-4a28-83b9-f70985020b54" + Metal = "dde4c033-4e86-420c-a63e-0dd931031962" + OneHotArrays = "0b1bfda6-eb8a-41d2-88d8-f5af5cad476f" + OpenCL = "08131aa3-fb12-5dee-8b74-c09406e224a2" + Reactant = "3c362404-f566-11ee-1572-e11a4b42c853" + RecursiveArrayTools = "731186ca-8d62-57ce-b412-fbd966d074cd" + ReverseDiff = "37e2e3b7-166d-5795-8a7a-e32c996b4267" + SparseArrays = "2f01184e-e22b-5df5-ae63-d93ebab69eaf" + Tracker = "9f7883ad-71c0-57eb-9f7f-b5c9e6d3789c" + Zygote = "e88e6eb3-aa80-5325-afca-941959d7151f" + cuDNN = "02a925ec-e4fe-4b08-9a7e-0d78e3d38ccd" + oneAPI = "8f75cd03-7ff8-4ecb-9b8f-daf728133b1b" + [[deps.MLStyle]] git-tree-sha1 = "bc38dff0548128765760c79eb7388a4b37fae2c8" uuid = "d8e11817-5142-5d16-987a-aa16d5891078" version = "0.4.17" +[[deps.MLUtils]] +deps = ["ChainRulesCore", "Compat", "DataAPI", "DelimitedFiles", "FLoops", "MLCore", "NNlib", "Random", "ShowCases", "SimpleTraits", "Statistics", "StatsBase", "Tables", "Transducers"] +git-tree-sha1 = "a772d8d1987433538a5c226f79393324b55f7846" +uuid = "f1d291b0-491e-4a28-83b9-f70985020b54" +version = "0.4.8" + [[deps.MacroTools]] -deps = ["Markdown", "Random"] -git-tree-sha1 = "2fa9ee3e63fd3a4f7a9a4f4744a52f4856de82df" +git-tree-sha1 = "1e0228a030642014fe5cfe68c2c0a818f9e3f522" uuid = "1914dd2f-81c6-5fcd-8719-6d5c9610ff09" -version = "0.5.13" +version = "0.5.16" [[deps.ManualMemory]] git-tree-sha1 = "bcaef4fc7a0cfe2cba636d84cda54b5e4e4ca3cd" @@ -477,22 +787,33 @@ deps = ["Base64"] uuid = "d6f4376e-aef5-505a-96c1-9c027394607a" [[deps.MaskedArrays]] -deps = ["Adapt", "ArrayInterface", "GPUArrays"] -git-tree-sha1 = "d694fb741c3ffa113d4d5e80aa9b23a1d1be2936" +git-tree-sha1 = "0221f710bab1510075abac7a2b107fa5465b1aef" uuid = "e3e6debb-e142-42bc-8e83-ba8646d1d252" -version = "0.2.0" +version = "0.1.0" [[deps.MathOptInterface]] -deps = ["BenchmarkTools", "CodecBzip2", "CodecZlib", "DataStructures", "ForwardDiff", "JSON", "LinearAlgebra", "MutableArithmetics", "NaNMath", "OrderedCollections", "PrecompileTools", "Printf", "SparseArrays", "SpecialFunctions", "Test", "Unicode"] -git-tree-sha1 = "91b08d27a27d83cf1e63e50837403e7f53a0fd74" +deps = ["BenchmarkTools", "CodecBzip2", "CodecZlib", "ForwardDiff", "JSON3", "LinearAlgebra", "MutableArithmetics", "NaNMath", "OrderedCollections", "PrecompileTools", "Printf", "SparseArrays", "SpecialFunctions", "Test"] +git-tree-sha1 = "181c2611c7aa6a362fdf937b1e2af55e6691181f" uuid = "b8f27783-ece8-5eb3-8dc8-9495eed66fee" -version = "1.31.0" +version = "1.48.0" [[deps.MbedTLS_jll]] deps = ["Artifacts", "Libdl"] uuid = "c8ffd9c3-330d-5841-b78e-0817d7145fa1" version = "2.28.2+1" +[[deps.MicroCollections]] +deps = ["Accessors", "BangBang", "InitialValues"] +git-tree-sha1 = "44d32db644e84c75dab479f1bc15ee76a1a3618f" +uuid = "128add7d-3638-4c79-886c-908ea0c25c34" +version = "0.2.0" + +[[deps.Missings]] +deps = ["DataAPI"] +git-tree-sha1 = "ec4f7fbeab05d7747bdf98eb74d130a2a2ed298d" +uuid = "e1d29d7a-bbdc-5cf2-9ac0-f12de2c33e28" +version = "1.2.0" + [[deps.Mmap]] uuid = "a63ad114-7e13-5084-954f-fe012c677804" @@ -508,15 +829,47 @@ version = "0.4.7" [[deps.MutableArithmetics]] deps = ["LinearAlgebra", "SparseArrays", "Test"] -git-tree-sha1 = "898c56fbf8bf71afb0c02146ef26f3a454e88873" +git-tree-sha1 = "22df8573f8e7c593ac205455ca088989d0a2c7a0" uuid = "d8a4904e-b15c-11e9-3269-09a3773c0cb0" -version = "1.4.5" +version = "1.6.7" + +[[deps.NNlib]] +deps = ["Adapt", "Atomix", "ChainRulesCore", "GPUArraysCore", "KernelAbstractions", "LinearAlgebra", "Random", "ScopedValues", "Statistics"] +git-tree-sha1 = "09701dc1df4281fa9212b269a69210dfa81ee52a" +uuid = "872c559c-99b0-510c-b3b7-b6c96a88d5cd" +version = "0.9.32" + + [deps.NNlib.extensions] + NNlibAMDGPUExt = "AMDGPU" + NNlibCUDACUDNNExt = ["CUDA", "cuDNN"] + NNlibCUDAExt = "CUDA" + NNlibEnzymeCoreExt = "EnzymeCore" + NNlibFFTWExt = "FFTW" + NNlibForwardDiffExt = "ForwardDiff" + NNlibMetalExt = "Metal" + NNlibSpecialFunctionsExt = "SpecialFunctions" + + [deps.NNlib.weakdeps] + AMDGPU = "21141c5a-9bdb-4563-92ae-f87d6854732e" + CUDA = "052768ef-5323-5732-b1bb-66c8b64840ba" + EnzymeCore = "f151be2c-9106-41f4-ab19-57ee4f262869" + FFTW = "7a1cc6ca-52ef-59f5-83cd-3a7055c09341" + ForwardDiff = "f6369f11-7733-5829-9624-2563aa707210" + Metal = "dde4c033-4e86-420c-a63e-0dd931031962" + SpecialFunctions = "276daf66-3868-5448-9aa4-cd146d93841b" + cuDNN = "02a925ec-e4fe-4b08-9a7e-0d78e3d38ccd" [[deps.NaNMath]] deps = ["OpenLibm_jll"] -git-tree-sha1 = "0877504529a3e5c3343c6f8b4c0381e57e4387e4" +git-tree-sha1 = "9b8215b1ee9e78a293f99797cd31375471b2bcae" uuid = "77ba4419-2d1f-58cd-9bb1-8ffee604a2e3" -version = "1.0.2" +version = "1.1.3" + +[[deps.NameResolution]] +deps = ["PrettyPrint"] +git-tree-sha1 = "1a0fa0e9613f46c9b8c11eee38ebb4f590013c5e" +uuid = "71a1bf82-56d0-4bbc-8a3c-48b961074391" +version = "0.1.5" [[deps.NetworkOptions]] uuid = "ca575930-c2e3-43a9-ace4-1e988b2c1908" @@ -531,6 +884,12 @@ weakdeps = ["Adapt"] [deps.OffsetArrays.extensions] OffsetArraysAdaptExt = "Adapt" +[[deps.OneHotArrays]] +deps = ["Adapt", "ChainRulesCore", "Compat", "GPUArraysCore", "LinearAlgebra", "NNlib"] +git-tree-sha1 = "bfe8e84c71972f77e775f75e6d8048ad3fdbe8bc" +uuid = "0b1bfda6-eb8a-41d2-88d8-f5af5cad476f" +version = "0.2.10" + [[deps.OpenBLAS_jll]] deps = ["Artifacts", "CompilerSupportLibraries_jll", "Libdl"] uuid = "4536629a-c528-5b80-bd46-f80d51c5b363" @@ -539,30 +898,41 @@ version = "0.3.23+4" [[deps.OpenLibm_jll]] deps = ["Artifacts", "Libdl"] uuid = "05823500-19ac-5b8b-9628-191a04bc5112" -version = "0.8.1+2" +version = "0.8.5+0" [[deps.OpenSpecFun_jll]] -deps = ["Artifacts", "CompilerSupportLibraries_jll", "JLLWrappers", "Libdl", "Pkg"] -git-tree-sha1 = "13652491f6856acfd2db29360e1bbcd4565d04f1" +deps = ["Artifacts", "CompilerSupportLibraries_jll", "JLLWrappers", "Libdl"] +git-tree-sha1 = "1346c9208249809840c91b26703912dff463d335" uuid = "efe28fd5-8261-553b-a9e1-b2916fc3738e" -version = "0.5.5+0" +version = "0.5.6+0" + +[[deps.Optimisers]] +deps = ["ChainRulesCore", "Functors", "LinearAlgebra", "Random", "Statistics"] +git-tree-sha1 = "53ff746a3a2b232a37dbcd262ac8bbb2b18202b8" +uuid = "3bd65402-5787-11e9-1adc-39752487f4e2" +version = "0.4.4" +weakdeps = ["Adapt", "EnzymeCore"] + + [deps.Optimisers.extensions] + OptimisersAdaptExt = ["Adapt"] + OptimisersEnzymeCoreExt = "EnzymeCore" [[deps.OrderedCollections]] -git-tree-sha1 = "dfdf5519f235516220579f949664f1bf44e741c5" +git-tree-sha1 = "05868e21324cede2207c6f0f466b4bfef6d5e7ee" uuid = "bac558e1-5e72-5ebc-8fee-abe8a469f55d" -version = "1.6.3" +version = "1.8.1" [[deps.PackageCompiler]] deps = ["Artifacts", "Glob", "LazyArtifacts", "Libdl", "Pkg", "Printf", "RelocatableFolders", "TOML", "UUIDs", "p7zip_jll"] -git-tree-sha1 = "5d13e5b70011762b74f86fc08385303589f80272" +git-tree-sha1 = "92a5702bc1b7f2c0d3a395d5553fa8ec7342ce09" uuid = "9b87118b-4619-50d2-8e1e-99f35a4d4d9d" -version = "2.2.0" +version = "2.2.4" [[deps.Parsers]] deps = ["Dates", "PrecompileTools", "UUIDs"] -git-tree-sha1 = "8489905bcdbcfac64d1daa51ca07c0d8f0283821" +git-tree-sha1 = "7d2f8f21da5db6a806faf7b9b292296da42b2810" uuid = "69de0a69-1ddd-5017-9359-2bf0b02dc9f0" -version = "2.8.1" +version = "2.8.3" [[deps.Pkg]] deps = ["Artifacts", "Dates", "Downloads", "FileWatching", "LibGit2", "Libdl", "Logging", "Markdown", "Printf", "REPL", "Random", "SHA", "Serialization", "TOML", "Tar", "UUIDs", "p7zip_jll"] @@ -576,16 +946,20 @@ uuid = "1d0040c9-8b98-4ee7-8388-3f51789ca0ad" version = "0.2.2" [[deps.PreallocationTools]] -deps = ["Adapt", "ArrayInterfaceCore", "ForwardDiff", "Requires"] -git-tree-sha1 = "2c7658dd593e3adc118b00429e1048829f1abb8c" +deps = ["Adapt", "ArrayInterface", "PrecompileTools"] +git-tree-sha1 = "c05b4c6325262152483a1ecb6c69846d2e01727b" uuid = "d236fae5-4411-538c-8e31-a6e3d9e00b46" -version = "0.4.11" +version = "0.4.34" [deps.PreallocationTools.extensions] + PreallocationToolsForwardDiffExt = "ForwardDiff" PreallocationToolsReverseDiffExt = "ReverseDiff" + PreallocationToolsSparseConnectivityTracerExt = "SparseConnectivityTracer" [deps.PreallocationTools.weakdeps] + ForwardDiff = "f6369f11-7733-5829-9624-2563aa707210" ReverseDiff = "37e2e3b7-166d-5795-8a7a-e32c996b4267" + SparseConnectivityTracer = "9f842d2f-2579-4b1d-911e-f412cf18a3f5" [[deps.PrecompileTools]] deps = ["Preferences"] @@ -595,9 +969,14 @@ version = "1.2.1" [[deps.Preferences]] deps = ["TOML"] -git-tree-sha1 = "9306f6085165d270f7e3db02af26a400d580f5c6" +git-tree-sha1 = "522f093a29b31a93e34eaea17ba055d850edea28" uuid = "21216c6a-2e73-6563-6e65-726566657250" -version = "1.4.3" +version = "1.5.1" + +[[deps.PrettyPrint]] +git-tree-sha1 = "632eb4abab3449ab30c5e1afaa874f0b98b586e4" +uuid = "8162dcfd-2161-5ef2-ae6c-7681170c5f98" +version = "0.2.0" [[deps.Printf]] deps = ["Unicode"] @@ -607,11 +986,22 @@ uuid = "de0858da-6303-5e67-8744-51eddeeeb8d7" deps = ["Printf"] uuid = "9abbd945-dff8-562f-b5e8-e1ebf5ef1b79" +[[deps.ProgressLogging]] +deps = ["Logging", "SHA", "UUIDs"] +git-tree-sha1 = "f0803bc1171e455a04124affa9c21bba5ac4db32" +uuid = "33c8b6b6-d38a-422a-b730-caa89a2f386c" +version = "0.1.6" + [[deps.ProtoBuf]] -deps = ["BufferedStreams", "Dates", "EnumX", "TOML", "TranscodingStreams"] -git-tree-sha1 = "f2bfddd629ba7a53ed789d6427d64e0e4c378ef8" +deps = ["BufferedStreams", "Dates", "EnumX", "TOML"] +git-tree-sha1 = "eabdb811dbacadc9d7e0dee9ac11c1a12705e12a" uuid = "3349acd9-ac6a-5e09-bcdb-63829b23a429" -version = "1.0.15" +version = "1.2.0" + +[[deps.PtrArrays]] +git-tree-sha1 = "1d36ef11a9aaf1e8b74dacc6a731dd1de8fd493d" +uuid = "43287f4e-b6f4-7ad1-bb20-aadabca52c3d" +version = "1.3.0" [[deps.REPL]] deps = ["InteractiveUtils", "Markdown", "Sockets", "Unicode"] @@ -621,6 +1011,12 @@ uuid = "3fa0cd96-eef1-5676-8a61-b3b8758bbffb" deps = ["SHA"] uuid = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c" +[[deps.RealDot]] +deps = ["LinearAlgebra"] +git-tree-sha1 = "9f0a1b71baaf7650f4fa8a1d168c7fb6ee41f0c9" +uuid = "c1ae055f-0cd5-4b69-90a6-9a35b1a98df9" +version = "0.1.0" + [[deps.RecipesBase]] deps = ["PrecompileTools"] git-tree-sha1 = "5c3d09cc4f31f5fc6af001c250bf1278733100ff" @@ -628,16 +1024,38 @@ uuid = "3cdcf5f2-1ef4-517c-9805-6587b60abb01" version = "1.3.4" [[deps.RecursiveArrayTools]] -deps = ["Adapt", "ArrayInterfaceCore", "ArrayInterfaceStaticArraysCore", "ChainRulesCore", "DocStringExtensions", "FillArrays", "GPUArraysCore", "IteratorInterfaceExtensions", "LinearAlgebra", "RecipesBase", "Requires", "StaticArraysCore", "Statistics", "SymbolicIndexingInterface", "Tables", "ZygoteRules"] -git-tree-sha1 = "54e055256bbd41fd10566880bc4baa5316bca6fe" +deps = ["Adapt", "ArrayInterface", "DocStringExtensions", "GPUArraysCore", "LinearAlgebra", "PrecompileTools", "RecipesBase", "StaticArraysCore", "SymbolicIndexingInterface"] +git-tree-sha1 = "31b3d7b7e14faad39583475b89aadbd9c3e7ef8b" uuid = "731186ca-8d62-57ce-b412-fbd966d074cd" -version = "2.37.0" +version = "3.44.0" [deps.RecursiveArrayTools.extensions] + RecursiveArrayToolsFastBroadcastExt = "FastBroadcast" + RecursiveArrayToolsForwardDiffExt = "ForwardDiff" + RecursiveArrayToolsKernelAbstractionsExt = "KernelAbstractions" + RecursiveArrayToolsMeasurementsExt = "Measurements" + RecursiveArrayToolsMonteCarloMeasurementsExt = "MonteCarloMeasurements" + RecursiveArrayToolsReverseDiffExt = ["ReverseDiff", "Zygote"] + RecursiveArrayToolsSparseArraysExt = ["SparseArrays"] + RecursiveArrayToolsStatisticsExt = "Statistics" + RecursiveArrayToolsStructArraysExt = "StructArrays" + RecursiveArrayToolsTablesExt = ["Tables"] RecursiveArrayToolsTrackerExt = "Tracker" + RecursiveArrayToolsZygoteExt = "Zygote" [deps.RecursiveArrayTools.weakdeps] + FastBroadcast = "7034ab61-46d4-4ed7-9d0f-46aef9175898" + ForwardDiff = "f6369f11-7733-5829-9624-2563aa707210" + KernelAbstractions = "63c18a36-062a-441e-b654-da1e3ab1ce7c" + Measurements = "eff96d63-e80a-5855-80a2-b1b0885c5ab7" + MonteCarloMeasurements = "0987c9cc-fe09-11e8-30f0-b96dd679fdca" + ReverseDiff = "37e2e3b7-166d-5795-8a7a-e32c996b4267" + SparseArrays = "2f01184e-e22b-5df5-ae63-d93ebab69eaf" + Statistics = "10745b16-79ce-11e8-11f9-7d13ad32a3b2" + StructArrays = "09ab397b-f2b6-538f-b94a-2f83cf4a842a" + Tables = "bd369af6-aec1-5ad0-b16a-f7cc5008161c" Tracker = "9f7883ad-71c0-57eb-9f7f-b5c9e6d3789c" + Zygote = "e88e6eb3-aa80-5325-afca-941959d7151f" [[deps.Reexport]] git-tree-sha1 = "45e428421666073eab6f2da5c9d310d99bb12f9b" @@ -652,9 +1070,15 @@ version = "1.0.1" [[deps.Requires]] deps = ["UUIDs"] -git-tree-sha1 = "838a3a4188e2ded87a4f9f184b4b0d78a1e91cb7" +git-tree-sha1 = "62389eeff14780bfe55195b7204c0d8738436d64" uuid = "ae029012-a4dd-5104-9daa-d747884805df" -version = "1.3.0" +version = "1.3.1" + +[[deps.RuntimeGeneratedFunctions]] +deps = ["ExprTools", "SHA", "Serialization"] +git-tree-sha1 = "2f609ec2295c452685d3142bc4df202686e555d2" +uuid = "7e49a35a-f44a-4d26-94aa-eba1b4ca6b47" +version = "0.5.16" [[deps.SHA]] uuid = "ea8e919c-243c-51af-8825-aaa63cd721ce" @@ -671,61 +1095,106 @@ git-tree-sha1 = "456f610ca2fbd1c14f5fcf31c6bfadc55e7d66e0" uuid = "476501e8-09a2-5ece-8869-fb82de89a1fa" version = "0.6.43" +[[deps.SciMLPublic]] +git-tree-sha1 = "0ba076dbdce87ba230fff48ca9bca62e1f345c9b" +uuid = "431bcebd-1456-4ced-9d72-93c2757fff0b" +version = "1.0.1" + +[[deps.ScopedValues]] +deps = ["HashArrayMappedTries", "Logging"] +git-tree-sha1 = "c3b2323466378a2ba15bea4b2f73b081e022f473" +uuid = "7e506255-f358-4e82-b7e4-beb19740aa63" +version = "1.5.0" + [[deps.Scratch]] deps = ["Dates"] -git-tree-sha1 = "3bac05bc7e74a75fd9cba4295cde4045d9fe2386" +git-tree-sha1 = "9b81b8393e50b7d4e6d0a9f14e192294d3b7c109" uuid = "6c6a2e73-6563-6170-7368-637461726353" -version = "1.2.1" +version = "1.3.0" [[deps.Serialization]] uuid = "9e88b42a-f829-5b0c-bbe9-9e923198166b" [[deps.Setfield]] deps = ["ConstructionBase", "Future", "MacroTools", "StaticArraysCore"] -git-tree-sha1 = "e2cc6d8c88613c05e1defb55170bf5ff211fbeac" +git-tree-sha1 = "c5391c6ace3bc430ca630251d02ea9687169ca68" uuid = "efcf1570-3423-57d1-acb7-fd33fddbac46" -version = "1.1.1" +version = "1.1.2" -[[deps.SnoopPrecompile]] -deps = ["Preferences"] -git-tree-sha1 = "e760a70afdcd461cf01a575947738d359234665c" -uuid = "66db9d55-30c0-4569-8b51-7e840670fc0c" -version = "1.0.3" +[[deps.ShowCases]] +git-tree-sha1 = "7f534ad62ab2bd48591bdeac81994ea8c445e4a5" +uuid = "605ecd9f-84a6-4c9e-81e2-4798472b76a3" +version = "0.1.0" + +[[deps.SimpleTraits]] +deps = ["InteractiveUtils", "MacroTools"] +git-tree-sha1 = "be8eeac05ec97d379347584fa9fe2f5f76795bcb" +uuid = "699a6c99-e7fa-54fc-8d76-47d257e15c1d" +version = "0.9.5" [[deps.Sockets]] uuid = "6462fe0b-24de-5631-8697-dd941f90decc" +[[deps.SortingAlgorithms]] +deps = ["DataStructures"] +git-tree-sha1 = "64d974c2e6fdf07f8155b5b2ca2ffa9069b608d9" +uuid = "a2af1166-a08f-5f64-846c-94a0d3cef48c" +version = "1.2.2" + [[deps.SparseArrays]] deps = ["Libdl", "LinearAlgebra", "Random", "Serialization", "SuiteSparse_jll"] uuid = "2f01184e-e22b-5df5-ae63-d93ebab69eaf" version = "1.10.0" +[[deps.SparseInverseSubset]] +deps = ["LinearAlgebra", "SparseArrays", "SuiteSparse"] +git-tree-sha1 = "52962839426b75b3021296f7df242e40ecfc0852" +uuid = "dc90abb0-5640-4711-901d-7e5b23a2fada" +version = "0.1.2" + [[deps.SpecialFunctions]] deps = ["IrrationalConstants", "LogExpFunctions", "OpenLibm_jll", "OpenSpecFun_jll"] -git-tree-sha1 = "2f5d4697f21388cbe1ff299430dd169ef97d7e14" +git-tree-sha1 = "f2685b435df2613e25fc10ad8c26dddb8640f547" uuid = "276daf66-3868-5448-9aa4-cd146d93841b" -version = "2.4.0" +version = "2.6.1" weakdeps = ["ChainRulesCore"] [deps.SpecialFunctions.extensions] SpecialFunctionsChainRulesCoreExt = "ChainRulesCore" +[[deps.SplittablesBase]] +deps = ["Setfield", "Test"] +git-tree-sha1 = "e08a62abc517eb79667d0a29dc08a3b589516bb5" +uuid = "171d559e-b47b-412a-8079-5efa626c420e" +version = "0.1.15" + [[deps.StableTasks]] -git-tree-sha1 = "073d5c20d44129b20fe954720b97069579fa403b" +git-tree-sha1 = "c4f6610f85cb965bee5bfafa64cbeeda55a4e0b2" uuid = "91464d47-22a1-43fe-8b7f-2d57ee82463f" -version = "0.1.5" +version = "0.1.7" [[deps.Static]] -deps = ["IfElse"] -git-tree-sha1 = "d2fdac9ff3906e27f7a618d47b676941baa6c80c" +deps = ["CommonWorldInvalidations", "IfElse", "PrecompileTools", "SciMLPublic"] +git-tree-sha1 = "49440414711eddc7227724ae6e570c7d5559a086" uuid = "aedffcd0-7271-4cad-89d0-dc628f76c6d3" -version = "0.8.10" +version = "1.3.1" + +[[deps.StaticArrayInterface]] +deps = ["ArrayInterface", "Compat", "IfElse", "LinearAlgebra", "PrecompileTools", "Static"] +git-tree-sha1 = "96381d50f1ce85f2663584c8e886a6ca97e60554" +uuid = "0d7ed370-da01-4f52-bd93-41d350b8b718" +version = "1.8.0" +weakdeps = ["OffsetArrays", "StaticArrays"] + + [deps.StaticArrayInterface.extensions] + StaticArrayInterfaceOffsetArraysExt = "OffsetArrays" + StaticArrayInterfaceStaticArraysExt = "StaticArrays" [[deps.StaticArrays]] deps = ["LinearAlgebra", "PrecompileTools", "Random", "StaticArraysCore"] -git-tree-sha1 = "6e00379a24597be4ae1ee6b2d882e15392040132" +git-tree-sha1 = "eee1b9ad8b29ef0d936e3ec9838c7ec089620308" uuid = "90137ffa-7385-5640-81b9-e52037218182" -version = "1.9.5" +version = "1.9.16" weakdeps = ["ChainRulesCore", "Statistics"] [deps.StaticArrays.extensions] @@ -733,15 +1202,61 @@ weakdeps = ["ChainRulesCore", "Statistics"] StaticArraysStatisticsExt = "Statistics" [[deps.StaticArraysCore]] -git-tree-sha1 = "192954ef1208c7019899fbf8049e717f92959682" +git-tree-sha1 = "6ab403037779dae8c514bad259f32a447262455a" uuid = "1e83bf80-4336-4d27-bf5d-d5a4f845583c" -version = "1.4.3" +version = "1.4.4" [[deps.Statistics]] deps = ["LinearAlgebra", "SparseArrays"] uuid = "10745b16-79ce-11e8-11f9-7d13ad32a3b2" version = "1.10.0" +[[deps.StatsAPI]] +deps = ["LinearAlgebra"] +git-tree-sha1 = "178ed29fd5b2a2cfc3bd31c13375ae925623ff36" +uuid = "82ae8749-77ed-4fe6-ae5f-f523153014b0" +version = "1.8.0" + +[[deps.StatsBase]] +deps = ["AliasTables", "DataAPI", "DataStructures", "LinearAlgebra", "LogExpFunctions", "Missings", "Printf", "Random", "SortingAlgorithms", "SparseArrays", "Statistics", "StatsAPI"] +git-tree-sha1 = "be5733d4a2b03341bdcab91cea6caa7e31ced14b" +uuid = "2913bbd2-ae8a-5f71-8c99-4fb6c76f3a91" +version = "0.34.9" + +[[deps.StructArrays]] +deps = ["ConstructionBase", "DataAPI", "Tables"] +git-tree-sha1 = "a2c37d815bf00575332b7bd0389f771cb7987214" +uuid = "09ab397b-f2b6-538f-b94a-2f83cf4a842a" +version = "0.7.2" +weakdeps = ["Adapt", "GPUArraysCore", "KernelAbstractions", "LinearAlgebra", "SparseArrays", "StaticArrays"] + + [deps.StructArrays.extensions] + StructArraysAdaptExt = "Adapt" + StructArraysGPUArraysCoreExt = ["GPUArraysCore", "KernelAbstractions"] + StructArraysLinearAlgebraExt = "LinearAlgebra" + StructArraysSparseArraysExt = "SparseArrays" + StructArraysStaticArraysExt = "StaticArrays" + +[[deps.StructTypes]] +deps = ["Dates", "UUIDs"] +git-tree-sha1 = "159331b30e94d7b11379037feeb9b690950cace8" +uuid = "856f2bd8-1eba-4b0a-8007-ebc267875bd4" +version = "1.11.0" + +[[deps.StructUtils]] +deps = ["Dates", "UUIDs"] +git-tree-sha1 = "b0290a55d9e047841d7f5c472edbdc39c72cd0ce" +uuid = "ec057cc2-7a8d-4b58-b3b3-92acb9f63b42" +version = "2.6.1" + + [deps.StructUtils.extensions] + StructUtilsMeasurementsExt = ["Measurements"] + StructUtilsTablesExt = ["Tables"] + + [deps.StructUtils.weakdeps] + Measurements = "eff96d63-e80a-5855-80a2-b1b0885c5ab7" + Tables = "bd369af6-aec1-5ad0-b16a-f7cc5008161c" + [[deps.SuiteSparse]] deps = ["Libdl", "LinearAlgebra", "Serialization", "SparseArrays"] uuid = "4607b0f0-06f3-5cda-b6b1-a6196a1729e9" @@ -752,10 +1267,16 @@ uuid = "bea87d4a-7f5b-5778-9afe-8cc45184846c" version = "7.2.1+1" [[deps.SymbolicIndexingInterface]] -deps = ["DocStringExtensions"] -git-tree-sha1 = "f8ab052bfcbdb9b48fad2c80c873aa0d0344dfe5" +deps = ["Accessors", "ArrayInterface", "RuntimeGeneratedFunctions", "StaticArraysCore"] +git-tree-sha1 = "94c58884e013efff548002e8dc2fdd1cb74dfce5" uuid = "2efcf032-c050-4f8e-a9bb-153293bab1f5" -version = "0.2.2" +version = "0.3.46" + + [deps.SymbolicIndexingInterface.extensions] + SymbolicIndexingInterfacePrettyTablesExt = "PrettyTables" + + [deps.SymbolicIndexingInterface.weakdeps] + PrettyTables = "08abe8d2-0d0c-5749-adfa-8a2ac140af0d" [[deps.SymbolicUtils]] deps = ["AbstractTrees", "Bijections", "ChainRulesCore", "Combinatorics", "ConstructionBase", "DataStructures", "DocStringExtensions", "DynamicPolynomials", "IfElse", "LabelledArrays", "LinearAlgebra", "MultivariatePolynomials", "NaNMath", "Setfield", "SparseArrays", "SpecialFunctions", "StaticArrays", "TimerOutputs", "Unityper"] @@ -764,6 +1285,12 @@ pinned = true uuid = "d1185830-fcd6-423d-90d6-eec64667417b" version = "1.1.0" +[[deps.SysInfo]] +deps = ["Dates", "DelimitedFiles", "Hwloc", "PrecompileTools", "Random", "Serialization"] +git-tree-sha1 = "7aaebfbf5b3a39268f4a0caaa43e878e1138d25c" +uuid = "90a7ee08-a23f-48b9-9006-0e0e2a9e4608" +version = "0.3.0" + [[deps.TOML]] deps = ["Dates"] uuid = "fa267f1f-6049-4f14-aa54-33bafae1ed76" @@ -776,16 +1303,21 @@ uuid = "3783bdb8-4a98-5b6b-af9a-565f29a5fe9c" version = "1.0.1" [[deps.Tables]] -deps = ["DataAPI", "DataValueInterfaces", "IteratorInterfaceExtensions", "LinearAlgebra", "OrderedCollections", "TableTraits"] -git-tree-sha1 = "cb76cf677714c095e535e3501ac7954732aeea2d" +deps = ["DataAPI", "DataValueInterfaces", "IteratorInterfaceExtensions", "OrderedCollections", "TableTraits"] +git-tree-sha1 = "f2c1efbc8f3a609aadf318094f8fc5204bdaf344" uuid = "bd369af6-aec1-5ad0-b16a-f7cc5008161c" -version = "1.11.1" +version = "1.12.1" [[deps.Tar]] deps = ["ArgTools", "SHA"] uuid = "a4e569a6-e804-4fa4-b0f3-eef7a1d5b13e" version = "1.10.0" +[[deps.TermInterface]] +git-tree-sha1 = "d673e0aca9e46a2f63720201f55cc7b3e7169b16" +uuid = "8ea1fca8-c5ef-4a55-8b96-4e9afe9c9a3c" +version = "2.0.0" + [[deps.Test]] deps = ["InteractiveUtils", "Logging", "Random", "Serialization"] uuid = "8dfed614-e22c-5e08-85e1-65c5234f0b40" @@ -796,10 +1328,24 @@ uuid = "b718987f-49a8-5099-9789-dcd902bef87d" version = "1.0.2" [[deps.ThreadPinning]] -deps = ["DelimitedFiles", "DocStringExtensions", "Libdl", "LinearAlgebra", "PrecompileTools", "Preferences", "Random", "StableTasks"] -git-tree-sha1 = "333748c6fa62868fa039f00ba670d619776a6752" +deps = ["DelimitedFiles", "Libdl", "LinearAlgebra", "PrecompileTools", "Preferences", "Random", "StableTasks", "SysInfo", "ThreadPinningCore"] +git-tree-sha1 = "d47dbc7862f69ce1973fff227237275ff4a10781" uuid = "811555cd-349b-4f26-b7bc-1f208b848042" -version = "0.7.22" +version = "1.0.2" + + [deps.ThreadPinning.extensions] + DistributedExt = "Distributed" + MPIExt = "MPI" + + [deps.ThreadPinning.weakdeps] + Distributed = "8ba89e20-285c-5b6f-9357-94700520ee1b" + MPI = "da04e1cc-30fd-572f-bb4f-1f8673147195" + +[[deps.ThreadPinningCore]] +deps = ["LinearAlgebra", "PrecompileTools", "StableTasks"] +git-tree-sha1 = "bb3c6f3b5600fbff028c43348365681b34d06499" +uuid = "6f48bc29-05ce-4cc8-baad-4adcba581a18" +version = "0.4.5" [[deps.ThreadingUtilities]] deps = ["ManualMemory"] @@ -809,9 +1355,15 @@ version = "0.5.5" [[deps.TimerOutputs]] deps = ["ExprTools", "Printf"] -git-tree-sha1 = "5a13ae8a41237cff5ecf34f73eb1b8f42fff6531" +git-tree-sha1 = "3748bd928e68c7c346b52125cf41fff0de6937d0" uuid = "a759f4b9-e2f1-59dc-863e-4aeb61b1ea8f" -version = "0.5.24" +version = "0.5.29" + + [deps.TimerOutputs.extensions] + FlameGraphsExt = "FlameGraphs" + + [deps.TimerOutputs.weakdeps] + FlameGraphs = "08572546-2f56-4bcf-ba4e-bab62c3a3f89" [[deps.Tokenize]] git-tree-sha1 = "468b4685af4abe0e9fd4d7bf495a6554a6276e75" @@ -819,13 +1371,31 @@ uuid = "0796e94c-ce3b-5d07-9a54-7f471281c624" version = "0.5.29" [[deps.TranscodingStreams]] -git-tree-sha1 = "d73336d81cafdc277ff45558bb7eaa2b04a8e472" +git-tree-sha1 = "0c45878dcfdcfa8480052b6ab162cdd138781742" uuid = "3bb67fe8-82b1-5028-8e26-92a6c54297fa" -version = "0.10.10" -weakdeps = ["Random", "Test"] - - [deps.TranscodingStreams.extensions] - TestExt = ["Test", "Random"] +version = "0.11.3" + +[[deps.Transducers]] +deps = ["Accessors", "ArgCheck", "BangBang", "Baselet", "CompositionsBase", "ConstructionBase", "DefineSingletons", "Distributed", "InitialValues", "Logging", "Markdown", "MicroCollections", "SplittablesBase", "Tables"] +git-tree-sha1 = "4aa1fdf6c1da74661f6f5d3edfd96648321dade9" +uuid = "28d57a85-8fef-5791-bfe6-a80928e7c999" +version = "0.4.85" + + [deps.Transducers.extensions] + TransducersAdaptExt = "Adapt" + TransducersBlockArraysExt = "BlockArrays" + TransducersDataFramesExt = "DataFrames" + TransducersLazyArraysExt = "LazyArrays" + TransducersOnlineStatsBaseExt = "OnlineStatsBase" + TransducersReferenceablesExt = "Referenceables" + + [deps.Transducers.weakdeps] + Adapt = "79e6a3ab-5dfb-504d-930d-738a2a938a0e" + BlockArrays = "8e7c35d0-a365-5155-bbbb-fb81a777f24e" + DataFrames = "a93c6f00-e57d-5684-b7b6-d8193f3e46c0" + LazyArrays = "5078a376-72f3-5289-bfd5-ec5146d43c02" + OnlineStatsBase = "925886fa-5bf2-5e8e-b522-a9147a512338" + Referenceables = "42d2dcc6-99eb-4e98-b66c-637b7d73030e" [[deps.UUIDs]] deps = ["Random", "SHA"] @@ -845,35 +1415,76 @@ git-tree-sha1 = "25008b734a03736c41e2a7dc314ecb95bd6bbdb0" uuid = "a7c27f48-0311-42f6-a7f8-2c11e75eb415" version = "0.1.6" +[[deps.UnsafeAtomics]] +git-tree-sha1 = "b13c4edda90890e5b04ba24e20a310fbe6f249ff" +uuid = "013be700-e6cd-48c3-b4a1-df204f14c38f" +version = "0.3.0" + + [deps.UnsafeAtomics.extensions] + UnsafeAtomicsLLVM = ["LLVM"] + + [deps.UnsafeAtomics.weakdeps] + LLVM = "929cbde3-209d-540e-8aea-75f648917ca0" + [[deps.VNNLib]] -deps = ["LinearAlgebra", "MLStyle", "Mmap", "ProtoBuf", "SymbolicUtils", "Tokenize"] -git-tree-sha1 = "890088581945a793a25e16bbd4ac15ee837d5bf7" -repo-rev = "c6bf990" +deps = ["DataStructures", "Flux", "LinearAlgebra", "MLStyle", "Mmap", "ProtoBuf", "SymbolicUtils", "TermInterface", "Tokenize"] +git-tree-sha1 = "45cb59f28413edd7a1f9bd0850b63a652876f68c" +repo-rev = "9327e5c" repo-url = "https://github.com/samysweb/VNNLib.jl" uuid = "286915b0-5841-4eea-9013-d818f395ad8c" -version = "0.2.3" +version = "0.3.0" [[deps.VectorizationBase]] -deps = ["ArrayInterface", "CPUSummary", "HostCPUFeatures", "IfElse", "LayoutPointers", "Libdl", "LinearAlgebra", "SIMDTypes", "Static"] -git-tree-sha1 = "4c59c2df8d2676c4691a39fa70495a6db0c5d290" +deps = ["ArrayInterface", "CPUSummary", "HostCPUFeatures", "IfElse", "LayoutPointers", "Libdl", "LinearAlgebra", "SIMDTypes", "Static", "StaticArrayInterface"] +git-tree-sha1 = "d1d9a935a26c475ebffd54e9c7ad11627c43ea85" uuid = "3d5dd08c-fd9d-11e8-17fa-ed2836048c2f" -version = "0.21.58" +version = "0.21.72" + +[[deps.XML2_jll]] +deps = ["Artifacts", "JLLWrappers", "Libdl", "Libiconv_jll", "Zlib_jll"] +git-tree-sha1 = "80d3930c6347cfce7ccf96bd3bafdf079d9c0390" +uuid = "02c8fc9c-b97f-50b9-bbe4-9be30ff0a78a" +version = "2.13.9+0" + +[[deps.Xorg_libpciaccess_jll]] +deps = ["Artifacts", "JLLWrappers", "Libdl", "Zlib_jll"] +git-tree-sha1 = "4909eb8f1cbf6bd4b1c30dd18b2ead9019ef2fad" +uuid = "a65dc6b1-eb27-53a1-bb3e-dea574b5389e" +version = "0.18.1+0" [[deps.Zlib_jll]] deps = ["Libdl"] uuid = "83775a58-1f1d-513f-b197-d71354ab007a" version = "1.2.13+1" +[[deps.Zygote]] +deps = ["AbstractFFTs", "ChainRules", "ChainRulesCore", "DiffRules", "Distributed", "FillArrays", "ForwardDiff", "GPUArraysCore", "IRTools", "InteractiveUtils", "LinearAlgebra", "LogExpFunctions", "MacroTools", "NaNMath", "PrecompileTools", "Random", "SparseArrays", "SpecialFunctions", "Statistics", "ZygoteRules"] +git-tree-sha1 = "a29cbf3968d36022198bcc6f23fdfd70f7caf737" +uuid = "e88e6eb3-aa80-5325-afca-941959d7151f" +version = "0.7.10" + + [deps.Zygote.extensions] + ZygoteAtomExt = "Atom" + ZygoteColorsExt = "Colors" + ZygoteDistancesExt = "Distances" + ZygoteTrackerExt = "Tracker" + + [deps.Zygote.weakdeps] + Atom = "c52e3926-4ff0-5f6e-af25-54175e0327b1" + Colors = "5ae59095-9a9b-59fe-a467-6f913c188581" + Distances = "b4f34e82-e78d-54a5-968a-f98e89d6e8f7" + Tracker = "9f7883ad-71c0-57eb-9f7f-b5c9e6d3789c" + [[deps.ZygoteRules]] deps = ["ChainRulesCore", "MacroTools"] -git-tree-sha1 = "27798139afc0a2afa7b1824c206d5e87ea587a00" +git-tree-sha1 = "434b3de333c75fc446aa0d19fc394edafd07ab08" uuid = "700de1a5-db45-46bc-99cf-38207098b444" -version = "0.2.5" +version = "0.2.7" [[deps.libblastrampoline_jll]] deps = ["Artifacts", "Libdl"] uuid = "8e850b90-86db-534c-a0d3-1478176c7d93" -version = "5.8.0+1" +version = "5.11.0+0" [[deps.nghttp2_jll]] deps = ["Artifacts", "Libdl"] diff --git a/src/Definitions/Definitions.jl b/src/Definitions/Definitions.jl index 307d8fed..9d6372fa 100644 --- a/src/Definitions/Definitions.jl +++ b/src/Definitions/Definitions.jl @@ -3,7 +3,8 @@ module Definitions using LinearAlgebra using Statistics -using VNNLib.NNLoader: Network,Dense,ReLU,Layer +using VNNLib +using VNNLib.OnnxParser: Node, ONNXLinear, ONNXRelu using VeryDiff @@ -14,7 +15,10 @@ include("DataStructures.jl") include("PropState.jl") include("Zonotope.jl") -export Network,GeminiNetwork,Layer,Dense,ReLU,ZeroDense, DiffLayer, get_input_indices, get_layer_inputs +Dense = ONNXLinear +ReLU = ONNXRelu + +export Network,GeminiNetwork,Layer,ZeroDense,Dense,ReLU,DiffLayer, get_input_indices, get_layer_inputs export Zonotope,DiffZonotope,BoundsCache,CachedZonotope,ZonotopeStorage export VerificationTask, PropState, reset_ps!, first_pass, get_zonotope, get_layer, get_zonotope!, get_free_generator_id! export SortedVector, union, intersect_indices, find_index_position, attempt_find_index_position diff --git a/src/Definitions/Network.jl b/src/Definitions/Network.jl index 3457ebe0..1baa9f2f 100644 --- a/src/Definitions/Network.jl +++ b/src/Definitions/Network.jl @@ -1,110 +1,170 @@ -function cleanup_network(network1) + +struct OnnxLayer{LayerIdT} <: Node{LayerIdT} + layer_id :: LayerIdT + node :: Node{LayerIdT} + input_ids :: Vector{Int64} +end + +function cleanup_network(layers :: Vector{OnnxLayer{LayerIdT}}) :: Vector{OnnxLayer{LayerIdT}} where {LayerIdT} valid_layers = [] - for i in 1:length(network1.layers) - if network1.layers[i] isa Dense - if all(isone.(diag(network1.layers[i].W))) && all([all(iszero.(diag(network1.layers[i].W, k))) && all(iszero.(diag(network1.layers[i].W, -k))) for k in 1:size(network1.layers[i].W,1)-1]) + for i in 1:length(layers) + if layers[i].node isa ONNXLinear{LayerIdT} + W = layers[i].node.dense.weight + b = layers[i].node.dense.bias + f = layers[i].node.dense.σ + if all(isone.(diag(W))) && all([all(iszero.(diag(W, k))) && all(iszero.(diag(W, -k))) for k in 1:size(W,1)-1]) && all(iszero.(b)) && f == identity + @info "Removing identity Dense layer at index $i" continue end end push!(valid_layers, i) end print(valid_layers) - @assert length(valid_layers) == length(network2.layers) - return Network(network1.layers[valid_layers]) -end - -function get_input_indices(layer_idx :: Int64, :: Layer) - # TODO: Needs to be updated for comp graphs - return Int64[layer_idx - 1] + return layers[valid_layers] end -struct DiffLayer{L1<:Layer, Ld<:Layer, L2<:Layer} +struct DiffLayer{L1<:Node, Ld<:Node, L2<:Node} layer_idx :: Int64 inputs :: Vector{Int64} layer1 :: L1 diff_layer :: Ld layer2 :: L2 - function DiffLayer(layer_idx :: Int64, layer1 :: L1, diff_layer :: Ld, layer2 :: L2) where {L1<:Layer, Ld<:Layer, L2<:Layer} - inputs = union(get_input_indices(layer_idx, layer1), get_input_indices(layer_idx, layer2)) + function DiffLayer(layer_idx :: Int64, inputs :: Vector{Int64}, layer1 :: L1, diff_layer :: Ld, layer2 :: L2) where {L1<:Node, Ld<:Node, L2<:Node} return new{L1,Ld,L2}(layer_idx, inputs, layer1, diff_layer, layer2) end end -struct ZeroDense <: Layer +struct ZeroDense{LayerIdT} <: Node{LayerIdT} end +function topological_sort!(network :: OnnxNet{LayerIdT,NShapeIn, NShapeOut}, node_id :: LayerIdT, visited :: Set{LayerIdT}, sorting :: Dict{LayerIdT, Int64}) where {LayerIdT,NShapeIn,NShapeOut} + if node_id in visited + return + end + push!(visited, node_id) + for next_node in network.node_nexts[node_id] + topological_sort!(network, next_node, visited, sorting) + end + sorting[node_id] = length(sorting) + 1 +end -struct GeminiNetwork - network1 :: Network - network2 :: Network - diff_network :: Network - function GeminiNetwork(network1 :: Network, network2 :: Network) - diff_layers = Layer[] - if length(network1.layers) > length(network2.layers) - network1 = cleanup_network(network1) - elseif length(network2.layers) > length(network1.layers) - network2 = cleanup_network(network2) +function sort_network(network :: OnnxNet{LayerIdT,NShapeIn, NShapeOut}) :: Vector{OnnxLayer{LayerIdT}} where {LayerIdT,NShapeIn,NShapeOut} + @assert length(network.input_shapes) == 1 "Currently only single input networks are supported" + @assert length(network.output_shapes) == 1 "Currently only single output networks are supported" + sorting = Dict{LayerIdT, Int64}() + visited = Set{LayerIdT}() + for input_node in network.start_nodes + topological_sort!(network, input_node, visited, sorting) + end + num_nodes = length(sorting) + # Map i to num_nodes - i + 1 + for (k,v) in sorting + sorting[k] = num_nodes - v + 1 + end + layers = OnnxLayer{LayerIdT}[] + for (node_id, node) in network.nodes + input_ids = Int64[] + for input_id in node.inputs + if haskey(network.output_dict, input_id) + push!(input_ids, sorting[network.output_dict[input_id]]) + else + # Input node (currently only one input supported) + @assert haskey(network.input_shapes, input_id) "Input node $input_id not found in network inputs" + push!(input_ids, 0) + end end - @assert length(network1.layers) == length(network2.layers) - for (l1, l2) in zip(network1.layers, network2.layers) - @assert typeof(l1) == typeof(l2) - if typeof(l1) == Dense - @assert size(l1.W) == size(l2.W) "Mismatch in weight matrix size: $(size(l1.W)) vs $(size(l2.W))" - @assert size(l1.b) == size(l2.b) - new_W = l1.W .- l2.W - new_b = l1.b .- l2.b - if all(iszero.(new_W)) && all(iszero.(new_b)) - @info "Detected zero difference in Dense layer, replacing with ZeroDense layer." - push!(diff_layers, ZeroDense()) - else - push!(diff_layers, Dense(new_W, new_b)) - println("Distance: ", sum(abs,diff_layers[end].W)) - end - elseif typeof(l1) == ReLU - push!(diff_layers, ReLU()) + push!(layers, OnnxLayer{LayerIdT}(node_id, node, input_ids)) + end + sorted_layers = sort(layers, by = x -> sorting[x.layer_id]) + return sorted_layers +end + +function sort_mirror_network(layers :: Vector{OnnxLayer{LayerIdT}}, network :: OnnxNet{LayerIdT,NShapeIn, NShapeOut}) :: Vector{Node{LayerIdT}} where {LayerIdT,NShapeIn,NShapeOut} + sorted_layers = Node{LayerIdT}[] + for cur_layer in layers + cur_node = network.nodes[cur_layer.layer_id] + inputs = Int64[] + for input_node in cur_node.inputs + if haskey(network.output_dict, input_node) + push!(inputs, findfirst(x -> x.layer_id == network.output_dict[input_node], layers)) else - error("Unsupported layer type") + # Input node (currently only one input supported) + @assert haskey(network.input_shapes, input_node) "Input node $input_node not found in network inputs" + push!(inputs, 0) end end - return new(network1, network2, Network(diff_layers)) + push!(sorted_layers, OnnxLayer{LayerIdT}(cur_layer.layer_id, cur_node, inputs)) end + return sorted_layers end -function parse_network(n::Network) - return n +function mk_dense(W::AbstractMatrix{Float64}, b::AbstractVector{Float64}) + return ONNXLinear{Int64}(Dense(W, b, identity)) end -function get_layers(N::Network) - return N.layers -end -function to_diff_layer(input :: Tuple{Int64,Tuple{L1,Ld,L2}}) :: DiffLayer{L1,Ld,L2} where {L1<:Layer, Ld<:Layer, L2<:Layer} - (layer_idx,(l1,ld,l2)) = input - # Index 1 is input => Every subsequent layer is shifted by one - return DiffLayer(layer_idx + 1,l1,ld,l2) +struct GeminiNetwork + network1 :: OnnxNet + network2 :: OnnxNet + diff_layers :: Vector{DiffLayer} + function GeminiNetwork(network1 :: OnnxNet{LayerIdT,NShapeIn, NShapeOut}, network2 :: OnnxNet{LayerIdT,NShapeIn, NShapeOut}) where {LayerIdT,NShapeIn,NShapeOut} + n1_layers = sort_network(network1) + n2_layers = sort_mirror_network(n1_layers, network2) + diff_layers = DiffLayer[] + if length(n1_layers) > length(n2_layers) + n1_layers = cleanup_network(network1) + elseif length(n2_layers) > length(n1_layers) + n2_layers = cleanup_network(network2) + end + @assert length(n1_layers) == length(n2_layers) "Networks have different number of layers after cleanup: $(length(n1_layers)) vs $(length(n2_layers))" + for (idx, (l1, l2)) in enumerate(zip(n1_layers, n2_layers)) + @assert typeof(l1.node) == typeof(l2.node) "Mismatch in layer types: $(typeof(l1.node)) vs $(typeof(l2.node))" + @assert l1.input_ids == l2.input_ids "Mismatch in input ids for layers at index $(l1.layer_id) and $(l2.layer_id)" + if typeof(l1.node) == ONNXLinear{LayerIdT} + W1 = l1.node.dense.weight + b1 = l1.node.dense.bias + W2 = l2.node.dense.weight + b2 = l2.node.dense.bias + f1 = l1.node.dense.σ + f2 = l2.node.dense.σ + @assert f1 == identity "Unsupported activation function in network1: $f1" + @assert f2 == identity "Unsupported activation function in network2: $f2" + @assert size(W1) == size(W2) "Mismatch in weight matrix size: $(size(W1)) vs $(size(W2))" + @assert size(b1) == size(b2) + new_W = W1 .- W2 + new_b = b1 .- b2 + if all(iszero.(new_W)) && all(iszero.(new_b)) + @info "Detected zero difference in Dense layer, replacing with ZeroDense layer." + diff_l = ZeroDense{LayerIdT}() + else + diff_l = mk_dense(new_W, new_b) + end + push!(diff_layers, DiffLayer(idx + 1, map(x->x+1, l1.input_ids), l1.node, diff_l, l2.node)) + else + push!(diff_layers, DiffLayer(idx + 1, map(x->x+1, l1.input_ids), l1.node, l1.node, l2.node)) + end + end + return new(network1, network2, diff_layers) + end end -function get_inputs(L :: DiffLayer{<:Layer,<:Layer,<:Layer}) :: Vector{Int64} +function get_inputs(L :: DiffLayer{<:Node,<:Node,<:Node}) :: Vector{Int64} return L.inputs end -function get_layer1(L :: DiffLayer{L1, Ld, L2}) :: L1 where {L1<:Layer, Ld<:Layer, L2<:Layer} +function get_layer1(L :: DiffLayer{L1, Ld, L2}) :: L1 where {L1<:Node, Ld<:Node, L2<:Node} return L.layer1 end -function get_diff_layer(L :: DiffLayer{L1, Ld, L2}) :: Ld where {L1<:Layer, Ld<:Layer, L2<:Layer} +function get_diff_layer(L :: DiffLayer{L1, Ld, L2}) :: Ld where {L1<:Node, Ld<:Node, L2<:Node} return L.diff_layer end -function get_layer2(L :: DiffLayer{L1, Ld, L2}) :: L2 where {L1<:Layer, Ld<:Layer, L2<:Layer} +function get_layer2(L :: DiffLayer{L1, Ld, L2}) :: L2 where {L1<:Node, Ld<:Node, L2<:Node} return L.layer2 end function get_layers(N::GeminiNetwork) - return map(to_diff_layer,enumerate(zip( - get_layers(N.network1), - get_layers(N.diff_network), - get_layers(N.network2) - ))) + return N.diff_layers end \ No newline at end of file diff --git a/src/Transformers/Diff_Transformers.jl b/src/Transformers/Diff_Transformers.jl index 51cfb0a6..ecf6795d 100644 --- a/src/Transformers/Diff_Transformers.jl +++ b/src/Transformers/Diff_Transformers.jl @@ -1,9 +1,3 @@ -import VNNLib.NNLoader.Network -import VNNLib.NNLoader.Dense -import VNNLib.NNLoader.ReLU - -# TODO: ReLU, ZeroDense layers - function propagate_layer!(ZoutRef :: CachedZonotope, Ls :: DiffLayer{Dense,Dense,Dense}, inputs :: Vector{DiffZonotope}; bounds_cache :: Union{Nothing,BoundsCache}=nothing) @assert length(inputs) == 1 "Dense layer should have exactly one input zonotope" # @debug "Propagating DiffDense Layer" diff --git a/src/Transformers/Single_Transformers.jl b/src/Transformers/Single_Transformers.jl index 2f6f7bdc..072b1f1c 100644 --- a/src/Transformers/Single_Transformers.jl +++ b/src/Transformers/Single_Transformers.jl @@ -1,11 +1,3 @@ -import VNNLib.NNLoader.Network -import VNNLib.NNLoader.Dense -import VNNLib.NNLoader.ReLU - -function (N::Network)(Z :: Zonotope, P :: PropState) - return foldl((Z,L) -> L(Z,P),N.layers,init=Z) -end - function propagate_layer!(ZoutRef :: Zonotope, L :: Dense, inputs :: Vector{Zonotope}) @assert length(inputs) == 1 "Dense layer should have exactly one input" Zin = inputs[1] diff --git a/src/Util.jl b/src/Util.jl deleted file mode 100644 index 3d73857c..00000000 --- a/src/Util.jl +++ /dev/null @@ -1,17 +0,0 @@ -import Base: size - -using Statistics - -function truncate_network(T::Type,N::Network) - layers = [] - for l in N.layers - if l isa ReLU - push!(layers, l) - elseif l isa Dense - push!(layers,Dense(convert.(Float64,convert.(T,deepcopy(l.W))),convert.(Float64,convert.(T,deepcopy(l.b))))) - else - throw("Unknown layer type") - end - end - return Network(layers) -end diff --git a/src/Verifier.jl b/src/Verifier.jl index 065a7ad8..8183fa6a 100644 --- a/src/Verifier.jl +++ b/src/Verifier.jl @@ -3,13 +3,13 @@ @enum VerificationStatus UNKNOWN SAFE UNSAFE function verify_network( - N1 :: Network, - N2 :: Network, + N1 :: OnnxNet{LayerIdT,NShapeIn, NShapeOut}, + N2 :: OnnxNet{LayerIdT,NShapeIn, NShapeOut}, bounds, property_check, split_heuristic; timeout=Inf, - init_eps=0.0) + init_eps=0.0) where {LayerIdT,NShapeIn,NShapeOut} global FIRST_ROUND[] = true verification_result = nothing # Prepare Zonotope Initialization diff --git a/src/VeryDiff.jl b/src/VeryDiff.jl index bcefd25a..b0c04c5e 100644 --- a/src/VeryDiff.jl +++ b/src/VeryDiff.jl @@ -22,7 +22,6 @@ include("Util/simd_bool.jl") include("Debugger/Debugger.jl") include("Definitions/Definitions.jl") using .Definitions -include("Util.jl") include("Transformers/Transformers.jl") using .Transformers From 914490f61f5f733b1720f215951b218e76ff1c52 Mon Sep 17 00:00:00 2001 From: Samuel Teuber Date: Thu, 15 Jan 2026 13:53:52 +0100 Subject: [PATCH 2/5] Working version of new ONNX loader? (modulo constant adding/subtracting) TODO: Update tests to generate ONNX nodes instead of Dense/ReLU layers --- Manifest.toml | 211 +++++++++++------------- Project.toml | 3 + src/Cli.jl | 5 +- src/Definitions/AbstractDomains.jl | 14 +- src/Definitions/Definitions.jl | 10 +- src/Definitions/Network.jl | 123 +++++++++----- src/Definitions/PropState.jl | 17 +- src/Transformers/Diff_Transformers.jl | 60 +++++-- src/Transformers/Init.jl | 21 ++- src/Transformers/Network.jl | 17 +- src/Transformers/Single_Transformers.jl | 18 +- src/Transformers/Transformers.jl | 3 + src/Transformers/Util.jl | 8 +- src/Verifier.jl | 10 ++ 14 files changed, 312 insertions(+), 208 deletions(-) diff --git a/Manifest.toml b/Manifest.toml index 1ace84af..ee380550 100644 --- a/Manifest.toml +++ b/Manifest.toml @@ -1,8 +1,8 @@ # This file is machine-generated - editing it directly is not advised -julia_version = "1.10.10" +julia_version = "1.11.8" manifest_format = "2.0" -project_hash = "abf3877108b478f6b9583465c99f8b2dffaf0ef6" +project_hash = "faa349a4d3547f9ef2fcb1409af40245d41fd476" [[deps.AbstractFFTs]] deps = ["LinearAlgebra"] @@ -74,7 +74,7 @@ version = "1.2.0" [[deps.ArgTools]] uuid = "0dad84c5-d112-42e6-8d28-ef12dabb789f" -version = "1.1.1" +version = "1.1.2" [[deps.ArrayInterface]] deps = ["Adapt", "LinearAlgebra"] @@ -112,6 +112,7 @@ version = "7.22.0" [[deps.Artifacts]] uuid = "56f22d72-fd6d-98f1-02f0-08ddc0907c33" +version = "1.11.0" [[deps.Atomix]] deps = ["UnsafeAtomics"] @@ -155,6 +156,7 @@ version = "0.4.6" [[deps.Base64]] uuid = "2a0f44e3-6c83-55bd-87e4-b1978d98bd5f" +version = "1.11.0" [[deps.Baselet]] git-tree-sha1 = "aebf55e6d7795e02ca500a689d326ac979aaf89e" @@ -168,9 +170,9 @@ uuid = "6e4b80f9-dd63-53aa-95a3-0cdb28fa8baf" version = "1.6.3" [[deps.Bijections]] -git-tree-sha1 = "6aaafea90a56dc1fc8cbc15e3cf26d6bc81eb0a3" +git-tree-sha1 = "a2d308fcd4c2fb90e943cf9cd2fbfa9c32b69733" uuid = "e2ed5e7c-b2de-5872-ae92-c73ca462fb04" -version = "0.1.10" +version = "0.2.2" [[deps.BitTwiddlingConvenienceFunctions]] deps = ["Static"] @@ -235,9 +237,9 @@ uuid = "944b1d66-785c-5afd-91f1-9de20f533193" version = "0.7.8" [[deps.Combinatorics]] -git-tree-sha1 = "c761b00e7755700f9cdf5b02039939d1359330e1" +git-tree-sha1 = "08c8b6831dc00bfea825826be0bc8336fc369860" uuid = "861a8166-3701-5b0c-9a16-15d98fcdc6aa" -version = "1.1.0" +version = "1.0.2" [[deps.CommonSubexpressions]] deps = ["MacroTools"] @@ -275,17 +277,18 @@ weakdeps = ["InverseFunctions"] CompositionsBaseInverseFunctionsExt = "InverseFunctions" [[deps.ConstructionBase]] -deps = ["LinearAlgebra"] -git-tree-sha1 = "d8a9c0b6ac2d9081bf76324b39c78ca3ce4f0c98" +git-tree-sha1 = "b4b092499347b18a015186eae3042f72267106cb" uuid = "187b0558-2788-49d3-abe0-74a17ed4e7c9" -version = "1.5.6" +version = "1.6.0" [deps.ConstructionBase.extensions] ConstructionBaseIntervalSetsExt = "IntervalSets" + ConstructionBaseLinearAlgebraExt = "LinearAlgebra" ConstructionBaseStaticArraysExt = "StaticArrays" [deps.ConstructionBase.weakdeps] IntervalSets = "8197267c-284f-5f27-9208-e0e47529a953" + LinearAlgebra = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e" StaticArrays = "90137ffa-7385-5640-81b9-e52037218182" [[deps.ContextVariablesX]] @@ -319,6 +322,7 @@ version = "1.0.0" [[deps.Dates]] deps = ["Printf"] uuid = "ade2ca70-3891-5945-98fb-dc099432e06a" +version = "1.11.0" [[deps.DefineSingletons]] git-tree-sha1 = "0fba8b706d0178b4dc7fd44a96a92382c9065c2c" @@ -346,6 +350,7 @@ version = "1.15.1" [[deps.Distributed]] deps = ["Random", "Serialization", "Sockets"] uuid = "8ba89e20-285c-5b6f-9357-94700520ee1b" +version = "1.11.0" [[deps.DocStringExtensions]] git-tree-sha1 = "7442a5dfe1ebb773c29cc2962a8980f47221d76c" @@ -358,10 +363,10 @@ uuid = "f43a241f-c20a-4ad4-852c-f6b1247861c6" version = "1.6.0" [[deps.DynamicPolynomials]] -deps = ["DataStructures", "Future", "LinearAlgebra", "MultivariatePolynomials", "MutableArithmetics", "Pkg", "Reexport", "Test"] -git-tree-sha1 = "8b84876e31fa39479050e2d3395c4b3b210db8b0" +deps = ["Future", "LinearAlgebra", "MultivariatePolynomials", "MutableArithmetics", "Reexport", "Test"] +git-tree-sha1 = "ca693f8707a77a0e365d49fe4622203b72b6cf1d" uuid = "7c1d4256-1411-5781-91ec-d7bc3513ac07" -version = "0.4.6" +version = "0.6.3" [[deps.EnumX]] git-tree-sha1 = "bddad79635af6aec424f53ed8aad5d7555dc6f00" @@ -383,6 +388,11 @@ git-tree-sha1 = "27415f162e6028e81c72b82ef756bf321213b6ec" uuid = "e2ba6199-217a-4e67-a87a-7c52f15ade04" version = "0.1.10" +[[deps.ExproniconLite]] +git-tree-sha1 = "c13f0b150373771b0fdc1713c97860f8df12e6c2" +uuid = "55351af7-c7e9-48d6-89ff-24e801d99491" +version = "0.10.14" + [[deps.FLoops]] deps = ["BangBang", "Compat", "FLoopsBase", "InitialValues", "JuliaVariables", "MLStyle", "Serialization", "Setfield", "Transducers"] git-tree-sha1 = "0a2e5873e9a5f54abb06418d57a8df689336a660" @@ -397,6 +407,7 @@ version = "0.1.1" [[deps.FileWatching]] uuid = "7b1f6079-737a-58dc-b8bc-7a2ca5c1b5ee" +version = "1.11.0" [[deps.FillArrays]] deps = ["LinearAlgebra"] @@ -455,6 +466,7 @@ version = "0.5.2" [[deps.Future]] deps = ["Random"] uuid = "9fa8497b-333b-5362-9e8d-4d0656e87820" +version = "1.11.0" [[deps.GLPK]] deps = ["GLPK_jll", "MathOptInterface"] @@ -471,7 +483,7 @@ version = "5.0.1+1" [[deps.GMP_jll]] deps = ["Artifacts", "Libdl"] uuid = "781609d7-10c4-51f6-84f2-b8444358ff6d" -version = "6.2.1+6" +version = "6.3.0+0" [[deps.GPUArraysCore]] deps = ["Adapt"] @@ -542,6 +554,7 @@ version = "0.3.1" [[deps.InteractiveUtils]] deps = ["Markdown"] uuid = "b77e0a4c-d291-57a0-90e8-8db25a27a240" +version = "1.11.0" [[deps.InverseFunctions]] git-tree-sha1 = "a779299d77cd080bf77b97535acecd73e1c5e5cb" @@ -623,12 +636,6 @@ weakdeps = ["EnzymeCore", "LinearAlgebra", "SparseArrays"] LinearAlgebraExt = "LinearAlgebra" SparseArraysExt = "SparseArrays" -[[deps.LabelledArrays]] -deps = ["ArrayInterface", "ChainRulesCore", "ForwardDiff", "LinearAlgebra", "MacroTools", "PreallocationTools", "RecursiveArrayTools", "StaticArrays"] -git-tree-sha1 = "fccbe22c5a5602237870694d08f2040532a04b66" -uuid = "2ee39098-c373-598a-b85f-a56591580800" -version = "1.17.0" - [[deps.LayoutPointers]] deps = ["ArrayInterface", "LinearAlgebra", "ManualMemory", "SIMDTypes", "Static", "StaticArrayInterface"] git-tree-sha1 = "a9eaadb366f5493a5654e843864c13d8b107548c" @@ -638,6 +645,7 @@ version = "0.1.17" [[deps.LazyArtifacts]] deps = ["Artifacts", "Pkg"] uuid = "4af54fe1-eca0-43a8-85a7-787d91b784e3" +version = "1.11.0" [[deps.LibCURL]] deps = ["LibCURL_jll", "MozillaCACerts_jll"] @@ -647,16 +655,17 @@ version = "0.6.4" [[deps.LibCURL_jll]] deps = ["Artifacts", "LibSSH2_jll", "Libdl", "MbedTLS_jll", "Zlib_jll", "nghttp2_jll"] uuid = "deac9b47-8bc7-5906-a0fe-35ac56dc84c0" -version = "8.4.0+0" +version = "8.6.0+0" [[deps.LibGit2]] deps = ["Base64", "LibGit2_jll", "NetworkOptions", "Printf", "SHA"] uuid = "76f85450-5226-5b5a-8eaa-529ad045b433" +version = "1.11.0" [[deps.LibGit2_jll]] deps = ["Artifacts", "LibSSH2_jll", "Libdl", "MbedTLS_jll"] uuid = "e37daf67-58a4-590a-8e99-b0245dd2ffc5" -version = "1.6.4+0" +version = "1.7.2+0" [[deps.LibSSH2_jll]] deps = ["Artifacts", "Libdl", "MbedTLS_jll"] @@ -665,6 +674,7 @@ version = "1.11.0+1" [[deps.Libdl]] uuid = "8f399da3-3557-5675-b5ff-fb832c97cbdb" +version = "1.11.0" [[deps.Libiconv_jll]] deps = ["Artifacts", "JLLWrappers", "Libdl"] @@ -675,6 +685,7 @@ version = "1.18.0+0" [[deps.LinearAlgebra]] deps = ["Libdl", "OpenBLAS_jll", "libblastrampoline_jll"] uuid = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e" +version = "1.11.0" [[deps.LogExpFunctions]] deps = ["DocStringExtensions", "IrrationalConstants", "LinearAlgebra"] @@ -694,6 +705,7 @@ version = "0.3.29" [[deps.Logging]] uuid = "56ddb016-857b-54e1-b83d-db4d58db5568" +version = "1.11.0" [[deps.LoopVectorization]] deps = ["ArrayInterface", "CPUSummary", "CloseOpenIntervals", "DocStringExtensions", "HostCPUFeatures", "IfElse", "LayoutPointers", "LinearAlgebra", "OffsetArrays", "PolyesterWeave", "PrecompileTools", "SIMDTypes", "SLEEFPirates", "Static", "StaticArrayInterface", "ThreadingUtilities", "UnPack", "VectorizationBase"] @@ -785,6 +797,7 @@ version = "0.1.8" [[deps.Markdown]] deps = ["Base64"] uuid = "d6f4376e-aef5-505a-96c1-9c027394607a" +version = "1.11.0" [[deps.MaskedArrays]] git-tree-sha1 = "0221f710bab1510075abac7a2b107fa5465b1aef" @@ -800,7 +813,7 @@ version = "1.48.0" [[deps.MbedTLS_jll]] deps = ["Artifacts", "Libdl"] uuid = "c8ffd9c3-330d-5841-b78e-0817d7145fa1" -version = "2.28.2+1" +version = "2.28.6+0" [[deps.MicroCollections]] deps = ["Accessors", "BangBang", "InitialValues"] @@ -816,16 +829,17 @@ version = "1.2.0" [[deps.Mmap]] uuid = "a63ad114-7e13-5084-954f-fe012c677804" +version = "1.11.0" [[deps.MozillaCACerts_jll]] uuid = "14a3606d-f60d-562e-9121-12d972cd8159" -version = "2023.1.10" +version = "2023.12.12" [[deps.MultivariatePolynomials]] deps = ["ChainRulesCore", "DataStructures", "LinearAlgebra", "MutableArithmetics"] -git-tree-sha1 = "eaa98afe2033ffc0629f9d0d83961d66a021dfcc" +git-tree-sha1 = "fade91fe9bee7b142d332fc6ab3f0deea29f637b" uuid = "102ac46a-7ee4-5c85-9060-abc95bfdeaa3" -version = "0.4.7" +version = "0.5.9" [[deps.MutableArithmetics]] deps = ["LinearAlgebra", "SparseArrays", "Test"] @@ -835,9 +849,9 @@ version = "1.6.7" [[deps.NNlib]] deps = ["Adapt", "Atomix", "ChainRulesCore", "GPUArraysCore", "KernelAbstractions", "LinearAlgebra", "Random", "ScopedValues", "Statistics"] -git-tree-sha1 = "09701dc1df4281fa9212b269a69210dfa81ee52a" +git-tree-sha1 = "6dc9ffc3a9931e6b988f913b49630d0fb986d0a8" uuid = "872c559c-99b0-510c-b3b7-b6c96a88d5cd" -version = "0.9.32" +version = "0.9.33" [deps.NNlib.extensions] NNlibAMDGPUExt = "AMDGPU" @@ -893,7 +907,7 @@ version = "0.2.10" [[deps.OpenBLAS_jll]] deps = ["Artifacts", "CompilerSupportLibraries_jll", "Libdl"] uuid = "4536629a-c528-5b80-bd46-f80d51c5b363" -version = "0.3.23+4" +version = "0.3.27+1" [[deps.OpenLibm_jll]] deps = ["Artifacts", "Libdl"] @@ -907,15 +921,20 @@ uuid = "efe28fd5-8261-553b-a9e1-b2916fc3738e" version = "0.5.6+0" [[deps.Optimisers]] -deps = ["ChainRulesCore", "Functors", "LinearAlgebra", "Random", "Statistics"] -git-tree-sha1 = "53ff746a3a2b232a37dbcd262ac8bbb2b18202b8" +deps = ["ChainRulesCore", "ConstructionBase", "Functors", "LinearAlgebra", "Random", "Statistics"] +git-tree-sha1 = "36b5d2b9dd06290cd65fcf5bdbc3a551ed133af5" uuid = "3bd65402-5787-11e9-1adc-39752487f4e2" -version = "0.4.4" -weakdeps = ["Adapt", "EnzymeCore"] +version = "0.4.7" [deps.Optimisers.extensions] OptimisersAdaptExt = ["Adapt"] OptimisersEnzymeCoreExt = "EnzymeCore" + OptimisersReactantExt = "Reactant" + + [deps.Optimisers.weakdeps] + Adapt = "79e6a3ab-5dfb-504d-930d-738a2a938a0e" + EnzymeCore = "f151be2c-9106-41f4-ab19-57ee4f262869" + Reactant = "3c362404-f566-11ee-1572-e11a4b42c853" [[deps.OrderedCollections]] git-tree-sha1 = "05868e21324cede2207c6f0f466b4bfef6d5e7ee" @@ -935,9 +954,15 @@ uuid = "69de0a69-1ddd-5017-9359-2bf0b02dc9f0" version = "2.8.3" [[deps.Pkg]] -deps = ["Artifacts", "Dates", "Downloads", "FileWatching", "LibGit2", "Libdl", "Logging", "Markdown", "Printf", "REPL", "Random", "SHA", "Serialization", "TOML", "Tar", "UUIDs", "p7zip_jll"] +deps = ["Artifacts", "Dates", "Downloads", "FileWatching", "LibGit2", "Libdl", "Logging", "Markdown", "Printf", "Random", "SHA", "TOML", "Tar", "UUIDs", "p7zip_jll"] uuid = "44cfe95a-1eb2-52ea-b672-e2afdf69b78f" -version = "1.10.0" +version = "1.11.0" + + [deps.Pkg.extensions] + REPLExt = "REPL" + + [deps.Pkg.weakdeps] + REPL = "3fa0cd96-eef1-5676-8a61-b3b8758bbffb" [[deps.PolyesterWeave]] deps = ["BitTwiddlingConvenienceFunctions", "CPUSummary", "IfElse", "Static", "ThreadingUtilities"] @@ -945,22 +970,6 @@ git-tree-sha1 = "645bed98cd47f72f67316fd42fc47dee771aefcd" uuid = "1d0040c9-8b98-4ee7-8388-3f51789ca0ad" version = "0.2.2" -[[deps.PreallocationTools]] -deps = ["Adapt", "ArrayInterface", "PrecompileTools"] -git-tree-sha1 = "c05b4c6325262152483a1ecb6c69846d2e01727b" -uuid = "d236fae5-4411-538c-8e31-a6e3d9e00b46" -version = "0.4.34" - - [deps.PreallocationTools.extensions] - PreallocationToolsForwardDiffExt = "ForwardDiff" - PreallocationToolsReverseDiffExt = "ReverseDiff" - PreallocationToolsSparseConnectivityTracerExt = "SparseConnectivityTracer" - - [deps.PreallocationTools.weakdeps] - ForwardDiff = "f6369f11-7733-5829-9624-2563aa707210" - ReverseDiff = "37e2e3b7-166d-5795-8a7a-e32c996b4267" - SparseConnectivityTracer = "9f842d2f-2579-4b1d-911e-f412cf18a3f5" - [[deps.PrecompileTools]] deps = ["Preferences"] git-tree-sha1 = "5aa36f7049a63a1528fe8f7c3f2113413ffd4e1f" @@ -981,10 +990,11 @@ version = "0.2.0" [[deps.Printf]] deps = ["Unicode"] uuid = "de0858da-6303-5e67-8744-51eddeeeb8d7" +version = "1.11.0" [[deps.Profile]] -deps = ["Printf"] uuid = "9abbd945-dff8-562f-b5e8-e1ebf5ef1b79" +version = "1.11.0" [[deps.ProgressLogging]] deps = ["Logging", "SHA", "UUIDs"] @@ -1003,13 +1013,10 @@ git-tree-sha1 = "1d36ef11a9aaf1e8b74dacc6a731dd1de8fd493d" uuid = "43287f4e-b6f4-7ad1-bb20-aadabca52c3d" version = "1.3.0" -[[deps.REPL]] -deps = ["InteractiveUtils", "Markdown", "Sockets", "Unicode"] -uuid = "3fa0cd96-eef1-5676-8a61-b3b8758bbffb" - [[deps.Random]] deps = ["SHA"] uuid = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c" +version = "1.11.0" [[deps.RealDot]] deps = ["LinearAlgebra"] @@ -1017,46 +1024,6 @@ git-tree-sha1 = "9f0a1b71baaf7650f4fa8a1d168c7fb6ee41f0c9" uuid = "c1ae055f-0cd5-4b69-90a6-9a35b1a98df9" version = "0.1.0" -[[deps.RecipesBase]] -deps = ["PrecompileTools"] -git-tree-sha1 = "5c3d09cc4f31f5fc6af001c250bf1278733100ff" -uuid = "3cdcf5f2-1ef4-517c-9805-6587b60abb01" -version = "1.3.4" - -[[deps.RecursiveArrayTools]] -deps = ["Adapt", "ArrayInterface", "DocStringExtensions", "GPUArraysCore", "LinearAlgebra", "PrecompileTools", "RecipesBase", "StaticArraysCore", "SymbolicIndexingInterface"] -git-tree-sha1 = "31b3d7b7e14faad39583475b89aadbd9c3e7ef8b" -uuid = "731186ca-8d62-57ce-b412-fbd966d074cd" -version = "3.44.0" - - [deps.RecursiveArrayTools.extensions] - RecursiveArrayToolsFastBroadcastExt = "FastBroadcast" - RecursiveArrayToolsForwardDiffExt = "ForwardDiff" - RecursiveArrayToolsKernelAbstractionsExt = "KernelAbstractions" - RecursiveArrayToolsMeasurementsExt = "Measurements" - RecursiveArrayToolsMonteCarloMeasurementsExt = "MonteCarloMeasurements" - RecursiveArrayToolsReverseDiffExt = ["ReverseDiff", "Zygote"] - RecursiveArrayToolsSparseArraysExt = ["SparseArrays"] - RecursiveArrayToolsStatisticsExt = "Statistics" - RecursiveArrayToolsStructArraysExt = "StructArrays" - RecursiveArrayToolsTablesExt = ["Tables"] - RecursiveArrayToolsTrackerExt = "Tracker" - RecursiveArrayToolsZygoteExt = "Zygote" - - [deps.RecursiveArrayTools.weakdeps] - FastBroadcast = "7034ab61-46d4-4ed7-9d0f-46aef9175898" - ForwardDiff = "f6369f11-7733-5829-9624-2563aa707210" - KernelAbstractions = "63c18a36-062a-441e-b654-da1e3ab1ce7c" - Measurements = "eff96d63-e80a-5855-80a2-b1b0885c5ab7" - MonteCarloMeasurements = "0987c9cc-fe09-11e8-30f0-b96dd679fdca" - ReverseDiff = "37e2e3b7-166d-5795-8a7a-e32c996b4267" - SparseArrays = "2f01184e-e22b-5df5-ae63-d93ebab69eaf" - Statistics = "10745b16-79ce-11e8-11f9-7d13ad32a3b2" - StructArrays = "09ab397b-f2b6-538f-b94a-2f83cf4a842a" - Tables = "bd369af6-aec1-5ad0-b16a-f7cc5008161c" - Tracker = "9f7883ad-71c0-57eb-9f7f-b5c9e6d3789c" - Zygote = "e88e6eb3-aa80-5325-afca-941959d7151f" - [[deps.Reexport]] git-tree-sha1 = "45e428421666073eab6f2da5c9d310d99bb12f9b" uuid = "189a3867-3050-52da-a836-e630ba90ab69" @@ -1114,6 +1081,7 @@ version = "1.3.0" [[deps.Serialization]] uuid = "9e88b42a-f829-5b0c-bbe9-9e923198166b" +version = "1.11.0" [[deps.Setfield]] deps = ["ConstructionBase", "Future", "MacroTools", "StaticArraysCore"] @@ -1134,6 +1102,7 @@ version = "0.9.5" [[deps.Sockets]] uuid = "6462fe0b-24de-5631-8697-dd941f90decc" +version = "1.11.0" [[deps.SortingAlgorithms]] deps = ["DataStructures"] @@ -1144,7 +1113,7 @@ version = "1.2.2" [[deps.SparseArrays]] deps = ["Libdl", "LinearAlgebra", "Random", "Serialization", "SuiteSparse_jll"] uuid = "2f01184e-e22b-5df5-ae63-d93ebab69eaf" -version = "1.10.0" +version = "1.11.0" [[deps.SparseInverseSubset]] deps = ["LinearAlgebra", "SparseArrays", "SuiteSparse"] @@ -1207,9 +1176,14 @@ uuid = "1e83bf80-4336-4d27-bf5d-d5a4f845583c" version = "1.4.4" [[deps.Statistics]] -deps = ["LinearAlgebra", "SparseArrays"] +deps = ["LinearAlgebra"] +git-tree-sha1 = "ae3bb1eb3bba077cd276bc5cfc337cc65c3075c0" uuid = "10745b16-79ce-11e8-11f9-7d13ad32a3b2" -version = "1.10.0" +version = "1.11.1" +weakdeps = ["SparseArrays"] + + [deps.Statistics.extensions] + SparseArraysExt = ["SparseArrays"] [[deps.StatsAPI]] deps = ["LinearAlgebra"] @@ -1218,10 +1192,10 @@ uuid = "82ae8749-77ed-4fe6-ae5f-f523153014b0" version = "1.8.0" [[deps.StatsBase]] -deps = ["AliasTables", "DataAPI", "DataStructures", "LinearAlgebra", "LogExpFunctions", "Missings", "Printf", "Random", "SortingAlgorithms", "SparseArrays", "Statistics", "StatsAPI"] -git-tree-sha1 = "be5733d4a2b03341bdcab91cea6caa7e31ced14b" +deps = ["AliasTables", "DataAPI", "DataStructures", "IrrationalConstants", "LinearAlgebra", "LogExpFunctions", "Missings", "Printf", "Random", "SortingAlgorithms", "SparseArrays", "Statistics", "StatsAPI"] +git-tree-sha1 = "aceda6f4e598d331548e04cc6b2124a6148138e3" uuid = "2913bbd2-ae8a-5f71-8c99-4fb6c76f3a91" -version = "0.34.9" +version = "0.34.10" [[deps.StructArrays]] deps = ["ConstructionBase", "DataAPI", "Tables"] @@ -1264,7 +1238,7 @@ uuid = "4607b0f0-06f3-5cda-b6b1-a6196a1729e9" [[deps.SuiteSparse_jll]] deps = ["Artifacts", "Libdl", "libblastrampoline_jll"] uuid = "bea87d4a-7f5b-5778-9afe-8cc45184846c" -version = "7.2.1+1" +version = "7.7.0+0" [[deps.SymbolicIndexingInterface]] deps = ["Accessors", "ArrayInterface", "RuntimeGeneratedFunctions", "StaticArraysCore"] @@ -1279,11 +1253,18 @@ version = "0.3.46" PrettyTables = "08abe8d2-0d0c-5749-adfa-8a2ac140af0d" [[deps.SymbolicUtils]] -deps = ["AbstractTrees", "Bijections", "ChainRulesCore", "Combinatorics", "ConstructionBase", "DataStructures", "DocStringExtensions", "DynamicPolynomials", "IfElse", "LabelledArrays", "LinearAlgebra", "MultivariatePolynomials", "NaNMath", "Setfield", "SparseArrays", "SpecialFunctions", "StaticArrays", "TimerOutputs", "Unityper"] -git-tree-sha1 = "e7bf8868bd1acad8e0bb59f6fd964410b82f3eef" -pinned = true +deps = ["AbstractTrees", "ArrayInterface", "Bijections", "ChainRulesCore", "Combinatorics", "ConstructionBase", "DataStructures", "DocStringExtensions", "DynamicPolynomials", "ExproniconLite", "LinearAlgebra", "MultivariatePolynomials", "NaNMath", "Setfield", "SparseArrays", "SpecialFunctions", "StaticArrays", "SymbolicIndexingInterface", "TaskLocalValues", "TermInterface", "TimerOutputs", "Unityper"] +git-tree-sha1 = "a85b4262a55dbd1af39bb6facf621d79ca6a322d" uuid = "d1185830-fcd6-423d-90d6-eec64667417b" -version = "1.1.0" +version = "3.32.0" + + [deps.SymbolicUtils.extensions] + SymbolicUtilsLabelledArraysExt = "LabelledArrays" + SymbolicUtilsReverseDiffExt = "ReverseDiff" + + [deps.SymbolicUtils.weakdeps] + LabelledArrays = "2ee39098-c373-598a-b85f-a56591580800" + ReverseDiff = "37e2e3b7-166d-5795-8a7a-e32c996b4267" [[deps.SysInfo]] deps = ["Dates", "DelimitedFiles", "Hwloc", "PrecompileTools", "Random", "Serialization"] @@ -1313,6 +1294,11 @@ deps = ["ArgTools", "SHA"] uuid = "a4e569a6-e804-4fa4-b0f3-eef7a1d5b13e" version = "1.10.0" +[[deps.TaskLocalValues]] +git-tree-sha1 = "67e469338d9ce74fc578f7db1736a74d93a49eb8" +uuid = "ed4db957-447d-4319-bfb6-7fa9ae7ecf34" +version = "0.1.3" + [[deps.TermInterface]] git-tree-sha1 = "d673e0aca9e46a2f63720201f55cc7b3e7169b16" uuid = "8ea1fca8-c5ef-4a55-8b96-4e9afe9c9a3c" @@ -1321,6 +1307,7 @@ version = "2.0.0" [[deps.Test]] deps = ["InteractiveUtils", "Logging", "Random", "Serialization"] uuid = "8dfed614-e22c-5e08-85e1-65c5234f0b40" +version = "1.11.0" [[deps.TextWrap]] git-tree-sha1 = "43044b737fa70bc12f6105061d3da38f881a3e3c" @@ -1400,6 +1387,7 @@ version = "0.4.85" [[deps.UUIDs]] deps = ["Random", "SHA"] uuid = "cf7118a7-6976-5b1a-9a39-7adc72f591a4" +version = "1.11.0" [[deps.UnPack]] git-tree-sha1 = "387c1f73762231e86e0c9c5443ce3b4a0a9a0c2b" @@ -1408,6 +1396,7 @@ version = "1.0.2" [[deps.Unicode]] uuid = "4ec0a83e-493e-50e2-b9ac-8f72acf5a8f5" +version = "1.11.0" [[deps.Unityper]] deps = ["ConstructionBase"] @@ -1427,9 +1416,9 @@ version = "0.3.0" LLVM = "929cbde3-209d-540e-8aea-75f648917ca0" [[deps.VNNLib]] -deps = ["DataStructures", "Flux", "LinearAlgebra", "MLStyle", "Mmap", "ProtoBuf", "SymbolicUtils", "TermInterface", "Tokenize"] -git-tree-sha1 = "45cb59f28413edd7a1f9bd0850b63a652876f68c" -repo-rev = "9327e5c" +deps = ["DataStructures", "Flux", "LinearAlgebra", "MLStyle", "Mmap", "ProtoBuf", "Statistics", "SymbolicUtils", "TermInterface", "Tokenize"] +git-tree-sha1 = "4060fa791ffdb8906df192068f6fef6b627dce73" +repo-rev = "verydiff-compat" repo-url = "https://github.com/samysweb/VNNLib.jl" uuid = "286915b0-5841-4eea-9013-d818f395ad8c" version = "0.3.0" @@ -1489,7 +1478,7 @@ version = "5.11.0+0" [[deps.nghttp2_jll]] deps = ["Artifacts", "Libdl"] uuid = "8e850ede-7688-5339-a07c-302acd2aaf8d" -version = "1.52.0+1" +version = "1.59.0+0" [[deps.p7zip_jll]] deps = ["Artifacts", "Libdl"] diff --git a/Project.toml b/Project.toml index 73b8f243..f081a476 100644 --- a/Project.toml +++ b/Project.toml @@ -21,6 +21,9 @@ ThreadPinning = "811555cd-349b-4f26-b7bc-1f208b848042" TimerOutputs = "a759f4b9-e2f1-59dc-863e-4aeb61b1ea8f" VNNLib = "286915b0-5841-4eea-9013-d818f395ad8c" +[compat] +VNNLib = "0.3.0" + [extras] Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40" diff --git a/src/Cli.jl b/src/Cli.jl index 0c10fe58..06aff850 100644 --- a/src/Cli.jl +++ b/src/Cli.jl @@ -1,7 +1,6 @@ using ArgParse using VNNLib -import VNNLib.NNLoader: load_network function parse_commandline(cmd_args) s = ArgParseSettings() @@ -64,7 +63,7 @@ function run_cmd(args) return 1 end try - net1 = load_network(net1) + net1 = load_onnx_model(net1) catch error("Failed to parse network: $net1") return 1 @@ -80,7 +79,7 @@ function run_cmd(args) return 1 end try - net2 = load_network(net2) + net2 = load_onnx_model(net2) catch error("Failed to parse network: $net2") return 1 diff --git a/src/Definitions/AbstractDomains.jl b/src/Definitions/AbstractDomains.jl index 9def3a48..a8280c08 100644 --- a/src/Definitions/AbstractDomains.jl +++ b/src/Definitions/AbstractDomains.jl @@ -58,7 +58,19 @@ mutable struct CachedZonotope end struct ZonotopeStorage - zonotopes :: Vector{CachedZonotope} + zonotopes :: Vector{Union{Nothing,CachedZonotope}} +end + +function length(zs :: ZonotopeStorage) :: Int64 + return length(zs.zonotopes) +end + +function resize_zonotope_storage!(zs :: ZonotopeStorage, new_size :: Int64) + current_size = length(zs.zonotopes) + @assert new_size > current_size + for _ in 1:(new_size - current_size) + push!(zs.zonotopes, nothing) + end end # WARNING: This method is dangerous! We are generating Matrix pointers to sub-matrices of existing matrices. diff --git a/src/Definitions/Definitions.jl b/src/Definitions/Definitions.jl index 9d6372fa..0bc32ba8 100644 --- a/src/Definitions/Definitions.jl +++ b/src/Definitions/Definitions.jl @@ -15,15 +15,13 @@ include("DataStructures.jl") include("PropState.jl") include("Zonotope.jl") -Dense = ONNXLinear -ReLU = ONNXRelu - -export Network,GeminiNetwork,Layer,ZeroDense,Dense,ReLU,DiffLayer, get_input_indices, get_layer_inputs +export Network,GeminiNetwork,Layer,ZeroDense,DiffLayer, get_input_indices, get_zonos_at_pos, executable_network export Zonotope,DiffZonotope,BoundsCache,CachedZonotope,ZonotopeStorage +export resize_zonotope_storage! export VerificationTask, PropState, reset_ps!, first_pass, get_zonotope, get_layer, get_zonotope!, get_free_generator_id! export SortedVector, union, intersect_indices, find_index_position, attempt_find_index_position -export parse_network, get_layers, get_inputs, get_layer1, get_diff_layer, get_layer2 -export configure_first_usage!, prepare_prop_state!, has_layer +export parse_network, get_layers, get_inputs, get_outputs, get_layer1, get_diff_layer, get_layer2 +export configure_first_usage!, prepare_prop_state!, zonos_initialized export updateGenerators!, updateGeneratorsMul!, updateGeneratorsAdd!, updateGeneratorsAddMul!, updateGeneratorsSub!, updateGeneratorsSubMul! export zono_optimize, zono_bounds, zono_get_max_vector diff --git a/src/Definitions/Network.jl b/src/Definitions/Network.jl index 1baa9f2f..71695dcd 100644 --- a/src/Definitions/Network.jl +++ b/src/Definitions/Network.jl @@ -1,9 +1,11 @@ struct OnnxLayer{LayerIdT} <: Node{LayerIdT} + layer_index :: Int64 layer_id :: LayerIdT node :: Node{LayerIdT} input_ids :: Vector{Int64} + output_ids :: Vector{Int64} end function cleanup_network(layers :: Vector{OnnxLayer{LayerIdT}}) :: Vector{OnnxLayer{LayerIdT}} where {LayerIdT} @@ -27,11 +29,12 @@ end struct DiffLayer{L1<:Node, Ld<:Node, L2<:Node} layer_idx :: Int64 inputs :: Vector{Int64} + outputs :: Vector{Int64} layer1 :: L1 diff_layer :: Ld layer2 :: L2 - function DiffLayer(layer_idx :: Int64, inputs :: Vector{Int64}, layer1 :: L1, diff_layer :: Ld, layer2 :: L2) where {L1<:Node, Ld<:Node, L2<:Node} - return new{L1,Ld,L2}(layer_idx, inputs, layer1, diff_layer, layer2) + function DiffLayer(layer_idx :: Int64, inputs :: Vector{Int64}, outputs :: Vector{Int64}, layer1 :: L1, diff_layer :: Ld, layer2 :: L2) where {L1<:Node, Ld<:Node, L2<:Node} + return new{L1,Ld,L2}(layer_idx, inputs, outputs, layer1, diff_layer, layer2) end end @@ -49,52 +52,69 @@ function topological_sort!(network :: OnnxNet{LayerIdT,NShapeIn, NShapeOut}, nod sorting[node_id] = length(sorting) + 1 end -function sort_network(network :: OnnxNet{LayerIdT,NShapeIn, NShapeOut}) :: Vector{OnnxLayer{LayerIdT}} where {LayerIdT,NShapeIn,NShapeOut} +function compute_io( + io_mapping :: Dict{LayerIdT, Int64}, + to_map :: Vector{String} +) :: Vector{Int64} where {LayerIdT} + result_ids = Int64[] + for input_id in to_map + push!(result_ids, io_mapping[input_id]) + end + return result_ids +end + +function sort_network(network :: OnnxNet{LayerIdT,NShapeIn, NShapeOut}) :: Tuple{Vector{OnnxLayer{LayerIdT}}, Dict{LayerIdT, Int64}} where {LayerIdT,NShapeIn,NShapeOut} @assert length(network.input_shapes) == 1 "Currently only single input networks are supported" @assert length(network.output_shapes) == 1 "Currently only single output networks are supported" + io_map = Dict{LayerIdT, Int64}() + for (idx, (input_id, _)) in enumerate(network.input_shapes) + io_map[input_id] = idx + end + io_offset = length(io_map) sorting = Dict{LayerIdT, Int64}() visited = Set{LayerIdT}() for input_node in network.start_nodes topological_sort!(network, input_node, visited, sorting) end + sorting_inverse = Dict{Int64, LayerIdT}() num_nodes = length(sorting) # Map i to num_nodes - i + 1 for (k,v) in sorting sorting[k] = num_nodes - v + 1 + sorting_inverse[sorting[k]] = k + end + for lid in 1:num_nodes + node = network.nodes[sorting_inverse[lid]] + for in_id in node.inputs + @assert haskey(io_map, in_id) + end + for out_id in node.outputs + io_offset += 1 + io_map[out_id] = io_offset + end + end + for (idx, (output_id, _)) in enumerate(network.output_shapes) + if !haskey(io_map, output_id) + io_map[output_id] = idx + io_offset + end end layers = OnnxLayer{LayerIdT}[] for (node_id, node) in network.nodes - input_ids = Int64[] - for input_id in node.inputs - if haskey(network.output_dict, input_id) - push!(input_ids, sorting[network.output_dict[input_id]]) - else - # Input node (currently only one input supported) - @assert haskey(network.input_shapes, input_id) "Input node $input_id not found in network inputs" - push!(input_ids, 0) - end - end - push!(layers, OnnxLayer{LayerIdT}(node_id, node, input_ids)) + input_ids = compute_io(io_map, node.inputs) + output_ids = compute_io(io_map, node.outputs) + push!(layers, OnnxLayer{LayerIdT}(sorting[node_id], node_id, node, input_ids, output_ids)) end - sorted_layers = sort(layers, by = x -> sorting[x.layer_id]) - return sorted_layers + sorted_layers = sort(layers, by = x -> x.layer_index) + return sorted_layers, io_map end -function sort_mirror_network(layers :: Vector{OnnxLayer{LayerIdT}}, network :: OnnxNet{LayerIdT,NShapeIn, NShapeOut}) :: Vector{Node{LayerIdT}} where {LayerIdT,NShapeIn,NShapeOut} +function sort_mirror_network(layers :: Vector{OnnxLayer{LayerIdT}}, io_map :: Dict{LayerIdT, Int64}, network :: OnnxNet{LayerIdT,NShapeIn, NShapeOut}) :: Vector{Node{LayerIdT}} where {LayerIdT,NShapeIn,NShapeOut} sorted_layers = Node{LayerIdT}[] for cur_layer in layers cur_node = network.nodes[cur_layer.layer_id] - inputs = Int64[] - for input_node in cur_node.inputs - if haskey(network.output_dict, input_node) - push!(inputs, findfirst(x -> x.layer_id == network.output_dict[input_node], layers)) - else - # Input node (currently only one input supported) - @assert haskey(network.input_shapes, input_node) "Input node $input_node not found in network inputs" - push!(inputs, 0) - end - end - push!(sorted_layers, OnnxLayer{LayerIdT}(cur_layer.layer_id, cur_node, inputs)) + input_ids = compute_io(io_map, cur_node.inputs) + output_ids = compute_io(io_map, cur_node.outputs) + push!(sorted_layers, OnnxLayer{LayerIdT}(cur_layer.layer_index, cur_layer.layer_id, cur_node, input_ids, output_ids)) end return sorted_layers end @@ -104,13 +124,12 @@ function mk_dense(W::AbstractMatrix{Float64}, b::AbstractVector{Float64}) end -struct GeminiNetwork - network1 :: OnnxNet - network2 :: OnnxNet +struct GeminiNetwork{LayerIdT} + inputs :: Dict{LayerIdT, Int64} diff_layers :: Vector{DiffLayer} function GeminiNetwork(network1 :: OnnxNet{LayerIdT,NShapeIn, NShapeOut}, network2 :: OnnxNet{LayerIdT,NShapeIn, NShapeOut}) where {LayerIdT,NShapeIn,NShapeOut} - n1_layers = sort_network(network1) - n2_layers = sort_mirror_network(n1_layers, network2) + n1_layers, io_map = sort_network(network1) + n2_layers = sort_mirror_network(n1_layers, io_map, network2) diff_layers = DiffLayer[] if length(n1_layers) > length(n2_layers) n1_layers = cleanup_network(network1) @@ -140,12 +159,16 @@ struct GeminiNetwork else diff_l = mk_dense(new_W, new_b) end - push!(diff_layers, DiffLayer(idx + 1, map(x->x+1, l1.input_ids), l1.node, diff_l, l2.node)) + push!(diff_layers, DiffLayer(l1.layer_index, l1.input_ids, l1.output_ids, l1.node, diff_l, l2.node)) else - push!(diff_layers, DiffLayer(idx + 1, map(x->x+1, l1.input_ids), l1.node, l1.node, l2.node)) + push!(diff_layers, DiffLayer(l1.layer_index, l1.input_ids, l1.output_ids, l1.node, l1.node, l2.node)) end end - return new(network1, network2, diff_layers) + input_map = Dict{LayerIdT, Int64}() + for (input_id, idx) in network1.input_shapes + input_map[input_id] = io_map[input_id] + end + return new{LayerIdT}(input_map, diff_layers) end end @@ -153,6 +176,10 @@ function get_inputs(L :: DiffLayer{<:Node,<:Node,<:Node}) :: Vector{Int64} return L.inputs end +function get_outputs(L :: DiffLayer{<:Node,<:Node,<:Node}) :: Vector{Int64} + return L.outputs +end + function get_layer1(L :: DiffLayer{L1, Ld, L2}) :: L1 where {L1<:Node, Ld<:Node, L2<:Node} return L.layer1 end @@ -167,4 +194,26 @@ end function get_layers(N::GeminiNetwork) return N.diff_layers -end \ No newline at end of file +end + +struct Network{LayerIdT,NShapeIn,NShapeOut} + model :: OnnxNet{LayerIdT,NShapeIn,NShapeOut} + input_id :: LayerIdT + output_id :: LayerIdT +end + +function (network::Network{LayerIdT,NShapeIn,NShapeOut})(x) where {LayerIdT,NShapeIn,NShapeOut} + input_data = Dict(network.input_id => x) + output_data = compute_outputs(network.model, input_data) + return output_data[network.output_id] +end + +function executable_network(model :: OnnxNet{LayerIdT,NShapeIn, NShapeOut}) :: Network where {LayerIdT,NShapeIn,NShapeOut} + inputs = model.input_shapes + outputs = model.output_shapes + @assert length(inputs) == 1 "Currently only single input networks are supported" + @assert length(outputs) == 1 "Currently only single output networks are supported" + input_id = first(keys(inputs)) + output_id = first(keys(outputs)) + return Network(model, input_id, output_id) +end diff --git a/src/Definitions/PropState.jl b/src/Definitions/PropState.jl index fadac66c..d8502c2e 100644 --- a/src/Definitions/PropState.jl +++ b/src/Definitions/PropState.jl @@ -22,8 +22,12 @@ function first_pass(PS :: PropState) :: Bool return PS.first end -function get_layer_inputs(idxs :: Vector{Int64}, PS :: PropState) :: Vector{CachedZonotope} - return @view PS.zono_storage.zonotopes[idxs] +""" +Retrieves the CachedZonotope references at the given indices from the PropState's ZonotopeStorage. +Expects that all indices are valid (i.e., positions are no longer filled with `nothing`). +""" +function get_zonos_at_pos(idxs :: Vector{Int64}, PS :: PropState) :: Vector{CachedZonotope} + return convert(Vector{CachedZonotope}, @view PS.zono_storage.zonotopes[idxs]) end function get_zonotope(Z :: CachedZonotope) :: DiffZonotope @@ -179,13 +183,8 @@ function prepare_prop_state!(PS :: PropState, task :: VerificationTask) PS.task_bounds = task.task_bounds end -function has_layer(PS :: PropState, layer :: DiffLayer) :: Bool - return length(PS.zono_storage.zonotopes) >= layer.layer_idx -end - -function get_layer(PS :: PropState, layer :: DiffLayer) :: CachedZonotope - @assert has_layer(PS, layer) "Layer $(layer.layer_idx) not initialized in PropState!" - return PS.zono_storage.zonotopes[layer.layer_idx] +function zonos_initialized(PS :: PropState, output_positions :: Vector{Int64}) :: Bool + return length(PS.zono_storage) >= maximum(output_positions) && all(!isnothing(PS.zono_storage.zonotopes[pos]) for pos in output_positions) end function get_free_generator_id!(PS :: PropState) :: Int64 diff --git a/src/Transformers/Diff_Transformers.jl b/src/Transformers/Diff_Transformers.jl index ecf6795d..a5786050 100644 --- a/src/Transformers/Diff_Transformers.jl +++ b/src/Transformers/Diff_Transformers.jl @@ -1,5 +1,14 @@ -function propagate_layer!(ZoutRef :: CachedZonotope, Ls :: DiffLayer{Dense,Dense,Dense}, inputs :: Vector{DiffZonotope}; bounds_cache :: Union{Nothing,BoundsCache}=nothing) +function propagate_layer!( + ZoutRefVec :: Vector{CachedZonotope}, + Ls :: DiffLayer{ + ONNXLinear{S1}, + ONNXLinear{S2}, + ONNXLinear{S3}}, + inputs :: Vector{DiffZonotope}; + bounds_cache :: Union{Nothing,BoundsCache}=nothing) where {S1, S2, S3} @assert length(inputs) == 1 "Dense layer should have exactly one input zonotope" + @assert length(ZoutRefVec) == 1 "Dense layer should have exactly one output zonotope" + ZoutRef = ZoutRefVec[1] # @debug "Propagating DiffDense Layer" Zin = inputs[1] # Compute differential zonotope dimensions @@ -21,38 +30,54 @@ function propagate_layer!(ZoutRef :: CachedZonotope, Ls :: DiffLayer{Dense,Dense L1 = get_layer1(Ls) ∂L = get_diff_layer(Ls) L2 = get_layer2(Ls) + L1_W = L1.dense.weight + ∂L_W = ∂L.dense.weight + ∂L_b = ∂L.dense.bias if VeryDiff.USE_DIFFZONO[] # @debug "IDs of Output Zonotope Generators: $(Zout.∂Z.generator_ids)" ∂indices = intersect_indices(Zout.∂Z.generator_ids, Zin.∂Z.generator_ids) for (i, g) in zip(∂indices, Zin.∂Z.Gs) - mul!(Zout.∂Z.Gs[i], L1.W, g) + mul!(Zout.∂Z.Gs[i], L1_W, g) end indices₂ = intersect_indices(Zout.∂Z.generator_ids, Zin.Z₂.generator_ids) for (i, g) in zip(indices₂, Zin.Z₂.Gs) - mul!(Zout.∂Z.Gs[i], ∂L.W, g, 1.0, 1.0) + mul!(Zout.∂Z.Gs[i], ∂L_W, g, 1.0, 1.0) end # @assert length(intersect_indices(Zout.∂Z.generator_ids, union(Zin.∂Z.generator_ids, Zin.Z₂.generator_ids))) == length(Zout.∂Z.generator_ids) "Not all generators in ∂Z were processed during Dense propagation!" - mul!(Zout.∂Z.c, L1.W, Zin.∂Z.c) - mul!(Zout.∂Z.c, ∂L.W, Zin.Z₂.c, 1.0, 1.0) - Zout.∂Z.c .+= ∂L.b + mul!(Zout.∂Z.c, L1_W, Zin.∂Z.c) + mul!(Zout.∂Z.c, ∂L_W, Zin.Z₂.c, 1.0, 1.0) + Zout.∂Z.c .+= ∂L_b end propagate_layer!(Zout.Z₁, L1, Zin.Z₁) propagate_layer!(Zout.Z₂, L2, Zin.Z₂) end -function propagate_layer!(ZoutRef :: CachedZonotope, Ls :: DiffLayer{Dense,ZeroDense,Dense}, inputs :: Vector{DiffZonotope}; bounds_cache :: Union{Nothing,BoundsCache}=nothing) +function propagate_layer!( + ZoutRefVec :: Vector{CachedZonotope}, + Ls :: DiffLayer{ + ONNXLinear{S1}, + ZeroDense{S2}, + ONNXLinear{S3}}, + inputs :: Vector{DiffZonotope}; + bounds_cache :: Union{Nothing,BoundsCache}=nothing) where {S1, S2, S3} @assert length(inputs) == 1 "Dense layer should have exactly one input zonotope" + @assert length(ZoutRefVec) == 1 "Dense layer should have exactly one output zonotope" + ZoutRef = ZoutRefVec[1] Zin = inputs[1] Zout = get_zonotope!(ZoutRef, size.(Zin.Z₁.Gs,2), size.(Zin.Z₂.Gs,2), convert(Vector{Int64},size.(Zin.∂Z.Gs,2))) L1 = get_layer1(Ls) L2 = get_layer2(Ls) + L1_W = L1.dense.weight + L2_W = L2.dense.weight + L1_b = L1.dense.bias + L2_b = L2.dense.bias if VeryDiff.USE_DIFFZONO[] ∂indices = intersect_indices(Zout.∂Z.generator_ids, Zin.∂Z.generator_ids) # @assert length(union(Zout.∂Z.generator_ids,Zin.∂Z.generator_ids)) == length(Zout.∂Z.generator_ids) "Not all generators in ∂Z were processed during Dense propagation. Output IDs: $(Zout.∂Z.generator_ids), Processed IDs: $(Zin.∂Z.generator_ids)" for (i, g) in zip(∂indices, Zin.∂Z.Gs) - mul!(Zout.∂Z.Gs[i], L1.W, g) + mul!(Zout.∂Z.Gs[i], L1_W, g) end - mul!(Zout.∂Z.c, L1.W, Zin.∂Z.c) + mul!(Zout.∂Z.c, L1_W, Zin.∂Z.c) end propagate_layer!(Zout.Z₁, L1, Zin.Z₁) propagate_layer!(Zout.Z₂, L2, Zin.Z₂) @@ -87,8 +112,17 @@ function ∂a(any_any, ∂lower, ∂upper) #ifelse.(pos_pos .|| any_pos .|| pos_any, 1.0, 0.0)) end -function propagate_layer!(ZoutRef :: CachedZonotope, Ls :: DiffLayer{ReLU,ReLU,ReLU}, inputs :: Vector{DiffZonotope}; bounds_cache :: Union{Nothing,BoundsCache}=nothing) +function propagate_layer!( + ZoutRefVec :: Vector{CachedZonotope}, + Ls :: DiffLayer{ + ONNXRelu{S1}, + ONNXRelu{S2}, + ONNXRelu{S3}}, + inputs :: Vector{DiffZonotope}; + bounds_cache :: Union{Nothing,BoundsCache}=nothing) where {S1, S2, S3} @assert length(inputs) == 1 "ReLU layer should have exactly one input zonotope" + @assert length(ZoutRefVec) == 1 "Dense layer should have exactly one output zonotope" + ZoutRef = ZoutRefVec[1] Zin = inputs[1] @assert !isnothing(bounds_cache) @@ -264,10 +298,4 @@ function propagate_layer!(ZoutRef :: CachedZonotope, Ls :: DiffLayer{ReLU,ReLU,R ifelse.(any_pos, μ.(lower₁,upper₁), ifelse.(pos_any, .-μ.(lower₂,upper₂), 0.0))) end -end - - -function (N::GeminiNetwork)(Z :: DiffZonotope, P :: PropState) - #println("Prop network") - return foldl((Z,Ls) -> propagate_diff_layer(Ls,Z,P),zip(N.network1.layers,N.diff_network.layers,N.network2.layers),init=Z) end \ No newline at end of file diff --git a/src/Transformers/Init.jl b/src/Transformers/Init.jl index 198220e6..c06380fc 100644 --- a/src/Transformers/Init.jl +++ b/src/Transformers/Init.jl @@ -24,8 +24,9 @@ function init_default_zono(Z :: CachedZonotope) ) end -function init_layer!(PS :: PropState, diff_layer :: DiffLayer{ReLU, ReLU, ReLU}, inputs :: Vector{CachedZonotope}) +function init_layer!(PS :: PropState, diff_layer :: DiffLayer{ONNXRelu{S1}, ONNXRelu{S2}, ONNXRelu{S3}}, inputs :: Vector{CachedZonotope}, output_positions :: Vector{Int64}) where {S1, S2, S3} @assert length(inputs) == 1 "ReLU DiffLayer should have exactly one input" + @assert length(output_positions) == 1 "ReLU DiffLayer should have exactly one output" input_zono_cache = inputs[1] input_zono = get_zonotope(input_zono_cache) # Compute Bounds @@ -94,17 +95,20 @@ function init_layer!(PS :: PropState, diff_layer :: DiffLayer{ReLU, ReLU, ReLU}, nothing ) init_default_zono(Z) - push!(PS.zono_storage.zonotopes, Z) + PS.zono_storage.zonotopes[output_positions[1]] = Z end -function init_layer!(PS :: PropState, diff_layer :: DiffLayer{Dense, ZeroDense, Dense}, inputs :: Vector{CachedZonotope}) +function init_layer!(PS :: PropState, diff_layer :: DiffLayer{ONNXLinear{S1}, ZeroDense{S2}, ONNXLinear{S3}}, inputs :: Vector{CachedZonotope}, output_positions :: Vector{Int64}) where {S1, S2, S3} @assert length(inputs) == 1 "Dense DiffLayer should have exactly one input" + @assert length(output_positions) == 1 "Dense DiffLayer should have exactly one output" input_zono_cache = inputs[1] input_zono = get_zonotope(input_zono_cache) L1 = get_layer1(diff_layer) L2 = get_layer2(diff_layer) - @assert size(L1.W,2) == size(input_zono.Z₁.Gs[1],1) "Input dimension mismatch for Dense layer 1" - @assert size(L2.W,2) == size(input_zono.Z₂.Gs[1],1) "Input dimension mismatch for Dense layer 2" + L1_W = L1.dense.weight + L2_W = L2.dense.weight + @assert size(L1_W,2) == size(input_zono.Z₁.Gs[1],1) "Input dimension mismatch for Dense layer 1" + @assert size(L2_W,2) == size(input_zono.Z₂.Gs[1],1) "Input dimension mismatch for Dense layer 2" Z₁, Z₂ = init_layer_dense_z1_z2(L1, L2, input_zono, input_zono_cache, diff_layer.layer_idx) ∂Z = init_zonotope(L2, input_zono.∂Z, input_zono.∂Z.influence, input_zono.∂Z.owned_generators) Z =CachedZonotope( @@ -116,11 +120,12 @@ function init_layer!(PS :: PropState, diff_layer :: DiffLayer{Dense, ZeroDense, nothing ) init_default_zono(Z) - push!(PS.zono_storage.zonotopes, Z) + PS.zono_storage.zonotopes[output_positions[1]] = Z end -function init_layer!(PS :: PropState, diff_layer :: DiffLayer{Dense,Dense,Dense}, inputs :: Vector{CachedZonotope}) +function init_layer!(PS :: PropState, diff_layer :: DiffLayer{ONNXLinear{S1},ONNXLinear{S2},ONNXLinear{S3}}, inputs :: Vector{CachedZonotope}, output_positions :: Vector{Int64}) where {S1, S2, S3} @assert length(inputs) == 1 "Dense DiffLayer should have exactly one input" + @assert length(output_positions) == 1 "Dense DiffLayer should have exactly one output" input_zono_cache = inputs[1] input_zono = get_zonotope(input_zono_cache) L1 = get_layer1(diff_layer) @@ -183,5 +188,5 @@ function init_layer!(PS :: PropState, diff_layer :: DiffLayer{Dense,Dense,Dense} nothing ) init_default_zono(Z) - push!(PS.zono_storage.zonotopes, Z) + PS.zono_storage.zonotopes[output_positions[1]] = Z end \ No newline at end of file diff --git a/src/Transformers/Network.jl b/src/Transformers/Network.jl index d3b18ae8..0747c8d0 100644 --- a/src/Transformers/Network.jl +++ b/src/Transformers/Network.jl @@ -1,19 +1,24 @@ function propagate!(N :: GeminiNetwork, P :: PropState) + max_io_id = maximum(max(maximum(l.inputs), maximum(l.outputs)) for l in get_layers(N)) + if max_io_id > length(P.zono_storage) + resize_zonotope_storage!(P.zono_storage, max_io_id) + end for diff_layer in get_layers(N) # @debug "Propagating layer: $(typeof(diff_layer))" input_positions = get_inputs(diff_layer) + output_positions = get_outputs(diff_layer) # @debug "Input Positions: $input_positions" - inputs = get_layer_inputs(input_positions, P) + inputs = get_zonos_at_pos(input_positions, P) if first_pass(P) configure_first_usage!(diff_layer.layer_idx, inputs) end - if !has_layer(P, diff_layer) + if !zonos_initialized(P, output_positions) @assert first_pass(P) "Layer $diff_layer not initialized in PropState! This should only happen during the first pass." - init_layer!(P, diff_layer, inputs) + init_layer!(P, diff_layer, inputs, output_positions) end - # @assert has_layer(P, diff_layer) input_zonotopes = get_zonotope.(inputs) - output_zonotope_ref = get_layer(P, diff_layer) + output_positions = get_outputs(diff_layer) + outputs = get_zonos_at_pos(output_positions, P) if haskey(P.task_bounds.bounds_cache, diff_layer.layer_idx) # @debug "Bounds Cache: Found for layer index $(diff_layer.layer_idx)" bounds_cache = P.task_bounds.bounds_cache[diff_layer.layer_idx] @@ -23,7 +28,7 @@ function propagate!(N :: GeminiNetwork, P :: PropState) P.task_bounds.bounds_cache[diff_layer.layer_idx] = bounds_cache end # @debug "Processing DiffLayer at index $(diff_layer.layer_idx) with bounds cache initialized=$(bounds_cache.initialized)" - propagate_layer!(output_zonotope_ref, diff_layer, input_zonotopes; bounds_cache=bounds_cache) + propagate_layer!(outputs, diff_layer, input_zonotopes; bounds_cache=bounds_cache) #@debug "Layer $(diff_layer.layer_idx) output Zonotope ∂Z bounds: $(zono_bounds(output_zonotope_ref.zonotope.∂Z)[1:5,:])" #@debug "Layer $(diff_layer.layer_idx) output Zonotope Z₁ bounds: $(zono_bounds(output_zonotope_ref.zonotope.Z₁)[1:5,:])" end diff --git a/src/Transformers/Single_Transformers.jl b/src/Transformers/Single_Transformers.jl index 072b1f1c..fce3e219 100644 --- a/src/Transformers/Single_Transformers.jl +++ b/src/Transformers/Single_Transformers.jl @@ -1,17 +1,19 @@ -function propagate_layer!(ZoutRef :: Zonotope, L :: Dense, inputs :: Vector{Zonotope}) +function propagate_layer!(ZoutRefVec :: Vector{Zonotope}, L :: ONNXLinear{S1}, inputs :: Vector{Zonotope}) where {S1} @assert length(inputs) == 1 "Dense layer should have exactly one input" + @assert length(ZoutRefVec) == 1 "Dense layer should have exactly one output" + ZoutRef = ZoutRefVec[1] Zin = inputs[1] return propagate_layer!(ZoutRef, L, Zin) end -function propagate_layer!(ZoutRef :: Zonotope, L :: Dense, Zin :: Zonotope) +function propagate_layer!(ZoutRef :: Zonotope, L :: ONNXLinear{S1}, Zin :: Zonotope) where {S1} # Zout must have exactly the same ids as Zin # @assert all(ZoutRef.generator_ids .== Zin.generator_ids) "Zonotope generator IDs do not match during Dense propagation!" for i in 1:length(Zin.Gs) - mul!(ZoutRef.Gs[i], L.W, Zin.Gs[i]) + mul!(ZoutRef.Gs[i], L.dense.weight, Zin.Gs[i]) end - mul!(ZoutRef.c, L.W, Zin.c) - ZoutRef.c .+= L.b + mul!(ZoutRef.c, L.dense.weight, Zin.c) + ZoutRef.c .+= L.dense.bias end function get_slope(l,u, alpha) @@ -24,13 +26,15 @@ function get_slope(l,u, alpha) end end -function propagate_layer!(ZoutRef :: Zonotope, L :: ReLU, inputs :: Vector{Zonotope}; lower=nothing, upper=nothing) +function propagate_layer!(ZoutRefVec :: Vector{Zonotope}, L :: ONNXRelu{S}, inputs :: Vector{Zonotope}; lower=nothing, upper=nothing) where {S} @assert length(inputs) == 1 "Dense layer should have exactly one input" + @assert length(ZoutRefVec) == 1 "Dense layer should have exactly one output" + ZoutRef = ZoutRefVec[1] Zin = inputs[1] return propagate_layer!(ZoutRef, L, Zin; lower=lower, upper=upper) end -function propagate_layer!(ZoutRef :: Zonotope, L :: ReLU, Zin :: Zonotope; lower=nothing, upper=nothing) +function propagate_layer!(ZoutRef :: Zonotope, _L :: ONNXRelu{S}, Zin :: Zonotope; lower=nothing, upper=nothing) where {S} if isnothing(lower) || isnothing(upper) bounds = zono_bounds(Zin) lower = @view bounds[:,1] diff --git a/src/Transformers/Transformers.jl b/src/Transformers/Transformers.jl index 996d4022..384d78ef 100644 --- a/src/Transformers/Transformers.jl +++ b/src/Transformers/Transformers.jl @@ -2,6 +2,9 @@ module Transformers using LinearAlgebra +using VNNLib +using VNNLib.OnnxParser: ONNXLinear, ONNXRelu + using TimerOutputs import ..VeryDiff: zono_bounds, @simd_bool_expr diff --git a/src/Transformers/Util.jl b/src/Transformers/Util.jl index 55909c6b..ff8e7dbf 100644 --- a/src/Transformers/Util.jl +++ b/src/Transformers/Util.jl @@ -1,16 +1,16 @@ -function init_zonotope(layer :: Dense, input :: Zonotope, influence::Union{Vector{Matrix{Float64}},Nothing}, owned_generators :: Union{Int64, Nothing}) +function init_zonotope(layer :: ONNXLinear{S}, input :: Zonotope, influence::Union{Vector{Matrix{Float64}},Nothing}, owned_generators :: Union{Int64, Nothing}) where {S} # Compute new generators generators = Vector{Matrix{Float64}}() generator_ids = deepcopy(input.generator_ids) for g in input.Gs - new_g = zeros(Float64, size(layer.W,1), size(g,2)) + new_g = zeros(Float64, size(layer.dense.weight,1), size(g,2)) push!(generators, new_g) end - c = zeros(Float64, size(layer.W,1)) + c = zeros(Float64, size(layer.dense.weight,1)) return Zonotope(generators, c, influence, generator_ids, owned_generators) end -function init_layer_dense_z1_z2(L1 :: Dense, L2 :: Dense, input_zono :: DiffZonotope, input_zono_cache :: CachedZonotope, layer_idx :: Int64) :: Tuple{Zonotope,Zonotope} +function init_layer_dense_z1_z2(L1 :: ONNXLinear{S1}, L2 :: ONNXLinear{S2}, input_zono :: DiffZonotope, input_zono_cache :: CachedZonotope, layer_idx :: Int64) :: Tuple{Zonotope,Zonotope} where {S1,S2} # Instantiate Z₁ # Dense Layer can reuse influence matrix from input (nocopy) influence = input_zono.Z₁.influence diff --git a/src/Verifier.jl b/src/Verifier.jl index 8183fa6a..0c5caeeb 100644 --- a/src/Verifier.jl +++ b/src/Verifier.jl @@ -43,7 +43,17 @@ function verify_network( end N = GeminiNetwork(N1,N2) + + N1 = executable_network(N1) + N2 = executable_network(N2) + println("Network initialized.") + if N.diff_layers[end] isa VeryDiff.Definitions.DiffLayer{VNNLib.OnnxParser.ONNXSoftmax{S},VNNLib.OnnxParser.ONNXSoftmax{S},VNNLib.OnnxParser.ONNXSoftmax{S}} where S + pop!(N.diff_layers) + @warn "Removed final Softmax layer from differential network for verification." + @warn "VeryDiff assumes this is handled by the choice of an appropriate property!" + end + @assert length(N.inputs) == 1 "VeryDiff currently only supports single input networks." # Statistics total_zonos = 1 From 220490c2ed9309bb7fd1fb31b5d32bec71a023bb Mon Sep 17 00:00:00 2001 From: Samuel Teuber Date: Mon, 19 Jan 2026 18:56:23 +0100 Subject: [PATCH 3/5] Making tests work --- src/Definitions/Network.jl | 2 +- src/Transformers/Init.jl | 19 +++-- test/runtests.jl | 4 + test/unit/propagation/dense.jl | 43 +++++----- test/unit/propagation/dense_zero_diff.jl | 46 +++++----- test/unit/propagation/relu.jl | 41 +++++---- test/unit/propagation/utils.jl | 103 +++++++++++++++++------ 7 files changed, 158 insertions(+), 100 deletions(-) diff --git a/src/Definitions/Network.jl b/src/Definitions/Network.jl index 71695dcd..28f1a040 100644 --- a/src/Definitions/Network.jl +++ b/src/Definitions/Network.jl @@ -157,7 +157,7 @@ struct GeminiNetwork{LayerIdT} @info "Detected zero difference in Dense layer, replacing with ZeroDense layer." diff_l = ZeroDense{LayerIdT}() else - diff_l = mk_dense(new_W, new_b) + diff_l = ONNXLinear(l1.node.inputs, l1.node.outputs, l1.node.name, new_W, new_b) end push!(diff_layers, DiffLayer(l1.layer_index, l1.input_ids, l1.output_ids, l1.node, diff_l, l2.node)) else diff --git a/src/Transformers/Init.jl b/src/Transformers/Init.jl index c06380fc..2670ae53 100644 --- a/src/Transformers/Init.jl +++ b/src/Transformers/Init.jl @@ -131,8 +131,11 @@ function init_layer!(PS :: PropState, diff_layer :: DiffLayer{ONNXLinear{S1},ONN L1 = get_layer1(diff_layer) diff_layer_output =get_diff_layer(diff_layer) L2 = get_layer2(diff_layer) - @assert size(L1.W,2) == size(input_zono.Z₁.Gs[1],1) "Input dimension mismatch for Dense layer 1" - @assert size(L2.W,2) == size(input_zono.Z₂.Gs[1],1) "Input dimension mismatch for Dense layer 2" + L1_W = L1.dense.weight + L2_W = L2.dense.weight + diff_layer_output_W = diff_layer_output.dense.weight + @assert size(L1_W,2) == size(input_zono.Z₁.Gs[1],1) "Input dimension mismatch for Dense layer 1" + @assert size(L2_W,2) == size(input_zono.Z₂.Gs[1],1) "Input dimension mismatch for Dense layer 2" Z₁, Z₂ = init_layer_dense_z1_z2(L1, L2, input_zono, input_zono_cache, diff_layer.layer_idx) # Instantiate ∂Z influence = input_zono.∂Z.influence @@ -147,38 +150,38 @@ function init_layer!(PS :: PropState, diff_layer :: DiffLayer{ONNXLinear{S1},ONN i_2 = 1 while i_d <= length(input_zono.∂Z.generator_ids) && i_2 <= length(input_zono.Z₂.generator_ids) if input_zono.∂Z.generator_ids[i_d] == input_zono.Z₂.generator_ids[i_2] - new_g = zeros(Float64, size(diff_layer_output.W,1), size(input_zono.∂Z.Gs[i_d],2)) + new_g = zeros(Float64, size(diff_layer_output_W,1), size(input_zono.∂Z.Gs[i_d],2)) push!(generators, new_g) push!(generator_ids, input_zono.∂Z.generator_ids[i_d]) i_d += 1 i_2 += 1 elseif input_zono.∂Z.generator_ids[i_d] < input_zono.Z₂.generator_ids[i_2] - new_g = zeros(Float64, size(diff_layer_output.W,1), size(input_zono.∂Z.Gs[i_d],2)) + new_g = zeros(Float64, size(diff_layer_output_W,1), size(input_zono.∂Z.Gs[i_d],2)) push!(generators, new_g) push!(generator_ids, input_zono.∂Z.generator_ids[i_d]) i_d += 1 else # input_zono.∂Z.generator_ids[i_d] > input_zono.Z₂.generator_ids[i_2] - new_g = zeros(Float64, size(diff_layer_output.W,1), size(input_zono.Z₂.Gs[i_2],2)) + new_g = zeros(Float64, size(diff_layer_output_W,1), size(input_zono.Z₂.Gs[i_2],2)) push!(generators, new_g) push!(generator_ids, input_zono.Z₂.generator_ids[i_2]) i_2 += 1 end end while i_d <= length(input_zono.∂Z.generator_ids) - new_g = zeros(Float64, size(diff_layer_output.W,1), size(input_zono.∂Z.Gs[i_d],2)) + new_g = zeros(Float64, size(diff_layer_output_W,1), size(input_zono.∂Z.Gs[i_d],2)) push!(generators, new_g) push!(generator_ids, input_zono.∂Z.generator_ids[i_d]) i_d += 1 end while i_2 <= length(input_zono.Z₂.generator_ids) - new_g = zeros(Float64, size(diff_layer_output.W,1), size(input_zono.Z₂.Gs[i_2],2)) + new_g = zeros(Float64, size(diff_layer_output_W,1), size(input_zono.Z₂.Gs[i_2],2)) push!(generators, new_g) push!(generator_ids, input_zono.Z₂.generator_ids[i_2]) i_2 += 1 end ∂Z = Zonotope(generators, - zeros(Float64, size(diff_layer_output.W,1)), influence, generator_ids, owned_generator_id === nothing ? nothing : find_index_position(generator_ids, owned_generator_id)) + zeros(Float64, size(diff_layer_output_W,1)), influence, generator_ids, owned_generator_id === nothing ? nothing : find_index_position(generator_ids, owned_generator_id)) Z = CachedZonotope( DiffZonotope( Z₁, diff --git a/test/runtests.jl b/test/runtests.jl index de2ceade..db75eb6b 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -1,6 +1,10 @@ using Test +using VNNLib +using VNNLib.OnnxParser: Node, ONNXLinear, ONNXRelu, OnnxNet + using VeryDiff +using VeryDiff.Definitions: executable_network VeryDiff.USE_DIFFZONO[] = true VeryDiff.NEW_HEURISTIC[] = true diff --git a/test/unit/propagation/dense.jl b/test/unit/propagation/dense.jl index 83d1ccf3..c88ca0e4 100644 --- a/test/unit/propagation/dense.jl +++ b/test/unit/propagation/dense.jl @@ -91,30 +91,31 @@ using Random @testset "Sampled Points Within Output Bounds" begin input_dim = 10 - num_layers = rand(5:15) num_samples = 20_000 tolerance = 1e-4 + + for depth in 1:15 - # Create layer dimensions (same for both networks) - layer_dims = [rand(20:100) for _ in 1:(num_layers-1)] - push!(layer_dims, 10) # Output dimension is 10 - - @debug "Creating networks..." - # Create networks with same structure - N1, N2 = make_dense_pair(input_dim, layer_dims) - depth = length(layer_dims) + # Create layer dimensions (same for both networks) + layer_dims = [rand(20:100) for _ in 1:depth] + push!(layer_dims, 10) # Output dimension is 10 + + @debug "Creating networks..." + # Create networks with same structure + N1, N2 = make_dense_pair(input_dim, layer_dims) + depth = length(layer_dims) - # Create input bounds [-1, 1]^input_dim - low = fill(-1.0, input_dim) - high = fill(1.0, input_dim) - # Sample points from input space and propagate through both networks - input_samples = sample_points_in_hypercube(low, high, num_samples) + # Create input bounds [-1, 1]^input_dim + low = fill(-1.0, input_dim) + high = fill(1.0, input_dim) + # Sample points from input space and propagate through both networks + input_samples = sample_points_in_hypercube(low, high, num_samples) + + + N_gemini = GeminiNetwork(N1, N2) - for l in 1:depth - @info "Checking up to layer $l / $depth" - N1_partial = Network(N1.layers[1:l]) - N2_partial = Network(N2.layers[1:l]) - N_gemini = GeminiNetwork(N1_partial, N2_partial) + N1 = executable_network(N1) + N2 = executable_network(N2) # Create VerificationTask verification_task = create_verification_task(low, high) @@ -146,10 +147,10 @@ using Random @assert Zin2.c .+ Zin2.Gs[1]*x ≈ x atol=1e-8 # Propagate through N1 - y1 = N1_partial(x) + y1 = N1(x) # Propagate through N2 - y2 = N2_partial(x) + y2 = N2(x) Zout = prop_state.zono_storage.zonotopes[end].zonotope @test Zout.Z₁.c .+ Zout.Z₁.Gs[1]*x ≈ y1 atol=1e-8 diff --git a/test/unit/propagation/dense_zero_diff.jl b/test/unit/propagation/dense_zero_diff.jl index e18ce14c..14340e35 100644 --- a/test/unit/propagation/dense_zero_diff.jl +++ b/test/unit/propagation/dense_zero_diff.jl @@ -97,29 +97,29 @@ using Random num_samples = 20_000 tolerance = 1e-4 - # Create layer dimensions (same for both networks) - layer_dims = [rand(20:100) for _ in 1:(num_layers-1)] - push!(layer_dims, 10) # Output dimension is 10 - depth = length(layer_dims) - - # Create networks with same structure and identical weights - N1, N2 = make_dense_pair(input_dim, layer_dims; identical=true) - - # Create input bounds [-1, 1]^input_dim - low = fill(-1.0, input_dim) - high = fill(1.0, input_dim) + for depth in 1:15 + # Create layer dimensions (same for both networks) + layer_dims = [rand(20:100) for _ in 1:depth] + push!(layer_dims, 10) # Output dimension is 10 + depth = length(layer_dims) + + # Create networks with same structure and identical weights + N1, N2 = make_dense_pair(input_dim, layer_dims; identical=true) + + # Create input bounds [-1, 1]^input_dim + low = fill(-1.0, input_dim) + high = fill(1.0, input_dim) + + # Sample points from input space and propagate through both networks + # Secondary dimensions share same span as primary + sec_low = fill(-execution_difference, input_dim * 2) + sec_high = fill(execution_difference, input_dim * 2) + input_samples = sample_points_in_hypercube(low, high, num_samples; secondary_low=sec_low, secondary_high=sec_high) - # Sample points from input space and propagate through both networks - # Secondary dimensions share same span as primary - sec_low = fill(-execution_difference, input_dim * 2) - sec_high = fill(execution_difference, input_dim * 2) - input_samples = sample_points_in_hypercube(low, high, num_samples; secondary_low=sec_low, secondary_high=sec_high) + N_gemini = GeminiNetwork(N1, N2) - for l in 1:depth - @info "Checking up to layer $l / $depth" - N1_partial = Network(N1.layers[1:l]) - N2_partial = Network(N2.layers[1:l]) - N_gemini = GeminiNetwork(N1_partial, N2_partial) + N1 = executable_network(N1) + N2 = executable_network(N2) # Create VerificationTask with secondary distances to capture zero difference verification_task = create_verification_task(low, high; with_secondary=true, secondary_scale=execution_difference) @@ -162,10 +162,10 @@ using Random @assert Zin2.c .+ Zin2.Gs[1]*prim .+ Zin2.Gs[2]*sec2 ≈ x2 atol=1e-8 # Propagate through N1 - y1 = N1_partial(x1) + y1 = N1(x1) # Propagate through N2 - y2 = N2_partial(x2) + y2 = N2(x2) Zout = prop_state.zono_storage.zonotopes[end].zonotope @test Zout.Z₁.c .+ Zout.Z₁.Gs[1]*prim .+ Zout.Z₁.Gs[2]*sec1 ≈ y1 atol=1e-8 diff --git a/test/unit/propagation/relu.jl b/test/unit/propagation/relu.jl index cf952d8e..5520cf5d 100644 --- a/test/unit/propagation/relu.jl +++ b/test/unit/propagation/relu.jl @@ -92,30 +92,29 @@ using Random @testset "Sampled Points Within Output Bounds" begin input_dim = 10 - num_layers = rand(5:15) num_samples = 20_000 tolerance = 1e-4 - # Create layer dimensions (same for both networks) - layer_dims = [rand(20:100) for _ in 1:(num_layers-1)] - push!(layer_dims, 10) # Output dimension is 10 - - @debug "Creating networks..." - # Create networks with same structure - N1, N2 = make_dense_pair(input_dim, layer_dims;relu=true) - depth = length(layer_dims) + for depth in 1:15 + # Create layer dimensions (same for both networks) + layer_dims = [rand(20:100) for _ in 1:depth] + push!(layer_dims, 10) # Output dimension is 10 + + @debug "Creating networks..." + # Create networks with same structure + N1, N2 = make_dense_pair(input_dim, layer_dims;relu=true) + depth = length(layer_dims) - # Create input bounds [-1, 1]^input_dim - low = fill(-1.0, input_dim) - high = fill(1.0, input_dim) - # Sample points from input space and propagate through both networks - input_samples = sample_points_in_hypercube(low, high, num_samples) + # Create input bounds [-1, 1]^input_dim + low = fill(-1.0, input_dim) + high = fill(1.0, input_dim) + # Sample points from input space and propagate through both networks + input_samples = sample_points_in_hypercube(low, high, num_samples) + + N_gemini = GeminiNetwork(N1, N2) - for l in 1:depth - @info "Checking up to layer $l / $depth" - N1_partial = Network(N1.layers[1:l]) - N2_partial = Network(N2.layers[1:l]) - N_gemini = GeminiNetwork(N1_partial, N2_partial) + N1 = executable_network(N1) + N2 = executable_network(N2) # Create VerificationTask verification_task = create_verification_task(low, high) @@ -147,10 +146,10 @@ using Random @assert Zin2.c .+ Zin2.Gs[1]*x ≈ x atol=1e-8 # Propagate through N1 - y1 = N1_partial(x) + y1 = N1(x) # Propagate through N2 - y2 = N2_partial(x) + y2 = N2(x) # Now we may have additional constraints so we must check Zonotope containment # Sum up additional generators diff --git a/test/unit/propagation/utils.jl b/test/unit/propagation/utils.jl index 6de5a07c..75b12fad 100644 --- a/test/unit/propagation/utils.jl +++ b/test/unit/propagation/utils.jl @@ -6,10 +6,14 @@ using Random create_random_dense_network(input_dim::Int, layer_dims::Vector{Int}) Create a randomized neural network with only Dense layers using the provided layer dimensions. +Returns both a Network and an OnnxNet representation. """ function create_random_dense_network(input_dim::Int, layer_dims::Vector{Int}; relu=false) - layers = Layer[] + layers = Vector{Node{String}}() cur_dim = input_dim + layer_count = 0 + prev_output_id = "network_input" + for new_dim in layer_dims W = 0.1*randn(Float64, (new_dim, cur_dim)) b = 0.1*randn(Float64, new_dim) @@ -20,44 +24,73 @@ function create_random_dense_network(input_dim::Int, layer_dims::Vector{Int}; re # Set some components to zero zero_one_components = randn(size(W)) .< -3.0 W[zero_one_components] .= 0.0 - push!(layers, Dense(W, b)) + layer_count += 1 + input_id = prev_output_id + output_id = "output_$layer_count" + push!(layers, ONNXLinear([input_id], [output_id], "dense_$layer_count", W, b)) + prev_output_id = output_id if relu - push!(layers, ReLU()) + layer_count += 1 + relu_input_id = output_id + relu_output_id = "output_$layer_count" + push!(layers, ONNXRelu([relu_input_id], [relu_output_id], "relu_$layer_count")) + prev_output_id = relu_output_id end cur_dim = new_dim end - return Network(layers) + + # Create OnnxNet with appropriate input/output shapes and node structure + node_dict = Dict{String, Node{String}}() + for layer in layers + node_dict[layer.name] = layer + end + + start_nodes = ["dense_1"] + final_nodes = [layers[end].name] + input_shapes = Dict("network_input" => (input_dim,)) + output_shapes = Dict(layers[end].outputs[1] => (layer_dims[end],)) + + onnx_net = OnnxNet(layers, start_nodes, final_nodes, input_shapes, output_shapes) + + return onnx_net end """ - create_randon_network_mutant(network :: Network) + create_random_network_mutant(onnx_net :: OnnxNet) -Create a mutated version of the provided network layers by slightly perturbing weights and biases according to different strategies. +Create a mutated version of the provided ONNX network by mutating every ONNXLinear layer. """ -function create_random_network_mutant(network :: Network) - new_layers = Layer[] - for layer in network.layers - push!(new_layers, create_random_layer_mutant(layer)) +function create_random_network_mutant(onnx_net :: OnnxNet) + new_layers = Vector{Node{String}}() + for (node_name, node) in onnx_net.nodes + push!(new_layers, create_random_layer_mutant(node)) end - return Network(new_layers) + + # Reconstruct OnnxNet with mutated layers + start_nodes = onnx_net.start_nodes + final_nodes = onnx_net.final_nodes + input_shapes = onnx_net.input_shapes + output_shapes = onnx_net.output_shapes + + return OnnxNet(new_layers, start_nodes, final_nodes, input_shapes, output_shapes) end """ create_random_layer_mutant(layer :: Layer) Create a mutated version of the provided layer by slightly perturbing weights and biases according to different strategies. """ -function create_random_layer_mutant(layer :: Dense) +function create_random_layer_mutant(layer :: ONNXLinear{String}) mutation_type = rand(1:4) if mutation_type == 1 @debug "Independent layer" # New random weights and biases - W_new = 0.1*randn(Float64, size(layer.W)) - b_new = 0.1*randn(Float64, size(layer.b)) + W_new = 0.1*randn(Float64, size(layer.dense.weight)) + b_new = 0.1*randn(Float64, size(layer.dense.bias)) elseif mutation_type == 2 @debug "Zeroed components" # Set some weights / biases to zero - W_new = deepcopy(layer.W) - b_new = deepcopy(layer.b) + W_new = deepcopy(layer.dense.weight) + b_new = deepcopy(layer.dense.bias) W_mask = randn(size(W_new)) .< -2.0 b_mask = randn(size(b_new)) .< -2.0 W_new[W_mask] .= 0.0 @@ -65,35 +98,53 @@ function create_random_layer_mutant(layer :: Dense) elseif mutation_type == 3 @debug "Pruned rows" # Prune some rows - W_new = deepcopy(layer.W) - b_new = deepcopy(layer.b) + W_new = deepcopy(layer.dense.weight) + b_new = deepcopy(layer.dense.bias) row_mask = randn(size(W_new, 1)) .< -2.0 W_new[row_mask, :] .= 0.0 b_new[row_mask] .= 0.0 elseif mutation_type == 4 @debug "Small perturbation" # Small random perturbation - W_new = layer.W .+ 0.01*randn(Float64, size(layer.W)) - b_new = layer.b .+ 0.01*randn(Float64, size(layer.b)) + W_new = layer.dense.weight .+ 0.01*randn(Float64, size(layer.dense.weight)) + b_new = layer.dense.bias .+ 0.01*randn(Float64, size(layer.dense.bias)) else error("Unknown mutation type") end - return Dense(W_new, b_new) + return ONNXLinear(layer.inputs, layer.outputs, layer.name, W_new, b_new, transpose=layer.transpose) end -function create_random_layer_mutant(layer :: ReLU) - return deepcopy(ReLU()) +function create_random_layer_mutant(layer :: ONNXRelu{String}) + return deepcopy(layer) end """ make_dense_pair(input_dim::Int, layer_dims::Vector{Int}; identical::Bool=false) Create two networks sharing the same architecture. When `identical` is true, the weights/biases are identical. +Returns tuples of (Network, OnnxNet) pairs. """ function make_dense_pair(input_dim::Int, layer_dims::Vector{Int}; identical::Bool=false, relu=false) - N1 = create_random_dense_network(input_dim, layer_dims; relu=relu) - N2 = identical ? deepcopy(N1) : create_random_network_mutant(N1) - return N1, N2 + N1_onnx = create_random_dense_network(input_dim, layer_dims; relu=relu) + if identical + N2_onnx = deepcopy(N1_onnx) + else + N2_onnx = create_random_network_mutant(N1_onnx) + end + return N1_onnx, N2_onnx +end + +""" + create_mutant_layers(layers::Vector{Node{String}}) + +Helper function to create mutated versions of layers. +""" +function create_mutant_layers(layers::Vector{Node{String}}) + new_layers = Vector{Node{String}}() + for layer in layers + push!(new_layers, create_random_layer_mutant(layer)) + end + return new_layers end """ From 36f0faa47df7fbb59ce52507230532bb2507af4f Mon Sep 17 00:00:00 2001 From: Samuel Teuber Date: Mon, 19 Jan 2026 20:09:02 +0100 Subject: [PATCH 4/5] add constant fix --- src/Definitions/Definitions.jl | 2 +- src/Definitions/Network.jl | 10 +- src/Transformers/Diff_Transformers.jl | 41 ++++ src/Transformers/Init.jl | 25 +- src/Transformers/Single_Transformers.jl | 9 + src/Transformers/Transformers.jl | 2 +- src/Transformers/Util.jl | 12 +- test/compare_fuzz.jl | 305 ++++++++++++++++++++++++ test/runtests.jl | 2 +- test/unit/propagation/main.jl | 7 +- test/unit/propagation/relu_addConst.jl | 212 ++++++++++++++++ test/unit/propagation/utils.jl | 101 +++++++- 12 files changed, 700 insertions(+), 28 deletions(-) create mode 100644 test/compare_fuzz.jl create mode 100644 test/unit/propagation/relu_addConst.jl diff --git a/src/Definitions/Definitions.jl b/src/Definitions/Definitions.jl index 0bc32ba8..ee99a529 100644 --- a/src/Definitions/Definitions.jl +++ b/src/Definitions/Definitions.jl @@ -4,7 +4,7 @@ using LinearAlgebra using Statistics using VNNLib -using VNNLib.OnnxParser: Node, ONNXLinear, ONNXRelu +using VNNLib.OnnxParser: Node, ONNXLinear, ONNXRelu, ONNXAddConst using VeryDiff diff --git a/src/Definitions/Network.jl b/src/Definitions/Network.jl index 28f1a040..9fe3dd15 100644 --- a/src/Definitions/Network.jl +++ b/src/Definitions/Network.jl @@ -119,10 +119,6 @@ function sort_mirror_network(layers :: Vector{OnnxLayer{LayerIdT}}, io_map :: Di return sorted_layers end -function mk_dense(W::AbstractMatrix{Float64}, b::AbstractVector{Float64}) - return ONNXLinear{Int64}(Dense(W, b, identity)) -end - struct GeminiNetwork{LayerIdT} inputs :: Dict{LayerIdT, Int64} @@ -160,6 +156,12 @@ struct GeminiNetwork{LayerIdT} diff_l = ONNXLinear(l1.node.inputs, l1.node.outputs, l1.node.name, new_W, new_b) end push!(diff_layers, DiffLayer(l1.layer_index, l1.input_ids, l1.output_ids, l1.node, diff_l, l2.node)) + elseif typeof(l1.node) == ONNXAddConst{LayerIdT} + b1 = l1.node.c + b2 = l2.node.c + new_b = b1 .- b2 + diff_l = ONNXAddConst(l1.node.inputs, l1.node.outputs, l1.node.name, new_b) + push!(diff_layers, DiffLayer(l1.layer_index, l1.input_ids, l1.output_ids, l1.node, diff_l, l2.node)) else push!(diff_layers, DiffLayer(l1.layer_index, l1.input_ids, l1.output_ids, l1.node, l1.node, l2.node)) end diff --git a/src/Transformers/Diff_Transformers.jl b/src/Transformers/Diff_Transformers.jl index a5786050..5cc6692a 100644 --- a/src/Transformers/Diff_Transformers.jl +++ b/src/Transformers/Diff_Transformers.jl @@ -52,6 +52,47 @@ function propagate_layer!( propagate_layer!(Zout.Z₂, L2, Zin.Z₂) end +function propagate_layer!( + ZoutRefVec :: Vector{CachedZonotope}, + Ls :: DiffLayer{ + ONNXAddConst{S1}, + ONNXAddConst{S2}, + ONNXAddConst{S3}}, + inputs :: Vector{DiffZonotope}; + bounds_cache :: Union{Nothing,BoundsCache}=nothing) where {S1, S2, S3} + @assert length(inputs) == 1 "Dense layer should have exactly one input zonotope" + @assert length(ZoutRefVec) == 1 "Dense layer should have exactly one output zonotope" + ZoutRef = ZoutRefVec[1] + Zin = inputs[1] + i_out = 1 + ∂g_dims = Int64[] + resize!(∂g_dims, length(ZoutRef.zonotope_proto.∂Z.Gs)) + for i_out in 1:length(∂g_dims) + res = attempt_find_index_position(Zin.∂Z.generator_ids, ZoutRef.zonotope_proto.∂Z.generator_ids[i_out]) + if res > 0 + ∂g_dims[i_out] = size(Zin.∂Z.Gs[res],2) + else + res = find_index_position(Zin.Z₂.generator_ids, ZoutRef.zonotope_proto.∂Z.generator_ids[i_out]) + ∂g_dims[i_out] = size(Zin.Z₂.Gs[res],2) + end + end + Zout = get_zonotope!(ZoutRef, size.(Zin.Z₁.Gs,2), size.(Zin.Z₂.Gs,2), ∂g_dims) + L1 = get_layer1(Ls) + ∂L = get_diff_layer(Ls) + ∂L_b = ∂L.c + L2 = get_layer2(Ls) + if VeryDiff.USE_DIFFZONO[] + # @debug "IDs of Output Zonotope Generators: $(Zout.∂Z.generator_ids)" + ∂indices = intersect_indices(Zout.∂Z.generator_ids, Zin.∂Z.generator_ids) + for (i, g) in zip(∂indices, Zin.∂Z.Gs) + Zout.∂Z.Gs[i] .= g + end + Zout.∂Z.c .= Zin.∂Z.c .+ ∂L_b + end + propagate_layer!(Zout.Z₁, L1, Zin.Z₁) + propagate_layer!(Zout.Z₂, L2, Zin.Z₂) +end + function propagate_layer!( ZoutRefVec :: Vector{CachedZonotope}, Ls :: DiffLayer{ diff --git a/src/Transformers/Init.jl b/src/Transformers/Init.jl index 2670ae53..3b6355cd 100644 --- a/src/Transformers/Init.jl +++ b/src/Transformers/Init.jl @@ -109,8 +109,27 @@ function init_layer!(PS :: PropState, diff_layer :: DiffLayer{ONNXLinear{S1}, Ze L2_W = L2.dense.weight @assert size(L1_W,2) == size(input_zono.Z₁.Gs[1],1) "Input dimension mismatch for Dense layer 1" @assert size(L2_W,2) == size(input_zono.Z₂.Gs[1],1) "Input dimension mismatch for Dense layer 2" - Z₁, Z₂ = init_layer_dense_z1_z2(L1, L2, input_zono, input_zono_cache, diff_layer.layer_idx) - ∂Z = init_zonotope(L2, input_zono.∂Z, input_zono.∂Z.influence, input_zono.∂Z.owned_generators) + Z₁, Z₂ = init_layer_dense_z1_z2(size(L1_W,1), input_zono, input_zono_cache, diff_layer.layer_idx) + ∂Z = init_zonotope(size(L1_W,1), input_zono.∂Z, input_zono.∂Z.influence, input_zono.∂Z.owned_generators) + Z =CachedZonotope( + DiffZonotope( + Z₁, + Z₂, + ∂Z + ), + nothing + ) + init_default_zono(Z) + PS.zono_storage.zonotopes[output_positions[1]] = Z +end + +function init_layer!(PS :: PropState, diff_layer :: DiffLayer{ONNXAddConst{S1},ONNXAddConst{S2},ONNXAddConst{S3}}, inputs :: Vector{CachedZonotope}, output_positions :: Vector{Int64}) where {S1, S2, S3} + @assert length(inputs) == 1 "Dense DiffLayer should have exactly one input" + @assert length(output_positions) == 1 "Dense DiffLayer should have exactly one output" + input_zono_cache = inputs[1] + input_zono = get_zonotope(input_zono_cache) + Z₁, Z₂ = init_layer_dense_z1_z2(length(input_zono.Z₁.c), input_zono, input_zono_cache, diff_layer.layer_idx) + ∂Z = init_zonotope(length(input_zono.Z₁.c), input_zono.∂Z, input_zono.∂Z.influence, input_zono.∂Z.owned_generators) Z =CachedZonotope( DiffZonotope( Z₁, @@ -136,7 +155,7 @@ function init_layer!(PS :: PropState, diff_layer :: DiffLayer{ONNXLinear{S1},ONN diff_layer_output_W = diff_layer_output.dense.weight @assert size(L1_W,2) == size(input_zono.Z₁.Gs[1],1) "Input dimension mismatch for Dense layer 1" @assert size(L2_W,2) == size(input_zono.Z₂.Gs[1],1) "Input dimension mismatch for Dense layer 2" - Z₁, Z₂ = init_layer_dense_z1_z2(L1, L2, input_zono, input_zono_cache, diff_layer.layer_idx) + Z₁, Z₂ = init_layer_dense_z1_z2(size(L1_W,1), input_zono, input_zono_cache, diff_layer.layer_idx) # Instantiate ∂Z influence = input_zono.∂Z.influence if diff_layer.layer_idx == input_zono_cache.first_usage && !isnothing(input_zono.∂Z.owned_generators) diff --git a/src/Transformers/Single_Transformers.jl b/src/Transformers/Single_Transformers.jl index fce3e219..55da8731 100644 --- a/src/Transformers/Single_Transformers.jl +++ b/src/Transformers/Single_Transformers.jl @@ -16,6 +16,15 @@ function propagate_layer!(ZoutRef :: Zonotope, L :: ONNXLinear{S1}, Zin :: Zonot ZoutRef.c .+= L.dense.bias end +function propagate_layer!(ZoutRef :: Zonotope, L :: ONNXAddConst{S1}, Zin :: Zonotope) where {S1} + # Zout must have exactly the same ids as Zin + # @assert all(ZoutRef.generator_ids .== Zin.generator_ids) "Zonotope generator IDs do not match during Dense propagation!" + for i in 1:length(Zin.Gs) + ZoutRef.Gs[i] .= Zin.Gs[i] + end + ZoutRef.c .= Zin.c .+ L.c +end + function get_slope(l,u, alpha) if u <= 0 return 0.0 diff --git a/src/Transformers/Transformers.jl b/src/Transformers/Transformers.jl index 384d78ef..bfd53202 100644 --- a/src/Transformers/Transformers.jl +++ b/src/Transformers/Transformers.jl @@ -3,7 +3,7 @@ module Transformers using LinearAlgebra using VNNLib -using VNNLib.OnnxParser: ONNXLinear, ONNXRelu +using VNNLib.OnnxParser: ONNXLinear, ONNXRelu, ONNXAddConst using TimerOutputs diff --git a/src/Transformers/Util.jl b/src/Transformers/Util.jl index ff8e7dbf..a97daa87 100644 --- a/src/Transformers/Util.jl +++ b/src/Transformers/Util.jl @@ -1,16 +1,16 @@ -function init_zonotope(layer :: ONNXLinear{S}, input :: Zonotope, influence::Union{Vector{Matrix{Float64}},Nothing}, owned_generators :: Union{Int64, Nothing}) where {S} +function init_zonotope(output_dim :: Int, input :: Zonotope, influence::Union{Vector{Matrix{Float64}},Nothing}, owned_generators :: Union{Int64, Nothing}) # Compute new generators generators = Vector{Matrix{Float64}}() generator_ids = deepcopy(input.generator_ids) for g in input.Gs - new_g = zeros(Float64, size(layer.dense.weight,1), size(g,2)) + new_g = zeros(Float64, output_dim, size(g,2)) push!(generators, new_g) end - c = zeros(Float64, size(layer.dense.weight,1)) + c = zeros(Float64, output_dim) return Zonotope(generators, c, influence, generator_ids, owned_generators) end -function init_layer_dense_z1_z2(L1 :: ONNXLinear{S1}, L2 :: ONNXLinear{S2}, input_zono :: DiffZonotope, input_zono_cache :: CachedZonotope, layer_idx :: Int64) :: Tuple{Zonotope,Zonotope} where {S1,S2} +function init_layer_dense_z1_z2(output_dim :: Int, input_zono :: DiffZonotope, input_zono_cache :: CachedZonotope, layer_idx :: Int64) :: Tuple{Zonotope,Zonotope} # Instantiate Z₁ # Dense Layer can reuse influence matrix from input (nocopy) influence = input_zono.Z₁.influence @@ -19,7 +19,7 @@ function init_layer_dense_z1_z2(L1 :: ONNXLinear{S1}, L2 :: ONNXLinear{S2}, inpu else owned_generators = nothing end - Z₁ = init_zonotope(L1, input_zono.Z₁, influence, owned_generators) + Z₁ = init_zonotope(output_dim, input_zono.Z₁, influence, owned_generators) # Instantiate Z₂ influence = input_zono.Z₂.influence if layer_idx == input_zono_cache.first_usage @@ -27,7 +27,7 @@ function init_layer_dense_z1_z2(L1 :: ONNXLinear{S1}, L2 :: ONNXLinear{S2}, inpu else owned_generators = nothing end - Z₂ = init_zonotope(L2, input_zono.Z₂, influence, owned_generators) + Z₂ = init_zonotope(output_dim, input_zono.Z₂, influence, owned_generators) return Z₁, Z₂ end diff --git a/test/compare_fuzz.jl b/test/compare_fuzz.jl new file mode 100644 index 00000000..7d2c3b11 --- /dev/null +++ b/test/compare_fuzz.jl @@ -0,0 +1,305 @@ +""" +Comparison fuzzer that runs Julia and PyTorch implementations in parallel +and verifies they produce matching results layer-by-layer. +""" + +using VeryDiff +import VeryDiff: VerificationTask, PropState, prepare_prop_state!, propagate!, GeminiNetwork, Zonotope, DiffZonotope, zono_bounds, reset_ps!, get_layers +using Test +using LinearAlgebra +using Random +using PyCall +import VNNLib: NNLoader + +# Include utility functions +include("unit/propagation/utils.jl") + +# Import PyTorch implementation +pushfirst!(PyVector(pyimport("sys")."path"), joinpath(@__DIR__, "..", "torch")) +py_src = pyimport("src") + +""" + julia_to_python_network(network::VeryDiff.Network) + +Convert Julia network to PyTorch network. +""" +function julia_to_python_network(network::VeryDiff.Network) + torch = pyimport("torch") + nn = pyimport("torch.nn") + + py_layers = PyObject[] + for layer in network.layers + if isa(layer, NNLoader.Dense) + # Create PyTorch Linear layer + in_features = size(layer.W, 2) + out_features = size(layer.W, 1) + py_layer = nn.Linear(in_features, out_features) + + # Copy weights (note: PyTorch uses transposed convention) + py_layer.weight.data = torch.from_numpy(collect(layer.W)) + py_layer.bias.data = torch.from_numpy(collect(layer.b)) + + push!(py_layers, py_layer) + elseif isa(layer, NNLoader.ReLU) + push!(py_layers, nn.ReLU()) + else + error("Unsupported layer type: $(typeof(layer))") + end + end + + return nn.Sequential(py_layers...) +end + +""" + julia_zonotope_to_python(Z::Zonotope) + +Convert Julia Zonotope to Python Zonotope. +""" +function julia_zonotope_to_python(Z::Zonotope) + torch = pyimport("torch") + + # Convert generator matrices + py_Gs = [torch.from_numpy(collect(G)) for G in Z.Gs] + + # Convert center + py_c = torch.from_numpy(collect(Z.c)) + + # Convert generator IDs + py_generator_ids = py_src.SortedVector(collect(Z.generator_ids.data)) + + # Convert owned generators + py_owned = isnothing(Z.owned_generators) ? nothing : (Z.owned_generators - 1) # Python 0-indexed + + return py_src.Zonotope(py_Gs, py_c, py_generator_ids, py_owned) +end + +""" + julia_diffzonotope_to_python(DZ::DiffZonotope) + +Convert Julia DiffZonotope to Python DiffZonotope. +""" +function julia_diffzonotope_to_python(DZ::DiffZonotope) + py_Z1 = julia_zonotope_to_python(DZ.Z₁) + py_Z2 = julia_zonotope_to_python(DZ.Z₂) + py_dZ = julia_zonotope_to_python(DZ.∂Z) + + return py_src.DiffZonotope(py_Z1, py_Z2, py_dZ) +end + +""" + python_zonotope_to_julia(py_Z) + +Convert Python Zonotope to Julia Zonotope. +""" +function python_zonotope_to_julia(py_Z) + # Convert generator matrices + Gs = AbstractMatrix{Float64}[py_Z.Gs[i].detach().numpy() for i in 1:(length(py_Z.Gs))] + + # Convert center + c = py_Z.c.detach().numpy() + + # Convert generator IDs + generator_ids = VeryDiff.Definitions.SortedVector{Int64}(collect(py_Z.generator_ids.data)) + + # Convert owned generators (Python is 0-indexed, Julia is 1-indexed) + owned = isnothing(py_Z.owned_generators) ? nothing : (py_Z.owned_generators + 1) + + return Zonotope(Gs, c, nothing, generator_ids, owned) +end + +""" + python_diffzonotope_to_julia(py_DZ) + +Convert Python DiffZonotope to Julia DiffZonotope. +""" +function python_diffzonotope_to_julia(py_DZ) + Z1 = python_zonotope_to_julia(py_DZ.Z1) + Z2 = python_zonotope_to_julia(py_DZ.Z2) + dZ = python_zonotope_to_julia(py_DZ.dZ) + + return DiffZonotope(Z1, Z2, dZ) +end + +""" + compare_zonotopes(Z_julia::Zonotope, Z_python, label::String; rtol=1e-5, atol=1e-6) + +Compare Julia and Python zonotopes and assert they match. +""" +function compare_zonotopes(Z_julia::Zonotope, Z_python, label::String; rtol=1e-5, atol=1e-6) + # Convert Python zonotope to Julia for comparison + Z_py_julia = python_zonotope_to_julia(Z_python) + + # Compare centers + @test isapprox(Z_julia.c, Z_py_julia.c, rtol=rtol, atol=atol) + if !(isapprox(Z_julia.c, Z_py_julia.c, rtol=rtol, atol=atol)) + @warn "$label: Centers differ" Z_julia.c Z_py_julia.c + end + + # Compare number of generators + @test length(Z_julia.Gs) == length(Z_py_julia.Gs) + if length(Z_julia.Gs) != length(Z_py_julia.Gs) + @warn "$label: Different number of generator matrices" length(Z_julia.Gs) length(Z_py_julia.Gs) + end + + # Compare generator matrices + for (i, (G_jl, G_py)) in enumerate(zip(Z_julia.Gs, Z_py_julia.Gs)) + @test isapprox(G_jl, G_py, rtol=rtol, atol=atol) + if !(isapprox(G_jl, G_py, rtol=rtol, atol=atol)) + @warn "$label: Generator $i differs" maximum(abs.(G_jl .- G_py)) + end + end + + # Compare generator IDs + @test Z_julia.generator_ids.data == Z_py_julia.generator_ids.data + if Z_julia.generator_ids.data != Z_py_julia.generator_ids.data + @warn "$label: Generator IDs differ" Z_julia.generator_ids.data Z_py_julia.generator_ids.data + end +end + +""" + compare_diffzonotopes(DZ_julia::DiffZonotope, DZ_python, label::String; rtol=1e-5, atol=1e-6) + +Compare Julia and Python differential zonotopes. +""" +function compare_diffzonotopes(DZ_julia::DiffZonotope, DZ_python, label::String; rtol=1e-5, atol=1e-6) + compare_zonotopes(DZ_julia.Z₁, DZ_python.Z1, "$label Z₁", rtol=rtol, atol=atol) + compare_zonotopes(DZ_julia.Z₂, DZ_python.Z2, "$label Z₂", rtol=rtol, atol=atol) + compare_zonotopes(DZ_julia.∂Z, DZ_python.dZ, "$label ∂Z", rtol=rtol, atol=atol) +end + +""" + test_layer_by_layer_comparison(;input_dim=5, num_layers=5, use_relu=true, rtol=1e-5, atol=1e-6) + +Test that Julia and Python implementations produce matching results layer-by-layer. +""" +function test_layer_by_layer_comparison(;input_dim=5, num_layers=5, use_relu=true, rtol=1e-5, atol=1e-6) + # Create layer dimensions + layer_dims = [rand(10:30) for _ in 1:(num_layers-1)] + push!(layer_dims, 10) # Output dimension + + @info "Testing network: input_dim=$input_dim, layers=$layer_dims, relu=$use_relu" + + # Create Julia networks + N1_jl, N2_jl = make_dense_pair(input_dim, layer_dims; relu=use_relu) + N_gemini_jl = GeminiNetwork(N1_jl, N2_jl) + + # Convert to Python + N1_py = julia_to_python_network(N1_jl) + N2_py = julia_to_python_network(N2_jl) + N_gemini_py = py_src.GeminiNetwork(N1_py, N2_py) + + # Create input bounds + low = fill(-1.0, input_dim) + high = fill(1.0, input_dim) + + # Create verification task (Julia) + verification_task = create_verification_task(low, high) + + # Initialize Julia propagation + prop_state_jl = PropState(true) + prepare_prop_state!(prop_state_jl, verification_task) + + # Initialize Python propagation + prop_state_py = py_src.PropState() + + # Get initial zonotope from Julia + initial_zono_jl = prop_state_jl.zono_storage.zonotopes[1].zonotope_proto + + # Convert to Python + initial_zono_py = julia_diffzonotope_to_python(initial_zono_jl) + + @info "Comparing initial zonotopes" + compare_diffzonotopes(initial_zono_jl, initial_zono_py, "Initial", rtol=rtol, atol=atol) + + # Propagate layer by layer + current_zono_jl = initial_zono_jl + current_zono_py = initial_zono_py + + diff_layers_jl = get_layers(N_gemini_jl) + diff_layers_py = N_gemini_py.diff_layers + + for (layer_idx, (diff_layer_jl, diff_layer_py)) in enumerate(zip(diff_layers_jl, diff_layers_py)) + @info "Propagating layer $layer_idx: $(typeof(diff_layer_jl))" + + # Julia propagation + if !VeryDiff.Transformers.has_layer(prop_state_jl, diff_layer_jl) + VeryDiff.Transformers.init_layer!(prop_state_jl, diff_layer_jl, [prop_state_jl.zono_storage.zonotopes[layer_idx]]) + end + + output_ref_jl = VeryDiff.Transformers.get_layer(prop_state_jl, diff_layer_jl) + input_zonotopes_jl = [current_zono_jl] + + # Get bounds cache + if haskey(prop_state_jl.task_bounds.bounds_cache, diff_layer_jl.layer_idx) + bounds_cache_jl = prop_state_jl.task_bounds.bounds_cache[diff_layer_jl.layer_idx] + else + bounds_cache_jl = VeryDiff.Definitions.BoundsCache() + prop_state_jl.task_bounds.bounds_cache[diff_layer_jl.layer_idx] = bounds_cache_jl + end + + VeryDiff.Transformers.propagate_layer!(output_ref_jl, diff_layer_jl, input_zonotopes_jl; bounds_cache=bounds_cache_jl) + current_zono_jl = VeryDiff.Transformers.get_zonotope(output_ref_jl) + + # Python propagation + if !prop_state_py.has_layer(layer_idx - 1) # Python is 0-indexed + output_ref_py = N_gemini_py._init_layer(diff_layer_py, current_zono_py, prop_state_py, layer_idx - 1) + prop_state_py.add_zonotope(output_ref_py) + else + output_ref_py = prop_state_py.get_layer_output(layer_idx - 1) + end + + bounds_cache_py = prop_state_py.get_bounds_cache(layer_idx - 1) + current_zono_py = diff_layer_py.forward(current_zono_py, output_ref_py, bounds_cache_py) + + # Compare outputs + @info "Comparing layer $layer_idx outputs" + compare_diffzonotopes(current_zono_jl, current_zono_py, "Layer $layer_idx", rtol=rtol, atol=atol) + end + + @info "Layer-by-layer comparison successful!" +end + +if "VERYDIFF_COMPARE_FUZZ" in keys(ENV) + iterations = parse(Int, ENV["VERYDIFF_COMPARE_FUZZ"]) + @testset "Julia-Python Comparison Fuzzer" begin + i = 1 + @info "Starting comparison fuzzing with $(iterations > 0 ? iterations : "infinite") iterations" + while true + ENV["VERYDIFF_TEST_SEED"] = string(rand(1:999999)) + cur_ts = @testset "Comparison iteration $i" begin + test_seed = parse(Int, ENV["VERYDIFF_TEST_SEED"]) + Random.seed!(test_seed) + @info "Comparison iteration $i with seed $test_seed" + + # Test with different configurations + @testset "Dense only network" begin + test_layer_by_layer_comparison( + input_dim=rand(3:8), + num_layers=rand(3:7), + use_relu=false, + rtol=1e-5, + atol=1e-6 + ) + end + + @testset "Dense + ReLU network" begin + test_layer_by_layer_comparison( + input_dim=rand(3:8), + num_layers=rand(3:7), + use_relu=true, + rtol=1e-5, + atol=1e-6 + ) + end + end + Test.print_test_results(cur_ts) + if iterations > 0 && i >= iterations + break + end + i += 1 + # Flush stdout and stderr to ensure logs are written in case of crash + flush(stdout) + flush(stderr) + end + end +end diff --git a/test/runtests.jl b/test/runtests.jl index db75eb6b..5a366978 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -1,7 +1,7 @@ using Test using VNNLib -using VNNLib.OnnxParser: Node, ONNXLinear, ONNXRelu, OnnxNet +using VNNLib.OnnxParser: Node, ONNXLinear, ONNXRelu, OnnxNet, ONNXAddConst using VeryDiff using VeryDiff.Definitions: executable_network diff --git a/test/unit/propagation/main.jl b/test/unit/propagation/main.jl index 7e34e8b0..f75136e0 100644 --- a/test/unit/propagation/main.jl +++ b/test/unit/propagation/main.jl @@ -1,4 +1,5 @@ include("utils.jl") -#include("dense.jl") -#include("dense_zero_diff.jl") -include("relu.jl") \ No newline at end of file +include("dense.jl") +include("dense_zero_diff.jl") +include("relu.jl") +include("relu_addConst.jl") \ No newline at end of file diff --git a/test/unit/propagation/relu_addConst.jl b/test/unit/propagation/relu_addConst.jl new file mode 100644 index 00000000..c9da91f9 --- /dev/null +++ b/test/unit/propagation/relu_addConst.jl @@ -0,0 +1,212 @@ +using VeryDiff +import VeryDiff: VerificationTask, PropState, prepare_prop_state!, propagate!, GeminiNetwork, Zonotope, zono_bounds, reset_ps! +using Test +using LinearAlgebra +using Random + +@testset "ReLU + AddConst + Dense Layer Propagation Tests" begin + @info "Starting ReLU + AddConst + Dense Layer Propagation Tests" + + if "VERYDIFF_TEST_SEED" in keys(ENV) + test_seed = parse(Int, ENV["VERYDIFF_TEST_SEED"]) + @info "Using VERYDIFF_TEST_SEED: $(test_seed)" + else + test_seed = rand(1:999999) + end + Random.seed!(test_seed) + @info "Test seed: $(test_seed)" + + @testset "Basic Gemini Network Propagation with AddConst" begin + input_dim = 5 + num_layers = rand(5:15) + + # Create layer dimensions (same for both networks) + layer_dims = [rand(20:50) for _ in 1:(num_layers-1)] + push!(layer_dims, 10) # Output dimension is 10 + + # Create two randomized networks with same structure, including ReLU and AddConst + N1, N2 = make_dense_pair(input_dim, layer_dims; relu=true, add_const=true) + + # Create Gemini Network + N_gemini = GeminiNetwork(N1, N2) + + # Create input bounds [-1, 1]^input_dim + low = fill(-1.0, input_dim) + high = fill(1.0, input_dim) + + # Create VerificationTask to encode the property + verification_task = create_verification_task(low, high) + + # Create PropState and initialize with verification task + prop_state = PropState(true) + prepare_prop_state!(prop_state, verification_task) + + # Propagate through Gemini Network + prop_state = propagate!(N_gemini, prop_state) + + # Extract output zonotopes + Zout = prop_state.zono_storage.zonotopes[end].zonotope + + # Basic checks + @test !isnothing(Zout) + @test size(Zout.Z₁.c) == (10,) # Output dimension should be 10 + @test size(Zout.Z₂.c) == (10,) + end + + @testset "Memory Allocation Reduction on Second Run with AddConst" begin + input_dim = 5 + num_layers = rand(5:15) + + # Create layer dimensions (same for both networks) + layer_dims = [rand(400:600) for _ in 1:(num_layers-1)] + push!(layer_dims, 10) # Output dimension is 10 + + # Create networks with same structure, including ReLU and AddConst + N1, N2 = make_dense_pair(input_dim, layer_dims; relu=true, add_const=true) + N_gemini = GeminiNetwork(N1, N2) + + # Create input bounds + low = fill(-1.0, input_dim) + high = fill(1.0, input_dim) + + # Create VerificationTask + verification_task = create_verification_task(low, high) + + # First propagation - counts allocations + prop_state_1 = PropState(true) + prepare_prop_state!(prop_state_1, verification_task) + res_1, time_1, alloc_1, _ = @timed propagate!(N_gemini, prop_state_1) + + # Second propagation - should allocate less + reset_ps!(prop_state_1) + prepare_prop_state!(prop_state_1, verification_task) + res_2, time_2, alloc_2, _ = @timed propagate!(N_gemini, prop_state_1) + + @info "First run allocations: $alloc_1 bytes, Second run allocations: $alloc_2 bytes" + @info "First run time: $time_1 s, Second run time: $time_2 s" + + # Check that second run allocates less (allowing for small variance) + # TODO: Renable when we don't run two versions of RELU + #@test alloc_2 < alloc_1 * 0.4 + end + + @testset "Sampled Points Within Output Bounds with AddConst" begin + input_dim = 10 + num_samples = 20_000 + tolerance = 1e-4 + + for depth in 1:15 + # Create layer dimensions (same for both networks) + layer_dims = [rand(20:100) for _ in 1:depth] + push!(layer_dims, 10) # Output dimension is 10 + + @debug "Creating networks..." + # Create networks with same structure, including ReLU and AddConst + N1, N2 = make_dense_pair(input_dim, layer_dims; relu=true, add_const=true) + depth = length(layer_dims) + + # Create input bounds [-1, 1]^input_dim + low = fill(-1.0, input_dim) + high = fill(1.0, input_dim) + # Sample points from input space and propagate through both networks + input_samples = sample_points_in_hypercube(low, high, num_samples) + + N_gemini = GeminiNetwork(N1, N2) + + N1 = executable_network(N1) + N2 = executable_network(N2) + + # Create VerificationTask + verification_task = create_verification_task(low, high) + + # Propagate zonotope through network + prop_state = PropState(true) + prepare_prop_state!(prop_state, verification_task) + prop_state = propagate!(N_gemini, prop_state) + @debug "Propagation through Gemini Network complete." + @debug "$(length(prop_state.zono_storage.zonotopes)) zonotopes in storage." + Zout = prop_state.zono_storage.zonotopes[end].zonotope + + # Get output bounds from zonotope + bounds_z1 = zono_bounds(Zout.Z₁) + bounds_z2 = zono_bounds(Zout.Z₂) + bounds_z∂ = zono_bounds(Zout.∂Z) + # @info "Output bounds for Network 1: $bounds_z1" + # @info "Output bounds for Network 2: $bounds_z2" + + n1_violations = 0 + n2_violations = 0 + diff_violations = 0 + for i in 1:num_samples + x = input_samples[:, i] + + Zin = prop_state.zono_storage.zonotopes[1].zonotope.Z₁ + @assert Zin.c .+ Zin.Gs[1]*x ≈ x atol=1e-8 + Zin2 = prop_state.zono_storage.zonotopes[1].zonotope.Z₂ + @assert Zin2.c .+ Zin2.Gs[1]*x ≈ x atol=1e-8 + + # Propagate through N1 + y1 = N1(x) + + # Propagate through N2 + y2 = N2(x) + + # Now we may have additional constraints so we must check Zonotope containment + # Sum up additional generators + Z1_range = sum(g->sum(abs, g, dims=2),Zout.Z₁.Gs[2:end];init=zeros(size(Zout.Z₁.c))) + Z2_range = sum(g->sum(abs, g, dims=2),Zout.Z₂.Gs[2:end];init=zeros(size(Zout.Z₂.c))) + input_component = Zout.Z₁.c .+ Zout.Z₁.Gs[1]*x + @test all(input_component .- Z1_range .<= y1 .+ 1e-8) + @test all(y1 .<= input_component .+ Z1_range .+ 1e-8) + if !all(input_component .- Z1_range .<= y1 .+ 1e-8) || !all(y1 .<= input_component .+ Z1_range .+ 1e-8) + @info "Output: $y1" + @info "Zonotope bounds (agnostic): $(bounds_z1)" + @info "Zonotope bounds (generator sum): $((input_component .- Z1_range, input_component .+ Z1_range))" + return + end + input_component2 = Zout.Z₂.c .+ Zout.Z₂.Gs[1]*x + @test all(input_component2 .- Z2_range .<= y2 .+ 1e-8) + @test all(y2 .<= input_component2 .+ Z2_range .+ 1e-8) + if !all(input_component2 .- Z2_range .<= y2 .+ 1e-8) || !all(y2 .<= input_component2 .+ Z2_range .+ 1e-8) + @info "Output: $y2" + @info "Zonotope bounds (agnostic): $(bounds_z2)" + @info "Zonotope bounds (generator sum): $((input_component2 .- Z2_range, input_component2 .+ Z2_range))" + return + end + # Difference Zonotope + diff_range = sum(g->sum(abs, g, dims=2),Zout.∂Z.Gs[2:end];init=zeros(size(Zout.∂Z.c))) + if length(Zout.∂Z.Gs) >= 1 + input_component_diff = Zout.∂Z.c .+ Zout.∂Z.Gs[1]*x + else + input_component_diff = Zout.∂Z.c + end + @test all((input_component_diff .- diff_range) .<= (y1 .- y2) .+ 1e-8) + @test all((y1 .- y2) .<= (input_component_diff .+ diff_range) .+ 1e-8) + + # Check if outputs are within bounds + for d in 1:10 + if y1[d] < bounds_z1[d, 1] - tolerance || y1[d] > bounds_z1[d, 2] + tolerance + n1_violations += 1 + end + + if y2[d] < bounds_z2[d, 1] - tolerance || y2[d] > bounds_z2[d, 2] + tolerance + n2_violations += 1 + end + if (y1[d] - y2[d]) < bounds_z∂[d, 1] - tolerance || (y1[d] - y2[d]) > bounds_z∂[d, 2] + tolerance + diff_violations += 1 + end + end + end + violations = n1_violations + n2_violations + diff_violations + @info "Found $violations bound violations out of $(num_samples * 30) total checks" + if violations > 0 + @info "Of which N1: $n1_violations" + @info "Of which N2: $n2_violations" + @info "Of which Diff: $diff_violations" + end + # All sampled points should be within bounds + @test violations == 0 + end + end + +end diff --git a/test/unit/propagation/utils.jl b/test/unit/propagation/utils.jl index 75b12fad..53065936 100644 --- a/test/unit/propagation/utils.jl +++ b/test/unit/propagation/utils.jl @@ -8,8 +8,9 @@ using Random Create a randomized neural network with only Dense layers using the provided layer dimensions. Returns both a Network and an OnnxNet representation. """ -function create_random_dense_network(input_dim::Int, layer_dims::Vector{Int}; relu=false) +function create_random_dense_network(input_dim::Int, layer_dims::Vector{Int}; relu=false, add_const=false) layers = Vector{Node{String}}() + layer_metadata = Vector{Tuple{String, Int}}() # Track (layer_name, mutation_type) for synchronization cur_dim = input_dim layer_count = 0 prev_output_id = "network_input" @@ -29,9 +30,24 @@ function create_random_dense_network(input_dim::Int, layer_dims::Vector{Int}; re output_id = "output_$layer_count" push!(layers, ONNXLinear([input_id], [output_id], "dense_$layer_count", W, b)) prev_output_id = output_id + + if add_const + layer_count += 1 + addconst_input_id = output_id + addconst_output_id = "output_$layer_count" + # Create a non-zero constant to add (random values in range [-0.5, 0.5]) + const_vec = 0.1 .* randn(Float64, new_dim) + # Ensure at least one non-zero element + if all(c ≈ 0 for c in const_vec) + const_vec[1] = 0.1 + end + push!(layers, ONNXAddConst([addconst_input_id], [addconst_output_id], "addconst_$layer_count", const_vec)) + prev_output_id = addconst_output_id + end + if relu layer_count += 1 - relu_input_id = output_id + relu_input_id = prev_output_id relu_output_id = "output_$layer_count" push!(layers, ONNXRelu([relu_input_id], [relu_output_id], "relu_$layer_count")) prev_output_id = relu_output_id @@ -59,11 +75,33 @@ end create_random_network_mutant(onnx_net :: OnnxNet) Create a mutated version of the provided ONNX network by mutating every ONNXLinear layer. +Synchronizes mutations between ONNXLinear and corresponding ONNXAddConst layers. """ function create_random_network_mutant(onnx_net :: OnnxNet) new_layers = Vector{Node{String}}() + # Store mutation types for each dense layer to sync with addconst + mutation_map = Dict{String, Int}() + + # First pass: determine mutation types for dense layers + for (node_name, node) in onnx_net.nodes + if node isa ONNXLinear{String} && startswith(node_name, "dense_") + mutation_map[node_name] = rand(1:4) + end + end + + # Second pass: apply mutations for (node_name, node) in onnx_net.nodes - push!(new_layers, create_random_layer_mutant(node)) + if node isa ONNXLinear{String} + mutation_type = get(mutation_map, node_name, rand(1:4)) + push!(new_layers, create_random_layer_mutant(node, mutation_type)) + elseif node isa ONNXAddConst{String} + # Find corresponding dense layer + dense_name = replace(node_name, "addconst_" => "dense_") + mutation_type = get(mutation_map, dense_name, rand(1:4)) + push!(new_layers, create_random_layer_mutant(node, mutation_type)) + else + push!(new_layers, create_random_layer_mutant(node)) + end end # Reconstruct OnnxNet with mutated layers @@ -76,11 +114,10 @@ function create_random_network_mutant(onnx_net :: OnnxNet) end """ - create_random_layer_mutant(layer :: Layer) -Create a mutated version of the provided layer by slightly perturbing weights and biases according to different strategies. + create_random_layer_mutant(layer :: ONNXLinear, mutation_type :: Int) +Create a mutated version of the provided layer using the specified mutation type. """ -function create_random_layer_mutant(layer :: ONNXLinear{String}) - mutation_type = rand(1:4) +function create_random_layer_mutant(layer :: ONNXLinear{String}, mutation_type :: Int) if mutation_type == 1 @debug "Independent layer" # New random weights and biases @@ -114,18 +151,64 @@ function create_random_layer_mutant(layer :: ONNXLinear{String}) return ONNXLinear(layer.inputs, layer.outputs, layer.name, W_new, b_new, transpose=layer.transpose) end +""" + create_random_layer_mutant(layer :: ONNXAddConst, mutation_type :: Int) +Create a mutated version of the AddConst layer using the specified mutation type (synchronized with linear layer). +""" +function create_random_layer_mutant(layer :: ONNXAddConst{String}, mutation_type :: Int) + if mutation_type == 1 + @debug "Independent AddConst layer" + # New random constant + c_new = 0.1 .* randn(Float64, size(layer.c)) + if all(c ≈ 0 for c in c_new) + c_new[1] = 0.1 + end + elseif mutation_type == 2 + @debug "Zeroed components in AddConst" + # Set some components to zero + c_new = deepcopy(layer.c) + c_mask = randn(size(c_new)) .< -2.0 + c_new[c_mask] .= 0.0 + elseif mutation_type == 3 + @debug "Zeroed all components in AddConst (pruned)" + # Zero out the entire constant + c_new = zeros(size(layer.c)) + elseif mutation_type == 4 + @debug "Small perturbation in AddConst" + # Small random perturbation + c_new = layer.c .+ 0.01*randn(Float64, size(layer.c)) + else + error("Unknown mutation type") + end + return ONNXAddConst(layer.inputs, layer.outputs, layer.name, c_new) +end + +""" + create_random_layer_mutant(layer :: Layer) +Create a mutated version of the provided layer by slightly perturbing weights and biases according to different strategies. +""" +function create_random_layer_mutant(layer :: ONNXLinear{String}) + mutation_type = rand(1:4) + return create_random_layer_mutant(layer, mutation_type) +end + function create_random_layer_mutant(layer :: ONNXRelu{String}) return deepcopy(layer) end +function create_random_layer_mutant(layer :: ONNXAddConst{String}) + mutation_type = rand(1:4) + return create_random_layer_mutant(layer, mutation_type) +end + """ make_dense_pair(input_dim::Int, layer_dims::Vector{Int}; identical::Bool=false) Create two networks sharing the same architecture. When `identical` is true, the weights/biases are identical. Returns tuples of (Network, OnnxNet) pairs. """ -function make_dense_pair(input_dim::Int, layer_dims::Vector{Int}; identical::Bool=false, relu=false) - N1_onnx = create_random_dense_network(input_dim, layer_dims; relu=relu) +function make_dense_pair(input_dim::Int, layer_dims::Vector{Int}; identical::Bool=false, relu=false, add_const=false) + N1_onnx = create_random_dense_network(input_dim, layer_dims; relu=relu, add_const=add_const) if identical N2_onnx = deepcopy(N1_onnx) else From c0f641a669961aec998a96956a5e640309526a55 Mon Sep 17 00:00:00 2001 From: Samuel Teuber Date: Mon, 19 Jan 2026 21:37:06 +0100 Subject: [PATCH 5/5] VNNLib version --- .github/workflows/tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index cda12dfe..eeb5b628 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -51,7 +51,7 @@ jobs: #- name: Build package # uses: julia-actions/julia-buildpkg@v1 - name: Instantiate Julia Package - run: julia --project=. -e 'using Pkg; Pkg.add(url="https://github.com/samysweb/VNNLib.jl", rev="c6bf990"); Pkg.pin("VNNLib"); Pkg.resolve()' + run: julia --project=. -e 'using Pkg; Pkg.add(url="https://github.com/samysweb/VNNLib.jl", rev="9327e5c"); Pkg.pin("VNNLib"); Pkg.resolve()' - name: Run tests uses: julia-actions/julia-runtest@v1 env: