From 9b95ab320ac0eccbb6e711fd5a5a0b4ad5223bde Mon Sep 17 00:00:00 2001 From: Pranav Gaddamadugu <23022326+d0cd@users.noreply.github.com> Date: Mon, 18 Mar 2024 17:50:39 -0700 Subject: [PATCH] Update examples --- auction/leo.lock | 1 + basic_bank/build/main.aleo | 6 +- basic_bank/leo.lock | 1 + battleship/board/.gitignore | 5 ++ battleship/board/README.md | 13 +++ battleship/board/build/main.aleo | 46 ++++++++++ battleship/board/build/program.json | 6 ++ battleship/board/inputs/board.in | 4 + battleship/board/leo.lock | 1 + battleship/board/program.json | 6 ++ battleship/board/src/main.leo | 110 +++++++++++++++++++++++ battleship/build/imports/board.aleo | 2 +- battleship/build/imports/move.aleo | 2 +- battleship/build/program.json | 19 +++- battleship/leo.lock | 20 +++++ battleship/move/.gitignore | 5 ++ battleship/move/README.md | 13 +++ battleship/move/build/main.aleo | 24 +++++ battleship/move/build/program.json | 6 ++ battleship/move/inputs/move.in | 4 + battleship/move/leo.lock | 1 + battleship/move/program.json | 6 ++ battleship/move/src/main.leo | 46 ++++++++++ battleship/program.json | 19 +++- battleship/src/main.leo | 54 ++++++------ battleship/verify/.gitignore | 5 ++ battleship/verify/README.md | 13 +++ battleship/verify/build/main.aleo | 73 ++++++++++++++++ battleship/verify/build/program.json | 6 ++ battleship/verify/inputs/verify.in | 4 + battleship/verify/leo.lock | 1 + battleship/verify/program.json | 6 ++ battleship/verify/src/main.leo | 125 +++++++++++++++++++++++++++ check.sh => check-run.sh | 1 + tictactoe/leo.lock | 1 + token/build/main.aleo | 12 ++- token/leo.lock | 1 + vote/README.md | 4 +- vote/build/main.aleo | 12 ++- vote/leo.lock | 1 + vote/src/main.leo | 2 +- 41 files changed, 642 insertions(+), 45 deletions(-) create mode 100644 auction/leo.lock create mode 100644 basic_bank/leo.lock create mode 100644 battleship/board/.gitignore create mode 100644 battleship/board/README.md create mode 100644 battleship/board/build/main.aleo create mode 100644 battleship/board/build/program.json create mode 100644 battleship/board/inputs/board.in create mode 100644 battleship/board/leo.lock create mode 100644 battleship/board/program.json create mode 100644 battleship/board/src/main.leo create mode 100644 battleship/leo.lock create mode 100644 battleship/move/.gitignore create mode 100644 battleship/move/README.md create mode 100644 battleship/move/build/main.aleo create mode 100644 battleship/move/build/program.json create mode 100644 battleship/move/inputs/move.in create mode 100644 battleship/move/leo.lock create mode 100644 battleship/move/program.json create mode 100644 battleship/move/src/main.leo create mode 100644 battleship/verify/.gitignore create mode 100644 battleship/verify/README.md create mode 100644 battleship/verify/build/main.aleo create mode 100644 battleship/verify/build/program.json create mode 100644 battleship/verify/inputs/verify.in create mode 100644 battleship/verify/leo.lock create mode 100644 battleship/verify/program.json create mode 100644 battleship/verify/src/main.leo rename check.sh => check-run.sh (93%) create mode 100644 tictactoe/leo.lock create mode 100644 token/leo.lock create mode 100644 vote/leo.lock diff --git a/auction/leo.lock b/auction/leo.lock new file mode 100644 index 0000000..c4293b3 --- /dev/null +++ b/auction/leo.lock @@ -0,0 +1 @@ +package = [] diff --git a/basic_bank/build/main.aleo b/basic_bank/build/main.aleo index b8274fa..963c29e 100644 --- a/basic_bank/build/main.aleo +++ b/basic_bank/build/main.aleo @@ -23,7 +23,8 @@ function deposit: sub r0.amount r1 into r2; cast r0.owner r2 into r3 as Token.record; hash.bhp256 r0.owner into r4 as field; - async deposit r4 r1 into r5; output r3 as Token.record; + async deposit r4 r1 into r5; + output r3 as Token.record; output r5 as basic_bank.aleo/deposit.future; finalize deposit: @@ -550,7 +551,8 @@ function withdraw: hash.bhp256 r0 into r4 as field; call calculate_interest r1 r2 r3 into r5; cast r0 r5 into r6 as Token.record; - async withdraw r4 r1 into r7; output r6 as Token.record; + async withdraw r4 r1 into r7; + output r6 as Token.record; output r7 as basic_bank.aleo/withdraw.future; finalize withdraw: diff --git a/basic_bank/leo.lock b/basic_bank/leo.lock new file mode 100644 index 0000000..c4293b3 --- /dev/null +++ b/basic_bank/leo.lock @@ -0,0 +1 @@ +package = [] diff --git a/battleship/board/.gitignore b/battleship/board/.gitignore new file mode 100644 index 0000000..f721f7f --- /dev/null +++ b/battleship/board/.gitignore @@ -0,0 +1,5 @@ +.env +*.avm +*.prover +*.verifier +outputs/ diff --git a/battleship/board/README.md b/battleship/board/README.md new file mode 100644 index 0000000..d7d689e --- /dev/null +++ b/battleship/board/README.md @@ -0,0 +1,13 @@ +# board.aleo + +## Build Guide + +To compile this Aleo program, run: +```bash +snarkvm build +``` + +To execute this Aleo program, run: +```bash +snarkvm run hello +``` diff --git a/battleship/board/build/main.aleo b/battleship/board/build/main.aleo new file mode 100644 index 0000000..fac2e70 --- /dev/null +++ b/battleship/board/build/main.aleo @@ -0,0 +1,46 @@ +program board.aleo; + +record board_state: + owner as address.private; + hits_and_misses as u64.private; + played_tiles as u64.private; + ships as u64.private; + player_1 as address.private; + player_2 as address.private; + game_started as boolean.private; + + +function new_board_state: + input r0 as u64.private; + input r1 as address.private; + cast self.caller 0u64 0u64 r0 self.caller r1 false into r2 as board_state.record; + output r2 as board_state.record; + + +function start_board: + input r0 as board_state.record; + not r0.game_started into r1; + assert.eq r1 true; + cast r0.owner r0.hits_and_misses r0.played_tiles r0.ships r0.player_1 r0.player_2 true into r2 as board_state.record; + output r2 as board_state.record; + + +function update_played_tiles: + input r0 as board_state.record; + input r1 as u64.private; + sub r1 1u64 into r2; + and r1 r2 into r3; + assert.eq r3 0u64; + and r1 r0.played_tiles into r4; + assert.eq r4 0u64; + or r0.played_tiles r1 into r5; + cast r0.owner r0.hits_and_misses r5 r0.ships r0.player_1 r0.player_2 r0.game_started into r6 as board_state.record; + output r6 as board_state.record; + + +function update_hits_and_misses: + input r0 as board_state.record; + input r1 as u64.private; + or r0.hits_and_misses r1 into r2; + cast r0.owner r2 r0.played_tiles r0.ships r0.player_1 r0.player_2 r0.game_started into r3 as board_state.record; + output r3 as board_state.record; diff --git a/battleship/board/build/program.json b/battleship/board/build/program.json new file mode 100644 index 0000000..b140f09 --- /dev/null +++ b/battleship/board/build/program.json @@ -0,0 +1,6 @@ +{ + "program": "board.aleo", + "version": "0.0.0", + "description": "", + "license": "MIT" +} diff --git a/battleship/board/inputs/board.in b/battleship/board/inputs/board.in new file mode 100644 index 0000000..d414604 --- /dev/null +++ b/battleship/board/inputs/board.in @@ -0,0 +1,4 @@ +// The program input for board/src/main.leo +[main] +public a: u32 = 1u32; +b: u32 = 2u32; diff --git a/battleship/board/leo.lock b/battleship/board/leo.lock new file mode 100644 index 0000000..c4293b3 --- /dev/null +++ b/battleship/board/leo.lock @@ -0,0 +1 @@ +package = [] diff --git a/battleship/board/program.json b/battleship/board/program.json new file mode 100644 index 0000000..b140f09 --- /dev/null +++ b/battleship/board/program.json @@ -0,0 +1,6 @@ +{ + "program": "board.aleo", + "version": "0.0.0", + "description": "", + "license": "MIT" +} diff --git a/battleship/board/src/main.leo b/battleship/board/src/main.leo new file mode 100644 index 0000000..70f82cd --- /dev/null +++ b/battleship/board/src/main.leo @@ -0,0 +1,110 @@ +program board.aleo { + // Battleship boards are represented by 8x8 squares. + // A u64 is all that is required to represent a hit or a miss on a single board. + // Starting from the top row, left to right, a hit is 1 and a miss is 0. + // A first move resulting in a hit in row 1, column 3 would be: + // 00100000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 + // A second u64 is needed to represent which squares have been played, with 1s being played squares and 0s being + // unplayed squares. + record board_state { + owner: address, + // The hits and misses registered on the opponent's board. + hits_and_misses: u64, + // The squares that have been played on the opponent's board. + played_tiles: u64, + // The ship bitstring representing all ship positions on your own board + ships: u64, + player_1: address, + player_2: address, + game_started: bool, + } + + // Returns a new board_state. + transition new_board_state( + ships: u64, + opponent: address, + ) -> board_state { + return board_state { + owner: self.caller, + hits_and_misses: 0u64, + played_tiles: 0u64, + ships, + player_1: self.caller, + player_2: opponent, + game_started: false, + }; + } + + // Returns a new board state that has been started. + // Fails if this board has been started before. + transition start_board( + // The record of the board to start. A board can only be started once. + board: board_state, + ) -> board_state { + // Ensure this board hasn't been used to start a game before. + assert(!board.game_started); + + return board_state { + owner: board.owner, + hits_and_misses: board.hits_and_misses, + played_tiles: board.played_tiles, + ships: board.ships, + player_1: board.player_1, + player_2: board.player_2, + game_started: true, + }; + } + + // Returns a new board state record that includes all the played tiles. + // Fails if r1 has been played before. + transition update_played_tiles( + // The record of the board to update. + board: board_state, + // The u64 equivalent of a bitstring fire coordinate to send to the opponent. + shoot: u64, + ) -> board_state { + // Need to make sure r1 is a valid move. Only one bit of r1 should be flipped. + let flip_bit: u64 = shoot - 1u64; + // bitwise and operation + let check_move: u64 = shoot & flip_bit; + assert_eq(check_move, 0u64); + + // Need to make sure r1 is a valid move given the played_tiles. no bits should overlap. + let check_tiles: u64 = shoot & board.played_tiles; + assert_eq(check_tiles, 0u64); + + // Update played tiles. + let played_tiles: u64 = board.played_tiles | shoot; + + return board_state { + owner: board.owner, + hits_and_misses: board.hits_and_misses, + played_tiles, + ships: board.ships, + player_1: board.player_1, + player_2: board.player_2, + game_started: board.game_started, + }; + } + + // Returns a new board state record that includes all the hits and misses. + transition update_hits_and_misses( + // The record of the board to update. + board: board_state, + // The u64 equivalent of a bitstring of whether this player's previous move was a hit or miss. + hit_or_miss: u64, + ) -> board_state { + // Update hits and misses. + let hits_and_misses: u64 = board.hits_and_misses | hit_or_miss; + + return board_state { + owner: board.owner, + hits_and_misses, + played_tiles: board.played_tiles, + ships: board.ships, + player_1: board.player_1, + player_2: board.player_2, + game_started: board.game_started, + }; + } +} diff --git a/battleship/build/imports/board.aleo b/battleship/build/imports/board.aleo index 90212b4..fac2e70 100644 --- a/battleship/build/imports/board.aleo +++ b/battleship/build/imports/board.aleo @@ -13,7 +13,7 @@ record board_state: function new_board_state: input r0 as u64.private; input r1 as address.private; - cast self.signer 0u64 0u64 r0 self.signer r1 false into r2 as board_state.record; + cast self.caller 0u64 0u64 r0 self.caller r1 false into r2 as board_state.record; output r2 as board_state.record; diff --git a/battleship/build/imports/move.aleo b/battleship/build/imports/move.aleo index cd848b4..ed5247d 100644 --- a/battleship/build/imports/move.aleo +++ b/battleship/build/imports/move.aleo @@ -20,5 +20,5 @@ function create_move: function start_game: input r0 as address.private; - cast r0 0u64 self.signer r0 0u64 into r1 as move.record; + cast r0 0u64 self.caller r0 0u64 into r1 as move.record; output r1 as move.record; diff --git a/battleship/build/program.json b/battleship/build/program.json index 1d0c6e8..1a77ba1 100644 --- a/battleship/build/program.json +++ b/battleship/build/program.json @@ -2,5 +2,22 @@ "program": "battleship.aleo", "version": "0.0.0", "description": "", - "license": "MIT" + "license": "MIT", + "dependencies" : [ + { + "name": "board.aleo", + "location": "local", + "path": "board" + }, + { + "name": "move.aleo", + "location": "local", + "path": "move" + }, + { + "name": "verify.aleo", + "location": "local", + "path": "verify" + } + ] } diff --git a/battleship/leo.lock b/battleship/leo.lock new file mode 100644 index 0000000..601531f --- /dev/null +++ b/battleship/leo.lock @@ -0,0 +1,20 @@ +[[package]] +name = "board.aleo" +location = "local" +path = "/Users/pranav/work/Aleo/workshop/battleship/board" +checksum = "da94274230d0c0c3deb96d80e07ad9db8bbf53264286c14cc3231b7a8b7ef380" +dependencies = [] + +[[package]] +name = "move.aleo" +location = "local" +path = "/Users/pranav/work/Aleo/workshop/battleship/move" +checksum = "7d9fef5fe083eb24376e63935855e4ec709c17fb5ee46a0bb4594b0f9ef8eb08" +dependencies = [] + +[[package]] +name = "verify.aleo" +location = "local" +path = "/Users/pranav/work/Aleo/workshop/battleship/verify" +checksum = "2c2035ebd70500b7e5a9a6198bed1a1163cd1ddfd09128db8f4c16cf23ad2c62" +dependencies = [] diff --git a/battleship/move/.gitignore b/battleship/move/.gitignore new file mode 100644 index 0000000..f721f7f --- /dev/null +++ b/battleship/move/.gitignore @@ -0,0 +1,5 @@ +.env +*.avm +*.prover +*.verifier +outputs/ diff --git a/battleship/move/README.md b/battleship/move/README.md new file mode 100644 index 0000000..a8beca6 --- /dev/null +++ b/battleship/move/README.md @@ -0,0 +1,13 @@ +# move.aleo + +## Build Guide + +To compile this Aleo program, run: +```bash +snarkvm build +``` + +To execute this Aleo program, run: +```bash +snarkvm run hello +``` diff --git a/battleship/move/build/main.aleo b/battleship/move/build/main.aleo new file mode 100644 index 0000000..ed5247d --- /dev/null +++ b/battleship/move/build/main.aleo @@ -0,0 +1,24 @@ +program move.aleo; + +record move: + owner as address.private; + incoming_fire_coordinate as u64.private; + player_1 as address.private; + player_2 as address.private; + prev_hit_or_miss as u64.private; + + +function create_move: + input r0 as move.record; + input r1 as u64.private; + input r2 as u64.private; + is.eq r0.player_1 r0.owner into r3; + ternary r3 r0.player_2 r0.player_1 into r4; + cast r4 r1 r0.player_2 r0.player_1 r2 into r5 as move.record; + output r5 as move.record; + + +function start_game: + input r0 as address.private; + cast r0 0u64 self.caller r0 0u64 into r1 as move.record; + output r1 as move.record; diff --git a/battleship/move/build/program.json b/battleship/move/build/program.json new file mode 100644 index 0000000..b8acf29 --- /dev/null +++ b/battleship/move/build/program.json @@ -0,0 +1,6 @@ +{ + "program": "move.aleo", + "version": "0.0.0", + "description": "", + "license": "MIT" +} diff --git a/battleship/move/inputs/move.in b/battleship/move/inputs/move.in new file mode 100644 index 0000000..d632154 --- /dev/null +++ b/battleship/move/inputs/move.in @@ -0,0 +1,4 @@ +// The program input for move/src/main.leo +[main] +public a: u32 = 1u32; +b: u32 = 2u32; diff --git a/battleship/move/leo.lock b/battleship/move/leo.lock new file mode 100644 index 0000000..c4293b3 --- /dev/null +++ b/battleship/move/leo.lock @@ -0,0 +1 @@ +package = [] diff --git a/battleship/move/program.json b/battleship/move/program.json new file mode 100644 index 0000000..b8acf29 --- /dev/null +++ b/battleship/move/program.json @@ -0,0 +1,6 @@ +{ + "program": "move.aleo", + "version": "0.0.0", + "description": "", + "license": "MIT" +} diff --git a/battleship/move/src/main.leo b/battleship/move/src/main.leo new file mode 100644 index 0000000..f967643 --- /dev/null +++ b/battleship/move/src/main.leo @@ -0,0 +1,46 @@ +program move.aleo { + record move { + owner: address, + incoming_fire_coordinate: u64, + player_1: address, + player_2: address, + // One flipped bit indicates a hit. No flipped bits indicates a miss. + prev_hit_or_miss: u64, + } + + // Returns new move record owned by the opponent. + transition create_move( + // The move record created by the opponent. + move_record: move, + // The u64 representation of incoming_fire_coordinate, the bitstring fire coordinate to send to the opponent. + incoming_fire_coordinate: u64, + // The u64 representation of prev_hit_or_miss, this player's previous fire coordinate as a hit or miss. + prev_hit_or_miss: u64, + ) -> move { + // A new move record should be created and owned by the opponent. + let one_is_owner: bool = move_record.player_1 == move_record.owner; + let opponent: address = one_is_owner ? move_record.player_2 : move_record.player_1; + + return move { + owner: opponent, + incoming_fire_coordinate, + player_1: move_record.player_2, + player_2: move_record.player_1, + prev_hit_or_miss, + }; + } + + // Returns the move record owned by the opponent. + // Note, this move record contains dummy fire coordinates and previous hit or miss. + transition start_game(player_2: address) -> move { + return move { + owner: player_2, + incoming_fire_coordinate: 0u64, + player_1: self.caller, + player_2: player_2, + prev_hit_or_miss: 0u64, + }; + } +} + + diff --git a/battleship/program.json b/battleship/program.json index 1d0c6e8..1a77ba1 100644 --- a/battleship/program.json +++ b/battleship/program.json @@ -2,5 +2,22 @@ "program": "battleship.aleo", "version": "0.0.0", "description": "", - "license": "MIT" + "license": "MIT", + "dependencies" : [ + { + "name": "board.aleo", + "location": "local", + "path": "board" + }, + { + "name": "move.aleo", + "location": "local", + "path": "move" + }, + { + "name": "verify.aleo", + "location": "local", + "path": "verify" + } + ] } diff --git a/battleship/src/main.leo b/battleship/src/main.leo index 5b7401e..27e6ba2 100644 --- a/battleship/src/main.leo +++ b/battleship/src/main.leo @@ -1,9 +1,8 @@ -// The imported programs. -import board.leo; -import move.leo; -import verify.leo; +import board.aleo; +import move.aleo; +import verify.aleo; -// The `program` scope defines the data types, functions, and state associated with the `battleship` program. +// The 'battleship.aleo' program. program battleship.aleo { // Returns a new record representing a new game of battleship. transition initialize_board( @@ -17,25 +16,25 @@ program battleship.aleo { destroyer: u64, // The address of the opponent. player: address, - ) -> board.leo/board_state.record { + ) -> board.aleo/board_state.record { // Verify that each individual ship placement bitstring is valid. - let valid_carrier: bool = verify.leo/validate_ship(carrier, 5u64, 31u64, 4311810305u64); + let valid_carrier: bool = verify.aleo/validate_ship(carrier, 5u64, 31u64, 4311810305u64); assert(valid_carrier); - let valid_battleship: bool = verify.leo/validate_ship(battleship, 4u64, 15u64, 16843009u64); + let valid_battleship: bool = verify.aleo/validate_ship(battleship, 4u64, 15u64, 16843009u64); assert(valid_battleship); - let valid_cruiser: bool = verify.leo/validate_ship(cruiser, 3u64, 7u64, 65793u64); + let valid_cruiser: bool = verify.aleo/validate_ship(cruiser, 3u64, 7u64, 65793u64); assert(valid_cruiser); - let valid_destroyer: bool = verify.leo/validate_ship(destroyer, 2u64, 3u64, 257u64); + let valid_destroyer: bool = verify.aleo/validate_ship(destroyer, 2u64, 3u64, 257u64); assert(valid_destroyer); // Create the board with all the ship placements combined. - let board: u64 = verify.leo/create_board(carrier, battleship, cruiser, destroyer); + let board: u64 = verify.aleo/create_board(carrier, battleship, cruiser, destroyer); // Initialize the board state record. - let state: board_state = board.leo/new_board_state(board, player); + let state: board.aleo/board_state = board.aleo/new_board_state(board, player); return state; } @@ -45,10 +44,10 @@ program battleship.aleo { // This function commits a given board to a game with an opponent and creates the initial dummy move. transition offer_battleship( // The board record to start a game with. - board: board.leo/board_state.record, - ) -> (board.leo/board_state.record, move.leo/move.record) { - let state: board_state = board.leo/start_board(board); - let dummy: move = move.leo/start_game(board.player_2); + board: board.aleo/board_state.record, + ) -> (board.aleo/board_state.record, move.aleo/move.record) { + let state: board.aleo/board_state = board.aleo/start_board(board); + let dummy: move.aleo/move = move.aleo/start_game(board.player_2); return (state, dummy); } @@ -57,16 +56,16 @@ program battleship.aleo { // Returns dummy move record owned by the opponent. transition start_battleship( // The board record to play the game with. - board: board.leo/board_state.record, + board: board.aleo/board_state.record, // The move record to play to begin the game. This should be the dummy move record created from offer_battleship. - move_start: move.leo/move.record, - ) -> (board.leo/board_state.record, move.leo/move.record) { + move_start: move.aleo/move.record, + ) -> (board.aleo/board_state.record, move.aleo/move.record) { // Validate that the move players and board players match each other. assert_eq(board.player_1, move_start.player_2); assert_eq(board.player_2, move_start.player_1); - let state: board_state = board.leo/start_board(board); - let dummy: move = move.leo/start_game(board.player_2); + let state: board.aleo/board_state = board.aleo/start_board(board); + let dummy: move.aleo/move = move.aleo/start_game(board.player_2); return (state, dummy); } @@ -75,12 +74,12 @@ program battleship.aleo { // Returns new move record owned by opponent. transition play( // The board record to update. - board: board.leo/board_state.record, + board: board.aleo/board_state.record, // The incoming move from the opponent. - move_incoming: move.leo/move.record, + move_incoming: move.aleo/move.record, // The u64 equivalent of the bitwise representation of the next coordinate to play on the opponent's board. shoot: u64, - ) -> (board.leo/board_state.record, move.leo/move.record) { + ) -> (board.aleo/board_state.record, move.aleo/move.record) { // Verify the board has been started. This prevents players from starting a game and then creating // a brand new board to play with. assert(board.game_started); @@ -90,17 +89,16 @@ program battleship.aleo { assert_eq(board.player_2, move_incoming.player_1); // Play coordinate on own board. Will fail if not a valid move. - let hit_or_miss: board_state = board.leo/update_played_tiles(board, shoot); + let hit_or_miss: board.aleo/board_state = board.aleo/update_played_tiles(board, shoot); // Update own board with result of last shot. - let next_board: board_state = board.leo/update_hits_and_misses(hit_or_miss, move_incoming.prev_hit_or_miss); + let next_board: board.aleo/board_state = board.aleo/update_hits_and_misses(hit_or_miss, move_incoming.prev_hit_or_miss); // Assess whether incoming fire coordinate is a hit. let is_hit: u64 = move_incoming.incoming_fire_coordinate & board.ships; - let next_move: move = move.leo/create_move(move_incoming, shoot, is_hit); + let next_move: move.aleo/move = move.aleo/create_move(move_incoming, shoot, is_hit); return (next_board, next_move); } } - diff --git a/battleship/verify/.gitignore b/battleship/verify/.gitignore new file mode 100644 index 0000000..f721f7f --- /dev/null +++ b/battleship/verify/.gitignore @@ -0,0 +1,5 @@ +.env +*.avm +*.prover +*.verifier +outputs/ diff --git a/battleship/verify/README.md b/battleship/verify/README.md new file mode 100644 index 0000000..f5f2c67 --- /dev/null +++ b/battleship/verify/README.md @@ -0,0 +1,13 @@ +# verify.aleo + +## Build Guide + +To compile this Aleo program, run: +```bash +snarkvm build +``` + +To execute this Aleo program, run: +```bash +snarkvm run hello +``` diff --git a/battleship/verify/build/main.aleo b/battleship/verify/build/main.aleo new file mode 100644 index 0000000..804dcf2 --- /dev/null +++ b/battleship/verify/build/main.aleo @@ -0,0 +1,73 @@ +program verify.aleo; + + + +closure bitcount: + input r0 as u64; + div r0 2u64 into r1; + div r0 4u64 into r2; + div r0 8u64 into r3; + and r1 8608480567731124087u64 into r4; + and r2 3689348814741910323u64 into r5; + and r3 1229782938247303441u64 into r6; + sub r0 r4 into r7; + sub r7 r5 into r8; + sub r8 r6 into r9; + div r9 16u64 into r10; + add r9 r10 into r11; + and r11 1085102592571150095u64 into r12; + rem r12 255u64 into r13; + output r13 as u64; + + +closure adjacency_check: + input r0 as u64; + input r1 as u64; + div r0 r1 into r2; + is.eq r2 0u64 into r3; + ternary r3 3u64 r2 into r4; + sub r4 1u64 into r5; + and r5 r4 into r6; + is.eq r6 0u64 into r7; + output r7 as boolean; + + +closure horizontal_check: + input r0 as u64; + input r1 as u64; + rem r0 255u64 into r2; + div r2 r1 into r3; + is.eq r3 0u64 into r4; + ternary r4 3u64 r3 into r5; + sub r5 1u64 into r6; + and r6 r5 into r7; + is.eq r7 0u64 into r8; + output r8 as boolean; + + +function validate_ship: + input r0 as u64.private; + input r1 as u64.private; + input r2 as u64.private; + input r3 as u64.private; + call bitcount r0 into r4; + assert.eq r4 r1; + call adjacency_check r0 r2 into r5; + call horizontal_check r0 r2 into r6; + and r5 r6 into r7; + call adjacency_check r0 r3 into r8; + or r7 r8 into r9; + output r9 as boolean.private; + + +function create_board: + input r0 as u64.private; + input r1 as u64.private; + input r2 as u64.private; + input r3 as u64.private; + or r0 r1 into r4; + or r4 r2 into r5; + or r5 r3 into r6; + call bitcount r6 into r7; + assert.eq r7 14u64; + output r6 as u64.private; diff --git a/battleship/verify/build/program.json b/battleship/verify/build/program.json new file mode 100644 index 0000000..b9b28db --- /dev/null +++ b/battleship/verify/build/program.json @@ -0,0 +1,6 @@ +{ + "program": "verify.aleo", + "version": "0.0.0", + "description": "", + "license": "MIT" +} diff --git a/battleship/verify/inputs/verify.in b/battleship/verify/inputs/verify.in new file mode 100644 index 0000000..0321a56 --- /dev/null +++ b/battleship/verify/inputs/verify.in @@ -0,0 +1,4 @@ +// The program input for verify/src/main.leo +[main] +public a: u32 = 1u32; +b: u32 = 2u32; diff --git a/battleship/verify/leo.lock b/battleship/verify/leo.lock new file mode 100644 index 0000000..c4293b3 --- /dev/null +++ b/battleship/verify/leo.lock @@ -0,0 +1 @@ +package = [] diff --git a/battleship/verify/program.json b/battleship/verify/program.json new file mode 100644 index 0000000..b9b28db --- /dev/null +++ b/battleship/verify/program.json @@ -0,0 +1,6 @@ +{ + "program": "verify.aleo", + "version": "0.0.0", + "description": "", + "license": "MIT" +} diff --git a/battleship/verify/src/main.leo b/battleship/verify/src/main.leo new file mode 100644 index 0000000..336176b --- /dev/null +++ b/battleship/verify/src/main.leo @@ -0,0 +1,125 @@ +program verify.aleo { + // Returns the number of flipped bits. + // E.g. 17870283321406128128u64, in binary 11111000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, + // returns 5u64; + function bitcount(bits: u64) -> u64 { + let r1: u64 = bits / 2u64; + let r2: u64 = bits / 4u64; + let r3: u64 = bits / 8u64; + + let r4: u64 = r1 & 8608480567731124087u64; + let r5: u64 = r2 & 3689348814741910323u64; + let r6: u64 = r3 & 1229782938247303441u64; + + let r7: u64 = bits - r4 - r5 - r6; + + let r8: u64 = r7 / 16u64; + let r9: u64 = r7 + r8; + let r10: u64 = r9 & 1085102592571150095u64; + let r11: u64 = r10 % 255u64; + + return r11; + } + + // Returns boolean of whether all the flipped bits in location are "adjacent". Horizontally, this means all flipped bits are + // directly next to each other (111). Vertically, this means all flipped bits are separated by 7 unflipped bits + // (10000000100000001). + function adjacency_check( + // The u64 representation of a ship's placement in an 8x8 grid. + ship: u64, + // The u64 representation of a ship's bitstring, either horizontally or vertically. + // E.g. a ship of length 3's bit string horizontally would be: 000111 = 7u64. Vertically, the bit string would be: + // 10000000100000001 = 65793u64. + orientation: u64, + ) -> bool { + // This may result in 0. + let division: u64 = ship / orientation; + + // subtracting 1 from 0 will cause an underflow, so we should check for this edge case. + let is_eq: bool = division == 0u64; + + // if the above division resulted in 0, we know the adjacency check should return false. + // Setting to r4 to 3 (11) will guarantee failure here. + let ternary: u64 = is_eq ? 3u64 : division; + let subtraction: u64 = ternary - 1u64; + let and: u64 = subtraction & ternary; + + let bits_are_adjacent: bool = and == 0u64; + + return bits_are_adjacent; + } + + // Returns boolean of whether adjacent flipped bits don't split a row of size 8. + // E.g. 111000000 has adjacent flipped bits but splits a row: 00000001 11000000 + function horizontal_check( + // The u64 representation of a ship's placement in an 8x8 grid. + ship: u64, + // The u64 representation of a ship's bitstring horizontally. + horizontal: u64, + ) -> bool { + let remainder: u64 = ship % 255u64; + // This may result in 0. + let division: u64 = remainder / horizontal; + + // Subtracting 1 from 0 will cause an underflow. + let is_eq: bool = division == 0u64; + + // Setting to 3 will guarantee failure. + let ternary: u64 = is_eq ? 3u64 : division; + let subtraction: u64 = ternary - 1u64; + let and: u64 = subtraction & ternary; + + let bits_split_row: bool = and == 0u64; + + return bits_split_row; + } + + // Returns `true` if the ship placement is valid. + transition validate_ship( + // The u64 representation of a ship's placement in an 8x8 grid. + ship: u64, + // The length of the placed ship. + length: u64, + // The u64 equivalent of a ship's horizontal bitstring representation. + horizontal: u64, + // The u64 equivalent of a ship's vertical bitstring representation. + vertical: u64, + ) -> bool { + // Check bitcount -- all other validations depend on the bitcount being correct. + let num_bits: u64 = bitcount(ship); + assert_eq(num_bits, length); + + // Check horizontal bits of ship. + let is_adjacent: bool = adjacency_check(ship, horizontal); // True if bits are adjacent horizontally. + let is_horizontal: bool = horizontal_check(ship, horizontal); // True if those horizontal bits are not split across rows. + let valid_horizontal: bool = is_adjacent && is_horizontal; // True if bits are adjacent horizontally and not split across rows. + + // Check vertical bits of ship. + let valid_vertical: bool = adjacency_check(ship, vertical); // True if bits are adjacent vertically. + + let ship_is_valid: bool = valid_horizontal || valid_vertical; // Ship is valid if it is vertically or horizontally valid. + + return ship_is_valid; + } + + // Returns the u64 representation of all the ships' placements in an 8x8 grid. This function will fail + // if any of the ship placements overlap each other. + transition create_board( + // The u64 representation of a carrier's placement in an 8x8 grid. Length = 5. + carrier: u64, + // The u64 representation of a battleship's placement in an 8x8 grid. Length = 4. + battleship: u64, + // The u64 representation of a cruiser's placement in an 8x8 grid. Length = 3. + cruiser: u64, + // The u64 representation of a destroyer's placement in an 8x8 grid. Length = 2. + destroyer: u64, + ) -> u64 { + // Bitwise combine the ship placements together + let ships: u64 = carrier | battleship | cruiser | destroyer; + + let num_bits: u64 = bitcount(ships); + assert_eq(num_bits, 14u64); // Given 4 individually-valid ships, a valid combination should yield exactly 14 flipped bits. + + return ships; + } +} diff --git a/check.sh b/check-run.sh similarity index 93% rename from check.sh rename to check-run.sh index 1f61e84..cd95968 100755 --- a/check.sh +++ b/check-run.sh @@ -1,6 +1,7 @@ #!/bin/bash # A script to check that all examples compile and run. # Run this script from the root directory of the workshop repository. +# Note that this script is expected to run successfully. # Run the auction example. cd auction diff --git a/tictactoe/leo.lock b/tictactoe/leo.lock new file mode 100644 index 0000000..c4293b3 --- /dev/null +++ b/tictactoe/leo.lock @@ -0,0 +1 @@ +package = [] diff --git a/token/build/main.aleo b/token/build/main.aleo index 8f45b49..2f80ca2 100644 --- a/token/build/main.aleo +++ b/token/build/main.aleo @@ -12,7 +12,8 @@ mapping account: function mint_public: input r0 as address.public; input r1 as u64.public; - async mint_public r0 r1 into r2; output r2 as token.aleo/mint_public.future; + async mint_public r0 r1 into r2; + output r2 as token.aleo/mint_public.future; finalize mint_public: input r0 as address.public; @@ -32,7 +33,8 @@ function mint_private: function transfer_public: input r0 as address.public; input r1 as u64.public; - async transfer_public self.caller r0 r1 into r2; output r2 as token.aleo/transfer_public.future; + async transfer_public self.caller r0 r1 into r2; + output r2 as token.aleo/transfer_public.future; finalize transfer_public: input r0 as address.public; @@ -63,7 +65,8 @@ function transfer_private_to_public: input r2 as u64.public; sub r0.amount r2 into r3; cast r0.owner r3 into r4 as token.record; - async transfer_private_to_public r1 r2 into r5; output r4 as token.record; + async transfer_private_to_public r1 r2 into r5; + output r4 as token.record; output r5 as token.aleo/transfer_private_to_public.future; finalize transfer_private_to_public: @@ -78,7 +81,8 @@ function transfer_public_to_private: input r0 as address.public; input r1 as u64.public; cast r0 r1 into r2 as token.record; - async transfer_public_to_private self.caller r1 into r3; output r2 as token.record; + async transfer_public_to_private self.caller r1 into r3; + output r2 as token.record; output r3 as token.aleo/transfer_public_to_private.future; finalize transfer_public_to_private: diff --git a/token/leo.lock b/token/leo.lock new file mode 100644 index 0000000..c4293b3 --- /dev/null +++ b/token/leo.lock @@ -0,0 +1 @@ +package = [] diff --git a/vote/README.md b/vote/README.md index a5f3fd6..5a25598 100644 --- a/vote/README.md +++ b/vote/README.md @@ -3,7 +3,7 @@ ## Summary -`vote.leo` is a general vote program. +`vote.aleo` is a general vote program. Anyone can issue new proposals, proposers can issue tickets to the voters, and voters can vote without exposing their identity. @@ -135,4 +135,4 @@ leo run disagree "{ ## How votes are tallied -Votes on the ticket are private. But the sum total of the agreements and disagreements are shown on-chain in the public mapping. You can query this data on-chain. \ No newline at end of file +Votes on the ticket are private. But the sum total of the agreements and disagreements are shown on-chain in the public mapping. You can query this data on-chain. diff --git a/vote/build/main.aleo b/vote/build/main.aleo index 82cfdf4..57d566d 100644 --- a/vote/build/main.aleo +++ b/vote/build/main.aleo @@ -39,7 +39,8 @@ function propose: assert.eq self.caller r0.proposer; hash.bhp256 r0.title into r1 as field; cast self.caller r1 r0 into r2 as Proposal.record; - async propose r1 into r3; output r2 as Proposal.record; + async propose r1 into r3; + output r2 as Proposal.record; output r3 as vote.aleo/propose.future; finalize propose: @@ -51,7 +52,8 @@ function new_ticket: input r0 as field.public; input r1 as address.public; cast r1 r0 into r2 as Ticket.record; - async new_ticket r0 into r3; output r2 as Ticket.record; + async new_ticket r0 into r3; + output r2 as Ticket.record; output r3 as vote.aleo/new_ticket.future; finalize new_ticket: @@ -63,7 +65,8 @@ finalize new_ticket: function agree: input r0 as Ticket.record; - async agree r0.pid into r1; output r1 as vote.aleo/agree.future; + async agree r0.pid into r1; + output r1 as vote.aleo/agree.future; finalize agree: input r0 as field.public; @@ -74,7 +77,8 @@ finalize agree: function disagree: input r0 as Ticket.record; - async disagree r0.pid into r1; output r1 as vote.aleo/disagree.future; + async disagree r0.pid into r1; + output r1 as vote.aleo/disagree.future; finalize disagree: input r0 as field.public; diff --git a/vote/leo.lock b/vote/leo.lock new file mode 100644 index 0000000..c4293b3 --- /dev/null +++ b/vote/leo.lock @@ -0,0 +1 @@ +package = [] diff --git a/vote/src/main.leo b/vote/src/main.leo index 435902d..67bcd37 100644 --- a/vote/src/main.leo +++ b/vote/src/main.leo @@ -1,4 +1,4 @@ -// The 'vote.leo' program. +// The 'vote.aleo' program. program vote.aleo { // Proposal details struct ProposalInfo {