Skip to content

Commit

Permalink
Add a ppx for snarky with_label (#1362)
Browse files Browse the repository at this point in the history
* Add extremely basic with_label ppx

This expands [%with_label expr] to
  with_label (expr ^ ": " ^ Pervasives.__LOC__)

* Implement snarkydef ppx

* Use let%snarkydef in place of toplevel let _ = with_label __LOC__ _

* Revert let%snarkydef change for let (type _) and let (module _)

* Add support for let%snarkydef x (type y) ... = ...

* Use let%snarkydef in a few more places
  • Loading branch information
mrmr1993 committed Dec 28, 2018
1 parent bb0c6dc commit 775a434
Show file tree
Hide file tree
Showing 26 changed files with 659 additions and 636 deletions.
123 changes: 59 additions & 64 deletions src/lib/blockchain_snark/blockchain_state.ml
Expand Up @@ -46,80 +46,75 @@ module Make (Consensus_mechanism : Consensus.Mechanism.S) :
transition consensus data is valid
new consensus state is a function of the old consensus state
*)
let update
let%snarkydef update
((previous_state_hash, previous_state) :
State_hash.var * Protocol_state.var)
(transition : Snark_transition.var) :
( State_hash.var * Protocol_state.var * [`Success of Boolean.var]
, _ )
Tick.Checked.t =
with_label __LOC__
(let supply_increase = Snark_transition.supply_increase transition in
let%bind `Success updated_consensus_state, consensus_state =
Consensus_mechanism.next_state_checked ~prev_state:previous_state
~prev_state_hash:previous_state_hash transition supply_increase
in
let%bind success =
let%bind correct_transaction_snark =
T.verify_complete_merge
(Snark_transition.sok_digest transition)
( previous_state |> Protocol_state.blockchain_state
|> Blockchain_state.ledger_hash )
( transition |> Snark_transition.blockchain_state
|> Blockchain_state.ledger_hash )
supply_increase
(As_prover.return
(Option.value ~default:Tock.Proof.dummy
(Snark_transition.ledger_proof transition)))
and ledger_hash_didn't_change =
Frozen_ledger_hash.equal_var
( previous_state |> Protocol_state.blockchain_state
|> Blockchain_state.ledger_hash )
( transition |> Snark_transition.blockchain_state
|> Blockchain_state.ledger_hash )
in
let%bind correct_snark =
Boolean.(correct_transaction_snark || ledger_hash_didn't_change)
in
Boolean.(correct_snark && updated_consensus_state)
in
let new_state =
Protocol_state.create_var ~previous_state_hash
~blockchain_state:(Snark_transition.blockchain_state transition)
~consensus_state
in
let%bind state_triples = Protocol_state.var_to_triples new_state in
let%bind state_partial =
Pedersen.Checked.Section.extend Pedersen.Checked.Section.empty
~start:Hash_prefix.length_in_triples state_triples
in
let%map state_hash =
Pedersen.Checked.Section.create
~acc:(`Value Hash_prefix.protocol_state.acc)
~support:
(Interval_union.of_interval (0, Hash_prefix.length_in_triples))
|> Pedersen.Checked.Section.disjoint_union_exn state_partial
>>| Pedersen.Checked.Section.to_initial_segment_digest_exn >>| fst
in
( State_hash.var_of_hash_packed state_hash
, new_state
, `Success success ))
let supply_increase = Snark_transition.supply_increase transition in
let%bind `Success updated_consensus_state, consensus_state =
Consensus_mechanism.next_state_checked ~prev_state:previous_state
~prev_state_hash:previous_state_hash transition supply_increase
in
let%bind success =
let%bind correct_transaction_snark =
T.verify_complete_merge
(Snark_transition.sok_digest transition)
( previous_state |> Protocol_state.blockchain_state
|> Blockchain_state.ledger_hash )
( transition |> Snark_transition.blockchain_state
|> Blockchain_state.ledger_hash )
supply_increase
(As_prover.return
(Option.value ~default:Tock.Proof.dummy
(Snark_transition.ledger_proof transition)))
and ledger_hash_didn't_change =
Frozen_ledger_hash.equal_var
( previous_state |> Protocol_state.blockchain_state
|> Blockchain_state.ledger_hash )
( transition |> Snark_transition.blockchain_state
|> Blockchain_state.ledger_hash )
in
let%bind correct_snark =
Boolean.(correct_transaction_snark || ledger_hash_didn't_change)
in
Boolean.(correct_snark && updated_consensus_state)
in
let new_state =
Protocol_state.create_var ~previous_state_hash
~blockchain_state:(Snark_transition.blockchain_state transition)
~consensus_state
in
let%bind state_triples = Protocol_state.var_to_triples new_state in
let%bind state_partial =
Pedersen.Checked.Section.extend Pedersen.Checked.Section.empty
~start:Hash_prefix.length_in_triples state_triples
in
let%map state_hash =
Pedersen.Checked.Section.create
~acc:(`Value Hash_prefix.protocol_state.acc)
~support:
(Interval_union.of_interval (0, Hash_prefix.length_in_triples))
|> Pedersen.Checked.Section.disjoint_union_exn state_partial
>>| Pedersen.Checked.Section.to_initial_segment_digest_exn >>| fst
in
(State_hash.var_of_hash_packed state_hash, new_state, `Success success)
end
end

module Checked = struct
let is_base_hash h =
with_label __LOC__
(Field.Checked.equal
(Field.Checked.constant
( Protocol_state.hash Consensus_mechanism.genesis_protocol_state
:> Field.t ))
(State_hash.var_to_hash_packed h))
let%snarkydef is_base_hash h =
Field.Checked.equal
(Field.Checked.constant
( Protocol_state.hash Consensus_mechanism.genesis_protocol_state
:> Field.t ))
(State_hash.var_to_hash_packed h)

let hash (t : Protocol_state.var) =
with_label __LOC__
( Protocol_state.var_to_triples t
>>= Pedersen.Checked.digest_triples ~init:Hash_prefix.protocol_state
>>| State_hash.var_of_hash_packed )
let%snarkydef hash (t : Protocol_state.var) =
Protocol_state.var_to_triples t
>>= Pedersen.Checked.digest_triples ~init:Hash_prefix.protocol_state
>>| State_hash.var_of_hash_packed
end
end
2 changes: 1 addition & 1 deletion src/lib/blockchain_snark/jbuild
Expand Up @@ -7,5 +7,5 @@
(library_flags (-linkall))
(libraries (core cached cache_dir protocols snarky snark_params coda_base transaction_snark bignum_bigint consensus))
(inline_tests)
(preprocess (pps (ppx_jane ppx_deriving.eq bisect_ppx -conditional)))
(preprocess (pps (ppx_snarky ppx_jane ppx_deriving.eq bisect_ppx -conditional)))
(synopsis "blockchain state transition snarking library")))
24 changes: 10 additions & 14 deletions src/lib/coda_base/blockchain_state.ml
Expand Up @@ -185,21 +185,17 @@ end) : S = struct

let () = assert Insecure.signature_hash_function

let hash_checked t ~nonce =
let%snarkydef hash_checked t ~nonce =
let open Let_syntax in
with_label __LOC__
(let%bind trips = var_to_triples t in
let%bind hash =
Pedersen.Checked.digest_triples ~init:Hash_prefix.signature
( trips
@ Fold.(to_list (group3 ~default:Boolean.false_ (of_list nonce)))
)
in
let%map bs = Pedersen.Checked.Digest.choose_preimage hash in
Bitstring.Lsb_first.of_list
(List.take
(bs :> Boolean.var list)
Inner_curve.Scalar.length_in_bits))
let%bind trips = var_to_triples t in
let%bind hash =
Pedersen.Checked.digest_triples ~init:Hash_prefix.signature
( trips
@ Fold.(to_list (group3 ~default:Boolean.false_ (of_list nonce))) )
in
let%map bs = Pedersen.Checked.Digest.choose_preimage hash in
Bitstring.Lsb_first.of_list
(List.take (bs :> Boolean.var list) Inner_curve.Scalar.length_in_bits)
end

module Signature =
Expand Down
15 changes: 7 additions & 8 deletions src/lib/coda_base/data_hash.ml
Expand Up @@ -136,14 +136,13 @@ struct
>>| fun x -> (x :> Boolean.var list)
else Field.Checked.unpack ~length:length_in_bits

let var_to_bits t =
with_label __LOC__
( match t.bits with
| Some bits -> return (bits :> Boolean.var list)
| None ->
let%map bits = unpack t.digest in
t.bits <- Some (Bitstring.Lsb_first.of_list bits) ;
bits )
let%snarkydef var_to_bits t =
match t.bits with
| Some bits -> return (bits :> Boolean.var list)
| None ->
let%map bits = unpack t.digest in
t.bits <- Some (Bitstring.Lsb_first.of_list bits) ;
bits

let var_to_triples t =
var_to_bits t >>| Bitstring.pad_to_triple_list ~default:Boolean.false_
Expand Down
2 changes: 1 addition & 1 deletion src/lib/coda_base/jbuild
Expand Up @@ -37,7 +37,7 @@
yojson
codable))
(preprocessor_deps ("../../config.mlh"))
(preprocess (pps (ppx_jane ppx_deriving.eq ppx_deriving.enum ppx_deriving.ord ppx_deriving_yojson bisect_ppx -conditional)))
(preprocess (pps (ppx_snarky ppx_jane ppx_deriving.eq ppx_deriving.enum ppx_deriving.ord ppx_deriving_yojson bisect_ppx -conditional)))
(synopsis "Snarks and friends necessary for keypair generation")))

(rule
Expand Down
28 changes: 14 additions & 14 deletions src/lib/coda_base/ledger_hash.ml
Expand Up @@ -86,20 +86,20 @@ let get t addr = Merkle_tree.get_req ~depth (var_to_hash_packed t) addr
- returns a root [t'] of a tree of depth [depth]
which is [t] but with the account [f account] at path [addr].
*)
let modify_account t pk ~(filter : Account.var -> ('a, _) Checked.t) ~f =
with_label __LOC__
(let%bind addr =
request_witness Account.Index.Unpacked.typ
As_prover.(
map (read Public_key.Compressed.typ pk) ~f:(fun s -> Find_index s))
in
handle
(Merkle_tree.modify_req ~depth (var_to_hash_packed t) addr
~f:(fun account ->
let%bind x = filter account in
f x account ))
reraise_merkle_requests
>>| var_of_hash_packed)
let%snarkydef modify_account t pk ~(filter : Account.var -> ('a, _) Checked.t)
~f =
let%bind addr =
request_witness Account.Index.Unpacked.typ
As_prover.(
map (read Public_key.Compressed.typ pk) ~f:(fun s -> Find_index s))
in
handle
(Merkle_tree.modify_req ~depth (var_to_hash_packed t) addr
~f:(fun account ->
let%bind x = filter account in
f x account ))
reraise_merkle_requests
>>| var_of_hash_packed

(*
[modify_account_send t pk ~f] implements the following spec:
Expand Down
9 changes: 4 additions & 5 deletions src/lib/coda_base/payment_payload.ml
Expand Up @@ -44,11 +44,10 @@ let fold {receiver; amount} =
(* TODO: This could be a bit more efficient by packing across triples,
but I think the added confusion-possibility
is not worth it. *)
let var_to_triples {receiver; amount} =
with_label __LOC__
(let%map receiver = Public_key.Compressed.var_to_triples receiver in
let amount = Amount.var_to_triples amount in
receiver @ amount)
let%snarkydef var_to_triples {receiver; amount} =
let%map receiver = Public_key.Compressed.var_to_triples receiver in
let amount = Amount.var_to_triples amount in
receiver @ amount

let length_in_triples =
Public_key.Compressed.length_in_triples + Amount.length_in_triples
Expand Down
52 changes: 25 additions & 27 deletions src/lib/coda_base/schnorr.ml
Expand Up @@ -29,34 +29,32 @@ module Message = struct

let () = assert Insecure.signature_hash_function

let hash_checked t ~nonce =
let%snarkydef hash_checked t ~nonce =
let open Let_syntax in
with_label __LOC__
(let init =
Pedersen.Checked.Section.create
~acc:(`Value Hash_prefix.signature.acc)
~support:
(Interval_union.of_interval (0, Hash_prefix.length_in_triples))
in
let%bind with_t = Pedersen.Checked.Section.disjoint_union_exn init t in
let%bind digest =
let%map final =
Pedersen.Checked.Section.extend with_t
(Bitstring_lib.Bitstring.pad_to_triple_list
~default:Boolean.false_ nonce)
~start:
( Hash_prefix.length_in_triples
+ User_command_payload.length_in_triples )
in
let d, _ =
Pedersen.Checked.Section.to_initial_segment_digest final
|> Or_error.ok_exn
in
d
in
let%bind bs = Pedersen.Checked.Digest.choose_preimage digest in
let%map d = Sha256_lib.Sha256.Checked.digest (bs :> Boolean.var list) in
Bitstring.Lsb_first.of_list (d :> Boolean.var list))
let init =
Pedersen.Checked.Section.create ~acc:(`Value Hash_prefix.signature.acc)
~support:
(Interval_union.of_interval (0, Hash_prefix.length_in_triples))
in
let%bind with_t = Pedersen.Checked.Section.disjoint_union_exn init t in
let%bind digest =
let%map final =
Pedersen.Checked.Section.extend with_t
(Bitstring_lib.Bitstring.pad_to_triple_list ~default:Boolean.false_
nonce)
~start:
( Hash_prefix.length_in_triples
+ User_command_payload.length_in_triples )
in
let d, _ =
Pedersen.Checked.Section.to_initial_segment_digest final
|> Or_error.ok_exn
in
d
in
let%bind bs = Pedersen.Checked.Digest.choose_preimage digest in
let%map d = Sha256_lib.Sha256.Checked.digest (bs :> Boolean.var list) in
Bitstring.Lsb_first.of_list (d :> Boolean.var list)
end

include Signature_lib.Checked.Schnorr (Tick) (Snark_params.Tick.Inner_curve)
Expand Down

0 comments on commit 775a434

Please sign in to comment.