rdp_protocol

Microsoft Remote Desktop Connection protocol implementation.

A pure RDP protocol library following the Sans-I/O architecture (no sockets, no crypto inside; all side effects are delegated to the shell/driver). The core is written in Ada 2012 + SPARK and proved with GNATprove. See doc/design.md for the detailed design.

Prerequisites

• Alire (alr 2.1.0+)
• FSF GNAT + GNATprove toolchain (managed by Alire; the default gnat_native toolchain is used)

Build the library

alr build

The library is built with -gnatwe (warnings as errors) and -gnata (contract checks enabled at run time).

Run the tests

Unit tests live in a nested AUnit crate under tests/:

cd tests
alr build
./bin/tests

Prove with GNATprove

The SPARK core (currently RDP_Protocol.Types / Bytes / Endian / Fifo / Queue) is proved with:

alr gnatprove -P rdp_protocol.gpr -U -j0 --level=2

Project layout

src/     protocol library (SPARK core)
tests/   AUnit test crate (pinned to this crate)
doc/     design, progress notes and protocol specs