| Sticky Revision: |
make nonce explicit
s/stream_nonce/series_nonce/
change syntax of hash and uia principals.
implement one-time-authenticator authority for alpaca. current only used to implement ping-of-death in llamalab.
Implemented a model version of planetlab. Supported operation: - contribute resources (disk) to the node - principal a grants quota to principal b - principal creates a "sliver" (virtual machine) on the node - sliver requests to grow its resource (disk) usage (modeled by a request by the principal)
fix error message handling.
move alpaca source tree into the uia trunk
change name to "sandbox" authority
implement vx wrapper (yet untested)
Move directory name pcp->alpaca
simple demo
fix __future__ in wrong place; add small demo harness add some random notes; set svn:ignore properties
caching to improve performance a bit...
handle newer version of pyparsing, with memoization changes I suggested to maintainer
further reorg
package reorganization and some resultant renames and bugfixes
paths change
reorganize and refactor tests
updated to use new pkcs1 framework
massive overhaul of pkcs1 code for spec compatibility
needed an __init__.py
update certificate chain and fix some minor bugs
after long travails, generated a single precious certificate chain.
fix x509 signature computation
x509 signature checking
x509 encoding/decoding
expanded ca endorsement theorem, sign using hash
ASN.1, DER, PKCS1 implemented. Many related changes.
various changes to support named integration.
various performance tuning, bug fixes, etc.
proof compression / serialization --- only gimpy version works.
streamlined api
untested eid delegation lemmas
fixup fresh variables
kill let command
streamline some theorem code.
eid principals with rsa signatures
encapsulate into principal classes
rsa proof
write lemmas and contexts for prover to support hash principals
logic axioms
tidy up interfaces again.
clean up lemmas and last usage, refactoring mostly done.
tabular authorities as instances, not classes.
get witnesses provisionally working again
bring principals into theorem land
encapsulate theorems as a statement with a proof.
proof combinator
fix subtle alpha-substitution/free-variable bugs.
replace all uses of 'apply' with new magic 'deduce', and fix consequent bugs.
new magic deducer, thank god that's working.
rsa key proving works.
importing authorities
function authorities, general refactoring of authorities.
math and encoding for integers
create integer constants
streamline parser. sadly, tests with psyco indicate that psyco is broken.
fix transition-related bugs, clean up code.
test cases
rewrite case->union, expression, proof classes.
finish tree and test-case reorg.
more tree reorg
reorganize tree
reorganize package
test suite tests right thing
swap names of beta-reduce and beta-abstract to be consistent with others.
reduce proof-generating kludginess.
main proof for hash principals compiles and checks out.
prove delegation theorems.
implement substitute and apply
keep track of lemmas.
proof inference in principals' contexts.
fix base64 encoding implement several authorities refactor proof command interpreter using decorator new claim checker
names
equals and says
modify sandbox branch
new sandbox branch
many changes dealing with level inference for contexts. kind of kludgey.
refactor some expression-munging code out of proof.py.
OK, level solving in proof inference seems to work, albeit in a minimal way! What a nice way to start the week.
new beta-reduction code works well now.
reworking beta-reduction search, taking a break for food.
new beta reduction checker, hopefully also better.
checkpoint last night's proof inference code.
partial proof inference engine.
more prover automation is good.
more believable level code
generalize level structure for proof inference
some definitions for data, skeletal uia context for reference only
hit a darn hairy snag.
various logic definitions
some very difficult manual proofs
pretty up the test suite.
proofs work again, with fancy generic types and all. 17 proofs in test suite all work again.
pull implicit levels from context
first step in reformulating parser for context. also some cleanup.
midway through restructuring more robust proof code
another checkpoint with broken proofs
more sophisticated generics support in parser
intermediate check-in --- non-working state, but there's just too many changes to kep everything in working copy anymore.
more related work
many bug fixes, progress on the message verification front, but unexpected badness on the paradox-avoiding front.
empty file needed to find modules
substitute constant
renaming of modules
rename directory
a whole bunch of stuff I've failed to check in before...
some hastily scribbled notes
notes dump
| Maintained by PDOS | ViewVC Help |
| Powered by ViewVC 1.0.3 |
Directory Listing