diff --git a/examples/inputs/synchronization/Declassify-alice.txt b/examples/inputs/synchronization/Declassify-alice.txt new file mode 100644 index 0000000000..d81cc0710e --- /dev/null +++ b/examples/inputs/synchronization/Declassify-alice.txt @@ -0,0 +1 @@ +42 diff --git a/examples/inputs/synchronization/Declassify-bob.txt b/examples/inputs/synchronization/Declassify-bob.txt new file mode 100644 index 0000000000..920a139664 --- /dev/null +++ b/examples/inputs/synchronization/Declassify-bob.txt @@ -0,0 +1 @@ +43 diff --git a/examples/outputs/synchronization/Declassify-alice.txt b/examples/outputs/synchronization/Declassify-alice.txt new file mode 100644 index 0000000000..c508d5366f --- /dev/null +++ b/examples/outputs/synchronization/Declassify-alice.txt @@ -0,0 +1 @@ +false diff --git a/examples/outputs/synchronization/Declassify-bob.txt b/examples/outputs/synchronization/Declassify-bob.txt new file mode 100644 index 0000000000..e69de29bb2 diff --git a/examples/src/main/viaduct/synchronization/Declassify.via b/examples/src/main/viaduct/synchronization/Declassify.via new file mode 100644 index 0000000000..1134a1206f --- /dev/null +++ b/examples/src/main/viaduct/synchronization/Declassify.via @@ -0,0 +1,15 @@ +host alice : {A & B} +host bob : {B} + +fun main() { + let $pick = input int from alice; + + let $guess = input int from bob; + let $trusted_guess = endorse $guess from {B}; + + let $revealed_pick@Replication(hosts = {alice, bob}) = declassify $pick to {A ⊓ B}; + let $bob_wins = $revealed_pick == $trusted_guess; + + output $bob_wins to alice; + /* output $bob_wins to bob; */ +}