An Idris2 command-line client for Poland's National e-Invoice System. The authentication protocol is a compile-time state machine — call the wrong API in the wrong state and the compiler rejects your program.
data Session : SessionState -> Type where SUnauth : Config -> Session Unauthenticated SChallenged : Config -> ChallengeData -> Session Challenged STokenSent : Config -> AuthTokenData -> Session TokenSent SAuthed : Config -> AccessTokenData -> Session Authenticated SActive : Config -> SessionData -> Session Active SClosed : Config -> Session Closed
Dependent types turn protocol violations into compile-time errors. If it type-checks, the API contract is satisfied.
The KSeF authentication protocol is modeled as a type-indexed state machine. Each API call consumes a session in one state and produces the next. Constructors are private — the only way to reach Authenticated is through the actual auth flow. Fabricating session states is impossible outside the module.
Polish tax IDs are validated using an erased So proof. When the NIP literal is known at compile time, an invalid checksum is a type error. Runtime values go through a smart constructor.
data NIP : Type where MkNIP : (value : String) -> {auto 0 prf : So (isValidNIP value)} -> NIP
Invoice numbers carry a So (isValidKSeFNumber value) proof: 10-digit NIP prefix, 8-digit date, code, and suffix — validated at construction. Invalid numbers from CLI args or API responses are rejected before any API call is made.
data KSeFNumber : Type where MkKSeFNumber : (value : String) -> {auto 0 prf : So (isValidKSeFNumber value)} -> KSeFNumber
Dates carry a So (isValidDate value) proof: YYYY-MM-DD format with month 1–12 and day 1–31 validated at construction. Invalid dates from CLI arguments or XML parsing are rejected immediately.
data Date : Type where MkDate : (value : String) -> {auto 0 prf : So (isValidDate value)} -> Date
HTTP goes through curl. RSA-OAEP encryption and AES-256-CBC go through openssl. No FFI, no C bindings. The exact same commands work when pasted into a terminal. Debugging is trivial.
requireSuccess centralizes HTTP status classification across all 7 API modules. One consistent 2xx check replaces the ad-hoc mix of == 200 and >= 200 && < 300 comparisons. Success-path code only handles validated responses.
Each state transition is a function that consumes a session in one state and produces the next. Invalid transitions are compile-time errors. Auth polling is bounded by Data.Fuel — provably terminates. All HTTP responses flow through requireSuccess for consistent 2xx classification.
Stops after token redemption. Supports fetchInvoiceReadOnly and queryInvoicesReadOnly. No interactive session needed — most read operations work with just an access token.
Opens an interactive session with an AES-256 symmetric key. Required for InvoiceWrite operations. Supports fetchInvoice, queryInvoices, and must be explicitly closed.
Build with pack build idris-ksef and run. Each command maps directly to a KSeF API workflow.
connectivity Test KSeF API reachabilityauth-test Verify full authentication flowfetch Download a single invoice by KSeF numberquery Fetch all invoices in a date rangelocal list List cached invoices by monthlocal show Display full details of a cached invoiceFrom invoice fetching to financial intelligence. Each phase builds on compile-time guarantees.
Full integration with Poland's National e-Invoice System.
So proofsrequireSuccessAutomated matching of bank statement entries to KSeF invoices.
Forecast receivables and payables from historical invoice and payment patterns.