This PR now includes a typechecking model for the full handshake, instead of just one function.
Original PR
This PR includes a syntactically valid, typechecking model for tls13handshake::put_server_hello and some of it's dependencies. To typecheck, the driver is adapted to include a handwritten_lib.pvl which fills in missing types and constructors etc from the dependencies.
For now, this handwritten model does not contain any logic beyond what is need for typechecking. The next step would be to minimize the model by expanding the selection of dependencies we want to extract while at the same time giving proper reducs for those parts of the handwritten model that we don't want to translate.
This PR now includes a typechecking model for the full handshake, instead of just one function.
Original PR
This PR includes a syntactically valid, typechecking model for
tls13handshake::put_server_helloand some of it's dependencies. To typecheck, the driver is adapted to include ahandwritten_lib.pvlwhich fills in missing types and constructors etc from the dependencies.For now, this handwritten model does not contain any logic beyond what is need for typechecking. The next step would be to minimize the model by expanding the selection of dependencies we want to extract while at the same time giving proper
reducsfor those parts of the handwritten model that we don't want to translate.