

@1878

8 years 
campbell 
Enforce typing of constants in frontend, plus binops for RTLabs.



@1876

8 years 
campbell 
Update Cexec soundness proof.
Change finishes_with predicate to …



@1874

8 years 
campbell 
First cut at using backend memory model throughout.
Note the …



@1873

8 years 
campbell 
Fix up earlier frontend value conversion work.



@1872

8 years 
campbell 
Make binary operations in Cminor/RTLabs properly typed.
A few extra …



@1812

8 years 
campbell 
Provide a combined type for terminating and nonterminating structured …



@1808

8 years 
campbell 
Create a Prop version of the nonterminating structured traces so that …



@1806

8 years 
campbell 
Show that we could construct RTLabs nonterminating structured traces …



@1783

8 years 
campbell 
Remove junk from nonterminating structured traces.



@1709

8 years 
mulligan 
Changes to the execution of the MOVC instruction



@1658

9 years 
mulligan 
asm costs changes from today



@1654

9 years 
campbell 
Corrections to structured trace definitions (see the mailing list). …



@1652

9 years 
campbell 
Forgot to apply 1583 to nonterminating case.



@1647

9 years 
tranquil 
* corrected some notation problems
* adapted Cligth with slight …



@1640

9 years 
tranquil 
* finished fork of semantics.ma
* unification of Errors under the …



@1635

9 years 
tranquil 
* lists with binders and monads
* Joint.ma and other temprarily …



@1631

9 years 
campbell 
Use fact that type environments in Cminor have distinct variables to …



@1627

9 years 
campbell 
Add some notions of freshness, and start using them for temporary …



@1626

9 years 
campbell 
Add extra type safety in front end. NB: critical freshness parts …



@1609

9 years 
boender 
 added alias to ASM/BitVectorTrie
 removed double include from …



@1608

9 years 
sacerdot 
Porting to new library still in progress.



@1601

9 years 
sacerdot 
Files ported to new version of the standard library.



@1599

9 years 
sacerdot 
Start of merging of stuff into the standard library of Matita.



@1598

9 years 
mulligan 
changes over the last couple of days



@1583

9 years 
campbell 
More on RTLabs structured traces.
Fixed mistake in structure trace …



@1574

9 years 
campbell 
A little more progress on traces on RTLabs.



@1566

9 years 
campbell 
Pacify changes to destruct tactic.



@1562

9 years 
mulligan 
new version of assembly, fixed conflict in positivemap.ma, changed …



@1555

9 years 
boender 
 changes to assembly
 added lookup to PositiveMap?
 lightly changed …



@1551

9 years 
campbell 
Functions to translate between backend and frontend values.



@1545

9 years 
campbell 
Use pointer record in frontend.



@1544

9 years 
sacerdot 
StructuredTraces? inhabited for object code.



@1536

9 years 
campbell 
Use predicates throughout the structured traces.



@1535

9 years 
campbell 
Make RTLabs semantics use knowledge that the next instruction always …



@1532

9 years 
campbell 
Remove jump classification from structured traces.



@1531

9 years 
campbell 
A notion of abstract structured traces.



@1523

9 years 
campbell 
Separate out positive and Z definitions from extralib.ma.
Minor syntax …



@1516

9 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1515

9 years 
campbell 
Add type of maps on positive binary numbers, and use them for …



@1512

9 years 
campbell 
Shorten proof of goal that solves now.



@1510

9 years 
sacerdot 
All files ported to new dependent inversion.



@1480

9 years 
sacerdot 
Proof changed (to use new automation).
BUG FOUND: automation fails if …



@1465

9 years 
sacerdot 
Dead code removed.



@1410

9 years 
campbell 
Remove a few old workarounds.



@1401

9 years 
ricciott 
Changes concerning the new behavior of destruct.



@1395

9 years 
sacerdot 
1) New versions of pointer_of_beval/beval_of_pointer with a stricter …



@1369

9 years 
campbell 
Put type information into frontend unary ops.
Slight change to …



@1368

9 years 
sacerdot 
A bug in the clear tactic makes the previous (correct) commit wrong. …



@1367

9 years 
sacerdot 
Proof improvement, still somehow a bit slow.



@1355

9 years 
sacerdot 
monadic fold_lefti added



@1353

9 years 
sacerdot 
This commit is made necessary by the last Matita change.
Inclusion is …



@1351

9 years 
campbell 
Tidy up some loose ends from the invariants branch merge.



@1350

9 years 
sacerdot 
Porting to latest destruct tactic.
Note: the tactics has a few …



@1347

9 years 
campbell 
Remove obsolete definitions.



@1339

9 years 
sacerdot 
Automation is now stronger.



@1316

9 years 
campbell 
Merge in idlookupbranch to trunk.



@1268

9 years 
sacerdot 
1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …



@1253

9 years 
mulligan 
uses.ma finished



@1233

9 years 
sacerdot 
1) Ported to Brian's new dependent type for fullexec
2) Universe level …



@1231

9 years 
campbell 
Change SmallstepExec? so that states can depend on global information. …



@1225

9 years 
campbell 
Missing ; in proof



@1224

9 years 
sacerdot 
Type of programs in common/AST made more dependent.
In particular, the …



@1215

9 years 
sacerdot 
1) Added shifting directly on pointers
2) More temporary axioms closed.



@1214

9 years 
sacerdot 
res_to_opt function added to common/Errors and used in joint/semantics …



@1213

9 years 
sacerdot 
1) New values (joint/BEValues.ma) and memory model for the backends
…



@1181

9 years 
mulligan 
changed smallstep exec in order to remove matita bug (superposition.ml …



@1139

9 years 
campbell 
Shift init_data out of generic program record so that it only appears …



@1129

9 years 
mulligan 
removed conversions between Register and register



@1125

9 years 
sacerdot 
Monadic mfold_left2 added.



@1092

9 years 
campbell 
Some minor definitions for identifiers and lists.



@1082

9 years 
mulligan 
work from today on ertl > ltl pass



@1080

9 years 
mulligan 
more added



@1077

9 years 
mulligan 
ack, dependent types are scary



@1072

9 years 
campbell 
Use not equals form of showing entry/exit labels.



@1070

9 years 
campbell 
Show that entry and exit labels are in the RTLabs graph.



@1068

9 years 
mulligan 
rtlabs translation complete subject to axioms



@1064

9 years 
mulligan 
changes from today, nearly complete rtlabs translation pass



@1060

9 years 
mulligan 
work from this morning and yesterday



@1059

9 years 
mulligan 
work from today, bit of a mess at the moment



@1058

9 years 
campbell 
Evict CompCert? Maps interface in favour of BitVectorTries?.



@1057

9 years 
mulligan 
changes from today



@1056

9 years 
campbell 
Switch to delayed identifier error scheme.



@1055

9 years 
mulligan 
changes to how identifiers are generated



@1053

9 years 
mulligan 
changes



@1052

9 years 
mulligan 
removed offsets after reading cerco mailing list



@1049

9 years 
mulligan 
more stuff added



@1047

9 years 
mulligan 
more work from today



@1046

9 years 
mulligan 
syntax of rtlabs was wrong: cast not const. more added to rtlabs > …



@1045

9 years 
mulligan 
resolved conflict in rtlabs



@985

9 years 
sacerdot 
1) Major refactoring: proofs moved where they should be.
2) New …



@963

9 years 
campbell 
Extra debugging aid for animation of semantics.



@962

9 years 
campbell 
Casts should use source type's signedness, not the target's.



@961

9 years 
campbell 
Use precise bitvector sizes throughout the front end, rather than …



@891

9 years 
campbell 
Revise proofs affected by recent matita change.



@889

9 years 
sacerdot 
Minor changes because of the new, weaker (but much faster) delift.



@882

9 years 
campbell 
Fix up fragile proofs for current version of matita.



@881

9 years 
campbell 
Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.



@880

9 years 
campbell 
Add type information into Cminor.
As a result, the Clight to Cminor …



@879

9 years 
campbell 
Refine "AST" types to include size/signedness information.



@849

9 years 
sacerdot 
…


