CHANGELOG

# Changelog

All notable changes to this project (since version 1.0.0) will be documented in this file.

The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/),
and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).

## [Unreleased]

### Added

- Added the `LICENSE` file

### Changed

Protocol-level changes:
- Lowered `th_vote4vote` to be `f + 1` in `Protocols/RB/Protocol.v`
- Allowed the node to send light certificates only when it confirms for the first time in `Protocols/ABC/Protocol.v`

Proof-level changes:
- Improved the statement of `first_vote_due_to_echo` in `Protocols/RB/Invariant.v`
- Optimized the proofs of `first_vote_due_to_echo_is_invariant` and `vote_uniqueness_is_invariant` in `Protocols/RB/Invariant.v`

Other changes:
- Renamed `InternalTransition` into `InternalEvent`
- Incorporated a comment from the Artefact Evaluation Committee
- Simplified the definition of `lightsig_seen_in_history` in `Protocols/PB/Safety.v`
- Added more comments on the formalization of `uniqueness` in `Protocols/PB/Safety.v`
- Changed `lightcert_conflict_check` to a more efficient one in `Protocols/ABC/Types.v`

## [1.0.0] - 2024-07-20