Skip to content

Base64.Decode has quadratic runtime on Go #4794

Open
@robin-aws

Description

@robin-aws

See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/examples/Base64Examples.dfy#L33.

This isn't surprising on JS since its runtime doesn't have the sequence concatenation optimization, but Go does. Encode doesn't have the same issue. I suspect that sequence slicing is at fault: it should be O(1) time in the Go backend but perhaps is unintentionally making a copy.

Metadata

Metadata

Assignees

No one assigned

    Labels

    area: performancePerformance issueslang: golangDafny's transpiler to Go and its runtimepart: standard librariesStandard libraries packaged in the Dafny distribution

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions