CompCert-Chamois GL Thesis