update LOC counting

mit-plv · Apr 6, 2024 · 92bbe7d · 92bbe7d
1 parent 70bae7a
commit 92bbe7d
Show file tree

Hide file tree

Showing 3 changed files with 102 additions and 84 deletions.
diff --git a/loc/PrintLibraries.txt b/loc/PrintLibraries.txt
@@ -285,6 +285,77 @@ Loaded library files:
   Coq.ZArith.Zwf
   Coqprime.Z.Pmod
   Coqprime.PrimalityTest.PocklingtonCertificat
+  Crypto.Algebra.Hierarchy
+  Crypto.Util.ZUtil.Peano
+  Crypto.Util.Logic
+  Crypto.Util.Relations
+  Crypto.Algebra.Monoid
+  Crypto.Algebra.Group
+  Crypto.Algebra.ScalarMult
+  Coq.setoid_ring.Algebra_syntax
+  Coq.setoid_ring.Ncring
+  Coq.setoid_ring.Ncring_polynom
+  Coq.setoid_ring.Ncring_initial
+  Coq.setoid_ring.Ncring_tac
+  Coq.setoid_ring.Cring
+  Crypto.Util.Tactics.OnSubterms
+  Crypto.Util.Tactics.Revert
+  Crypto.Algebra.Ring
+  Crypto.Util.Tactics.FindHyp
+  Crypto.Util.Tactics.UniquePose
+  Crypto.Util.Tactics.DebugPrint
+  Coq.setoid_ring.Integral_domain
+  Coq.nsatz.NsatzTactic
+  Crypto.Algebra.Nsatz
+  Crypto.Util.Factorize
+  Crypto.Algebra.IntegralDomain
+  Crypto.Algebra.Field
+  Crypto.Arithmetic.ModularArithmeticTheorems
+  Coq.Logic.FunctionalExtensionality
+  Coq.Logic.HLevels
+  Coq.QArith.Qabs
+  Coq.QArith.Qpower
+  Coq.QArith.Qround
+  Coq.Logic.ConstructiveEpsilon
+  Coq.Reals.Cauchy.PosExtra
+  Coq.Reals.Cauchy.QExtra
+  Coq.Reals.Cauchy.ConstructiveExtra
+  Coq.Reals.Cauchy.ConstructiveCauchyReals
+  Coq.Reals.Abstract.ConstructiveReals
+  Coq.Reals.Cauchy.ConstructiveCauchyRealsMult
+  Coq.Reals.Cauchy.ConstructiveCauchyAbs
+  Coq.QArith.QOrderedType
+  Coq.QArith.Qminmax
+  Coq.Reals.Cauchy.ConstructiveRcomplete
+  Coq.Reals.ClassicalDedekindReals
+  Coq.Reals.Abstract.ConstructiveAbs
+  Coq.Reals.Abstract.ConstructiveLimits
+  Coq.Reals.Abstract.ConstructiveLUB
+  Coq.Reals.Rdefinitions
+  Coq.Reals.Raxioms
+  Coq.Reals.Rpow_def
+  Coq.setoid_ring.RealField
+  Coq.Reals.RIneq
+  Coq.Reals.DiscrR
+  Coq.Reals.Rbase
+  Coq.Reals.R_Ifp
+  Coq.Reals.Rbasic_fun
+  Coq.Reals.R_sqr
+  Coq.Reals.SplitAbsolu
+  Coq.Reals.SplitRmult
+  Coq.Arith.Even
+  Coq.Arith.Div2
+  Coq.Reals.ArithProp
+  Coq.Reals.Rfunctions
+  Coq.nsatz.Nsatz
+  Crypto.Util.ZUtil.Tactics.ZeroBounds
+  Crypto.Arithmetic.PrimeFieldTheorems
+  Crypto.Curves.Edwards.Pre
+  Crypto.Spec.CompleteEdwardsCurve
+  Crypto.Util.Tactics.Contains
+  Crypto.Util.Tactics.SetoidSubst
+  Crypto.Util.Sum
+  Crypto.Spec.MontgomeryCurve
   Crypto.Spec.Curve25519
   coqutil.sanity
   coqutil.Datatypes.PrimitivePair
@@ -304,7 +375,6 @@ Loaded library files:
   Coq.Logic.Hurkens
   Coq.Logic.ClassicalFacts
   Coq.Logic.PropExtensionality
-  Coq.Logic.FunctionalExtensionality
   coqutil.Datatypes.PropSet
   coqutil.Map.Interface
   bedrock2.Lift1Prop
@@ -348,6 +418,7 @@ Loaded library files:
   coqutil.Map.Solver
   compiler.util.Common
   riscv.Platform.MetricLogging
+  coqutil.Tactics.invert_hyp
   coqutil.Tactics.Simp
   bedrock2.MetricLogging
   bedrock2.MetricSemantics
@@ -464,6 +535,8 @@ Loaded library files:
   bedrock2.WeakestPreconditionProperties
   compiler.UseImmediateDef
   compiler.UseImmediate
+  compiler.DeadCodeElimDef
+  compiler.DeadCodeElim
   compiler.Pipeline
   Coq.Strings.HexString
   coqutil.Map.Z_keyed_SortedListMap
@@ -479,70 +552,6 @@ Loaded library files:
   coqutil.Word.Bitwidth32
   bedrock2.FE310CSemantics
   compiler.MMIO
-  Crypto.Algebra.Hierarchy
-  Crypto.Util.ZUtil.Peano
-  Crypto.Util.Logic
-  Crypto.Util.Relations
-  Crypto.Algebra.Monoid
-  Crypto.Algebra.Group
-  Crypto.Algebra.ScalarMult
-  Coq.setoid_ring.Algebra_syntax
-  Coq.setoid_ring.Ncring
-  Coq.setoid_ring.Ncring_polynom
-  Coq.setoid_ring.Ncring_initial
-  Coq.setoid_ring.Ncring_tac
-  Coq.setoid_ring.Cring
-  Crypto.Util.Tactics.OnSubterms
-  Crypto.Util.Tactics.Revert
-  Crypto.Algebra.Ring
-  Crypto.Util.Tactics.FindHyp
-  Crypto.Util.Tactics.UniquePose
-  Crypto.Util.Tactics.DebugPrint
-  Coq.setoid_ring.Integral_domain
-  Coq.nsatz.NsatzTactic
-  Crypto.Algebra.Nsatz
-  Crypto.Util.Factorize
-  Crypto.Algebra.IntegralDomain
-  Crypto.Algebra.Field
-  Crypto.Arithmetic.ModularArithmeticTheorems
-  Coq.Logic.HLevels
-  Coq.QArith.Qabs
-  Coq.QArith.Qpower
-  Coq.QArith.Qround
-  Coq.Logic.ConstructiveEpsilon
-  Coq.Reals.Cauchy.PosExtra
-  Coq.Reals.Cauchy.QExtra
-  Coq.Reals.Cauchy.ConstructiveExtra
-  Coq.Reals.Cauchy.ConstructiveCauchyReals
-  Coq.Reals.Abstract.ConstructiveReals
-  Coq.Reals.Cauchy.ConstructiveCauchyRealsMult
-  Coq.Reals.Cauchy.ConstructiveCauchyAbs
-  Coq.QArith.QOrderedType
-  Coq.QArith.Qminmax
-  Coq.Reals.Cauchy.ConstructiveRcomplete
-  Coq.Reals.ClassicalDedekindReals
-  Coq.Reals.Abstract.ConstructiveAbs
-  Coq.Reals.Abstract.ConstructiveLimits
-  Coq.Reals.Abstract.ConstructiveLUB
-  Coq.Reals.Rdefinitions
-  Coq.Reals.Raxioms
-  Coq.Reals.Rpow_def
-  Coq.setoid_ring.RealField
-  Coq.Reals.RIneq
-  Coq.Reals.DiscrR
-  Coq.Reals.Rbase
-  Coq.Reals.R_Ifp
-  Coq.Reals.Rbasic_fun
-  Coq.Reals.R_sqr
-  Coq.Reals.SplitAbsolu
-  Coq.Reals.SplitRmult
-  Coq.Arith.Even
-  Coq.Arith.Div2
-  Coq.Reals.ArithProp
-  Coq.Reals.Rfunctions
-  Coq.nsatz.Nsatz
-  Crypto.Util.ZUtil.Tactics.ZeroBounds
-  Crypto.Arithmetic.PrimeFieldTheorems
   bedrock2.ArrayCasts
   coqutil.Tactics.letexists
   coqutil.Tactics.eabstract
@@ -627,7 +636,6 @@ Loaded library files:
   Crypto.Util.ZUtil.ZSimplify.Simple
   Crypto.Util.ZUtil.Log2
   Crypto.Util.ZUtil.Tactics.PeelLe
-  Crypto.Util.Tactics.Contains
   Crypto.Util.ZUtil.Tactics.LinearSubstitute
   Crypto.Util.ZUtil.Tactics.SplitMinMax
   Crypto.Util.ZUtil.N2Z
@@ -641,8 +649,6 @@ Loaded library files:
   Crypto.Util.ZUtil.LandLorBounds
   Crypto.Util.ZUtil.Morphisms
   Crypto.Util.ListUtil.SetoidList
-  Crypto.Util.Tactics.SetoidSubst
-  Crypto.Util.Sum
   Crypto.Util.Comparison
   Crypto.Util.PrimitiveProd
   Crypto.Util.Bool.Reflect
@@ -1043,22 +1049,23 @@ Loaded library files:
   Rupicola.Lib.Arrays
   Rupicola.Lib.SepLocals
   Crypto.Bedrock.Group.ScalarMult.CSwap
+  Crypto.Util.Loops
+  Crypto.Bedrock.Group.Loops
+  Crypto.Spec.WeierstrassCurve
+  Crypto.Curves.Montgomery.Affine
+  Crypto.Curves.Montgomery.XZ
+  Crypto.Curves.Weierstrass.Affine
+  Crypto.Curves.Weierstrass.AffineProofs
+  Crypto.Curves.Montgomery.AffineProofs
+  Crypto.Curves.Montgomery.AffineInstances
+  Crypto.Curves.Montgomery.XZProofs
   bedrock2.NotationsCustomEntry
   Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder
   coqutil.Word.Naive
   coqutil.Map.SortedListWord
   Crypto.Bedrock.Field.Translation.Parameters.FE310
   Crypto.Bedrock.End2End.X25519.Field25519
-  bedrock2.ToCString
-  riscv.Utility.RegisterNameNotations
-  riscv.Utility.InstructionNotations
-  Crypto.Bedrock.End2End.X25519.MontgomeryLadder
-  bedrock2.ReversedListNotations
-  bedrock2.TracePredicate
-  bedrock2Examples.lightbulb_spec
-  bedrock2Examples.SPI
-  bedrock2.AbsintWordToZ
-  bedrock2Examples.LAN9250
+  bedrock2Examples.memmove
   coqutil.Datatypes.Inhabited
   coqutil.Sorting.OrderToPermutation
   bedrock2.TacticError
@@ -1068,6 +1075,17 @@ Loaded library files:
   bedrock2.TransferSepsOrder
   bedrock2.SepAuto
   bedrock2.SepAutoArray
+  Crypto.Bedrock.End2End.X25519.clamp
+  bedrock2.ToCString
+  Crypto.Bedrock.End2End.X25519.MontgomeryLadder
+  bedrock2.ReversedListNotations
+  bedrock2.TracePredicate
+  bedrock2Examples.lightbulb_spec
+  bedrock2Examples.SPI
+  bedrock2.AbsintWordToZ
+  Coq.Unicode.Utf8_core
+  Coq.Unicode.Utf8
+  bedrock2Examples.LAN9250
   bedrock2Examples.lightbulb
   bedrock2Examples.memequal
   bedrock2Examples.memswap
@@ -1076,17 +1094,14 @@ Loaded library files:
   Rupicola.Examples.Net.IPChecksum.Spec
   Rupicola.Examples.Net.IPChecksum.Impl
   Rupicola.Examples.Net.IPChecksum.IPChecksum
-  Coq.Unicode.Utf8_core
-  Coq.Unicode.Utf8
   Crypto.Bedrock.End2End.RupicolaCrypto.Broadcast
   Crypto.Bedrock.End2End.RupicolaCrypto.Spec
   Crypto.Bedrock.End2End.RupicolaCrypto.ChaCha20
   Crypto.Bedrock.End2End.X25519.GarageDoor
-  compiler.NaiveRiscvWordProperties
-  Crypto.Bedrock.End2End.X25519.MontgomeryLadderProperties
   compiler.ExprImpEventLoopSpec
   compiler.ToplevelLoop
   riscv.Utility.bverify
+  coqutil.Semantics.OmniSmallstepCombinators
   compiler.CompilerInvariant
-  bedrock2.WordNotations
+  compiler.NaiveRiscvWordProperties
   Crypto.Bedrock.End2End.X25519.GarageDoorTop
diff --git a/loc/PrintLoadPath.txt b/loc/PrintLoadPath.txt
@@ -30,6 +30,7 @@ compiler.util /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedro
 bedrock2Examples /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/bedrock2/src/bedrock2Examples
 bedrock2 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/bedrock2/src/bedrock2
 bedrock2.Map /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/bedrock2/src/bedrock2/Map
+bedrock2.old_dma /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/bedrock2/src/bedrock2/old_dma
 Rupicola /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola
 Rupicola.Examples /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples
 Rupicola.Examples.Assoc /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/Assoc
@@ -57,6 +58,7 @@ coqutil.Datatypes /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/b
 coqutil.Ltac2Lib /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil/Ltac2Lib
 coqutil.Macros /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil/Macros
 coqutil.Map /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil/Map
+coqutil.Semantics /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil/Semantics
 coqutil.Sorting /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil/Sorting
 coqutil.Tactics /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics
 coqutil.Word /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil/Word
@@ -121,6 +123,7 @@ Crypto.Curves.Edwards.XYZT /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/s
 Crypto.Curves.Montgomery /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Curves/Montgomery
 Crypto.Curves.TableMult /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Curves/TableMult
 Crypto.Curves.Weierstrass /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Curves/Weierstrass
+Crypto.Curves.Weierstrass.Jacobian /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Curves/Weierstrass/Jacobian
 Crypto.ExtractionHaskell /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/ExtractionHaskell
 Crypto.ExtractionJsOfOCaml /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/ExtractionJsOfOCaml
 Crypto.ExtractionOCaml /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/ExtractionOCaml

diff --git a/loc/new_work.txt b/loc/new_work.txt
@@ -17,11 +17,11 @@ Crypto.Bedrock.End2End.RupicolaCrypto.Broadcast
 
 ## Montgomery ladder (x25519, x25519_base) [Bedrock2]
 Crypto.Bedrock.End2End.X25519.MontgomeryLadder
+Crypto.Bedrock.End2End.X25519.clamp
 
 ## Montgomery ladder (montladder, ladderstep) [Rupicola]
 Crypto.Bedrock.Group.ScalarMult.LadderStep
 Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder
-Crypto.Bedrock.Group.ScalarMult.MontgomeryEquivalence
 Crypto.Bedrock.Group.ScalarMult.CSwap
 
 ## Modular inversion (fe25519_inv) [simpl, Rupicola]