|
|
@2079
|
7 years |
sacerdot |
sigma_policy_specification restyled
|
|
|
@2078
|
7 years |
sacerdot |
sigma_policy_specification has been
1) strengthened
2) made nicer to …
|
|
|
@2073
|
7 years |
sacerdot |
All false daemons removed.
|
|
|
@2072
|
7 years |
sacerdot |
We need to import Jaap's invariants now.
|
|
|
@2071
|
7 years |
sacerdot |
More daemons closed, but one is suspect now.
|
|
|
@2070
|
7 years |
sacerdot |
More daemons closed.
|
|
|
@2055
|
7 years |
sacerdot |
Warning: this commit adds an hypothesis that breaks all of assembly stuff.
|
|
|
@2051
|
7 years |
mulligan |
Finished the Jmp case in the main theorem.
|
|
|
@2048
|
7 years |
boender |
- factorised jump decisions
|
|
|
@2047
|
7 years |
mulligan |
Big bugs in policy calculations found. Waiting for Jaap's commit.
|
|
|
@2032
|
8 years |
sacerdot |
!! BEWARE: major commit !!
1) [affects everybody]
split for …
|
|
|
@2028
|
8 years |
boender |
- bugfix to Assembly (forgotten sigma)
- added …
|
|
|
@2022
|
8 years |
boender |
- corrected jump calculation algorithm
|
|
|
@2021
|
8 years |
sacerdot |
Proof skeleton in place. Several daemons to be closed adding invariants.
|
|
|
@2015
|
8 years |
mulligan |
Changes following a conversation with Jaap: as it stands computation …
|
|
|
@2005
|
8 years |
boender |
- minor changes to make things compile with a clean checkout
|
|
|
@1948
|
8 years |
mulligan |
Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so …
|
|
|
@1946
|
8 years |
sacerdot |
\snd half_add => add everywhere
|
|
|
@1943
|
8 years |
boender |
- changed 'labels okay' part of create_label_cost_map
|
|
|
@1942
|
8 years |
mulligan |
Work on showing the equivalence of two methods of looking up from the maps.
|
|
|
@1934
|
8 years |
boender |
- various & sundry moves of lemmas to better places
- integrated …
|
|
|
@1925
|
8 years |
boender |
- re-added jump_lenggh
|
|
|
@1905
|
8 years |
boender |
- plugging gap in assembly proof
|
|
|
@1887
|
8 years |
boender |
- added SEFM2012 directory
- some progress in assembly
|
|
|
@1885
|
8 years |
boender |
- updated assembler with new definition of occurs_exactly_once
|
|
|
@1870
|
8 years |
boender |
- changed sigma00 in Assembly to use foldl_strong + proved invariants …
|
|
|
@1668
|
8 years |
boender |
- split build_maps into build_maps and build_maps_ok
- work with CSC …
|
|
|
@1667
|
8 years |
sacerdot |
Main lemma for the main_thm of AssemblyProof? re-declared as an axiom …
|
|
|
@1649
|
8 years |
boender |
- changes to Assembly for integration with Policy and easier use of …
|
|
|
@1615
|
8 years |
sacerdot |
Policy now depends on Assembly and not the other way around.
|
|
|
@1614
|
8 years |
boender |
- split policy from assembly
|
|
|
@1613
|
8 years |
sacerdot |
Coercion moved to Matita standard lib.
|
|
|
@1609
|
8 years |
boender |
- added alias to ASM/BitVectorTrie
- removed double include from …
|
|
|
@1607
|
8 years |
sacerdot |
Porting to new library.
|
|
|
@1606
|
8 years |
sacerdot |
Porting to last library of Matita.
|
|
|
@1593
|
8 years |
boender |
- cleaned up Assembly, moved some definitions elsewhere
|
|
|
@1592
|
8 years |
boender |
- updated definitions to work with programs of maximum 216 instructions
|
|
|
@1578
|
8 years |
boender |
- proof of termination of policy completed (needs some clean-up work …
|
|
|
@1562
|
8 years |
mulligan |
new version of assembly, fixed conflict in positivemap.ma, changed …
|
|
|
@1556
|
8 years |
mulligan |
submitting to avoid conflicts
|
|
|
@1555
|
8 years |
boender |
- changes to assembly
- added lookup to PositiveMap?
- lightly changed …
|
|
|
@1528
|
8 years |
campbell |
Update most of Assembly.ma with new syntax and identifier maps.
Change …
|
|
|
@1493
|
8 years |
mulligan |
finished well labeled check, up to injectivity of the label map
|
|
|
@1482
|
8 years |
sacerdot |
1. very long standing conflict committed (but don't ask me what the …
|
|
|
@1479
|
8 years |
boender |
- added insert_lookup_opt
- assembly compiles now
|
|
|
@1459
|
8 years |
boender |
- moved stronger occurs_exactly_once lemma to its proper place in …
|
|
|
@1417
|
8 years |
boender |
- proved that jumps always increase - this should make termination easy
|
|
|
@1404
|
8 years |
boender |
- reworked + added
- added an axiom to arithmetic, but should be provable
|
|
|
@1393
|
8 years |
boender |
- added invariant for policy trie to assembly
- change (syntax only) …
|
|
|
@1363
|
8 years |
boender |
- done stuff with create_label_trie
|
|
|
@1309
|
8 years |
boender |
- refounded JEP
|
|
|
@1103
|
8 years |
boender |
- reverted to old policy
|
|
|
@1054
|
8 years |
boender |
- proven policy safe
|
|
|
@1040
|
8 years |
sacerdot |
Bug fixed in assembly.
|
|
|
@1014
|
8 years |
sacerdot |
The main theorem is completely broken (again).
|
|
|
@998
|
8 years |
sacerdot |
Half repaired, half broken. Most functions no longer return option …
|
|
|
@993
|
8 years |
sacerdot |
More Russell everywhere; getting closer to the goal.
|
|
|
@989
|
8 years |
sacerdot |
Type of build_maps strengthened.
|
|
|
@987
|
8 years |
sacerdot |
Real parameterization over the policy.
|
|
|
@985
|
8 years |
sacerdot |
1) Major refactoring: proofs moved where they should be.
2) New …
|
|
|
@982
|
8 years |
boender |
- this should work (see previous commit)
|
|
|
@938
|
9 years |
sacerdot |
…
|
|
|
@922
|
9 years |
mulligan |
changes to get assemblyproof to compile
|
|
|
@920
|
9 years |
boender |
- corrected mov instruction
|
|
|
@914
|
9 years |
boender |
- complete.
|
|
|
@913
|
9 years |
boender |
- temporary commit s.t. Assembly compiles
|
|
|
@907
|
9 years |
boender |
- added quadruples to Util
- start of implementation of new jump …
|
|
|
@846
|
9 years |
mulligan |
changes
|
|
|
@844
|
9 years |
sacerdot |
Useless code removed.
|
|
|
@842
|
9 years |
sacerdot |
Bug fixed.
|
|
|
@840
|
9 years |
sacerdot |
sigma defined
|
|
|
@837
|
9 years |
mulligan |
changes complete
|
|
|
@836
|
9 years |
mulligan |
changes to assembly functions
|
|
|
@833
|
9 years |
sacerdot |
Bug fixed to make the file compile.
But the type of the assembly …
|
|
|
@832
|
9 years |
mulligan |
work from today
|
|
|
@825
|
9 years |
mulligan |
lots of refactoring, finally got something to prove
|
|
|
@820
|
9 years |
mulligan |
changes to get the semantics of pseudoassembly working
|
|
|
@757
|
9 years |
mulligan |
Lots more fixing to get both front and backends using same conventions …
|
|
|
@719
|
9 years |
mulligan |
Added missing assembly file ported to matita.
|