|
|
@1941
|
9 years |
mulligan |
Changes to the AssemblyProof? with a few more (large) axioms closed.
|
|
|
@1940
|
9 years |
boender |
- committed new version of final invariant
|
|
|
@1939
|
9 years |
mulligan |
Changes to get things to compile and to avoid the dependency …
|
|
|
@1938
|
9 years |
sacerdot |
Definitions moved to the right places, now everything compiles again.
|
|
|
@1937
|
9 years |
boender |
- filled in some of the gaps in the proof of Policy
- reverted …
|
|
|
@1936
|
9 years |
mulligan |
Some holes filled in AssemblyProof?.ma.
|
|
|
@1935
|
9 years |
mulligan |
Generalized some lemma in ASM/CostsProof.ma to work on abstract …
|
|
|
@1934
|
9 years |
boender |
- various & sundry moves of lemmas to better places
- integrated …
|
|
|
@1933
|
9 years |
boender |
- slight revamp
|
|
|
@1932
|
9 years |
boender |
- added some more dependent types (we love 'em)
|
|
|
@1931
|
9 years |
boender |
- added latest bvt alias
- temporary "cases daemon" commit of new …
|
|
|
@1930
|
9 years |
campbell |
Tidy up labelling simulation stuff a bit.
|
|
|
@1929
|
9 years |
mulligan |
Simplified proof by removing most of the invariants on the statements …
|
|
|
@1928
|
9 years |
mulligan |
Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
|
|
|
@1927
|
9 years |
mulligan |
Reduced complexity of good_program predicate, ported to new notion of …
|
|
|
@1926
|
9 years |
tranquil |
* added as_label to abstract status, with as_costed defined with it. …
|
|
|
@1925
|
9 years |
boender |
- re-added jump_lenggh
|
|
|
@1924
|
9 years |
mulligan |
Added comment
|
|
|
@1923
|
9 years |
mulligan |
Small change, closing daemon that went under the RADAR
|
|
|
@1922
|
9 years |
campbell |
Main labelling simulation proof complete.
|
|
|
@1921
|
9 years |
mulligan |
Horror proof mostly finished (compiles all way until end of CostsProof?.ma).
|
|
|
@1920
|
9 years |
campbell |
Most of the labelling simulation. Still need to sort out switch …
|
|
|
@1919
|
9 years |
mulligan |
Fixes to get everything compiling again
|
|
|
@1918
|
9 years |
tranquil |
using listb.ma now
|
|
|
@1917
|
9 years |
tranquil |
predicate for unrepeating traces, fused final_abstract_status with …
|
|
|
@1916
|
9 years |
mulligan |
Closed remaining daemons in block_cost'. Rest of file now typechecks …
|
|
|
@1915
|
9 years |
garnier |
Correction of a typo in switchRemoval.
|
|
|
@1914
|
9 years |
campbell |
Fix bug in Clight semantics that misses goto-labels inside a cost …
|
|
|
@1913
|
9 years |
mulligan |
Got the rest of the file to typecheck as before.
|
|
|
@1912
|
9 years |
mulligan |
Patches to get block_cost' and dependencies working again after change …
|
|
|
@1911
|
9 years |
mulligan |
Changed statement of block_cost' to start on new termination argument
|
|
|
@1910
|
9 years |
mulligan |
Finished proof modulo termination argument
|
|
|
@1909
|
9 years |
mulligan |
Ported new statements to remainder of Interpret.ma file.
|
|
|
@1908
|
9 years |
fguidi |
notation fixup following last commit of matita
we shifted the levels …
|
|
|
@1907
|
9 years |
mulligan |
Fixes to get file to compile
|
|
|
@1906
|
9 years |
mulligan |
Statements simplified in block_cost and dependencies
|
|
|
@1905
|
9 years |
boender |
- plugging gap in assembly proof
|
|
|
@1904
|
9 years |
mulligan |
Problem with proof fixed by noting that problem is actually irrelevant
|
|
|
@1903
|
9 years |
mulligan |
Small changes prior to experiment
|
|
|
@1902
|
9 years |
mulligan |
Reverted needless changes to StructuredTraces?
|
|
|
@1901
|
9 years |
mulligan |
Slight changes to StructuredTraces?: should not change too much
|
|
|
@1900
|
9 years |
mulligan |
CostProof? complete, modulo some daemons and axioms in earlier files
|
|
|
@1899
|
9 years |
mulligan |
Changes to statements of theorems
|
|
|
@1898
|
9 years |
mulligan |
Ported changes from ASMCosts.ma into CostsProof?.ma and got everything …
|
|
|
@1897
|
9 years |
mulligan |
Changes to proof, and pushed through those changes to rest of the file.
|
|
|
@1896
|
9 years |
mulligan |
Finished horror proof
|
|
|
@1895
|
9 years |
mulligan |
Split the ASMCosts files while working on traverse_code_internal. A …
|
|
|
@1894
|
9 years |
mulligan |
Closed a hole in the proof by deriving a contradiction using even_p …
|
|
|
@1893
|
9 years |
campbell |
Show stronger result about labelling of expressions.
|
|
|
@1892
|
9 years |
mulligan |
Lots of work from today
|
|
|
@1891
|
9 years |
mulligan |
Nightmarish proofs on bitvectors. Trying to find some way of making …
|
|
|
@1890
|
9 years |
boender |
- added comment about bitvector translation
|
|
|
@1889
|
9 years |
boender |
- some pages of article
|
|
|
@1888
|
9 years |
campbell |
Show that labelling of expressions works ...
after fixing it to match …
|
|
|
@1887
|
9 years |
boender |
- added SEFM2012 directory
- some progress in assembly
|
|
|
@1886
|
9 years |
boender |
- improvements for disambiguation and quick(er) typing
|
|
|
@1885
|
9 years |
boender |
- updated assembler with new definition of occurs_exactly_once
|
|
|
@1884
|
9 years |
campbell |
Syntax changes to fit Paolo's commit.
|
|
|
@1883
|
9 years |
campbell |
Ilias' switch removal code, plus a test.
|
|
|
@1882
|
9 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
@1881
|
9 years |
campbell |
Resurrect version of exec_up_to which shows the final state.
|
|
|
@1880
|
9 years |
campbell |
Show that RTLabs flat traces are determined by their starting state, …
|
|
|
@1879
|
9 years |
boender |
- Policy compiles until the end, still some (fairly trivial) cases …
|
|
|
@1878
|
9 years |
campbell |
Enforce typing of constants in front-end, plus binops for RTLabs.
|
|
|
@1877
|
9 years |
campbell |
Update RTLabs structured traces for typed binops and new memory model.
|
|
|
@1876
|
9 years |
campbell |
Update Cexec soundness proof.
Change finishes_with predicate to …
|
|
|
@1875
|
9 years |
campbell |
Update brief memory model test.
|
|
|
@1874
|
9 years |
campbell |
First cut at using back-end memory model throughout.
Note the …
|
|
|
@1873
|
9 years |
campbell |
Fix up earlier front-end value conversion work.
|
|
|
@1872
|
9 years |
campbell |
Make binary operations in Cminor/RTLabs properly typed.
A few extra …
|
|
|
@1871
|
9 years |
campbell |
Change Clight to Cminor compilation to use gotos rather than loops, …
|
|
|
@1870
|
9 years |
boender |
- changed sigma00 in Assembly to use foldl_strong + proved invariants …
|
|
|
@1869
|
9 years |
mulligan |
a load of axioms closed in ASMCosts file
|
|
|
@1831
|
9 years |
mulligan |
small changes to asmcosts file to refactor proof
|
|
|
@1812
|
9 years |
campbell |
Provide a combined type for terminating and non-terminating structured …
|
|
|
@1811
|
9 years |
boender |
- corrected definition of geb
|
|
|
@1810
|
9 years |
boender |
- new version of policy that compiles up to the final glue
|
|
|
@1809
|
9 years |
boender |
- committed partially compiling version of policy (up until …
|
|
|
@1808
|
9 years |
campbell |
Create a Prop version of the non-terminating structured traces so that …
|
|
|
@1807
|
9 years |
mulligan |
some changes, as finally worked out what i was up to prior to working …
|
|
|
@1806
|
9 years |
campbell |
Show that we could construct RTLabs non-terminating structured traces …
|
|
|
@1805
|
9 years |
campbell |
RTLabs structured traces: package up some of the properties we need …
|
|
|
@1784
|
9 years |
campbell |
Start on proof of existence of nonterminating RTLabs structured traces.
|
|
|
@1783
|
9 years |
campbell |
Remove junk from non-terminating structured traces.
|
|
|
@1782
|
9 years |
campbell |
Correct bad inversion.
|
|
|
@1765
|
9 years |
campbell |
Rule out final states in non-terminating executions chunks (RTLabs …
|
|
|
@1764
|
9 years |
campbell |
Terminating function preserve the property that the execution does not …
|
|
|
@1736
|
9 years |
campbell |
Show that the bound on the number of instructions until a cost label …
|
|
|
@1730
|
9 years |
sacerdot |
Minor changes while studying the proof.
|
|
|
@1729
|
9 years |
sacerdot |
Comment left from SVN merge removed.
|
|
|
@1719
|
9 years |
campbell |
Show that non-termination survives a terminating function call.
|
|
|
@1713
|
9 years |
campbell |
Add a distinguished final state to the front-end languages to match up …
|
|
|
@1712
|
9 years |
campbell |
Show that constructing an RTLabs structure trace really does use a …
|
|
|
@1711
|
9 years |
mulligan |
finished block_cost' proof: 1.5 minutes to typecheck qed.
|
|
|
@1710
|
9 years |
mulligan |
changes from friday afternoon
|
|
|
@1709
|
9 years |
mulligan |
Changes to the execution of the MOVC instruction
|
|
|
@1707
|
9 years |
campbell |
Progress on finite segments of infinite RTLabs structured trace.
|
|
|
@1706
|
9 years |
campbell |
Checkpoint RTLabs structured traces.
|
|
|
@1705
|
9 years |
campbell |
Checkpoint RTLabs labelling soundness work.
|
|
|
@1697
|
9 years |
mulligan |
important bug found
|
|
|