PG

Definitions

record PGAuthentication : Type

Totality: total
Visibility: public export
Constructor: 

MkPGAuthentication : LTE n 64 => String -> Vect n Bits8 -> (Vect n Bits8 -> Vect 64 Bits8) -> PGAuthentication

Projections:

0 .n : PGAuthentication -> Nat

.password : ({rec:0} : PGAuthentication) -> Vect (n {rec:0}) Bits8

.prf : ({rec:0} : PGAuthentication) -> LTE (n {rec:0}) 64

.userName : PGAuthentication -> String

.zeroPadPassword : ({rec:0} : PGAuthentication) -> Vect (n {rec:0}) Bits8 -> Vect 64 Bits8

.prf : ({rec:0} : PGAuthentication) -> LTE (n {rec:0}) 64

Visibility: public export

prf : ({rec:0} : PGAuthentication) -> LTE (n {rec:0}) 64

Visibility: public export

.userName : PGAuthentication -> String

Visibility: public export

userName : PGAuthentication -> String

Visibility: public export

.password : ({rec:0} : PGAuthentication) -> Vect (n {rec:0}) Bits8

Visibility: public export

password : ({rec:0} : PGAuthentication) -> Vect (n {rec:0}) Bits8

Visibility: public export

.zeroPadPassword : ({rec:0} : PGAuthentication) -> Vect (n {rec:0}) Bits8 -> Vect 64 Bits8

Visibility: public export

zeroPadPassword : ({rec:0} : PGAuthentication) -> Vect (n {rec:0}) Bits8 -> Vect 64 Bits8

Visibility: public export

data PgErr : Type

Totality: total
Visibility: export
Constructors:

UnexpectedMessage : String -> PgErr

SCRAM2Failure : Phase2Err -> PgErr

SCRAM3Failure : Phase3Err -> PgErr

Hint: 

Show PgErr

initialPgIter : PGAuthentication -> DIterator (List Bits8) (List Bits8) PgInput PgRows PgErr

Visibility: export