fact: Definition MicroEncoders_Env : Env ADTValue := (GLabelMap.empty (FuncSpec _)) ### ("ByteString", "New") ->> (Axiomatic BytesADTSpec.New) ### ("ByteString", "Push") ->> (Axiomatic BytesADTSpec.Push) ### ("list[W]", "Pop") ->> (Axiomatic WordListADTSpec.Pop) ### ("list[W]", "Empty") ->> (Axiomatic WordListADTSpec.Empty) ### ("list[W]", "Delete") ->> (Axiomatic WordListADTSpec.Delete) ### ("list[W]", "Length") ->> (Axiomatic WordListADTSpec.Length).
imports: Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Compose Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Lib.FixList Fiat.Narcissus.BinLib.FixInt Fiat.CertifiedExtraction.RemoveSkips Fiat.CertifiedExtraction.Benchmarks.MicrobenchmarksSetup Fiat.CertifiedExtraction.Extraction.BinEncoders.BinEncoders Coq.Strings.String Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Computation Fiat.Narcissus.Automation.SolverOpt Fiat.Narcissus.BinLib.Bool Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.Enum Fiat.Narcissus.BinLib.FixInt Fiat.Narcissus.Common.Compose Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Lib.FixList Fiat.Narcissus.Lib.IList Fiat.Narcissus.Lib2.Bool Fiat.Narcissus.Lib2.EnumOpt Fiat.Narcissus.Lib2.FixListOpt Fiat.Narcissus.Lib2.NatOpt Fiat.Narcissus.Lib2.NoCache Fiat.Narcissus.Lib2.SumTypeOpt Fiat.Narcissus.Lib2.Vector Fiat.Narcissus.Lib2.WordOpt Fiat.Narcissus.Lib2.IPChecksum