[acl2/acl2] 6b484c: [C2C] Extend `simpadd0` proof generation.
0 views
Skip to first unread message
Alessandro Coglio
Jun 1, 2025, 12:18:44 AM6/1/25
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 6b484cf05ec26e4b2b5ad2ef6f51438030d77777
https://github.com/acl2/acl2/commit/6b484cf05ec26e4b2b5ad2ef6f51438030d77777
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Extend `simpadd0` proof generation.
Add preliminary support for conditional expressions. A few more things need to
be added for full support.
Commit: 3e3435038ff52b1c28d3cf512cd2fabdd013f83d
https://github.com/acl2/acl2/commit/3e3435038ff52b1c28d3cf512cd2fabdd013f83d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
Log Message:
-----------
[C$] Extend type calculation from annotations.
Add some initial handling for conditional expressions.
Commit: 3246ef100ec9e65c8875d03c373618aeec51544d
https://github.com/acl2/acl2/commit/3246ef100ec9e65c8875d03c373618aeec51544d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/language/implementation-environments.lisp
Log Message:
-----------
[C] Add a theorem.
Commit: 83fb1980286a57409d2ad3ee3d30255cc9dc9ea6
https://github.com/acl2/acl2/commit/83fb1980286a57409d2ad3ee3d30255cc9dc9ea6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/language/implementation-environments.lisp
Log Message:
-----------
[C] Add a theorem about implementation environments.
Commit: 423350e04317f9fc7a4a0af612d6b0321970075a
https://github.com/acl2/acl2/commit/423350e04317f9fc7a4a0af612d6b0321970075a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/language/implementation-environments.lisp
Log Message:
-----------
[C] Explain two theorems.
Also lowercase a rule name.
Commit: 248d6c5c9968d52e93ca4c39cf4d4368317fffea
https://github.com/acl2/acl2/commit/248d6c5c9968d52e93ca4c39cf4d4368317fffea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/language/implementation-environments.lisp
Log Message:
-----------
[C] Add a theorem about implementation environments.
Commit: 5137233dd1e87765858c5b377c4fd9399b6fd913
https://github.com/acl2/acl2/commit/5137233dd1e87765858c5b377c4fd9399b6fd913
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/auto-termination/td-cands.acl2
M books/kestrel/auto-termination/td-cands.lisp
A books/projects/aleo/README.md
M books/projects/aleo/bft/README.md
A books/projects/aleo/bft/addresses.lisp
A books/projects/aleo/bft/anchors-extension.lisp
A books/projects/aleo/bft/anchors.lisp
R books/projects/aleo/bft/arxiv/acl2-customization.lsp
R books/projects/aleo/bft/arxiv/addresses.lisp
R books/projects/aleo/bft/arxiv/anchors-extension.lisp
R books/projects/aleo/bft/arxiv/anchors.lisp
R books/projects/aleo/bft/arxiv/backward-closure.lisp
R books/projects/aleo/bft/arxiv/blockchain-redundant-def-and-init-and-next.lisp
R books/projects/aleo/bft/arxiv/blockchain-redundant.lisp
R books/projects/aleo/bft/arxiv/blockchains.lisp
R books/projects/aleo/bft/arxiv/blocks.lisp
R books/projects/aleo/bft/arxiv/cert.acl2
R books/projects/aleo/bft/arxiv/certificates.lisp
R books/projects/aleo/bft/arxiv/committed-anchor-sequences.lisp
R books/projects/aleo/bft/arxiv/committed-redundant-def-and-init-and-next.lisp
R books/projects/aleo/bft/arxiv/committed-redundant.lisp
R books/projects/aleo/bft/arxiv/committees.lisp
R books/projects/aleo/bft/arxiv/correctness.lisp
R books/projects/aleo/bft/arxiv/dag-certificate-next.lisp
R books/projects/aleo/bft/arxiv/dag-omni-paths.lisp
R books/projects/aleo/bft/arxiv/dag-previous-quorum-def-and-init-and-next.lisp
R books/projects/aleo/bft/arxiv/dag-previous-quorum.lisp
R books/projects/aleo/bft/arxiv/dags.lisp
R books/projects/aleo/bft/arxiv/definition.lisp
R books/projects/aleo/bft/arxiv/elections.lisp
R books/projects/aleo/bft/arxiv/events.lisp
R books/projects/aleo/bft/arxiv/fault-tolerance.lisp
R books/projects/aleo/bft/arxiv/initialization.lisp
R books/projects/aleo/bft/arxiv/last-anchor-def-and-init.lisp
R books/projects/aleo/bft/arxiv/last-anchor-next.lisp
R books/projects/aleo/bft/arxiv/last-anchor-present.lisp
R books/projects/aleo/bft/arxiv/last-anchor-voters-def-and-init-and-next.lisp
R books/projects/aleo/bft/arxiv/last-anchor-voters.lisp
R books/projects/aleo/bft/arxiv/last-blockchain-round.lisp
R books/projects/aleo/bft/arxiv/messages.lisp
R books/projects/aleo/bft/arxiv/no-self-endorsed.lisp
R books/projects/aleo/bft/arxiv/nonforking-anchors-def-and-init-and-next.lisp
R books/projects/aleo/bft/arxiv/nonforking-anchors.lisp
R books/projects/aleo/bft/arxiv/nonforking-blockchains-def-and-init.lisp
R books/projects/aleo/bft/arxiv/nonforking-blockchains-next.lisp
R books/projects/aleo/bft/arxiv/nonforking-blockchains.lisp
R books/projects/aleo/bft/arxiv/omni-paths-def-and-implied.lisp
R books/projects/aleo/bft/arxiv/omni-paths.lisp
R books/projects/aleo/bft/arxiv/ordered-even-blocks.lisp
R books/projects/aleo/bft/arxiv/package.lsp
R books/projects/aleo/bft/arxiv/portcullis.acl2
R books/projects/aleo/bft/arxiv/portcullis.lisp
R books/projects/aleo/bft/arxiv/quorum-intersection.lisp
R books/projects/aleo/bft/arxiv/reachability.lisp
R books/projects/aleo/bft/arxiv/same-committees-def-and-implied.lisp
R books/projects/aleo/bft/arxiv/same-committees.lisp
R books/projects/aleo/bft/arxiv/signed-certificates.lisp
R books/projects/aleo/bft/arxiv/signed-previous-quorum.lisp
R books/projects/aleo/bft/arxiv/signer-quorum.lisp
R books/projects/aleo/bft/arxiv/signer-records.lisp
R books/projects/aleo/bft/arxiv/simultaneous-induction.lisp
R books/projects/aleo/bft/arxiv/states.lisp
R books/projects/aleo/bft/arxiv/successor-predecessor-intersection.lisp
R books/projects/aleo/bft/arxiv/system-certificates.lisp
R books/projects/aleo/bft/arxiv/system-states.lisp
R books/projects/aleo/bft/arxiv/top.lisp
R books/projects/aleo/bft/arxiv/transactions.lisp
R books/projects/aleo/bft/arxiv/transitions-accept.lisp
R books/projects/aleo/bft/arxiv/transitions-advance.lisp
R books/projects/aleo/bft/arxiv/transitions-commit.lisp
R books/projects/aleo/bft/arxiv/transitions-create.lisp
R books/projects/aleo/bft/arxiv/transitions.lisp
R books/projects/aleo/bft/arxiv/unequivocal-dags-def-and-init.lisp
R books/projects/aleo/bft/arxiv/unequivocal-dags-next.lisp
R books/projects/aleo/bft/arxiv/unequivocal-dags.lisp
R books/projects/aleo/bft/arxiv/unequivocal-signed-certificates.lisp
R books/projects/aleo/bft/arxiv/validator-states.lisp
A books/projects/aleo/bft/backward-closure.lisp
A books/projects/aleo/bft/blockchain-redundant-def-and-init-and-next.lisp
A books/projects/aleo/bft/blockchain-redundant.lisp
A books/projects/aleo/bft/blockchains.lisp
A books/projects/aleo/bft/blocks.lisp
A books/projects/aleo/bft/certificates.lisp
A books/projects/aleo/bft/committed-anchor-sequences.lisp
A books/projects/aleo/bft/committed-redundant-def-and-init-and-next.lisp
A books/projects/aleo/bft/committed-redundant.lisp
A books/projects/aleo/bft/committees.lisp
A books/projects/aleo/bft/correctness.lisp
A books/projects/aleo/bft/dag-certificate-next.lisp
A books/projects/aleo/bft/dag-omni-paths.lisp
A books/projects/aleo/bft/dag-previous-quorum-def-and-init-and-next.lisp
A books/projects/aleo/bft/dag-previous-quorum.lisp
A books/projects/aleo/bft/dags.lisp
A books/projects/aleo/bft/definition.lisp
R books/projects/aleo/bft/dynamic/accepted-certificate-committee.lisp
R books/projects/aleo/bft/dynamic/acl2-customization.lsp
R books/projects/aleo/bft/dynamic/addresses.lisp
R books/projects/aleo/bft/dynamic/anchors-extension.lisp
R books/projects/aleo/bft/dynamic/anchors.lisp
R books/projects/aleo/bft/dynamic/backward-closure.lisp
R books/projects/aleo/bft/dynamic/blockchain-redundant-def-and-init-and-next.lisp
R books/projects/aleo/bft/dynamic/blockchain-redundant.lisp
R books/projects/aleo/bft/dynamic/blockchains.lisp
R books/projects/aleo/bft/dynamic/blocks.lisp
R books/projects/aleo/bft/dynamic/cert.acl2
R books/projects/aleo/bft/dynamic/certificates-of-validators.lisp
R books/projects/aleo/bft/dynamic/certificates.lisp
R books/projects/aleo/bft/dynamic/committed-anchor-sequences.lisp
R books/projects/aleo/bft/dynamic/committed-redundant-def-and-init-and-next.lisp
R books/projects/aleo/bft/dynamic/committed-redundant.lisp
R books/projects/aleo/bft/dynamic/committees-in-system.lisp
R books/projects/aleo/bft/dynamic/committees.lisp
R books/projects/aleo/bft/dynamic/correctness.lisp
R books/projects/aleo/bft/dynamic/dag-certificate-next.lisp
R books/projects/aleo/bft/dynamic/dag-omni-paths.lisp
R books/projects/aleo/bft/dynamic/dags.lisp
R books/projects/aleo/bft/dynamic/definition.lisp
R books/projects/aleo/bft/dynamic/elections.lisp
R books/projects/aleo/bft/dynamic/events.lisp
R books/projects/aleo/bft/dynamic/fault-tolerance.lisp
R books/projects/aleo/bft/dynamic/initialization.lisp
R books/projects/aleo/bft/dynamic/last-anchor-def-and-init.lisp
R books/projects/aleo/bft/dynamic/last-anchor-next.lisp
R books/projects/aleo/bft/dynamic/last-anchor-present.lisp
R books/projects/aleo/bft/dynamic/last-anchor-voters-def-and-init-and-next.lisp
R books/projects/aleo/bft/dynamic/last-anchor-voters.lisp
R books/projects/aleo/bft/dynamic/last-blockchain-round.lisp
R books/projects/aleo/bft/dynamic/messages.lisp
R books/projects/aleo/bft/dynamic/no-self-buffer.lisp
R books/projects/aleo/bft/dynamic/no-self-endorsed.lisp
R books/projects/aleo/bft/dynamic/no-self-messages.lisp
R books/projects/aleo/bft/dynamic/nonforking-anchors-def-and-init-and-next.lisp
R books/projects/aleo/bft/dynamic/nonforking-anchors.lisp
R books/projects/aleo/bft/dynamic/nonforking-blockchains-def-and-init.lisp
R books/projects/aleo/bft/dynamic/nonforking-blockchains-next.lisp
R books/projects/aleo/bft/dynamic/nonforking-blockchains.lisp
R books/projects/aleo/bft/dynamic/omni-paths-def-and-implied.lisp
R books/projects/aleo/bft/dynamic/omni-paths.lisp
R books/projects/aleo/bft/dynamic/ordered-even-blocks.lisp
R books/projects/aleo/bft/dynamic/package.lsp
R books/projects/aleo/bft/dynamic/portcullis.acl2
R books/projects/aleo/bft/dynamic/portcullis.lisp
R books/projects/aleo/bft/dynamic/previous-quorum.lisp
R books/projects/aleo/bft/dynamic/quorum-intersection.lisp
R books/projects/aleo/bft/dynamic/rounds-in-committees.lisp
R books/projects/aleo/bft/dynamic/same-committees-def-and-implied.lisp
R books/projects/aleo/bft/dynamic/same-committees.lisp
R books/projects/aleo/bft/dynamic/same-owned-certificates.lisp
R books/projects/aleo/bft/dynamic/signer-quorum.lisp
R books/projects/aleo/bft/dynamic/signer-records.lisp
R books/projects/aleo/bft/dynamic/simultaneous-induction.lisp
R books/projects/aleo/bft/dynamic/states.lisp
R books/projects/aleo/bft/dynamic/successor-predecessor-intersection.lisp
R books/projects/aleo/bft/dynamic/system-states.lisp
R books/projects/aleo/bft/dynamic/top.lisp
R books/projects/aleo/bft/dynamic/transactions.lisp
R books/projects/aleo/bft/dynamic/transitions-advance-round.lisp
R books/projects/aleo/bft/dynamic/transitions-commit-anchors.lisp
R books/projects/aleo/bft/dynamic/transitions-create-certificate.lisp
R books/projects/aleo/bft/dynamic/transitions-receive-certificate.lisp
R books/projects/aleo/bft/dynamic/transitions-store-certificate.lisp
R books/projects/aleo/bft/dynamic/transitions-timer-expires.lisp
R books/projects/aleo/bft/dynamic/transitions.lisp
R books/projects/aleo/bft/dynamic/unequivocal-accepted-certificates-def-and-init.lisp
R books/projects/aleo/bft/dynamic/unequivocal-accepted-certificates-next.lisp
R books/projects/aleo/bft/dynamic/unequivocal-accepted-certificates.lisp
R books/projects/aleo/bft/dynamic/unequivocal-signed-certificates.lisp
R books/projects/aleo/bft/dynamic/validator-states.lisp
A books/projects/aleo/bft/elections.lisp
A books/projects/aleo/bft/events.lisp
A books/projects/aleo/bft/fault-tolerance.lisp
A books/projects/aleo/bft/initialization.lisp
A books/projects/aleo/bft/last-anchor-def-and-init.lisp
A books/projects/aleo/bft/last-anchor-next.lisp
A books/projects/aleo/bft/last-anchor-present.lisp
A books/projects/aleo/bft/last-anchor-voters-def-and-init-and-next.lisp
A books/projects/aleo/bft/last-anchor-voters.lisp
A books/projects/aleo/bft/last-blockchain-round.lisp
M books/projects/aleo/bft/library-extensions/oset-theorems.lisp
A books/projects/aleo/bft/messages.lisp
A books/projects/aleo/bft/next/acl2-customization.lsp
A books/projects/aleo/bft/next/active-committees-after-commit.lisp
A books/projects/aleo/bft/next/addresses.lisp
A books/projects/aleo/bft/next/anchors.lisp
A books/projects/aleo/bft/next/author-round-pairs-in-validators.lisp
A books/projects/aleo/bft/next/blockchains.lisp
A books/projects/aleo/bft/next/blocks.lisp
A books/projects/aleo/bft/next/cert.acl2
A books/projects/aleo/bft/next/certificate-in-author.lisp
A books/projects/aleo/bft/next/certificate-to-other.lisp
A books/projects/aleo/bft/next/certificates.lisp
A books/projects/aleo/bft/next/committees.lisp
A books/projects/aleo/bft/next/correctness.lisp
A books/projects/aleo/bft/next/dag-previous-closed.lisp
A books/projects/aleo/bft/next/dags.lisp
A books/projects/aleo/bft/next/definition.lisp
A books/projects/aleo/bft/next/elections.lisp
A books/projects/aleo/bft/next/endorsed-author-other.lisp
A books/projects/aleo/bft/next/endorsed-in-author.lisp
A books/projects/aleo/bft/next/endorsed-previous-closed.lisp
A books/projects/aleo/bft/next/endorsed-round1-no-previous.lisp
A books/projects/aleo/bft/next/endorsement-from-other.lisp
A books/projects/aleo/bft/next/endorsement-in-author.lisp
A books/projects/aleo/bft/next/endorsement-in-endorser.lisp
A books/projects/aleo/bft/next/events.lisp
A books/projects/aleo/bft/next/fault-tolerance.lisp
A books/projects/aleo/bft/next/initialization.lisp
A books/projects/aleo/bft/next/last-anchor-def.lisp
A books/projects/aleo/bft/next/last-anchor-init-and-next.lisp
A books/projects/aleo/bft/next/last-anchor-present.lisp
A books/projects/aleo/bft/next/last-anchor-voters.lisp
A books/projects/aleo/bft/next/last-blockchain-round.lisp
A books/projects/aleo/bft/next/messages.lisp
A books/projects/aleo/bft/next/nonforking-blockchains-def-and-init.lisp
A books/projects/aleo/bft/next/ordered-blockchain.lisp
A books/projects/aleo/bft/next/portcullis.acl2
A books/projects/aleo/bft/next/portcullis.lisp
A books/projects/aleo/bft/next/proposal-in-author.lisp
A books/projects/aleo/bft/next/proposal-to-other.lisp
A books/projects/aleo/bft/next/proposals.lisp
A books/projects/aleo/bft/next/proposed-author-in-committee.lisp
A books/projects/aleo/bft/next/proposed-author-self.lisp
A books/projects/aleo/bft/next/proposed-disjoint-dag.lisp
A books/projects/aleo/bft/next/proposed-endorser-in-committee.lisp
A books/projects/aleo/bft/next/proposed-endorser-other.lisp
A books/projects/aleo/bft/next/proposed-previous-closed.lisp
A books/projects/aleo/bft/next/proposed-round1-no-previous.lisp
A books/projects/aleo/bft/next/quorum-intersection.lisp
A books/projects/aleo/bft/next/reachability.lisp
A books/projects/aleo/bft/next/round-after-last.lisp
A books/projects/aleo/bft/next/same-committees-def-and-implied.lisp
A books/projects/aleo/bft/next/signed-in-signer.lisp
A books/projects/aleo/bft/next/signed-proposals.lisp
A books/projects/aleo/bft/next/signer-quorum.lisp
A books/projects/aleo/bft/next/states.lisp
A books/projects/aleo/bft/next/system-states.lisp
A books/projects/aleo/bft/next/top.lisp
A books/projects/aleo/bft/next/transactions.lisp
A books/projects/aleo/bft/next/transitions-accept.lisp
A books/projects/aleo/bft/next/transitions-advance.lisp
A books/projects/aleo/bft/next/transitions-augment.lisp
A books/projects/aleo/bft/next/transitions-certify.lisp
A books/projects/aleo/bft/next/transitions-commit.lisp
A books/projects/aleo/bft/next/transitions-endorse.lisp
A books/projects/aleo/bft/next/transitions-propose.lisp
A books/projects/aleo/bft/next/transitions.lisp
A books/projects/aleo/bft/next/unequivocal-dag.lisp
A books/projects/aleo/bft/next/unequivocal-proposed.lisp
A books/projects/aleo/bft/next/unequivocal-signed-proposals.lisp
A books/projects/aleo/bft/next/validator-states.lisp
A books/projects/aleo/bft/no-self-endorsed.lisp
A books/projects/aleo/bft/nonforking-anchors-def-and-init-and-next.lisp
A books/projects/aleo/bft/nonforking-anchors.lisp
A books/projects/aleo/bft/nonforking-blockchains-def-and-init.lisp
A books/projects/aleo/bft/nonforking-blockchains-next.lisp
A books/projects/aleo/bft/nonforking-blockchains.lisp
A books/projects/aleo/bft/omni-paths-def-and-implied.lisp
A books/projects/aleo/bft/omni-paths.lisp
A books/projects/aleo/bft/ordered-even-blocks.lisp
M books/projects/aleo/bft/package.lsp
R books/projects/aleo/bft/proposals/acl2-customization.lsp
R books/projects/aleo/bft/proposals/active-committees-after-commit.lisp
R books/projects/aleo/bft/proposals/addresses.lisp
R books/projects/aleo/bft/proposals/anchors.lisp
R books/projects/aleo/bft/proposals/author-round-pairs-in-validators.lisp
R books/projects/aleo/bft/proposals/blockchains.lisp
R books/projects/aleo/bft/proposals/blocks.lisp
R books/projects/aleo/bft/proposals/cert.acl2
R books/projects/aleo/bft/proposals/certificate-in-author.lisp
R books/projects/aleo/bft/proposals/certificate-to-other.lisp
R books/projects/aleo/bft/proposals/certificates.lisp
R books/projects/aleo/bft/proposals/committees.lisp
R books/projects/aleo/bft/proposals/correctness.lisp
R books/projects/aleo/bft/proposals/dag-previous-closed.lisp
R books/projects/aleo/bft/proposals/dags.lisp
R books/projects/aleo/bft/proposals/definition.lisp
R books/projects/aleo/bft/proposals/elections.lisp
R books/projects/aleo/bft/proposals/endorsed-author-other.lisp
R books/projects/aleo/bft/proposals/endorsed-in-author.lisp
R books/projects/aleo/bft/proposals/endorsed-previous-closed.lisp
R books/projects/aleo/bft/proposals/endorsed-round1-no-previous.lisp
R books/projects/aleo/bft/proposals/endorsement-from-other.lisp
R books/projects/aleo/bft/proposals/endorsement-in-author.lisp
R books/projects/aleo/bft/proposals/endorsement-in-endorser.lisp
R books/projects/aleo/bft/proposals/events.lisp
R books/projects/aleo/bft/proposals/fault-tolerance.lisp
R books/projects/aleo/bft/proposals/initialization.lisp
R books/projects/aleo/bft/proposals/last-anchor-def.lisp
R books/projects/aleo/bft/proposals/last-anchor-init-and-next.lisp
R books/projects/aleo/bft/proposals/last-anchor-present.lisp
R books/projects/aleo/bft/proposals/last-anchor-voters.lisp
R books/projects/aleo/bft/proposals/last-blockchain-round.lisp
R books/projects/aleo/bft/proposals/messages.lisp
R books/projects/aleo/bft/proposals/nonforking-blockchains-def-and-init.lisp
R books/projects/aleo/bft/proposals/ordered-blockchain.lisp
R books/projects/aleo/bft/proposals/package.lsp
R books/projects/aleo/bft/proposals/portcullis.acl2
R books/projects/aleo/bft/proposals/portcullis.lisp
R books/projects/aleo/bft/proposals/proposal-in-author.lisp
R books/projects/aleo/bft/proposals/proposal-to-other.lisp
R books/projects/aleo/bft/proposals/proposals.lisp
R books/projects/aleo/bft/proposals/proposed-author-in-committee.lisp
R books/projects/aleo/bft/proposals/proposed-author-self.lisp
R books/projects/aleo/bft/proposals/proposed-disjoint-dag.lisp
R books/projects/aleo/bft/proposals/proposed-endorser-in-committee.lisp
R books/projects/aleo/bft/proposals/proposed-endorser-other.lisp
R books/projects/aleo/bft/proposals/proposed-previous-closed.lisp
R books/projects/aleo/bft/proposals/proposed-round1-no-previous.lisp
R books/projects/aleo/bft/proposals/quorum-intersection.lisp
R books/projects/aleo/bft/proposals/reachability.lisp
R books/projects/aleo/bft/proposals/round-after-last.lisp
R books/projects/aleo/bft/proposals/same-committees-def-and-implied.lisp
R books/projects/aleo/bft/proposals/signed-in-signer.lisp
R books/projects/aleo/bft/proposals/signed-proposals.lisp
R books/projects/aleo/bft/proposals/signer-quorum.lisp
R books/projects/aleo/bft/proposals/states.lisp
R books/projects/aleo/bft/proposals/system-states.lisp
R books/projects/aleo/bft/proposals/top.lisp
R books/projects/aleo/bft/proposals/transactions.lisp
R books/projects/aleo/bft/proposals/transitions-accept.lisp
R books/projects/aleo/bft/proposals/transitions-advance.lisp
R books/projects/aleo/bft/proposals/transitions-augment.lisp
R books/projects/aleo/bft/proposals/transitions-certify.lisp
R books/projects/aleo/bft/proposals/transitions-commit.lisp
R books/projects/aleo/bft/proposals/transitions-endorse.lisp
R books/projects/aleo/bft/proposals/transitions-propose.lisp
R books/projects/aleo/bft/proposals/transitions.lisp
R books/projects/aleo/bft/proposals/unequivocal-dag.lisp
R books/projects/aleo/bft/proposals/unequivocal-proposed.lisp
R books/projects/aleo/bft/proposals/unequivocal-signed-proposals.lisp
R books/projects/aleo/bft/proposals/validator-states.lisp
A books/projects/aleo/bft/quorum-intersection.lisp
A books/projects/aleo/bft/reachability.lisp
A books/projects/aleo/bft/same-committees-def-and-implied.lisp
A books/projects/aleo/bft/same-committees.lisp
A books/projects/aleo/bft/signed-certificates.lisp
A books/projects/aleo/bft/signed-previous-quorum.lisp
A books/projects/aleo/bft/signer-quorum.lisp
A books/projects/aleo/bft/signer-records.lisp
A books/projects/aleo/bft/simultaneous-induction.lisp
R books/projects/aleo/bft/stake/acl2-customization.lsp
R books/projects/aleo/bft/stake/addresses.lisp
R books/projects/aleo/bft/stake/anchors-extension.lisp
R books/projects/aleo/bft/stake/anchors.lisp
R books/projects/aleo/bft/stake/associated-certificates.lisp
R books/projects/aleo/bft/stake/backward-closure.lisp
R books/projects/aleo/bft/stake/blockchain-redundant-def-and-init-and-next.lisp
R books/projects/aleo/bft/stake/blockchain-redundant.lisp
R books/projects/aleo/bft/stake/blockchains.lisp
R books/projects/aleo/bft/stake/blocks.lisp
R books/projects/aleo/bft/stake/cert.acl2
R books/projects/aleo/bft/stake/certificates.lisp
R books/projects/aleo/bft/stake/committed-anchor-sequences.lisp
R books/projects/aleo/bft/stake/committed-redundant-def-and-init-and-next.lisp
R books/projects/aleo/bft/stake/committed-redundant.lisp
R books/projects/aleo/bft/stake/committees.lisp
R books/projects/aleo/bft/stake/correctness.lisp
R books/projects/aleo/bft/stake/dag-certificate-next.lisp
R books/projects/aleo/bft/stake/dag-committees.lisp
R books/projects/aleo/bft/stake/dag-omni-paths.lisp
R books/projects/aleo/bft/stake/dags.lisp
R books/projects/aleo/bft/stake/definition.lisp
R books/projects/aleo/bft/stake/elections.lisp
R books/projects/aleo/bft/stake/events.lisp
R books/projects/aleo/bft/stake/fault-tolerance.lisp
R books/projects/aleo/bft/stake/initialization.lisp
R books/projects/aleo/bft/stake/last-anchor-def-and-init.lisp
R books/projects/aleo/bft/stake/last-anchor-next.lisp
R books/projects/aleo/bft/stake/last-anchor-present.lisp
R books/projects/aleo/bft/stake/last-anchor-voters-def-and-init-and-next.lisp
R books/projects/aleo/bft/stake/last-anchor-voters.lisp
R books/projects/aleo/bft/stake/last-blockchain-round.lisp
R books/projects/aleo/bft/stake/messages.lisp
R books/projects/aleo/bft/stake/no-self-buffer.lisp
R books/projects/aleo/bft/stake/no-self-endorsed.lisp
R books/projects/aleo/bft/stake/no-self-messages.lisp
R books/projects/aleo/bft/stake/nonforking-anchors-def-and-init-and-next.lisp
R books/projects/aleo/bft/stake/nonforking-anchors.lisp
R books/projects/aleo/bft/stake/nonforking-blockchains-def-and-init.lisp
R books/projects/aleo/bft/stake/nonforking-blockchains-next.lisp
R books/projects/aleo/bft/stake/nonforking-blockchains.lisp
R books/projects/aleo/bft/stake/omni-paths-def-and-implied.lisp
R books/projects/aleo/bft/stake/omni-paths.lisp
R books/projects/aleo/bft/stake/ordered-even-blocks.lisp
R books/projects/aleo/bft/stake/package.lsp
R books/projects/aleo/bft/stake/portcullis.acl2
R books/projects/aleo/bft/stake/portcullis.lisp
R books/projects/aleo/bft/stake/previous-quorum-def-and-init-and-next.lisp
R books/projects/aleo/bft/stake/previous-quorum.lisp
R books/projects/aleo/bft/stake/quorum-intersection.lisp
R books/projects/aleo/bft/stake/same-associated-certificates.lisp
R books/projects/aleo/bft/stake/same-committees-def-and-implied.lisp
R books/projects/aleo/bft/stake/same-committees.lisp
R books/projects/aleo/bft/stake/signed-and-associated-cerificates.lisp
R books/projects/aleo/bft/stake/signed-certificates.lisp
R books/projects/aleo/bft/stake/signed-previous-quorum.lisp
R books/projects/aleo/bft/stake/signer-quorum.lisp
R books/projects/aleo/bft/stake/signer-records.lisp
R books/projects/aleo/bft/stake/simultaneous-induction.lisp
R books/projects/aleo/bft/stake/states.lisp
R books/projects/aleo/bft/stake/successor-predecessor-intersection.lisp
R books/projects/aleo/bft/stake/system-states.lisp
R books/projects/aleo/bft/stake/top.lisp
R books/projects/aleo/bft/stake/transactions.lisp
R books/projects/aleo/bft/stake/transitions-advance.lisp
R books/projects/aleo/bft/stake/transitions-commit.lisp
R books/projects/aleo/bft/stake/transitions-create.lisp
R books/projects/aleo/bft/stake/transitions-receive.lisp
R books/projects/aleo/bft/stake/transitions-store.lisp
R books/projects/aleo/bft/stake/transitions-timeout.lisp
R books/projects/aleo/bft/stake/transitions.lisp
R books/projects/aleo/bft/stake/unequivocal-dags-def-and-init.lisp
R books/projects/aleo/bft/stake/unequivocal-dags-next.lisp
R books/projects/aleo/bft/stake/unequivocal-dags.lisp
R books/projects/aleo/bft/stake/unequivocal-signed-certificates.lisp
R books/projects/aleo/bft/stake/validator-states.lisp
A books/projects/aleo/bft/states.lisp
R books/projects/aleo/bft/static/acl2-customization.lsp
R books/projects/aleo/bft/static/addresses.lisp
R books/projects/aleo/bft/static/blocks.lisp
R books/projects/aleo/bft/static/cert.acl2
R books/projects/aleo/bft/static/certificates.lisp
R books/projects/aleo/bft/static/correctness.lisp
R books/projects/aleo/bft/static/definition.lisp
R books/projects/aleo/bft/static/events.lisp
R books/projects/aleo/bft/static/initialization.lisp
R books/projects/aleo/bft/static/invariant-addresses.lisp
R books/projects/aleo/bft/static/invariant-anchors-not-forking.lisp
R books/projects/aleo/bft/static/invariant-blockchain-not-forking.lisp
R books/projects/aleo/bft/static/invariant-blockchain-redundant.lisp
R books/projects/aleo/bft/static/invariant-causal-histories.lisp
R books/projects/aleo/bft/static/invariant-certificate-retrieval.lisp
R books/projects/aleo/bft/static/invariant-committed-redundant.lisp
R books/projects/aleo/bft/static/invariant-dag-authors-are-validators.lisp
R books/projects/aleo/bft/static/invariant-dag-previous-are-quorum.lisp
R books/projects/aleo/bft/static/invariant-fault-tolerance.lisp
R books/projects/aleo/bft/static/invariant-last-anchor-present.lisp
R books/projects/aleo/bft/static/invariant-last-anchor-voters.lisp
R books/projects/aleo/bft/static/invariant-last-before-current.lisp
R books/projects/aleo/bft/static/invariant-last-is-even.lisp
R books/projects/aleo/bft/static/invariant-max-faulty.lisp
R books/projects/aleo/bft/static/invariant-messages-to-correct.lisp
R books/projects/aleo/bft/static/invariant-no-self-buffer.lisp
R books/projects/aleo/bft/static/invariant-no-self-endorsed.lisp
R books/projects/aleo/bft/static/invariant-no-self-messages.lisp
R books/projects/aleo/bft/static/invariant-paths-to-last-anchor.lisp
R books/projects/aleo/bft/static/invariant-paths-to-other-last-anchor.lisp
R books/projects/aleo/bft/static/invariant-previous-are-quorum.lisp
R books/projects/aleo/bft/static/invariant-previous-in-dag.lisp
R books/projects/aleo/bft/static/invariant-quorum.lisp
R books/projects/aleo/bft/static/invariant-same-certificates.lisp
R books/projects/aleo/bft/static/invariant-signers-are-quorum.lisp
R books/projects/aleo/bft/static/invariant-signers-are-validators.lisp
R books/projects/aleo/bft/static/invariant-signers-have-author-round.lisp
R books/projects/aleo/bft/static/invariant-unequivocal-certificates.lisp
R books/projects/aleo/bft/static/invariant-unequivocal-dag.lisp
R books/projects/aleo/bft/static/invariant-unequivocal-dags.lisp
R books/projects/aleo/bft/static/messages.lisp
R books/projects/aleo/bft/static/operations-additional.lisp
R books/projects/aleo/bft/static/operations-anchors.lisp
R books/projects/aleo/bft/static/operations-author-round-pairs.lisp
R books/projects/aleo/bft/static/operations-blockchain-additional.lisp
R books/projects/aleo/bft/static/operations-blockchain.lisp
R books/projects/aleo/bft/static/operations-certificates-for-validators.lisp
R books/projects/aleo/bft/static/operations-dags-additional.lisp
R books/projects/aleo/bft/static/operations-dags.lisp
R books/projects/aleo/bft/static/operations-fault-tolerance.lisp
R books/projects/aleo/bft/static/operations-faults-and-quora.lisp
R books/projects/aleo/bft/static/operations-leaders.lisp
R books/projects/aleo/bft/static/operations-message-creation.lisp
R books/projects/aleo/bft/static/operations-previous-certificates.lisp
R books/projects/aleo/bft/static/operations-unequivocal-certificates.lisp
R books/projects/aleo/bft/static/operations-voting.lisp
R books/projects/aleo/bft/static/operations.lisp
R books/projects/aleo/bft/static/package.lsp
R books/projects/aleo/bft/static/portcullis.acl2
R books/projects/aleo/bft/static/portcullis.lisp
R books/projects/aleo/bft/static/properties-anchors-extension.lisp
R books/projects/aleo/bft/static/properties-anchors.lisp
R books/projects/aleo/bft/static/properties-blockchain.lisp
R books/projects/aleo/bft/static/properties-certificate-retrieval.lisp
R books/projects/aleo/bft/static/properties-dags.lisp
R books/projects/aleo/bft/static/property-committed-anchors-of-next-event.lisp
R books/projects/aleo/bft/static/property-last-anchor-of-next-event.lisp
R books/projects/aleo/bft/static/property-paths-to-other-voted-anchor.lisp
R books/projects/aleo/bft/static/property-paths-to-voted-anchor.lisp
R books/projects/aleo/bft/static/states.lisp
R books/projects/aleo/bft/static/system-states.lisp
R books/projects/aleo/bft/static/top.lisp
R books/projects/aleo/bft/static/transactions.lisp
R books/projects/aleo/bft/static/transitions-advance-round.lisp
R books/projects/aleo/bft/static/transitions-commit-anchors.lisp
R books/projects/aleo/bft/static/transitions-create-certificate.lisp
R books/projects/aleo/bft/static/transitions-receive-certificate.lisp
R books/projects/aleo/bft/static/transitions-store-certificate.lisp
R books/projects/aleo/bft/static/transitions-timer-expires.lisp
R books/projects/aleo/bft/static/transitions.lisp
R books/projects/aleo/bft/static/validator-states.lisp
A books/projects/aleo/bft/successor-predecessor-intersection.lisp
A books/projects/aleo/bft/system-certificates.lisp
A books/projects/aleo/bft/system-states.lisp
M books/projects/aleo/bft/top.lisp
A books/projects/aleo/bft/transactions.lisp
A books/projects/aleo/bft/transitions-accept.lisp
A books/projects/aleo/bft/transitions-advance.lisp
A books/projects/aleo/bft/transitions-commit.lisp
A books/projects/aleo/bft/transitions-create.lisp
A books/projects/aleo/bft/transitions.lisp
A books/projects/aleo/bft/unequivocal-dags-def-and-init.lisp
A books/projects/aleo/bft/unequivocal-dags-next.lisp
A books/projects/aleo/bft/unequivocal-dags.lisp
A books/projects/aleo/bft/unequivocal-signed-certificates.lisp
A books/projects/aleo/bft/validator-states.lisp
R books/projects/aleo/leo/.sys/gra...@useless-runes.lsp
R books/projects/aleo/leo/.sys/portc...@useless-runes.lsp
R books/projects/aleo/leo/.sys/t...@useless-runes.lsp
A books/projects/aleo/leo/README.md
M books/projects/aleo/leo/cert.acl2
M books/projects/aleo/leo/grammar.lisp
M books/projects/aleo/leo/portcullis.lisp
Log Message:
-----------
Merge.
Commit: 893fe3694a4b260ee93d946e40dbaddf7440e07e
https://github.com/acl2/acl2/commit/893fe3694a4b260ee93d946e40dbaddf7440e07e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Extend `simpadd0` proof generation.
Refine the generated hints for conditional expressions, which are now thus
supported.
Commit: 3ad012b79a571b43a14c477a00aeaf3dd8234877
https://github.com/acl2/acl2/commit/3ad012b79a571b43a14c477a00aeaf3dd8234877
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
Merge.
Commit: 968a72cc5a0bcc33628c5384aece0ac23d376e42
https://github.com/acl2/acl2/commit/968a72cc5a0bcc33628c5384aece0ac23d376e42
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/risc-v/decoding.lisp
M books/kestrel/risc-v/features.lisp
M books/kestrel/risc-v/instructions.lisp
M books/kestrel/risc-v/semantics.lisp
M books/kestrel/risc-v/states.lisp
M books/kestrel/risc-v/top.lisp
Log Message:
-----------
[RISC-V] Add support for RV32E and RV64E.
Commit: 7919b43ec081e7099c4938b16a92ce1bd61efa27
https://github.com/acl2/acl2/commit/7919b43ec081e7099c4938b16a92ce1bd61efa27
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/risc-v/decoding.lisp
M books/kestrel/risc-v/features.lisp
M books/kestrel/risc-v/instructions.lisp
M books/kestrel/risc-v/semantics.lisp
M books/kestrel/risc-v/states.lisp
M books/kestrel/risc-v/top.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/d533f382bc79...7919b43ec081
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 6b484cf05ec26e4b2b5ad2ef6f51438030d77777
https://github.com/acl2/acl2/commit/6b484cf05ec26e4b2b5ad2ef6f51438030d77777
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Extend `simpadd0` proof generation.
Add preliminary support for conditional expressions. A few more things need to
be added for full support.
Commit: 3e3435038ff52b1c28d3cf512cd2fabdd013f83d
https://github.com/acl2/acl2/commit/3e3435038ff52b1c28d3cf512cd2fabdd013f83d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
Log Message:
-----------
[C$] Extend type calculation from annotations.
Add some initial handling for conditional expressions.
Commit: 3246ef100ec9e65c8875d03c373618aeec51544d
https://github.com/acl2/acl2/commit/3246ef100ec9e65c8875d03c373618aeec51544d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/language/implementation-environments.lisp
Log Message:
-----------
[C] Add a theorem.
Commit: 83fb1980286a57409d2ad3ee3d30255cc9dc9ea6
https://github.com/acl2/acl2/commit/83fb1980286a57409d2ad3ee3d30255cc9dc9ea6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/language/implementation-environments.lisp
Log Message:
-----------
[C] Add a theorem about implementation environments.
Commit: 423350e04317f9fc7a4a0af612d6b0321970075a
https://github.com/acl2/acl2/commit/423350e04317f9fc7a4a0af612d6b0321970075a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/language/implementation-environments.lisp
Log Message:
-----------
[C] Explain two theorems.
Also lowercase a rule name.
Commit: 248d6c5c9968d52e93ca4c39cf4d4368317fffea
https://github.com/acl2/acl2/commit/248d6c5c9968d52e93ca4c39cf4d4368317fffea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/language/implementation-environments.lisp
Log Message:
-----------
[C] Add a theorem about implementation environments.
Commit: 5137233dd1e87765858c5b377c4fd9399b6fd913
https://github.com/acl2/acl2/commit/5137233dd1e87765858c5b377c4fd9399b6fd913
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/auto-termination/td-cands.acl2
M books/kestrel/auto-termination/td-cands.lisp
A books/projects/aleo/README.md
M books/projects/aleo/bft/README.md
A books/projects/aleo/bft/addresses.lisp
A books/projects/aleo/bft/anchors-extension.lisp
A books/projects/aleo/bft/anchors.lisp
R books/projects/aleo/bft/arxiv/acl2-customization.lsp
R books/projects/aleo/bft/arxiv/addresses.lisp
R books/projects/aleo/bft/arxiv/anchors-extension.lisp
R books/projects/aleo/bft/arxiv/anchors.lisp
R books/projects/aleo/bft/arxiv/backward-closure.lisp
R books/projects/aleo/bft/arxiv/blockchain-redundant-def-and-init-and-next.lisp
R books/projects/aleo/bft/arxiv/blockchain-redundant.lisp
R books/projects/aleo/bft/arxiv/blockchains.lisp
R books/projects/aleo/bft/arxiv/blocks.lisp
R books/projects/aleo/bft/arxiv/cert.acl2
R books/projects/aleo/bft/arxiv/certificates.lisp
R books/projects/aleo/bft/arxiv/committed-anchor-sequences.lisp
R books/projects/aleo/bft/arxiv/committed-redundant-def-and-init-and-next.lisp
R books/projects/aleo/bft/arxiv/committed-redundant.lisp
R books/projects/aleo/bft/arxiv/committees.lisp
R books/projects/aleo/bft/arxiv/correctness.lisp
R books/projects/aleo/bft/arxiv/dag-certificate-next.lisp
R books/projects/aleo/bft/arxiv/dag-omni-paths.lisp
R books/projects/aleo/bft/arxiv/dag-previous-quorum-def-and-init-and-next.lisp
R books/projects/aleo/bft/arxiv/dag-previous-quorum.lisp
R books/projects/aleo/bft/arxiv/dags.lisp
R books/projects/aleo/bft/arxiv/definition.lisp
R books/projects/aleo/bft/arxiv/elections.lisp
R books/projects/aleo/bft/arxiv/events.lisp
R books/projects/aleo/bft/arxiv/fault-tolerance.lisp
R books/projects/aleo/bft/arxiv/initialization.lisp
R books/projects/aleo/bft/arxiv/last-anchor-def-and-init.lisp
R books/projects/aleo/bft/arxiv/last-anchor-next.lisp
R books/projects/aleo/bft/arxiv/last-anchor-present.lisp
R books/projects/aleo/bft/arxiv/last-anchor-voters-def-and-init-and-next.lisp
R books/projects/aleo/bft/arxiv/last-anchor-voters.lisp
R books/projects/aleo/bft/arxiv/last-blockchain-round.lisp
R books/projects/aleo/bft/arxiv/messages.lisp
R books/projects/aleo/bft/arxiv/no-self-endorsed.lisp
R books/projects/aleo/bft/arxiv/nonforking-anchors-def-and-init-and-next.lisp
R books/projects/aleo/bft/arxiv/nonforking-anchors.lisp
R books/projects/aleo/bft/arxiv/nonforking-blockchains-def-and-init.lisp
R books/projects/aleo/bft/arxiv/nonforking-blockchains-next.lisp
R books/projects/aleo/bft/arxiv/nonforking-blockchains.lisp
R books/projects/aleo/bft/arxiv/omni-paths-def-and-implied.lisp
R books/projects/aleo/bft/arxiv/omni-paths.lisp
R books/projects/aleo/bft/arxiv/ordered-even-blocks.lisp
R books/projects/aleo/bft/arxiv/package.lsp
R books/projects/aleo/bft/arxiv/portcullis.acl2
R books/projects/aleo/bft/arxiv/portcullis.lisp
R books/projects/aleo/bft/arxiv/quorum-intersection.lisp
R books/projects/aleo/bft/arxiv/reachability.lisp
R books/projects/aleo/bft/arxiv/same-committees-def-and-implied.lisp
R books/projects/aleo/bft/arxiv/same-committees.lisp
R books/projects/aleo/bft/arxiv/signed-certificates.lisp
R books/projects/aleo/bft/arxiv/signed-previous-quorum.lisp
R books/projects/aleo/bft/arxiv/signer-quorum.lisp
R books/projects/aleo/bft/arxiv/signer-records.lisp
R books/projects/aleo/bft/arxiv/simultaneous-induction.lisp
R books/projects/aleo/bft/arxiv/states.lisp
R books/projects/aleo/bft/arxiv/successor-predecessor-intersection.lisp
R books/projects/aleo/bft/arxiv/system-certificates.lisp
R books/projects/aleo/bft/arxiv/system-states.lisp
R books/projects/aleo/bft/arxiv/top.lisp
R books/projects/aleo/bft/arxiv/transactions.lisp
R books/projects/aleo/bft/arxiv/transitions-accept.lisp
R books/projects/aleo/bft/arxiv/transitions-advance.lisp
R books/projects/aleo/bft/arxiv/transitions-commit.lisp
R books/projects/aleo/bft/arxiv/transitions-create.lisp
R books/projects/aleo/bft/arxiv/transitions.lisp
R books/projects/aleo/bft/arxiv/unequivocal-dags-def-and-init.lisp
R books/projects/aleo/bft/arxiv/unequivocal-dags-next.lisp
R books/projects/aleo/bft/arxiv/unequivocal-dags.lisp
R books/projects/aleo/bft/arxiv/unequivocal-signed-certificates.lisp
R books/projects/aleo/bft/arxiv/validator-states.lisp
A books/projects/aleo/bft/backward-closure.lisp
A books/projects/aleo/bft/blockchain-redundant-def-and-init-and-next.lisp
A books/projects/aleo/bft/blockchain-redundant.lisp
A books/projects/aleo/bft/blockchains.lisp
A books/projects/aleo/bft/blocks.lisp
A books/projects/aleo/bft/certificates.lisp
A books/projects/aleo/bft/committed-anchor-sequences.lisp
A books/projects/aleo/bft/committed-redundant-def-and-init-and-next.lisp
A books/projects/aleo/bft/committed-redundant.lisp
A books/projects/aleo/bft/committees.lisp
A books/projects/aleo/bft/correctness.lisp
A books/projects/aleo/bft/dag-certificate-next.lisp
A books/projects/aleo/bft/dag-omni-paths.lisp
A books/projects/aleo/bft/dag-previous-quorum-def-and-init-and-next.lisp
A books/projects/aleo/bft/dag-previous-quorum.lisp
A books/projects/aleo/bft/dags.lisp
A books/projects/aleo/bft/definition.lisp
R books/projects/aleo/bft/dynamic/accepted-certificate-committee.lisp
R books/projects/aleo/bft/dynamic/acl2-customization.lsp
R books/projects/aleo/bft/dynamic/addresses.lisp
R books/projects/aleo/bft/dynamic/anchors-extension.lisp
R books/projects/aleo/bft/dynamic/anchors.lisp
R books/projects/aleo/bft/dynamic/backward-closure.lisp
R books/projects/aleo/bft/dynamic/blockchain-redundant-def-and-init-and-next.lisp
R books/projects/aleo/bft/dynamic/blockchain-redundant.lisp
R books/projects/aleo/bft/dynamic/blockchains.lisp
R books/projects/aleo/bft/dynamic/blocks.lisp
R books/projects/aleo/bft/dynamic/cert.acl2
R books/projects/aleo/bft/dynamic/certificates-of-validators.lisp
R books/projects/aleo/bft/dynamic/certificates.lisp
R books/projects/aleo/bft/dynamic/committed-anchor-sequences.lisp
R books/projects/aleo/bft/dynamic/committed-redundant-def-and-init-and-next.lisp
R books/projects/aleo/bft/dynamic/committed-redundant.lisp
R books/projects/aleo/bft/dynamic/committees-in-system.lisp
R books/projects/aleo/bft/dynamic/committees.lisp
R books/projects/aleo/bft/dynamic/correctness.lisp
R books/projects/aleo/bft/dynamic/dag-certificate-next.lisp
R books/projects/aleo/bft/dynamic/dag-omni-paths.lisp
R books/projects/aleo/bft/dynamic/dags.lisp
R books/projects/aleo/bft/dynamic/definition.lisp
R books/projects/aleo/bft/dynamic/elections.lisp
R books/projects/aleo/bft/dynamic/events.lisp
R books/projects/aleo/bft/dynamic/fault-tolerance.lisp
R books/projects/aleo/bft/dynamic/initialization.lisp
R books/projects/aleo/bft/dynamic/last-anchor-def-and-init.lisp
R books/projects/aleo/bft/dynamic/last-anchor-next.lisp
R books/projects/aleo/bft/dynamic/last-anchor-present.lisp
R books/projects/aleo/bft/dynamic/last-anchor-voters-def-and-init-and-next.lisp
R books/projects/aleo/bft/dynamic/last-anchor-voters.lisp
R books/projects/aleo/bft/dynamic/last-blockchain-round.lisp
R books/projects/aleo/bft/dynamic/messages.lisp
R books/projects/aleo/bft/dynamic/no-self-buffer.lisp
R books/projects/aleo/bft/dynamic/no-self-endorsed.lisp
R books/projects/aleo/bft/dynamic/no-self-messages.lisp
R books/projects/aleo/bft/dynamic/nonforking-anchors-def-and-init-and-next.lisp
R books/projects/aleo/bft/dynamic/nonforking-anchors.lisp
R books/projects/aleo/bft/dynamic/nonforking-blockchains-def-and-init.lisp
R books/projects/aleo/bft/dynamic/nonforking-blockchains-next.lisp
R books/projects/aleo/bft/dynamic/nonforking-blockchains.lisp
R books/projects/aleo/bft/dynamic/omni-paths-def-and-implied.lisp
R books/projects/aleo/bft/dynamic/omni-paths.lisp
R books/projects/aleo/bft/dynamic/ordered-even-blocks.lisp
R books/projects/aleo/bft/dynamic/package.lsp
R books/projects/aleo/bft/dynamic/portcullis.acl2
R books/projects/aleo/bft/dynamic/portcullis.lisp
R books/projects/aleo/bft/dynamic/previous-quorum.lisp
R books/projects/aleo/bft/dynamic/quorum-intersection.lisp
R books/projects/aleo/bft/dynamic/rounds-in-committees.lisp
R books/projects/aleo/bft/dynamic/same-committees-def-and-implied.lisp
R books/projects/aleo/bft/dynamic/same-committees.lisp
R books/projects/aleo/bft/dynamic/same-owned-certificates.lisp
R books/projects/aleo/bft/dynamic/signer-quorum.lisp
R books/projects/aleo/bft/dynamic/signer-records.lisp
R books/projects/aleo/bft/dynamic/simultaneous-induction.lisp
R books/projects/aleo/bft/dynamic/states.lisp
R books/projects/aleo/bft/dynamic/successor-predecessor-intersection.lisp
R books/projects/aleo/bft/dynamic/system-states.lisp
R books/projects/aleo/bft/dynamic/top.lisp
R books/projects/aleo/bft/dynamic/transactions.lisp
R books/projects/aleo/bft/dynamic/transitions-advance-round.lisp
R books/projects/aleo/bft/dynamic/transitions-commit-anchors.lisp
R books/projects/aleo/bft/dynamic/transitions-create-certificate.lisp
R books/projects/aleo/bft/dynamic/transitions-receive-certificate.lisp
R books/projects/aleo/bft/dynamic/transitions-store-certificate.lisp
R books/projects/aleo/bft/dynamic/transitions-timer-expires.lisp
R books/projects/aleo/bft/dynamic/transitions.lisp
R books/projects/aleo/bft/dynamic/unequivocal-accepted-certificates-def-and-init.lisp
R books/projects/aleo/bft/dynamic/unequivocal-accepted-certificates-next.lisp
R books/projects/aleo/bft/dynamic/unequivocal-accepted-certificates.lisp
R books/projects/aleo/bft/dynamic/unequivocal-signed-certificates.lisp
R books/projects/aleo/bft/dynamic/validator-states.lisp
A books/projects/aleo/bft/elections.lisp
A books/projects/aleo/bft/events.lisp
A books/projects/aleo/bft/fault-tolerance.lisp
A books/projects/aleo/bft/initialization.lisp
A books/projects/aleo/bft/last-anchor-def-and-init.lisp
A books/projects/aleo/bft/last-anchor-next.lisp
A books/projects/aleo/bft/last-anchor-present.lisp
A books/projects/aleo/bft/last-anchor-voters-def-and-init-and-next.lisp
A books/projects/aleo/bft/last-anchor-voters.lisp
A books/projects/aleo/bft/last-blockchain-round.lisp
M books/projects/aleo/bft/library-extensions/oset-theorems.lisp
A books/projects/aleo/bft/messages.lisp
A books/projects/aleo/bft/next/acl2-customization.lsp
A books/projects/aleo/bft/next/active-committees-after-commit.lisp
A books/projects/aleo/bft/next/addresses.lisp
A books/projects/aleo/bft/next/anchors.lisp
A books/projects/aleo/bft/next/author-round-pairs-in-validators.lisp
A books/projects/aleo/bft/next/blockchains.lisp
A books/projects/aleo/bft/next/blocks.lisp
A books/projects/aleo/bft/next/cert.acl2
A books/projects/aleo/bft/next/certificate-in-author.lisp
A books/projects/aleo/bft/next/certificate-to-other.lisp
A books/projects/aleo/bft/next/certificates.lisp
A books/projects/aleo/bft/next/committees.lisp
A books/projects/aleo/bft/next/correctness.lisp
A books/projects/aleo/bft/next/dag-previous-closed.lisp
A books/projects/aleo/bft/next/dags.lisp
A books/projects/aleo/bft/next/definition.lisp
A books/projects/aleo/bft/next/elections.lisp
A books/projects/aleo/bft/next/endorsed-author-other.lisp
A books/projects/aleo/bft/next/endorsed-in-author.lisp
A books/projects/aleo/bft/next/endorsed-previous-closed.lisp
A books/projects/aleo/bft/next/endorsed-round1-no-previous.lisp
A books/projects/aleo/bft/next/endorsement-from-other.lisp
A books/projects/aleo/bft/next/endorsement-in-author.lisp
A books/projects/aleo/bft/next/endorsement-in-endorser.lisp
A books/projects/aleo/bft/next/events.lisp
A books/projects/aleo/bft/next/fault-tolerance.lisp
A books/projects/aleo/bft/next/initialization.lisp
A books/projects/aleo/bft/next/last-anchor-def.lisp
A books/projects/aleo/bft/next/last-anchor-init-and-next.lisp
A books/projects/aleo/bft/next/last-anchor-present.lisp
A books/projects/aleo/bft/next/last-anchor-voters.lisp
A books/projects/aleo/bft/next/last-blockchain-round.lisp
A books/projects/aleo/bft/next/messages.lisp
A books/projects/aleo/bft/next/nonforking-blockchains-def-and-init.lisp
A books/projects/aleo/bft/next/ordered-blockchain.lisp
A books/projects/aleo/bft/next/portcullis.acl2
A books/projects/aleo/bft/next/portcullis.lisp
A books/projects/aleo/bft/next/proposal-in-author.lisp
A books/projects/aleo/bft/next/proposal-to-other.lisp
A books/projects/aleo/bft/next/proposals.lisp
A books/projects/aleo/bft/next/proposed-author-in-committee.lisp
A books/projects/aleo/bft/next/proposed-author-self.lisp
A books/projects/aleo/bft/next/proposed-disjoint-dag.lisp
A books/projects/aleo/bft/next/proposed-endorser-in-committee.lisp
A books/projects/aleo/bft/next/proposed-endorser-other.lisp
A books/projects/aleo/bft/next/proposed-previous-closed.lisp
A books/projects/aleo/bft/next/proposed-round1-no-previous.lisp
A books/projects/aleo/bft/next/quorum-intersection.lisp
A books/projects/aleo/bft/next/reachability.lisp
A books/projects/aleo/bft/next/round-after-last.lisp
A books/projects/aleo/bft/next/same-committees-def-and-implied.lisp
A books/projects/aleo/bft/next/signed-in-signer.lisp
A books/projects/aleo/bft/next/signed-proposals.lisp
A books/projects/aleo/bft/next/signer-quorum.lisp
A books/projects/aleo/bft/next/states.lisp
A books/projects/aleo/bft/next/system-states.lisp
A books/projects/aleo/bft/next/top.lisp
A books/projects/aleo/bft/next/transactions.lisp
A books/projects/aleo/bft/next/transitions-accept.lisp
A books/projects/aleo/bft/next/transitions-advance.lisp
A books/projects/aleo/bft/next/transitions-augment.lisp
A books/projects/aleo/bft/next/transitions-certify.lisp
A books/projects/aleo/bft/next/transitions-commit.lisp
A books/projects/aleo/bft/next/transitions-endorse.lisp
A books/projects/aleo/bft/next/transitions-propose.lisp
A books/projects/aleo/bft/next/transitions.lisp
A books/projects/aleo/bft/next/unequivocal-dag.lisp
A books/projects/aleo/bft/next/unequivocal-proposed.lisp
A books/projects/aleo/bft/next/unequivocal-signed-proposals.lisp
A books/projects/aleo/bft/next/validator-states.lisp
A books/projects/aleo/bft/no-self-endorsed.lisp
A books/projects/aleo/bft/nonforking-anchors-def-and-init-and-next.lisp
A books/projects/aleo/bft/nonforking-anchors.lisp
A books/projects/aleo/bft/nonforking-blockchains-def-and-init.lisp
A books/projects/aleo/bft/nonforking-blockchains-next.lisp
A books/projects/aleo/bft/nonforking-blockchains.lisp
A books/projects/aleo/bft/omni-paths-def-and-implied.lisp
A books/projects/aleo/bft/omni-paths.lisp
A books/projects/aleo/bft/ordered-even-blocks.lisp
M books/projects/aleo/bft/package.lsp
R books/projects/aleo/bft/proposals/acl2-customization.lsp
R books/projects/aleo/bft/proposals/active-committees-after-commit.lisp
R books/projects/aleo/bft/proposals/addresses.lisp
R books/projects/aleo/bft/proposals/anchors.lisp
R books/projects/aleo/bft/proposals/author-round-pairs-in-validators.lisp
R books/projects/aleo/bft/proposals/blockchains.lisp
R books/projects/aleo/bft/proposals/blocks.lisp
R books/projects/aleo/bft/proposals/cert.acl2
R books/projects/aleo/bft/proposals/certificate-in-author.lisp
R books/projects/aleo/bft/proposals/certificate-to-other.lisp
R books/projects/aleo/bft/proposals/certificates.lisp
R books/projects/aleo/bft/proposals/committees.lisp
R books/projects/aleo/bft/proposals/correctness.lisp
R books/projects/aleo/bft/proposals/dag-previous-closed.lisp
R books/projects/aleo/bft/proposals/dags.lisp
R books/projects/aleo/bft/proposals/definition.lisp
R books/projects/aleo/bft/proposals/elections.lisp
R books/projects/aleo/bft/proposals/endorsed-author-other.lisp
R books/projects/aleo/bft/proposals/endorsed-in-author.lisp
R books/projects/aleo/bft/proposals/endorsed-previous-closed.lisp
R books/projects/aleo/bft/proposals/endorsed-round1-no-previous.lisp
R books/projects/aleo/bft/proposals/endorsement-from-other.lisp
R books/projects/aleo/bft/proposals/endorsement-in-author.lisp
R books/projects/aleo/bft/proposals/endorsement-in-endorser.lisp
R books/projects/aleo/bft/proposals/events.lisp
R books/projects/aleo/bft/proposals/fault-tolerance.lisp
R books/projects/aleo/bft/proposals/initialization.lisp
R books/projects/aleo/bft/proposals/last-anchor-def.lisp
R books/projects/aleo/bft/proposals/last-anchor-init-and-next.lisp
R books/projects/aleo/bft/proposals/last-anchor-present.lisp
R books/projects/aleo/bft/proposals/last-anchor-voters.lisp
R books/projects/aleo/bft/proposals/last-blockchain-round.lisp
R books/projects/aleo/bft/proposals/messages.lisp
R books/projects/aleo/bft/proposals/nonforking-blockchains-def-and-init.lisp
R books/projects/aleo/bft/proposals/ordered-blockchain.lisp
R books/projects/aleo/bft/proposals/package.lsp
R books/projects/aleo/bft/proposals/portcullis.acl2
R books/projects/aleo/bft/proposals/portcullis.lisp
R books/projects/aleo/bft/proposals/proposal-in-author.lisp
R books/projects/aleo/bft/proposals/proposal-to-other.lisp
R books/projects/aleo/bft/proposals/proposals.lisp
R books/projects/aleo/bft/proposals/proposed-author-in-committee.lisp
R books/projects/aleo/bft/proposals/proposed-author-self.lisp
R books/projects/aleo/bft/proposals/proposed-disjoint-dag.lisp
R books/projects/aleo/bft/proposals/proposed-endorser-in-committee.lisp
R books/projects/aleo/bft/proposals/proposed-endorser-other.lisp
R books/projects/aleo/bft/proposals/proposed-previous-closed.lisp
R books/projects/aleo/bft/proposals/proposed-round1-no-previous.lisp
R books/projects/aleo/bft/proposals/quorum-intersection.lisp
R books/projects/aleo/bft/proposals/reachability.lisp
R books/projects/aleo/bft/proposals/round-after-last.lisp
R books/projects/aleo/bft/proposals/same-committees-def-and-implied.lisp
R books/projects/aleo/bft/proposals/signed-in-signer.lisp
R books/projects/aleo/bft/proposals/signed-proposals.lisp
R books/projects/aleo/bft/proposals/signer-quorum.lisp
R books/projects/aleo/bft/proposals/states.lisp
R books/projects/aleo/bft/proposals/system-states.lisp
R books/projects/aleo/bft/proposals/top.lisp
R books/projects/aleo/bft/proposals/transactions.lisp
R books/projects/aleo/bft/proposals/transitions-accept.lisp
R books/projects/aleo/bft/proposals/transitions-advance.lisp
R books/projects/aleo/bft/proposals/transitions-augment.lisp
R books/projects/aleo/bft/proposals/transitions-certify.lisp
R books/projects/aleo/bft/proposals/transitions-commit.lisp
R books/projects/aleo/bft/proposals/transitions-endorse.lisp
R books/projects/aleo/bft/proposals/transitions-propose.lisp
R books/projects/aleo/bft/proposals/transitions.lisp
R books/projects/aleo/bft/proposals/unequivocal-dag.lisp
R books/projects/aleo/bft/proposals/unequivocal-proposed.lisp
R books/projects/aleo/bft/proposals/unequivocal-signed-proposals.lisp
R books/projects/aleo/bft/proposals/validator-states.lisp
A books/projects/aleo/bft/quorum-intersection.lisp
A books/projects/aleo/bft/reachability.lisp
A books/projects/aleo/bft/same-committees-def-and-implied.lisp
A books/projects/aleo/bft/same-committees.lisp
A books/projects/aleo/bft/signed-certificates.lisp
A books/projects/aleo/bft/signed-previous-quorum.lisp
A books/projects/aleo/bft/signer-quorum.lisp
A books/projects/aleo/bft/signer-records.lisp
A books/projects/aleo/bft/simultaneous-induction.lisp
R books/projects/aleo/bft/stake/acl2-customization.lsp
R books/projects/aleo/bft/stake/addresses.lisp
R books/projects/aleo/bft/stake/anchors-extension.lisp
R books/projects/aleo/bft/stake/anchors.lisp
R books/projects/aleo/bft/stake/associated-certificates.lisp
R books/projects/aleo/bft/stake/backward-closure.lisp
R books/projects/aleo/bft/stake/blockchain-redundant-def-and-init-and-next.lisp
R books/projects/aleo/bft/stake/blockchain-redundant.lisp
R books/projects/aleo/bft/stake/blockchains.lisp
R books/projects/aleo/bft/stake/blocks.lisp
R books/projects/aleo/bft/stake/cert.acl2
R books/projects/aleo/bft/stake/certificates.lisp
R books/projects/aleo/bft/stake/committed-anchor-sequences.lisp
R books/projects/aleo/bft/stake/committed-redundant-def-and-init-and-next.lisp
R books/projects/aleo/bft/stake/committed-redundant.lisp
R books/projects/aleo/bft/stake/committees.lisp
R books/projects/aleo/bft/stake/correctness.lisp
R books/projects/aleo/bft/stake/dag-certificate-next.lisp
R books/projects/aleo/bft/stake/dag-committees.lisp
R books/projects/aleo/bft/stake/dag-omni-paths.lisp
R books/projects/aleo/bft/stake/dags.lisp
R books/projects/aleo/bft/stake/definition.lisp
R books/projects/aleo/bft/stake/elections.lisp
R books/projects/aleo/bft/stake/events.lisp
R books/projects/aleo/bft/stake/fault-tolerance.lisp
R books/projects/aleo/bft/stake/initialization.lisp
R books/projects/aleo/bft/stake/last-anchor-def-and-init.lisp
R books/projects/aleo/bft/stake/last-anchor-next.lisp
R books/projects/aleo/bft/stake/last-anchor-present.lisp
R books/projects/aleo/bft/stake/last-anchor-voters-def-and-init-and-next.lisp
R books/projects/aleo/bft/stake/last-anchor-voters.lisp
R books/projects/aleo/bft/stake/last-blockchain-round.lisp
R books/projects/aleo/bft/stake/messages.lisp
R books/projects/aleo/bft/stake/no-self-buffer.lisp
R books/projects/aleo/bft/stake/no-self-endorsed.lisp
R books/projects/aleo/bft/stake/no-self-messages.lisp
R books/projects/aleo/bft/stake/nonforking-anchors-def-and-init-and-next.lisp
R books/projects/aleo/bft/stake/nonforking-anchors.lisp
R books/projects/aleo/bft/stake/nonforking-blockchains-def-and-init.lisp
R books/projects/aleo/bft/stake/nonforking-blockchains-next.lisp
R books/projects/aleo/bft/stake/nonforking-blockchains.lisp
R books/projects/aleo/bft/stake/omni-paths-def-and-implied.lisp
R books/projects/aleo/bft/stake/omni-paths.lisp
R books/projects/aleo/bft/stake/ordered-even-blocks.lisp
R books/projects/aleo/bft/stake/package.lsp
R books/projects/aleo/bft/stake/portcullis.acl2
R books/projects/aleo/bft/stake/portcullis.lisp
R books/projects/aleo/bft/stake/previous-quorum-def-and-init-and-next.lisp
R books/projects/aleo/bft/stake/previous-quorum.lisp
R books/projects/aleo/bft/stake/quorum-intersection.lisp
R books/projects/aleo/bft/stake/same-associated-certificates.lisp
R books/projects/aleo/bft/stake/same-committees-def-and-implied.lisp
R books/projects/aleo/bft/stake/same-committees.lisp
R books/projects/aleo/bft/stake/signed-and-associated-cerificates.lisp
R books/projects/aleo/bft/stake/signed-certificates.lisp
R books/projects/aleo/bft/stake/signed-previous-quorum.lisp
R books/projects/aleo/bft/stake/signer-quorum.lisp
R books/projects/aleo/bft/stake/signer-records.lisp
R books/projects/aleo/bft/stake/simultaneous-induction.lisp
R books/projects/aleo/bft/stake/states.lisp
R books/projects/aleo/bft/stake/successor-predecessor-intersection.lisp
R books/projects/aleo/bft/stake/system-states.lisp
R books/projects/aleo/bft/stake/top.lisp
R books/projects/aleo/bft/stake/transactions.lisp
R books/projects/aleo/bft/stake/transitions-advance.lisp
R books/projects/aleo/bft/stake/transitions-commit.lisp
R books/projects/aleo/bft/stake/transitions-create.lisp
R books/projects/aleo/bft/stake/transitions-receive.lisp
R books/projects/aleo/bft/stake/transitions-store.lisp
R books/projects/aleo/bft/stake/transitions-timeout.lisp
R books/projects/aleo/bft/stake/transitions.lisp
R books/projects/aleo/bft/stake/unequivocal-dags-def-and-init.lisp
R books/projects/aleo/bft/stake/unequivocal-dags-next.lisp
R books/projects/aleo/bft/stake/unequivocal-dags.lisp
R books/projects/aleo/bft/stake/unequivocal-signed-certificates.lisp
R books/projects/aleo/bft/stake/validator-states.lisp
A books/projects/aleo/bft/states.lisp
R books/projects/aleo/bft/static/acl2-customization.lsp
R books/projects/aleo/bft/static/addresses.lisp
R books/projects/aleo/bft/static/blocks.lisp
R books/projects/aleo/bft/static/cert.acl2
R books/projects/aleo/bft/static/certificates.lisp
R books/projects/aleo/bft/static/correctness.lisp
R books/projects/aleo/bft/static/definition.lisp
R books/projects/aleo/bft/static/events.lisp
R books/projects/aleo/bft/static/initialization.lisp
R books/projects/aleo/bft/static/invariant-addresses.lisp
R books/projects/aleo/bft/static/invariant-anchors-not-forking.lisp
R books/projects/aleo/bft/static/invariant-blockchain-not-forking.lisp
R books/projects/aleo/bft/static/invariant-blockchain-redundant.lisp
R books/projects/aleo/bft/static/invariant-causal-histories.lisp
R books/projects/aleo/bft/static/invariant-certificate-retrieval.lisp
R books/projects/aleo/bft/static/invariant-committed-redundant.lisp
R books/projects/aleo/bft/static/invariant-dag-authors-are-validators.lisp
R books/projects/aleo/bft/static/invariant-dag-previous-are-quorum.lisp
R books/projects/aleo/bft/static/invariant-fault-tolerance.lisp
R books/projects/aleo/bft/static/invariant-last-anchor-present.lisp
R books/projects/aleo/bft/static/invariant-last-anchor-voters.lisp
R books/projects/aleo/bft/static/invariant-last-before-current.lisp
R books/projects/aleo/bft/static/invariant-last-is-even.lisp
R books/projects/aleo/bft/static/invariant-max-faulty.lisp
R books/projects/aleo/bft/static/invariant-messages-to-correct.lisp
R books/projects/aleo/bft/static/invariant-no-self-buffer.lisp
R books/projects/aleo/bft/static/invariant-no-self-endorsed.lisp
R books/projects/aleo/bft/static/invariant-no-self-messages.lisp
R books/projects/aleo/bft/static/invariant-paths-to-last-anchor.lisp
R books/projects/aleo/bft/static/invariant-paths-to-other-last-anchor.lisp
R books/projects/aleo/bft/static/invariant-previous-are-quorum.lisp
R books/projects/aleo/bft/static/invariant-previous-in-dag.lisp
R books/projects/aleo/bft/static/invariant-quorum.lisp
R books/projects/aleo/bft/static/invariant-same-certificates.lisp
R books/projects/aleo/bft/static/invariant-signers-are-quorum.lisp
R books/projects/aleo/bft/static/invariant-signers-are-validators.lisp
R books/projects/aleo/bft/static/invariant-signers-have-author-round.lisp
R books/projects/aleo/bft/static/invariant-unequivocal-certificates.lisp
R books/projects/aleo/bft/static/invariant-unequivocal-dag.lisp
R books/projects/aleo/bft/static/invariant-unequivocal-dags.lisp
R books/projects/aleo/bft/static/messages.lisp
R books/projects/aleo/bft/static/operations-additional.lisp
R books/projects/aleo/bft/static/operations-anchors.lisp
R books/projects/aleo/bft/static/operations-author-round-pairs.lisp
R books/projects/aleo/bft/static/operations-blockchain-additional.lisp
R books/projects/aleo/bft/static/operations-blockchain.lisp
R books/projects/aleo/bft/static/operations-certificates-for-validators.lisp
R books/projects/aleo/bft/static/operations-dags-additional.lisp
R books/projects/aleo/bft/static/operations-dags.lisp
R books/projects/aleo/bft/static/operations-fault-tolerance.lisp
R books/projects/aleo/bft/static/operations-faults-and-quora.lisp
R books/projects/aleo/bft/static/operations-leaders.lisp
R books/projects/aleo/bft/static/operations-message-creation.lisp
R books/projects/aleo/bft/static/operations-previous-certificates.lisp
R books/projects/aleo/bft/static/operations-unequivocal-certificates.lisp
R books/projects/aleo/bft/static/operations-voting.lisp
R books/projects/aleo/bft/static/operations.lisp
R books/projects/aleo/bft/static/package.lsp
R books/projects/aleo/bft/static/portcullis.acl2
R books/projects/aleo/bft/static/portcullis.lisp
R books/projects/aleo/bft/static/properties-anchors-extension.lisp
R books/projects/aleo/bft/static/properties-anchors.lisp
R books/projects/aleo/bft/static/properties-blockchain.lisp
R books/projects/aleo/bft/static/properties-certificate-retrieval.lisp
R books/projects/aleo/bft/static/properties-dags.lisp
R books/projects/aleo/bft/static/property-committed-anchors-of-next-event.lisp
R books/projects/aleo/bft/static/property-last-anchor-of-next-event.lisp
R books/projects/aleo/bft/static/property-paths-to-other-voted-anchor.lisp
R books/projects/aleo/bft/static/property-paths-to-voted-anchor.lisp
R books/projects/aleo/bft/static/states.lisp
R books/projects/aleo/bft/static/system-states.lisp
R books/projects/aleo/bft/static/top.lisp
R books/projects/aleo/bft/static/transactions.lisp
R books/projects/aleo/bft/static/transitions-advance-round.lisp
R books/projects/aleo/bft/static/transitions-commit-anchors.lisp
R books/projects/aleo/bft/static/transitions-create-certificate.lisp
R books/projects/aleo/bft/static/transitions-receive-certificate.lisp
R books/projects/aleo/bft/static/transitions-store-certificate.lisp
R books/projects/aleo/bft/static/transitions-timer-expires.lisp
R books/projects/aleo/bft/static/transitions.lisp
R books/projects/aleo/bft/static/validator-states.lisp
A books/projects/aleo/bft/successor-predecessor-intersection.lisp
A books/projects/aleo/bft/system-certificates.lisp
A books/projects/aleo/bft/system-states.lisp
M books/projects/aleo/bft/top.lisp
A books/projects/aleo/bft/transactions.lisp
A books/projects/aleo/bft/transitions-accept.lisp
A books/projects/aleo/bft/transitions-advance.lisp
A books/projects/aleo/bft/transitions-commit.lisp
A books/projects/aleo/bft/transitions-create.lisp
A books/projects/aleo/bft/transitions.lisp
A books/projects/aleo/bft/unequivocal-dags-def-and-init.lisp
A books/projects/aleo/bft/unequivocal-dags-next.lisp
A books/projects/aleo/bft/unequivocal-dags.lisp
A books/projects/aleo/bft/unequivocal-signed-certificates.lisp
A books/projects/aleo/bft/validator-states.lisp
R books/projects/aleo/leo/.sys/gra...@useless-runes.lsp
R books/projects/aleo/leo/.sys/portc...@useless-runes.lsp
R books/projects/aleo/leo/.sys/t...@useless-runes.lsp
A books/projects/aleo/leo/README.md
M books/projects/aleo/leo/cert.acl2
M books/projects/aleo/leo/grammar.lisp
M books/projects/aleo/leo/portcullis.lisp
Log Message:
-----------
Merge.
Commit: 893fe3694a4b260ee93d946e40dbaddf7440e07e
https://github.com/acl2/acl2/commit/893fe3694a4b260ee93d946e40dbaddf7440e07e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Extend `simpadd0` proof generation.
Refine the generated hints for conditional expressions, which are now thus
supported.
Commit: 3ad012b79a571b43a14c477a00aeaf3dd8234877
https://github.com/acl2/acl2/commit/3ad012b79a571b43a14c477a00aeaf3dd8234877
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
Merge.
Commit: 968a72cc5a0bcc33628c5384aece0ac23d376e42
https://github.com/acl2/acl2/commit/968a72cc5a0bcc33628c5384aece0ac23d376e42
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/risc-v/decoding.lisp
M books/kestrel/risc-v/features.lisp
M books/kestrel/risc-v/instructions.lisp
M books/kestrel/risc-v/semantics.lisp
M books/kestrel/risc-v/states.lisp
M books/kestrel/risc-v/top.lisp
Log Message:
-----------
[RISC-V] Add support for RV32E and RV64E.
Commit: 7919b43ec081e7099c4938b16a92ce1bd61efa27
https://github.com/acl2/acl2/commit/7919b43ec081e7099c4938b16a92ce1bd61efa27
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-05-31 (Sat, 31 May 2025)
Changed paths:
M books/kestrel/risc-v/decoding.lisp
M books/kestrel/risc-v/features.lisp
M books/kestrel/risc-v/instructions.lisp
M books/kestrel/risc-v/semantics.lisp
M books/kestrel/risc-v/states.lisp
M books/kestrel/risc-v/top.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/d533f382bc79...7919b43ec081
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
Jun 1, 2025, 1:43:32 AM6/1/25
to acl2-...@googlegroups.com
Branch: refs/heads/master
Alessandro Coglio
Jun 1, 2025, 2:23:27 AM6/1/25
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Alessandro Coglio
Jun 1, 2025, 10:27:08 AM6/1/25
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Reply all
Reply to author
Forward
0 new messages